The symplectic group is reductive

The coordinate Hopf algebra of the standard symplectic group Sp₂ₘ is reductive over every field, in every natural rank and in arbitrary characteristic.

The coordinate algebra is smooth and geometrically connected. To eliminate a normal smooth unipotent closed subgroup over an algebraically closed field, use the standard representation. It is simple in positive rank, hence completely reducible, while in rank zero its carrier is a singleton. Normal unipotent subgroups therefore act trivially on it. Since the standard representation is faithful in every rank, the subgroup is the identity subgroup.

The result over an arbitrary field follows by transporting this argument across the canonical base-change identification

AlgebraicClosure k ⊗[k] O(Sp₂ₘ) ≃ O(Sp₂ₘ, AlgebraicClosure k).

Main declarations

• TauCeti.Symplectic.eq_augmentation_of_isNormal_of_smoothUnipotent: a normal smooth unipotent closed subgroup of Sp₂ₘ over an algebraically closed field is trivial.
• TauCeti.Symplectic.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra: Sp₂ₘ is reductive over every field.

References

• J. S. Milne, Algebraic Groups (2017), §§19.b and 24.6.
• T. A. Springer, Linear Algebraic Groups, §§2.2, 2.4, and Chapter 8.

theorem TauCeti.Symplectic.eq_augmentation_of_isNormal_of_smoothUnipotent (k : Type u) [Field k] [IsAlgClosed k] (m : ℕ) (I : HopfIdeal k ↑(finiteTypeCoordinateHopfAlgebra k m).obj) (hI : I.IsNormal) (hU : smoothUnipotentCommHopfAlgProperty k ((finiteTypeCoordinateHopfAlgebra k m).quotient I)) : I = HopfIdeal.augmentation k ↑(finiteTypeCoordinateHopfAlgebra k m).obj

A normal smooth unipotent closed subgroup of Sp₂ₘ over an algebraically closed field is trivial. No positivity hypothesis on m is needed.

theorem TauCeti.Symplectic.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra (k : Type u) [Field k] (m : ℕ) : reductiveCommHopfAlgProperty k (finiteTypeCoordinateHopfAlgebra k m)

The standard symplectic group is reductive over every field.