The special linear group is semisimple

The group SL_n is semisimple over every field, including in characteristics dividing n. A connected smooth normal solvable subgroup acts by scalars on the simple standard representation. Determinant one restricts those scalars to the finite set of nth roots of unity. A regular function with finite image on a reduced connected affine scheme is constant, so the subgroup acts trivially. Faithfulness of the standard representation identifies its defining ideal with the augmentation ideal.

The argument uses HopfIdeal.exists_basePointsRepresentation_eq_smul, eq_algebraMap_of_finite_range_eval, and the standard special-linear comodule. Smoothness is essential for the subgroup: this does not assert triviality of non-smooth connected central subgroup schemes such as μ_p in SL_p. The zero-rank case uses the faithful zero-dimensional representation separately.

References

• J. E. Humphreys, Linear Algebraic Groups, §§19 and 27.
• J. S. Milne, Algebraic Groups (2017), Chapter 21.

theorem TauCeti.SpecialLinear.eq_augmentation_of_isNormal_of_isSolvable {k : Type u} [Field k] [IsAlgClosed k] (n : ℕ) (I : HopfIdeal k ↑(coordinateHopfAlgebra k n)) (hI : I.IsNormal) [IsReduced ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) I)] [ConnectedSpace (PrimeSpectrum ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) I))] [Group.IsSolvable (WithConv (↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) I) →ₐ[k] k))] : I = HopfIdeal.augmentation k ↑(coordinateHopfAlgebra k n)

Every connected reduced normal solvable closed subgroup of SL_n over an algebraically closed field is trivial. Reducedness may be supplied by smoothness, but is the only subgroup regularity needed here.

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

The special linear group is semisimple over every field and in every rank.