Smooth morphisms

An R-algebra A is formally smooth if Ω[A⁄R] is A-projective and H¹(L_{A/R}) = 0. This is equivalent to the standard definition that "for every R-algebra B, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists at least one lift A →ₐ[R] B". An R-algebra A is smooth if it is formally smooth and of finite presentation.

We show that the property of being formally smooth extends onto nilpotent ideals, and that it is stable under R-algebra homomorphisms and compositions.

We show that smooth is stable under algebra isomorphisms, composition and localization at an element.

Main results

• Algebra.FormallySmooth: The class of formally smooth algebras.
• Algebra.formallySmooth_iff : Formally smooth iff Ω[A⁄R] is A-projective and H¹(L_{A/R}) = 0.
• Algebra.FormallySmooth.lift: If A is formally smooth and I is nilpotent, any map A →ₐ[R] B ⧸ I lifts to A →ₐ[R] B.
• Algebra.FormallySmooth.iff_comp_surjective: A is formally smooth iff any map A →ₐ[R] B ⧸ I lifts to A →ₐ[R] B for any square zero I.

Suppose P is a formally smooth R algebra that surjects onto A with kernel I, then

• Algebra.FormallySmooth.iff_split_surjection: A is formally smooth iff the algebra map P ⧸ I² →ₐ[R] A has an R-algebra section.
• Algebra.Extension.equivH1CotangentOfFormallySmooth: H¹(L_{A/R}) is isomorphic to ker(I/I² → A ⊗[P] Ω[P⁄R]).
• Algebra.FormallySmooth.iff_split_injection: A is formally smooth iff the P-linear map I/I² → A ⊗[P] Ω[P⁄R] is split injective.

class Algebra.FormallySmooth (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] : Prop

An R-algebra A is formally smooth if Ω[A⁄R] is A-projective and H¹(L_{A/R}) = 0. For the infinitesimal lifting definition, see FormallySmooth.lift and FormallySmooth.iff_comp_surjective.

• projective_kaehlerDifferential : Module.Projective A Ω[A⁄R]
• subsingleton_h1Cotangent : Subsingleton (H1Cotangent R A)

theorem Algebra.formallySmooth_iff (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] : FormallySmooth R A ↔ Module.Projective A Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A)

@[deprecated Algebra.formallySmooth_iff (since := "2025-10-25")]

theorem Algebra.FormallySmooth.iff_subsingleton_and_projective (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] : FormallySmooth R A ↔ Module.Projective A Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A)

Alias of Algebra.formallySmooth_iff.

theorem Algebra.FormallySmooth.comp_surjective (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] [FormallySmooth R A] (I : Ideal B) (hI : I ^ 2 = ⊥) : Function.Surjective (Ideal.Quotient.mkₐ R I).comp

instance Algebra.mvPolynomial {R : Type u} [CommRing R] (σ : Type u_4) : FormallySmooth R (MvPolynomial σ R)

theorem Algebra.FormallySmooth.exists_lift {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] [FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) : ∃ (f : A →ₐ[R] B), (Ideal.Quotient.mkₐ R I).comp f = g

noncomputable def Algebra.FormallySmooth.lift {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] [FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) : A →ₐ[R] B

For a formally smooth R-algebra A and a map f : A →ₐ[R] B ⧸ I with I square-zero, this is an arbitrary lift A →ₐ[R] B.

Equations

• Algebra.FormallySmooth.lift I hI g = ⋯.choose

@[simp]

theorem Algebra.FormallySmooth.comp_lift {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] [FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) : (Ideal.Quotient.mkₐ R I).comp (lift I hI g) = g

@[simp]

theorem Algebra.FormallySmooth.mk_lift {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] [FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) (x : A) : (Ideal.Quotient.mk I) ((lift I hI g) x) = g x

noncomputable def Algebra.FormallySmooth.liftOfSurjective {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] {C : Type u_4} [CommRing C] [Algebra R C] [FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective ⇑g) (hg' : IsNilpotent (RingHom.ker ↑g)) : A →ₐ[R] B

For a formally smooth R-algebra A and a map f : A →ₐ[R] B ⧸ I with I nilpotent, this is an arbitrary lift A →ₐ[R] B.

Equations

• Algebra.FormallySmooth.liftOfSurjective f g hg hg' = Algebra.FormallySmooth.lift (RingHom.ker ↑g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)

@[simp]

theorem Algebra.FormallySmooth.liftOfSurjective_apply {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] {C : Type u_4} [CommRing C] [Algebra R C] [FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective ⇑g) (hg' : IsNilpotent (RingHom.ker g)) (x : A) : g ((liftOfSurjective f g hg hg') x) = f x

@[simp]

theorem Algebra.FormallySmooth.comp_liftOfSurjective {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_1} [CommRing B] [Algebra R B] {C : Type u_4} [CommRing C] [Algebra R C] [FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective ⇑g) (hg' : IsNilpotent (RingHom.ker ↑g)) : g.comp (liftOfSurjective f g hg hg') = f

