Smoothness of the symplectic group

The coordinate algebra of the standard symplectic group Sp_{2m} is smooth over every commutative ring. The infinitesimal lifting criterion turns a lift of a coordinate-algebra map through a square-zero quotient into a lift of the corresponding symplectic matrix. The matrix lift is supplied by TauCeti.GLSymplectic.map_quotient_mk_surjective_of_sq_eq_bot.

Finite presentation follows from the finite set of entries of the matrix equation X J_m X^T = J_m cutting the symplectic group out of GL_{2m}.

Main declarations

• TauCeti.Symplectic.instSmoothCoordinateHopfAlgebra: the coordinate algebra of Sp_{2m} is smooth over its ground ring.
• TauCeti.Symplectic.smoothCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra: the same result for the bundled finite-type commutative Hopf algebra.

References

• SGA 3, Exposé XXII, for the split symplectic group scheme.
• The Stacks Project, Tags 00TH, 00TI, 00T2, and 00TN, for formal smoothness and smooth algebras.

This supplies the smoothness prerequisite for the Sp_{2n} reductivity worked example in Layer 6 of the ReductiveGroups roadmap.

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

The coordinate algebra of Sp_{2m} is smooth over every commutative ring.

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

The finite-type commutative Hopf algebra representing Sp_{2m} has smooth coordinate ring.