Formally smooth local algebras

theorem Algebra.FormallySmooth.iff_injective_lTensor_residueField {R S : Type u_1} [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.