Relation of smoothness and Ω[S⁄R]

Main results

• retractionKerToTensorEquivSection: Given a surjective algebra homomorphism f : P →ₐ[R] S with square-zero kernel I, there is a one-to-one correspondence between P-linear retractions of I →ₗ[P] S ⊗[P] Ω[P/R] and algebra homomorphism sections of f.
• retractionKerCotangentToTensorEquivSection: Given a surjective algebra homomorphism f : P →ₐ[R] S with kernel I, there is a one-to-one correspondence between P-linear retractions of I/I² →ₗ[P] S ⊗[P] Ω[P/R] and algebra homomorphism sections of f‾ : P/I² → S.
• Algebra.FormallySmooth.iff_split_injection: 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.
• Algebra.FormallySmooth.iff_injective_and_projective: 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), then S is formally smooth iff Ω[S/R] is projective and I/I² → S ⊗[P] Ω[P⁄R] is injective.
• Algebra.FormallySmooth.iff_subsingleton_and_projective: An algebra is formally smooth if and only if H¹(L_{R/S}) = 0 and Ω_{S/R} is projective.
• Algebra.Extension.equivH1CotangentOfFormallySmooth: Any formally smooth extension can be used to calculate H¹(L_{S/R}).

Future projects

• Show that being smooth is local on stalks.
• Show that being formally smooth is Zariski-local (very hard).

References

• https://stacks.math.columbia.edu/tag/00TH
• [B. Iversen, Generic Local Structure of the Morphisms in Commutative Algebra][iversen]

def derivationOfSectionOfKerSqZero {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra R S] (f : P →ₐ[R] S) (hf' : RingHom.ker f ^ 2 = ⊥) (g : S →ₐ[R] P) (hg : f.comp g = AlgHom.id R S) : Derivation R P ↥(RingHom.ker f)

Given a surjective algebra homomorphism f : P →ₐ[R] S with square-zero kernel I, and a section g : S →ₐ[R] P (as an algebra homomorphism), we get an R-derivation P → I via x ↦ x - g (f x).

Equations

• derivationOfSectionOfKerSqZero f hf' g hg = { toFun := fun (x : P) => ⟨x - g (f x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

@[simp]

theorem derivationOfSectionOfKerSqZero_apply_coe {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra R S] (f : P →ₐ[R] S) (hf' : RingHom.ker f ^ 2 = ⊥) (g : S →ₐ[R] P) (hg : f.comp g = AlgHom.id R S) (x : P) : ↑((derivationOfSectionOfKerSqZero f hf' g hg) x) = x - g (f x)

theorem isScalarTower_of_section_of_ker_sqZero {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (g : S →ₐ[R] P) (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S) : IsScalarTower P S ↥(RingHom.ker (algebraMap P S))

noncomputable def retractionOfSectionOfKerSqZero {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (g : S →ₐ[R] P) (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S) : TensorProduct P S (Ω[P⁄R]) →ₗ[P] ↥(RingHom.ker (algebraMap P S))

Given a surjective algebra hom f : P →ₐ[R] S with square-zero kernel I, and a section g : S →ₐ[R] P (as algebra homs), we get a retraction of the injection I → S ⊗[P] Ω[P/R].

Equations

• retractionOfSectionOfKerSqZero g hf' hg = ↑P (LinearMap.liftBaseChange S (derivationOfSectionOfKerSqZero (IsScalarTower.toAlgHom R P S) hf' g hg).liftKaehlerDifferential)

@[simp]

theorem retractionOfSectionOfKerSqZero_tmul_D {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (g : S →ₐ[R] P) (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S) (s : S) (t : P) : ↑((retractionOfSectionOfKerSqZero g hf' hg) (s ⊗ₜ[P] (KaehlerDifferential.D R P) t)) = g s * t - g s * g ((algebraMap P S) t)

theorem retractionOfSectionOfKerSqZero_comp_kerToTensor {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (g : S →ₐ[R] P) (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S) : retractionOfSectionOfKerSqZero g hf' hg ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id

theorem sectionOfRetractionKerToTensorAux_prop {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (x y : P) (h : (algebraMap P S) x = (algebraMap P S) y) : x - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) x)) = y - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) y))

