Points of the multiplicative group are semisimple #
Transporting semisimplicity of points of the diagonalizable group D(ℤ) across the standard
bialgebra isomorphism proves that every point of the multiplicative group 𝔾ₘ is semisimple.
Main declarations #
TauCeti.MultiplicativeGroup.isSemisimplePoint: every point of𝔾ₘis semisimple.
This is the 𝔾ₘ = D(ℤ) example from Layer 4 of the ReductiveGroups roadmap.
theorem
TauCeti.MultiplicativeGroup.isSemisimplePoint
{R : Type u}
{K : Type x}
[CommSemiring R]
[Field K]
[Algebra R K]
(g : WithConv (LaurentPolynomial R →ₐ[R] K))
:
Every point of the multiplicative group 𝔾ₘ is a semisimple point.