Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedaudited 2026-09-30
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Relative dimension of a smooth morphism at a point

Definition

Let f:X→S be a morphism of schemes that is smooth at a point x∈X (Smooth morphism of schemes), and put s=f(x). For a scheme Y and a point y∈Y the local dimension of Y at y, written dim⁡yY, is the infimum of the Krull dimensions of the open neighbourhoods of y in Y (Krull dimension of a nonzero ring). If Y is locally of finite type over a field, this equals the largest dimension of an irreducible component through y in any finite-type affine neighbourhood of y: nonempty principal opens of a finite-type domain have the same fraction field and hence the same dimension by Affine-domain dimension equals transcendence degree, while components not containing y may be removed after shrinking that affine neighbourhood. The component formula need not hold for arbitrary locally Noetherian schemes: at the generic point of the spectrum of a discrete valuation ring, a principal open is a field of dimension zero although the whole space is an irreducible component of dimension one. This is the Stacks convention for dim⁡y; it is not the height of the local ring OY,y, which can be strictly smaller for a point lying on a lower-dimensional component (A local ring is a nonzero commutative ring with a unique maximal ideal).

Let K/κ(s) be a field extension and let Xs,K=Xs×Spec⁡κ(s)Spec⁡K be the base-changed fibre; it is the geometric fibre of Geometric fibres and geometric points when K is an algebraic closure of κ(s). We say f has relative dimension n at x when dim⁡yXs,K=n for every field extension K/κ(s) and every point y∈Xs,K lying over the image of x in Xs (the quantifier convention of Geometrically regular algebras and geometrically regular fibres). We say f has pure relative dimension n when it is smooth with relative dimension n at every point of X, that is, when f is smooth and every geometric fibre of f is pure n-dimensional in the sense that its local dimension equals n at each of its points.

Only the smooth case is used on this page. There, the condition holds for a unique n at each point x: the fibre is geometrically regular at the points over x by the definition of smoothness, and a computation with a standard smooth chart — m variables and c independent equations, hence m−c free parameters — gives the common value m−c of the local dimensions of the geometric fibre at the points lying over x, independent of the field extension K. On the model chart ASn→S the relative dimension is n everywhere, and for n=0 the morphism is étale; the chart computation is carried out in the standard-form and Jacobian results on this page. The integer is allowed to depend on the point x; pure relative dimension means that it does not, and the empty source case is vacuous.

Depends on

Used by

Dependency tree · two levels

24 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources