Smoothness of the special orthogonal group

When 2 is invertible in the ground ring, the coordinate algebra of the standard special orthogonal group SOₙ is smooth. The infinitesimal lifting criterion turns a lift of a coordinate-algebra map through a square-zero quotient into a lift of the corresponding special orthogonal matrix. The matrix lift is supplied by Matrix.SpecialOrthogonalGroup.map_quotient_mk_surjective_of_sq_eq_bot.

Finite presentation follows because the defining ideal is generated by the finitely many entries of X Xᵀ - 1 together with det X - 1. The proof follows the formal-smoothness route used for TauCeti.Symplectic, with the half-error correction particular to symmetric forms.

Main declarations

• TauCeti.SpecialOrthogonal.instSmoothCoordinateHopfAlgebra: the coordinate algebra of SOₙ is smooth when 2 is invertible.
• TauCeti.SpecialOrthogonal.smoothCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra: the same result for the bundled finite-type commutative Hopf algebra.

References

• SGA 3, Exposé XXIII, for split orthogonal group schemes away from characteristic two.
• The Stacks Project, Tags 00TH, 00TI, 00T2, and 00TN, for formal smoothness and smooth algebras.

This supplies the smoothness prerequisite for the SOₙ reductivity worked example in Layer 6 of the ReductiveGroups roadmap.

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

The coordinate algebra of SOₙ is smooth when 2 is invertible in the ground ring.

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

The finite-type commutative Hopf algebra representing SOₙ has smooth coordinate ring when 2 is invertible in the ground ring.