Smooth morphisms

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).

In other words, smooth (resp. smooth of relative dimension n) for scheme morphisms is associated to the property of ring homomorphisms Locally IsStandardSmooth (resp. Locally (IsStandardSmoothOfRelativeDimension n)).

Implementation details

• Our definition is equivalent to defining IsSmooth as the associated scheme morphism property of the property of ring maps induced by Algebra.Smooth. The equivalence will follow from the equivalence of Locally IsStandardSmooth and Algebra.IsSmooth, but the latter is a (hard) TODO.

The reason why we choose the definition via IsStandardSmooth, is because verifying that Algebra.IsSmooth is local in the sense of RingHom.PropertyIsLocal is a (hard) TODO.

• The definition RingHom.IsStandardSmooth depends on universe levels for the generators and relations. For morphisms of schemes we set both to 0 to avoid unnecessary complications.

Notes

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

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

A morphism of schemes f : X ⟶ Y is smooth 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.

• exists_isStandardSmooth (x : ↑↑X.toPresheafedSpace) : ∃ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), (Scheme.Hom.appLE f (↑U) (↑V) e).hom.IsStandardSmooth

theorem AlgebraicGeometry.isSmooth_iff {X Y : Scheme} (f : X ⟶ Y) : IsSmooth f ↔ ∀ (x : ↑↑X.toPresheafedSpace), ∃ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), (Scheme.Hom.appLE f (↑U) (↑V) e).hom.IsStandardSmooth

instance AlgebraicGeometry.instHasRingHomPropertyIsSmoothLocallyIsStandardSmooth : HasRingHomProperty @IsSmooth fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.IsStandardSmooth

The property of scheme morphisms IsSmooth is associated with the ring homomorphism property Locally IsStandardSmooth.{0, 0}.

instance AlgebraicGeometry.instIsStableUnderCompositionSchemeIsSmooth : CategoryTheory.MorphismProperty.IsStableUnderComposition @IsSmooth

Being smooth is stable under composition.

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

The composition of smooth morphisms is smooth.

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

Smooth of relative dimension n is stable under base change.

class AlgebraicGeometry.IsSmoothOfRelativeDimension (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.toPresheafedSpace) : ∃ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), RingHom.IsStandardSmoothOfRelativeDimension n (Scheme.Hom.appLE f (↑U) (↑V) e).hom

theorem AlgebraicGeometry.isSmoothOfRelativeDimension_iff (n : ℕ) {X Y : Scheme} (f : X ⟶ Y) : IsSmoothOfRelativeDimension n f ↔ ∀ (x : ↑↑X.toPresheafedSpace), ∃ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), RingHom.IsStandardSmoothOfRelativeDimension n (Scheme.Hom.appLE f (↑U) (↑V) e).hom

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

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

instance AlgebraicGeometry.instHasRingHomPropertyIsSmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension (n : ℕ) : HasRingHomProperty (@IsSmoothOfRelativeDimension 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 IsSmoothOfRelativeDimension n is associated with the ring homomorphism property Locally (IsStandardSmoothOfRelativeDimension.{0, 0} n).

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

Smooth of relative dimension n is stable under base change.

@[instance 900]

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

Open immersions are smooth of relative dimension 0.

@[instance 900]

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

Open immersions are smooth.

instance AlgebraicGeometry.isSmoothOfRelativeDimension_comp (n m : ℕ) {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [hf : IsSmoothOfRelativeDimension n f] [hg : IsSmoothOfRelativeDimension m g] : IsSmoothOfRelativeDimension (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.instIsSmoothOfRelativeDimensionOfNatNatCompScheme {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [IsSmoothOfRelativeDimension 0 f] [IsSmoothOfRelativeDimension 0 g] : IsSmoothOfRelativeDimension 0 (CategoryTheory.CategoryStruct.comp f g)

instance AlgebraicGeometry.instIsMultiplicativeSchemeIsSmoothOfRelativeDimensionOfNatNat : CategoryTheory.MorphismProperty.IsMultiplicative (@IsSmoothOfRelativeDimension 0)

Smooth of relative dimension 0 is multiplicative.

@[instance 100]

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

Smooth morphisms are locally of finite presentation.