Geometric connectedness of the symplectic group

The coordinate Hopf algebra of the standard symplectic group Sp_{2m} is geometrically connected over every field. The proof uses idempotents and algebraically closed points, avoiding an explicit presentation of the coordinate algebra as an integral domain.

The formal proof architecture is adapted from TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Connected.

Over an algebraically closed extension, an idempotent in a finite-type coordinate algebra is constant once right translation by every rational point fixes it. Every standard symplectic root subgroup is connected to the identity by its parameter over the polynomial ring. The root-subgroup generation theorem for Sp_{2m} therefore makes every rational-point translation fix every idempotent. This argument includes rank zero, where the family of roots is empty and the generation theorem still applies.

Main declaration

• TauCeti.Symplectic.geometricallyConnectedCommHopfAlgProperty_coordinateHopfAlgebra: Sp_{2m} is geometrically connected.

References

• R. W. Carter, Simple Groups of Lie Type, §5.2.
• J. E. Humphreys, Linear Algebraic Groups, §26.

theorem TauCeti.Symplectic.instIsScalarTowerPolynomial_tauCeti {k K : Type u} [Field k] [Field K] [Algebra k K] : IsScalarTower k K (Polynomial K)

theorem TauCeti.Symplectic.geometricallyConnectedCommHopfAlgProperty_coordinateHopfAlgebra (k : Type u) [Field k] (m : ℕ) : geometricallyConnectedCommHopfAlgProperty k (coordinateHopfAlgebra k m)

The coordinate Hopf algebra of Sp_{2m} is geometrically connected over every field.