The relative dimension of a smooth scheme over a field

A morphism f : X ⟶ Spec k to the spectrum of a field is smooth of relative dimension n exactly when it is smooth and the local ring of X at every closed point has Krull dimension n. In particular a smooth irreducible k-scheme of dimension n is smooth of relative dimension n, and a smooth curve, an integral smooth k-scheme whose function field is an algebraic function field of one variable over k, is smooth of relative dimension one. This turns the dimension hypothesis on a smooth curve into the relative-dimension hypothesis under which its sheaf of relative differentials Ω_{X/k} is invertible (TauCeti.AlgebraicGeometry.InvertibleSheaf.relativeDifferentials).

Around every point a smooth morphism has affine charts whose rings are standard smooth over k of some relative dimension. By TauCeti.height_eq_of_isStandardSmoothOfRelativeDimension that relative dimension is the height of every maximal ideal of the chart, which is the dimension of the local ring of X at every closed point of X lying in the chart. Charts are nonempty open subsets of a Jacobson scheme, so they contain closed points.

Main declarations

• TauCeti.AlgebraicGeometry.smoothOfRelativeDimension_iff_ringKrullDim_stalk_eq: f : X ⟶ Spec k is smooth of relative dimension n if and only if it is smooth and the local rings at closed points have dimension n;
• TauCeti.AlgebraicGeometry.smoothOfRelativeDimension_of_topologicalKrullDim_eq: a smooth irreducible k-scheme of dimension n is smooth of relative dimension n;
• TauCeti.AlgebraicGeometry.smoothOfRelativeDimension_one_of_isFunctionField: a smooth curve is smooth of relative dimension one.

References

• R. Hartshorne, Algebraic Geometry, Chapter III, Section 10.

theorem TauCeti.AlgebraicGeometry.smoothOfRelativeDimension_iff_ringKrullDim_stalk_eq {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) : AlgebraicGeometry.SmoothOfRelativeDimension n f ↔ AlgebraicGeometry.Smooth f ∧ ∀ (x : ↥X), IsClosed {x} → ringKrullDim ↑(X.presheaf.stalk x) = ↑n

A morphism f : X ⟶ Spec k is smooth of relative dimension n if and only if it is smooth and the local ring of X at every closed point has Krull dimension n.

theorem TauCeti.AlgebraicGeometry.smoothOfRelativeDimension_of_topologicalKrullDim_eq {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [IrreducibleSpace ↥X] {n : ℕ} (h : topologicalKrullDim ↥X = ↑n) : AlgebraicGeometry.SmoothOfRelativeDimension n f

A smooth irreducible scheme of dimension n over a field is smooth of relative dimension n.

theorem TauCeti.AlgebraicGeometry.smoothOfRelativeDimension_one_of_isFunctionField {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.Smooth (X ↘ AlgebraicGeometry.Spec ↧k)] (hF : IsFunctionField k ↑X.functionField) : AlgebraicGeometry.SmoothOfRelativeDimension 1 (X ↘ AlgebraicGeometry.Spec ↧k)

A smooth curve over a field, an integral smooth scheme whose function field is an algebraic function field of one variable, is smooth of relative dimension one.