The conormal sequence of a formally smooth quotient

Let P → S be a surjection of R-algebras with kernel I. The conormal sequence

I/I² → S ⊗[P] Ω[P⁄R] → Ω[S⁄R] → 0

is exact (KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange). If S is formally smooth over R, the identity of S lifts along the square-zero extension P/I² → S, and such a section is the same as a retraction of I/I² → S ⊗[P] Ω[P⁄R] (retractionKerCotangentToTensorEquivSection). So the first map is injective, and the sequence is exact on the left as well. If S is moreover formally unramified, then Ω[S⁄R] = 0 and the conormal module I/I² is identified with S ⊗[P] Ω[P⁄R].

For a closed point of a scheme over a field whose residue field is separable over the base, this identifies the Zariski cotangent space 𝔪/𝔪² with the fibre of the differentials.

Main results

• KaehlerDifferential.kerCotangentToTensor_injective_of_formallySmooth: the conormal map I/I² → S ⊗[P] Ω[P⁄R] is injective when S is formally smooth over R.
• KaehlerDifferential.kerCotangentToTensor_bijective_of_formallyEtale: it is bijective when S is formally étale over R.

References

• Stacks Project, Tag 031I: a quotient P/I is formally smooth exactly when the conormal sequence is split exact on the left, given P formally smooth. Only the implication from formal smoothness to injectivity is used here, and it needs no hypothesis on P.

theorem KaehlerDifferential.kerCotangentToTensor_injective_of_formallySmooth {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] [Algebra.FormallySmooth R S] (hf : Function.Surjective ⇑(algebraMap P S)) : Function.Injective ⇑(kerCotangentToTensor R P S)

For a surjection P → S with kernel I onto a formally smooth R-algebra, the conormal map I/I² → S ⊗[P] Ω[P⁄R] is injective.

theorem KaehlerDifferential.kerCotangentToTensor_bijective_of_formallyEtale {R : Type u_1} {P : Type u_2} {S : Type u_3} [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S] [IsScalarTower R P S] [Algebra.FormallyEtale R S] (hf : Function.Surjective ⇑(algebraMap P S)) : Function.Bijective ⇑(kerCotangentToTensor R P S)

For a surjection P → S with kernel I onto a formally étale R-algebra, the conormal map I/I² → S ⊗[P] Ω[P⁄R] is bijective.