Formally smooth local algebras

theorem Algebra.FormallySmooth.iff_injective_lTensor_residueField {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing S] [Algebra R S] (P : Extension R S) [FormallySmooth R P.Ring] [Module.Free P.Ring Ω[P.Ring⁄R]] [Module.Finite P.Ring Ω[P.Ring⁄R]] (h' : P.ker.FG) : FormallySmooth R S ↔ Function.Injective ⇑(LinearMap.lTensor (IsLocalRing.ResidueField S) P.cotangentComplex)

The Jacobian criterion for smoothness of local algebras. Suppose S is a local R-algebra, and 0 → I → P → S → 0 is a presentation such that P is formally-smooth over R, Ω[P⁄R] is finite free over P, (typically satisfied when P is the localization of a polynomial ring of finite type) and I is finitely generated. Then S is formally smooth iff k ⊗ₛ I/I² → k ⊗ₚ Ω[P/R] is injective, where k is the residue field of S.

theorem Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing S] [Algebra R S] (P : Type u_3) [CommRing P] [Algebra R P] [Algebra P S] [IsScalarTower R P S] [FormallySmooth R P] [Module.Free P Ω[P⁄R]] [Module.Finite P Ω[P⁄R]] (h₁ : Function.Surjective ⇑(algebraMap P S)) (h₂ : (RingHom.ker (algebraMap P S)).FG) : FormallySmooth R S ↔ Function.Injective ⇑(KaehlerDifferential.cotangentComplexBaseChange R S P (IsLocalRing.ResidueField S))

theorem Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing S] [Algebra R S] (P : Type u_3) (K : Type u_4) [Field K] [CommRing P] [Algebra R P] [Algebra P S] [IsScalarTower R P S] [Algebra S K] [Algebra P K] [IsScalarTower P S K] [FormallySmooth R P] [Module.Free P Ω[P⁄R]] [Module.Finite P Ω[P⁄R]] (h₁ : Function.Surjective ⇑(algebraMap P S)) (h₂ : (RingHom.ker (algebraMap P S)).FG) (h₃ : IsLocalRing.maximalIdeal S ≤ RingHom.ker (algebraMap S K)) : FormallySmooth R S ↔ Function.Injective ⇑(KaehlerDifferential.cotangentComplexBaseChange R S P K)

The Jacobian criterion for smoothness of local algebras. Suppose S is a local R-algebra, and 0 → I → P → S → 0 is a presentation such that P is formally-smooth over R, Ω[P⁄R] is finite free over P, (typically satisfied when P is the localization of a polynomial ring of finite type) and I is finitely generated. Then S is formally smooth iff k ⊗ₛ I → k ⊗ₚ Ω[P/R] is injective, where k any field extension of the residue field of S.