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 be a morphism of schemes that is smooth at a point (Smooth morphism of schemes), and put . For a scheme and a point the local dimension of at , written , is the infimum of the Krull dimensions of the open neighbourhoods of in (Krull dimension of a nonzero ring). If is locally of finite type over a field, this equals the largest dimension of an irreducible component through in any finite-type affine neighbourhood of : 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 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 ; it is not the height of the local ring , 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 be a field extension and let be the base-changed fibre; it is the geometric fibre of Geometric fibres and geometric points when is an algebraic closure of . We say has relative dimension at when for every field extension and every point lying over the image of in (the quantifier convention of Geometrically regular algebras and geometrically regular fibres). We say has pure relative dimension when it is smooth with relative dimension at every point of , that is, when is smooth and every geometric fibre of is pure -dimensional in the sense that its local dimension equals at each of its points.
Only the smooth case is used on this page. There, the condition holds for a unique at each point : the fibre is geometrically regular at the points over by the definition of smoothness, and a computation with a standard smooth chart — variables and independent equations, hence free parameters — gives the common value of the local dimensions of the geometric fibre at the points lying over , independent of the field extension . On the model chart the relative dimension is everywhere, and for 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 ; pure relative dimension means that it does not, and the empty source case is vacuous.
Depends on
Used by
- The affine line is smooth but not etale Counterexample
- Étale morphism of schemes Definition
- Polynomial rings are flat and smooth Example
- Coprime polynomial factorisations lift after an etale localisation Lemma
- Dense relative-dimension strata in flat finitely presented fibres Lemma
- Étale stability Lemma
- Local fibre dimension equals local ring dimension plus residue transcendence degree Lemma
- Local fibre-dimension bound from polynomial quasi-finiteness Lemma
- Upper semicontinuity of proper fibre dimension Lemma
- Differentials of a smooth morphism Theorem
- Étale equals flat and unramified in finite presentation Theorem
- Relative Jacobian criterion with its presentation hypothesis Theorem
- Smooth maps have étale local affine-space form Theorem
- Smoothness survives base change and composition Theorem
- The etale locus is open Theorem
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
- The Stacks Project, Morphisms of Schemes, Section 29.29 (morphisms and dimensions of fibres) (standard reference, not scraped)