Smoothness of the special linear group

The coordinate algebra of SLₙ is smooth over every commutative ring. The proof uses the infinitesimal lifting criterion for formal smoothness. Under the algebra-valued-points equivalence, lifting a coordinate-algebra map through a square-zero quotient is exactly lifting a special-linear matrix; Matrix.SpecialLinearGroup.map_quotient_mk_surjective_of_isNilpotent supplies that lift. Finite presentation is inherited from the determinant localization presenting GLₙ and the principal determinant-one quotient presenting SLₙ.

The result is valid in every natural rank, including rank zero, over bases with zero divisors and in every characteristic.

Main declarations

• TauCeti.SpecialLinear.instSmoothCoordinateHopfAlgebra: the coordinate algebra of SLₙ is smooth.
• TauCeti.SpecialLinear.smoothCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra: the same result stated for the finite-type commutative Hopf algebra.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 2.
• The Stacks Project, Tag 00TI (formal smoothness), and Tags 00T2 and 00TN (equivalent notions of smooth algebras).

instance TauCeti.SpecialLinear.instSmoothCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : Algebra.Smooth R ↑(coordinateHopfAlgebra R n)

The coordinate algebra of SLₙ is smooth over every commutative ring.

theorem TauCeti.SpecialLinear.smoothCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : smoothCommHopfAlgProperty R (finiteTypeCoordinateHopfAlgebra R n).obj

The finite-type commutative Hopf algebra representing SLₙ has smooth coordinate ring.