Smooth morphisms

TheoremKrull dimension does not increase along faithfully flat maps#✓fully proved

Krull dimension does not increase along faithfully flat ring maps.

theorem ringKrullDim_le_of_faithfullyFlat (R S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] [Module.FaithfullyFlat R S] : ringKrullDim R ≤ ringKrullDim S

Used by 1

Used byKrull dimension of a standard smooth algebra

TheoremKrull dimension of a standard smooth algebra#✓fully proved

A standard smooth algebra of relative dimension n has Krull dimension at most n.

theorem ringKrullDim_le_of_isStandardSmoothOfRelativeDimension
    {K : Type*} [Field K] {B : Type*} [CommRing B] [Algebra K B] (n : ℕ)
    [Algebra.IsStandardSmoothOfRelativeDimension n K B] : ringKrullDim B ≤ n

Uses 1 · Used by 1

Proof usesKrull dimension does not increase along faithfully flat maps

Used byKrull dimension of a standard smooth algebra over a field

TheoremKrull dimension of a standard smooth algebra over a field#✓fully proved

A standard smooth algebra map from a field has Krull dimension at most the relative dimension.

theorem ringKrullDim_le_of_ringHom {R S : Type*} [CommRing R] [CommRing S] (hR : IsField R)
    (φ : R →+* S) (n : ℕ) (hφ : φ.IsStandardSmoothOfRelativeDimension n) :
    ringKrullDim S ≤ n

Uses 1 · Used by 1

Proof usesKrull dimension of a standard smooth algebra

Used byDimension of a scheme smooth of relative dimension \(n\)

TheoremDimension of a scheme smooth of relative dimension \(n\)#✓fully proved

A scheme smooth of relative dimension n over a field has topological Krull dimension at most n.

theorem AlgebraicGeometry.SmoothOfRelativeDimension.topologicalKrullDim_le
    {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K)) (n : ℕ)
    [SmoothOfRelativeDimension n f] : topologicalKrullDim X ≤ n

Uses 1

Proof usesKrull dimension of a standard smooth algebra over a field

TheoremSmooth schemes over a field are reduced#✓fully proved

A scheme smooth over a field is reduced.

theorem AlgebraicGeometry.isReduced_of_smooth_over_field {k : Type u} [Field k]
    {Z : Scheme.{u}} {g : Z ⟶ Spec (.of k)} (hg : Smooth g) : IsReduced Z

Used by 1

Used bySmooth morphisms preserve reducedness

TheoremSmooth morphisms preserve reducedness#✓fully proved

A smooth morphism with reduced locally Noetherian target has reduced source.

theorem isReduced_of_isReduced_of_isLocallyNoetherian
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] [IsReduced Y] [IsLocallyNoetherian Y] :
    IsReduced X

Uses 1

Proof usesSmooth schemes over a field are reduced

TheoremSmooth maps from a preconnected scheme have constant relative dimension#✓fully proved

A smooth morphism from a preconnected scheme is smooth of some fixed relative dimension.

theorem AlgebraicGeometry.Smooth.exists_smoothOfRelativeDimension_of_preconnectedSpace
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] [PreconnectedSpace X] :
    ∃ n : ℕ, SmoothOfRelativeDimension n f

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.