The general linear group is reductive

The coordinate Hopf algebra of GL_n is reductive over every field and in every natural rank. The proof uses the geometric definition, so it works in arbitrary characteristic.

First, the determinant localization defining O(GL_n) is smooth and geometrically connected. For the normal-subgroup condition, work over an algebraically closed field and let I cut out a normal smooth unipotent closed subgroup. The simple standard GL_n-comodule is completely reducible, so the general normal-unipotent elimination theorem makes the subgroup act trivially. Faithfulness of the standard representation then identifies I with the augmentation ideal.

The final theorem transports this argument across the canonical identification

AlgebraicClosure k ⊗[k] O(GL_n) ≃ O(GL_n, AlgebraicClosure k).

Main declarations

• TauCeti.GeneralLinear.eq_augmentation_of_isNormal_of_smoothUnipotent: a normal smooth unipotent closed subgroup of GL_n over an algebraically closed field is trivial.
• TauCeti.GeneralLinear.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra: GL_n is reductive.

References

• J. S. Milne, Algebraic Groups (2017), §§4.a, 5, 19.b, and Chapter 14.
• T. A. Springer, Linear Algebraic Groups, §§2.2 and 2.4.

This gives the reductivity half of the GL_n worked example requested alongside Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. The characteristic-zero complete-reducibility route remains open.

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

A normal smooth unipotent closed subgroup of GL_n over an algebraically closed field is trivial. No positivity hypothesis on n is needed.

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

The general linear group is reductive over every field.