Points of diagonalizable groups are semisimple

A representation of a diagonalizable group D(G) = Spec R[G] decomposes into weight submodules (the internal direct sum of character spaces). Consequently, every point of D(G) acts on each representation by scalar multiplication on each weight space, making the underlying linear endomorphism diagonalizable and therefore semisimple.

This file proves that every point of a diagonalizable group is semisimple: for any commutative semiring R, any commutative group G, and any field K equipped with an R-algebra structure, every point g : WithConv (R[G] →ₐ[R] K) acts on every finitely generated comodule by a semisimple linear automorphism.

As a consequence, over a perfect field K, the multiplicative Jordan decomposition of every point g of a diagonalizable group is trivial: g_s = g and g_u = 1.

The result applies immediately to split tori and the roots-of-unity groups μ_n. Using the generic object property geometricallySemisimplePointsCommHopfAlgProperty, this file also packages the geometric statement for diagonalizable groups, which likewise applies directly to split tori.

Main declarations

• TauCeti.DiagonalizableGroup.isSemisimplePoint: every point of a diagonalizable group is a semisimple point.
• TauCeti.DiagonalizableGroup.semisimplePart_eq_self and TauCeti.DiagonalizableGroup.unipotentPart_eq_one: the Jordan factors of a point of a diagonalizable group are the point itself and the identity.
• TauCeti.DiagonalizableGroup.geometricallySemisimplePointsCommHopfAlgProperty: diagonalizable groups have only semisimple geometric points.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.2.
• T. A. Springer, Linear Algebraic Groups, §2.4.
• J. S. Milne, Algebraic Groups (2017), §12.c.

This supplies the semisimple-points theorem for diagonalizable groups and tori in Layer 4 of the ReductiveGroups roadmap.

theorem TauCeti.DiagonalizableGroup.isSemisimplePoint {R : Type u} {G : Type v} {K : Type x} [CommSemiring R] [CommGroup G] [Field K] [Algebra R K] (g : WithConv (MonoidAlgebra R G →ₐ[R] K)) : HopfAlgebra.IsSemisimplePoint g

Every point of the diagonalizable group D(G) is semisimple.

@[simp]

theorem TauCeti.DiagonalizableGroup.semisimplePart_eq_self {k G K : Type u} [Field k] [CommGroup G] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (MonoidAlgebra k G →ₐ[k] K)) : HopfAlgebra.Point.semisimplePart k (MonoidAlgebra k G) K g = g

The semisimple part of a point of a diagonalizable group is the point itself.

@[simp]

theorem TauCeti.DiagonalizableGroup.unipotentPart_eq_one {k G K : Type u} [Field k] [CommGroup G] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (MonoidAlgebra k G →ₐ[k] K)) : HopfAlgebra.Point.unipotentPart k (MonoidAlgebra k G) K g = 1

The unipotent part of a point of a diagonalizable group is trivial.

theorem TauCeti.DiagonalizableGroup.geometricallySemisimplePointsCommHopfAlgProperty (k : Type u) [Field k] (G : Type v) [CommGroup G] : TauCeti.geometricallySemisimplePointsCommHopfAlgProperty k ↧(MonoidAlgebra k G)

Every diagonalizable group has only semisimple geometric points.