noncomputable def Algebra.Extension.homInfinitesimal {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (P₁ : Extension R A) (P₂ : Extension R A) [FormallySmooth R P₁.Ring] : P₁.infinitesimal.Hom P₂.infinitesimal

Given extensions 0 → I₁ → P₁ → A → 0 and 0 → I₂ → P₂ → A → 0 with P₁ formally smooth, this is an arbitrarily chosen map P₁/I₁² → P₂/I₂² of extensions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebra.Extension.H1Cotangent.equivOfFormallySmooth {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (P₁ : Extension R A) (P₂ : Extension R A) [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] : P₁.H1Cotangent ≃ₗ[A] P₂.H1Cotangent

Formally smooth extensions have isomorphic H¹(L_P).

Equations

• One or more equations did not get rendered due to their size.

theorem Algebra.Extension.H1Cotangent.equivOfFormallySmooth_toLinearMap {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {P₁ : Extension R A} {P₂ : Extension R A} (f : P₁.Hom P₂) [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] : ↑(equivOfFormallySmooth P₁ P₂) = map f

theorem Algebra.Extension.H1Cotangent.equivOfFormallySmooth_apply {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {P₁ : Extension R A} {P₂ : Extension R A} (f : P₁.Hom P₂) [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] (x : P₁.H1Cotangent) : (equivOfFormallySmooth P₁ P₂) x = (map f) x

theorem Algebra.Extension.H1Cotangent.equivOfFormallySmooth_symm {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (P₁ : Extension R A) (P₂ : Extension R A) [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] : (equivOfFormallySmooth P₁ P₂).symm = equivOfFormallySmooth P₂ P₁

noncomputable def Algebra.Extension.equivH1CotangentOfFormallySmooth {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (P : Extension R A) [FormallySmooth R P.Ring] : P.H1Cotangent ≃ₗ[A] H1Cotangent R A

Any formally smooth extension can be used to calculate H¹(L_{A/R}).

Equations

• P.equivH1CotangentOfFormallySmooth = Algebra.Extension.H1Cotangent.equivOfFormallySmooth P (Algebra.Generators.self R A).toExtension

theorem Algebra.Extension.cotangentComplex_injective_iff {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (P : Extension R A) [FormallySmooth R P.Ring] : Function.Injective ⇑P.cotangentComplex ↔ Subsingleton (H1Cotangent R A)

theorem Algebra.FormallySmooth.kerCotangentToTensor_injective_iff {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {P : Type u_2} [CommRing P] [Algebra R P] [FormallySmooth R P] [Algebra P A] [IsScalarTower R P A] (hf : Function.Surjective ⇑(algebraMap P A)) : Function.Injective ⇑(KaehlerDifferential.kerCotangentToTensor R P A) ↔ Subsingleton (H1Cotangent R A)

theorem Algebra.FormallySmooth.iff_split_injection {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {P : Type u_2} [CommRing P] [Algebra R P] [FormallySmooth R P] [Algebra P A] [IsScalarTower R P A] (hf : Function.Surjective ⇑(algebraMap P A)) : FormallySmooth R A ↔ ∃ (l : TensorProduct P A Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P A)).Cotangent), l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P A = LinearMap.id

Given a formally smooth R-algebra P and a surjective algebra homomorphism f : P →ₐ[R] A with kernel I (typically a presentation R[X] → A), A is formally smooth iff the P-linear map I/I² → A ⊗[P] Ω[P⁄R] is split injective. Also see Algebra.Extension.formallySmooth_iff_split_injection for the version in terms of Extension.

theorem Algebra.Extension.formallySmooth_iff_split_injection {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (P : Extension R A) [FormallySmooth R P.Ring] : FormallySmooth R A ↔ ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id

Given a formally smooth R-algebra P and a surjective algebra homomorphism f : P →ₐ[R] S with kernel I (typically a presentation R[X] → S), S is formally smooth iff the P-linear map I/I² → S ⊗[P] Ω[P⁄R] is split injective.

theorem Algebra.FormallySmooth.iff_split_surjection {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {P : Type u_2} [CommRing P] [Algebra R P] [FormallySmooth R P] (f : P →ₐ[R] A) (hf : Function.Surjective ⇑f) : FormallySmooth R A ↔ ∃ (g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2), f.kerSquareLift.comp g = AlgHom.id R A

Let P →ₐ[R] A be a surjection with kernel J, and P a formally smooth R-algebra, then A is formally smooth over R iff the surjection P ⧸ J ^ 2 →ₐ[R] A has a section.

Geometric intuition: we require that a first-order thickening of Spec A inside Spec P admits a retraction.

theorem Algebra.FormallySmooth.of_split {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {P : Type u_2} [CommRing P] [Algebra R P] [FormallySmooth R P] (f : P →ₐ[R] A) (g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2) (h : f.kerSquareLift.comp g = AlgHom.id R A) : FormallySmooth R A

theorem Algebra.FormallySmooth.of_comp_surjective {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (H : ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp) : FormallySmooth R A

theorem Algebra.FormallySmooth.iff_comp_surjective {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] : FormallySmooth R A ↔ ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp

An R-algebra A is formally smooth iff "for every R-algebra B, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists at least one lift A →ₐ[R] B".

theorem Algebra.FormallySmooth.of_equiv {R : Type u_4} [CommRing R] {A : Type u_5} {B : Type u_6} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [FormallySmooth R A] (e : A ≃ₐ[R] B) : FormallySmooth R B

theorem Algebra.FormallySmooth.iff_of_equiv {R : Type u_4} [CommRing R] {A : Type u_5} {B : Type u_6} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (e : A ≃ₐ[R] B) : FormallySmooth R A ↔ FormallySmooth R B

instance Algebra.FormallySmooth.polynomial (R : Type u_4) [CommRing R] : FormallySmooth R (Polynomial R)

instance Algebra.FormallySmooth.inst {R : Type u} [CommRing R] : FormallySmooth R R

theorem Algebra.FormallySmooth.comp (R : Type u_4) [CommRing R] (A : Type u_5) [CommRing A] [Algebra R A] (B : Type u_6) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [FormallySmooth R A] [FormallySmooth A B] : FormallySmooth R B

theorem Algebra.FormallySmooth.of_restrictScalars (R : Type u_4) [CommRing R] (A : Type u_5) [CommRing A] [Algebra R A] (B : Type u_6) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [FormallyUnramified R A] [FormallySmooth R B] : FormallySmooth A B

theorem Algebra.FormallySmooth.iff_of_surjective {R : Type u_4} [CommRing R] {A : Type u_6} [CommRing A] [Algebra R A] (h : Function.Surjective ⇑(algebraMap R A)) : FormallySmooth R A ↔ IsIdempotentElem (RingHom.ker (algebraMap R A))

instance Algebra.FormallySmooth.instTensorProduct {R : Type u_4} [CommRing R] {A : Type u_5} [CommRing A] [Algebra R A] (B : Type u_6) [CommRing B] [Algebra R B] [FormallySmooth R A] : FormallySmooth B (TensorProduct R B A)

theorem Algebra.FormallySmooth.of_isLocalization {R : Type u_4} {Rₘ : Type u_6} [CommRing R] [CommRing Rₘ] (M : Submonoid R) [Algebra R Rₘ] [IsLocalization M Rₘ] : FormallySmooth R Rₘ

theorem Algebra.FormallySmooth.localization_base {R : Type u_4} {Rₘ : Type u_6} {Sₘ : Type u_7} [CommRing R] [CommRing Rₘ] [CommRing Sₘ] (M : Submonoid R) [Algebra R Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsLocalization M Rₘ] [FormallySmooth R Sₘ] : FormallySmooth Rₘ Sₘ

theorem Algebra.FormallySmooth.localization_map {R : Type u_4} {A : Type u_5} {Rₘ : Type u_6} {Sₘ : Type u_7} [CommRing R] [CommRing A] [CommRing Rₘ] [CommRing Sₘ] (M : Submonoid R) [Algebra R A] [Algebra R Sₘ] [Algebra A Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R A Sₘ] [IsLocalization M Rₘ] [IsLocalization (Submonoid.map (algebraMap R A) M) Sₘ] [FormallySmooth R A] : FormallySmooth Rₘ Sₘ

class Algebra.Smooth (R : Type u_4) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] : Prop

An R algebra A is smooth if it is formally smooth and of finite presentation.

• formallySmooth : FormallySmooth R A
• finitePresentation : FinitePresentation R A

theorem Algebra.smooth_iff (R : Type u_4) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] : Smooth R A ↔ autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧ autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam

theorem Algebra.Smooth.of_equiv {R : Type u_4} [CommRing R] {A : Type u_5} {B : Type u_6} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Smooth R A] (e : A ≃ₐ[R] B) : Smooth R B

Being smooth is transported via algebra isomorphisms.

theorem Algebra.Smooth.of_isLocalization_Away {R : Type u_4} [CommRing R] {A : Type u_5} [CommRing A] [Algebra R A] (r : R) [IsLocalization.Away r A] : Smooth R A

Localization at an element is smooth.

theorem Algebra.Smooth.comp (R : Type u_4) [CommRing R] (A : Type u_5) (B : Type u_6) [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Smooth R A] [Smooth A B] : Smooth R B

Smooth is stable under composition.

instance Algebra.Smooth.baseChange (R : Type u_4) [CommRing R] (A : Type u_5) (B : Type u_6) [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Smooth R A] : Smooth B (TensorProduct R B A)

Smooth is stable under base change.