The special linear group is reductive

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

Smoothness and geometric connectedness are established directly for the special-linear coordinate algebra. Over an algebraically closed field, smoothness makes a subgroup coordinate ring reduced, while geometric unipotence says that all of its points act unipotently. The general normal-invariants theorem then makes the subgroup act trivially on every completely reducible ambient representation. The standard representation of SL_n is simple in positive rank, hence completely reducible, and it is faithful in every rank. Faithfulness therefore identifies the subgroup's defining ideal with the augmentation ideal. The zero-rank case is handled directly using the zero-dimensional standard representation.

The final theorem transports the normal-subgroup argument across the canonical identification

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

Its final reductivity assembly is adapted from TauCeti.GeneralLinear.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra, with the common geometric-fibre transport factored through the generic reductivity API.

Main declaration

• TauCeti.SpecialLinear.eq_augmentation_of_isNormal_of_smoothUnipotent: a normal smooth unipotent closed subgroup of SL_n over an algebraically closed field is the identity subgroup.
• TauCeti.SpecialLinear.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra: SL_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 completes the SL_n worked example in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

theorem TauCeti.SpecialLinear.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 SL_n over an algebraically closed field is trivial. No positivity hypothesis on n is needed.

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

The special linear group is reductive over every field.