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