noncomputable def sectionOfRetractionKerToTensorAux {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (σ : S → P) (hσ : ∀ (x : S), (algebraMap P S) (σ x) = x) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) : S →ₐ[R] P

Given a surjective algebra homomorphism f : P →ₐ[R] S with square-zero kernel I. Let σ be an arbitrary (set-theoretic) section of f. Suppose we have a retraction l of the injection I →ₗ[P] S ⊗[P] Ω[P/R], then x ↦ σ x - l (1 ⊗ D (σ x)) is an algebra homomorphism and a section to f.

Equations

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

theorem sectionOfRetractionKerToTensorAux_algebraMap {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (σ : S → P) (hσ : ∀ (x : S), (algebraMap P S) (σ x) = x) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (x : P) : (sectionOfRetractionKerToTensorAux l hl σ hσ hf') ((algebraMap P S) x) = x - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) x))

theorem toAlgHom_comp_sectionOfRetractionKerToTensorAux {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (σ : S → P) (hσ : ∀ (x : S), (algebraMap P S) (σ x) = x) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) : (IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf') = AlgHom.id R S

noncomputable def sectionOfRetractionKerToTensor {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) : S →ₐ[R] P

Given a surjective algebra homomorphism f : P →ₐ[R] S with square-zero kernel I. Suppose we have a retraction l of the injection I →ₗ[P] S ⊗[P] Ω[P/R], then x ↦ σ x - l (1 ⊗ D (σ x)) is an algebra homomorphism and a section to f, where σ is an arbitrary (set-theoretic) section of f

Equations

• sectionOfRetractionKerToTensor l hl hf' hf = sectionOfRetractionKerToTensorAux l hl (fun (x : S) => ⋯.choose) ⋯ hf'

@[simp]

theorem sectionOfRetractionKerToTensor_algebraMap {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) (x : P) : (sectionOfRetractionKerToTensor l hl hf' hf) ((algebraMap P S) x) = x - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) x))

@[simp]

theorem toAlgHom_comp_sectionOfRetractionKerToTensor {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] ↥(RingHom.ker (algebraMap P S))) (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) : (IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensor l hl hf' hf) = AlgHom.id R S

noncomputable def retractionKerToTensorEquivSection {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) : { l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] ↥(RingHom.ker (algebraMap P S)) // l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id } ≃ { g : S →ₐ[R] P // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }

Given a surjective algebra homomorphism f : P →ₐ[R] S with square-zero kernel I, there is a one-to-one correspondence between P-linear retractions of I →ₗ[P] S ⊗[P] Ω[P/R] and algebra homomorphism sections of f.

Equations

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

noncomputable def derivationQuotKerSq (R P S : Type u) [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] : Derivation R (P ⧸ RingHom.ker (algebraMap P S) ^ 2) (TensorProduct P S (Ω[P⁄R]))

Given a tower of algebras S/P/R, with I = ker(P → S), this is the R-derivative P/I² → S ⊗[P] Ω[P⁄R] given by [x] ↦ 1 ⊗ D x.

Equations

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

@[simp]

theorem derivationQuotKerSq_mk {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (x : P) : (derivationQuotKerSq R P S) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) x) = 1 ⊗ₜ[P] (KaehlerDifferential.D R P) x

noncomputable def tensorKaehlerQuotKerSqEquiv (R P S : Type u) [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] : TensorProduct (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S (Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) ≃ₗ[S] TensorProduct P S (Ω[P⁄R])

Given a tower of algebras S/P/R, with I = ker(P → S) and Q := P/I², there is an isomorphism of S-modules S ⊗[Q] Ω[Q/R] ≃ S ⊗[P] Ω[P/R].

Equations

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

@[simp]

theorem tensorKaehlerQuotKerSqEquiv_tmul_D {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (s : S) (t : P) : (tensorKaehlerQuotKerSqEquiv R P S) (s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] (KaehlerDifferential.D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)) = s ⊗ₜ[P] (KaehlerDifferential.D R P) t

@[simp]

theorem tensorKaehlerQuotKerSqEquiv_symm_tmul_D {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (s : S) (t : P) : (tensorKaehlerQuotKerSqEquiv R P S).symm (s ⊗ₜ[P] (KaehlerDifferential.D R P) t) = s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] (KaehlerDifferential.D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)

noncomputable def retractionKerCotangentToTensorEquivSection {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (hf : Function.Surjective ⇑(algebraMap P S)) : { l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent // l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P S = LinearMap.id } ≃ { g : S →ₐ[R] P ⧸ RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom ^ 2 // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S }

Given a surjective algebra homomorphism f : P →ₐ[R] S with kernel I, there is a one-to-one correspondence between P-linear retractions of I/I² →ₗ[P] S ⊗[P] Ω[P/R] and algebra homomorphism sections of f‾ : P/I² → S.

Equations

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

theorem Algebra.FormallySmooth.iff_split_injection {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (hf : Function.Surjective ⇑(algebraMap P S)) [FormallySmooth R P] : FormallySmooth R S ↔ ∃ (l : TensorProduct P S (Ω[P⁄R]) →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent), l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P S = 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. Also see Algebra.Extension.formallySmooth_iff_split_injection for the version in terms of Extension.

Stacks Tag 031I

theorem Algebra.Extension.formallySmooth_iff_split_injection {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) [FormallySmooth R P.Ring] : FormallySmooth R S ↔ ∃ (l : P.CotangentSpace →ₗ[S] 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.

Stacks Tag 031I

theorem Algebra.FormallySmooth.iff_injective_and_split {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (hf : Function.Surjective ⇑(algebraMap P S)) [FormallySmooth R P] : FormallySmooth R S ↔ Function.Injective ⇑(KaehlerDifferential.kerCotangentToTensor R P S) ∧ ∃ (l : Ω[S⁄R] →ₗ[S] TensorProduct P S (Ω[P⁄R])), KaehlerDifferential.mapBaseChange R P S ∘ₗ l = 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), then S is formally smooth iff I/I² → S ⊗[P] Ω[S⁄R] is injective and S ⊗[P] Ω[P⁄R] → Ω[S⁄R] is split surjective.

instance instProjectiveKaehlerDifferential {R P : Type u} [CommRing R] [CommRing P] [Algebra R P] [Algebra.FormallySmooth R P] : Module.Projective P (Ω[P⁄R])

theorem Algebra.FormallySmooth.iff_injective_and_projective {R P S : Type u} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] (hf : Function.Surjective ⇑(algebraMap P S)) [FormallySmooth R P] : FormallySmooth R S ↔ Function.Injective ⇑(KaehlerDifferential.kerCotangentToTensor R P S) ∧ Module.Projective S (Ω[S⁄R])

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), then S is formally smooth iff I/I² → S ⊗[P] Ω[P⁄R] is injective and Ω[S/R] is projective.

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

An algebra is formally smooth if and only if H¹(L_{R/S}) = 0 and Ω_{S/R} is projective.

Stacks Tag 031J

instance instSubsingletonH1CotangentOfFormallySmooth {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallySmooth R S] : Subsingleton (Algebra.H1Cotangent R S)

theorem Algebra.Extension.CotangentSpace.map_toInfinitesimal_bijective {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Function.Bijective ⇑(CotangentSpace.map P.toInfinitesimal)

theorem Algebra.Extension.Cotangent.map_toInfinitesimal_bijective {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Function.Bijective ⇑(map P.toInfinitesimal)

theorem Algebra.Extension.H1Cotangent.map_toInfinitesimal_bijective {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) : Function.Bijective ⇑(map P.toInfinitesimal)

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

Given extensions 0 → I₁ → P₁ → S → 0 and 0 → I₂ → P₂ → S → 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 S : Type u} [CommRing R] [CommRing S] [Algebra R S] (P₁ P₂ : Extension R S) [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] : P₁.H1Cotangent ≃ₗ[S] 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 S : Type u} [CommRing R] [CommRing S] [Algebra R S] {P₁ P₂ : Extension R S} (f : P₁.Hom P₂) [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] : ↑(equivOfFormallySmooth P₁ P₂) = map f

theorem Algebra.Extension.H1Cotangent.equivOfFormallySmooth_apply {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] {P₁ P₂ : Extension R S} (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 S : Type u} [CommRing R] [CommRing S] [Algebra R S] (P₁ P₂ : Extension R S) [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] : (equivOfFormallySmooth P₁ P₂).symm = equivOfFormallySmooth P₂ P₁

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

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

Equations

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