Projective cotangent modules at augmented points #
For an augmentation f : A →ₐ[R] R, the module ker(f) / ker(f)² is projective over R
when A is formally smooth. This does not require a noetherian base or a finite-type
algebra. It supplies the projectivity input for forming the adjoint comodule of a
smooth affine group over a ring.
The comparison uses Mathlib's Algebra.Extension.cotangentComplex and its splitting
criterion for formal smoothness. This map is split injective, exhibiting the cotangent
module as a direct summand of the
fiber of the projective module of differentials of A.
References #
- The Stacks Project, Tags 00TH and 031I (cotangent sequence and formal smoothness).
- B. Conrad, Reductive Group Schemes, §3.1 (the Lie algebra over a base).
theorem
AlgHom.projective_cotangent_ker_of_formallySmooth
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[CommRing A]
[Algebra R A]
(f : A →ₐ[R] R)
[Algebra.FormallySmooth R A]
:
The cotangent module at an augmented point of a formally smooth algebra is projective over the base. No finiteness or noetherian hypothesis is needed.