Smooth morphisms

In this file we define smooth morphisms. The main definitions are:

• AlgebraicGeometry.Smooth: A morphism of schemes f : X ⟶ Y is smooth if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, the induced map Γ(Y, U) ⟶ Γ(X, V) is smooth.

• AlgebraicGeometry.SmoothOfRelativeDimension: A morphism of schemes f : X ⟶ Y is smooth of relative dimension n if for each x : X there exists an affine open neighborhood V of x and an affine open neighborhood U of f.base x with V ≤ f ⁻¹ᵁ U such that the induced map Γ(Y, U) ⟶ Γ(X, V) is standard smooth (of relative dimension n).

Main results

• AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth: A morphism of schemes is smooth if and only if for each x : X there exists an affine open neighborhood V of x and an affine open neighborhood U of f.base x with V ≤ f ⁻¹ᵁ U such that the induced map Γ(Y, U) ⟶ Γ(X, V) is standard smooth.

Notes

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

class AlgebraicGeometry.Smooth {X Y : Scheme} (f : X ⟶ Y) : Prop

A morphism of schemes f : X ⟶ Y is smooth if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is smooth.

• smooth_appLE {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth

theorem AlgebraicGeometry.smooth_iff {X Y : Scheme} (f : X ⟶ Y) : Smooth f ↔ ∀ {U : Y.Opens}, IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth

theorem AlgebraicGeometry.Scheme.Hom.smooth_appLE {X Y : Scheme} (f : X ⟶ Y) [self : Smooth f] {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (appLE f U V e)).Smooth

Alias of AlgebraicGeometry.Smooth.smooth_appLE.

@[deprecated AlgebraicGeometry.Smooth (since := "2026-02-09")]

def AlgebraicGeometry.IsSmooth {X Y : Scheme} (f : X ⟶ Y) : Prop

Alias of AlgebraicGeometry.Smooth.

---

A morphism of schemes f : X ⟶ Y is smooth if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is smooth.

instance AlgebraicGeometry.instHasRingHomPropertySmoothSmooth : HasRingHomProperty @Smooth fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.Smooth

The property of scheme morphisms Smooth is associated with the ring homomorphism property Smooth.

theorem AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth {X Y : Scheme} (f : X ⟶ Y) : Smooth f ↔ ∀ (x : ↥X), ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

A morphism of schemes is smooth if and only if for each x : X there exists an affine open neighborhood V of x and an affine open neighborhood U of f.base x with V ≤ f ⁻¹ᵁ U such that the induced map Γ(Y, U) ⟶ Γ(X, V) is standard smooth.

theorem AlgebraicGeometry.Smooth.exists_isStandardSmooth {X Y : Scheme} (f : X ⟶ Y) [Smooth f] (x : ↥X) : ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

instance AlgebraicGeometry.instIsStableUnderCompositionSchemeSmooth : CategoryTheory.MorphismProperty.IsStableUnderComposition @Smooth

Being smooth is stable under composition.

instance AlgebraicGeometry.smooth_comp {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [Smooth f] [Smooth g] : Smooth (CategoryTheory.CategoryStruct.comp f g)

The composition of smooth morphisms is smooth.

@[instance 100]

instance AlgebraicGeometry.instFlatOfSmooth {X Y : Scheme} (f : X ⟶ Y) [Smooth f] : Flat f

instance AlgebraicGeometry.smooth_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @Smooth

Smooth is stable under base change.

instance AlgebraicGeometry.instRespectsSchemeSmoothIsOpenImmersion : CategoryTheory.MorphismProperty.Respects (@Smooth) IsOpenImmersion

@[deprecated AlgebraicGeometry.smooth_isStableUnderBaseChange (since := "2026-02-09")]

theorem AlgebraicGeometry.isSmooth_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @Smooth

Alias of AlgebraicGeometry.smooth_isStableUnderBaseChange.

---

Smooth is stable under base change.

class AlgebraicGeometry.SmoothOfRelativeDimension (n : ℕ) {X Y : Scheme} (f : X ⟶ Y) : Prop

A morphism of schemes f : X ⟶ Y is smooth of relative dimension n if for each x : X there exists an affine open neighborhood V of x and an affine open neighborhood U of f.base x with V ≤ f ⁻¹ᵁ U such that the induced map Γ(Y, U) ⟶ Γ(X, V) is standard smooth of relative dimension n.

• exists_isStandardSmoothOfRelativeDimension (x : ↥X) : ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), RingHom.IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))

theorem AlgebraicGeometry.smoothOfRelativeDimension_iff (n : ℕ) {X Y : Scheme} (f : X ⟶ Y) : SmoothOfRelativeDimension n f ↔ ∀ (x : ↥X), ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), RingHom.IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))

@[deprecated AlgebraicGeometry.SmoothOfRelativeDimension (since := "2026-02-09")]

def AlgebraicGeometry.IsSmoothOfRelativeDimension (n : ℕ) {X Y : Scheme} (f : X ⟶ Y) : Prop

Alias of AlgebraicGeometry.SmoothOfRelativeDimension.

---

A morphism of schemes f : X ⟶ Y is smooth of relative dimension n if for each x : X there exists an affine open neighborhood V of x and an affine open neighborhood U of f.base x with V ≤ f ⁻¹ᵁ U such that the induced map Γ(Y, U) ⟶ Γ(X, V) is standard smooth of relative dimension n.

theorem AlgebraicGeometry.SmoothOfRelativeDimension.smooth (n : ℕ) {X Y : Scheme} (f : X ⟶ Y) [SmoothOfRelativeDimension n f] : Smooth f

If f is smooth of any relative dimension, it is smooth.

@[deprecated AlgebraicGeometry.SmoothOfRelativeDimension.smooth (since := "2026-02-09")]

theorem AlgebraicGeometry.IsSmoothOfRelativeDimension.isSmooth (n : ℕ) {X Y : Scheme} (f : X ⟶ Y) [SmoothOfRelativeDimension n f] : Smooth f

Alias of AlgebraicGeometry.SmoothOfRelativeDimension.smooth.

---

If f is smooth of any relative dimension, it is smooth.

instance AlgebraicGeometry.instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension (n : ℕ) : HasRingHomProperty (@SmoothOfRelativeDimension n) fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension n

The property of scheme morphisms SmoothOfRelativeDimension n is associated with the ring homomorphism property Locally (IsStandardSmoothOfRelativeDimension n).

theorem AlgebraicGeometry.smoothOfRelativeDimension_isStableUnderBaseChange (n : ℕ) : CategoryTheory.MorphismProperty.IsStableUnderBaseChange (@SmoothOfRelativeDimension n)

Smooth of relative dimension n is stable under base change.

@[deprecated AlgebraicGeometry.smoothOfRelativeDimension_isStableUnderBaseChange (since := "2026-02-09")]

theorem AlgebraicGeometry.isSmoothOfRelativeDimension_isStableUnderBaseChange (n : ℕ) : CategoryTheory.MorphismProperty.IsStableUnderBaseChange (@SmoothOfRelativeDimension n)

Alias of AlgebraicGeometry.smoothOfRelativeDimension_isStableUnderBaseChange.

---

Smooth of relative dimension n is stable under base change.

@[instance 900]

instance AlgebraicGeometry.instSmoothOfRelativeDimensionOfNatNatOfIsOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : SmoothOfRelativeDimension 0 f

Open immersions are smooth of relative dimension 0.

@[instance 900]

instance AlgebraicGeometry.instSmoothOfIsOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : Smooth f

Open immersions are smooth.

instance AlgebraicGeometry.instSmoothFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [Smooth g] : Smooth (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.instSmoothSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [Smooth f] : Smooth (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.instSmoothMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [Smooth f] : Smooth (f ∣_ V)

instance AlgebraicGeometry.instSmoothResLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [Smooth f] : Smooth (Scheme.Hom.resLE f V U e)

instance AlgebraicGeometry.smoothOfRelativeDimension_comp (n m : ℕ) {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [hf : SmoothOfRelativeDimension n f] [hg : SmoothOfRelativeDimension m g] : SmoothOfRelativeDimension (n + m) (CategoryTheory.CategoryStruct.comp f g)

If f is smooth of relative dimension n and g is smooth of relative dimension m, then f ≫ g is smooth of relative dimension n + m.

instance AlgebraicGeometry.instSmoothOfRelativeDimensionOfNatNatCompScheme {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [SmoothOfRelativeDimension 0 f] [SmoothOfRelativeDimension 0 g] : SmoothOfRelativeDimension 0 (CategoryTheory.CategoryStruct.comp f g)

instance AlgebraicGeometry.instIsMultiplicativeSchemeSmoothOfRelativeDimensionOfNatNat : CategoryTheory.MorphismProperty.IsMultiplicative (@SmoothOfRelativeDimension 0)

Smooth of relative dimension 0 is multiplicative.

@[instance 100]

instance AlgebraicGeometry.instLocallyOfFinitePresentationOfSmooth {X Y : Scheme} (f : X ⟶ Y) [hf : Smooth f] : LocallyOfFinitePresentation f

Smooth morphisms are locally of finite presentation.

theorem AlgebraicGeometry.formallySmooth_stalkMap_iff {X Y : Scheme} {f : X ⟶ Y} {x : ↥X} (U : Y.Opens) (hU : IsAffineOpen U) (V : X.Opens) (hV : IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (hx : x ∈ V) : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔ hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑(Y.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op V))

theorem AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (x : ↥X) (H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth) : ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U), x ∈ V ∧ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).Smooth

theorem AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] : IsOpen {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}

def AlgebraicGeometry.Scheme.Hom.smoothLocus {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] : X.Opens

The set of points smooth over a base, as a Scheme.Opens.

theorem AlgebraicGeometry.Scheme.Hom.mem_smoothLocus {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFinitePresentation f] {x : ↥X} : x ∈ smoothLocus f ↔ (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth

theorem AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top {X Y : Scheme} (f : X ⟶ Y) [Smooth f] : smoothLocus f = ⊤

theorem AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top_iff {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFinitePresentation f] : smoothLocus f = ⊤ ↔ Smooth f

theorem AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq {X Y U : Scheme} (f : U ⟶ X) (g : X ⟶ Y) [IsOpenImmersion f] [LocallyOfFinitePresentation g] : (TopologicalSpace.Opens.map f.base).obj (smoothLocus g) = smoothLocus (CategoryTheory.CategoryStruct.comp f g)

theorem AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField {X : Scheme} {K : Type u} [Field K] [PerfectField K] [IsIntegral X] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFinitePresentation f] : genericPoint ↥X ∈ smoothLocus f

instance AlgebraicGeometry.instIsReducedToScheme_1 {X : Scheme} [IsReduced X] (U : X.Opens) : IsReduced ↑U

theorem AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField {X : Scheme} {K : Type u} [Field K] [PerfectField K] [IsReduced X] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFinitePresentation f] : Dense ↑(smoothLocus f)