Tannakian characterization of semisimple points #
Let H be a Hopf algebra over a commutative semiring k, let K be a perfect field equipped with
a k-algebra structure, and let g : WithConv (H →ₐ[k] K) be a K-valued point. The natural
automorphism formed from the semisimple factors of the actions of g on finitely generated
comodules equals the original point-action automorphism exactly when g is semisimple.
Main declarations #
TauCeti.HopfAlgebra.isSemisimplePoint_iff_fgPointSemisimplePartNatIso_eq_fgPointNatIsoHom: the intrinsic characterization by the Tannakian semisimple-factor automorphism.
References #
- J. C. Jantzen, Representations of Algebraic Groups, I.2.
- T. A. Springer, Linear Algebraic Groups, §2.4.
This is a representation-theoretic step toward the Jordan decomposition of group elements in Layer 4 of the ReductiveGroups roadmap.
theorem
TauCeti.HopfAlgebra.isSemisimplePoint_iff_fgPointSemisimplePartNatIso_eq_fgPointNatIsoHom
{k : Type u}
{H : Type v}
{K : Type x}
[CommSemiring k]
[Semiring H]
[HopfAlgebra k H]
[Field K]
[Algebra k K]
[PerfectField K]
(g : WithConv (H →ₐ[k] K))
:
IsSemisimplePoint g ↔ Tannaka.fgPointSemisimplePartNatIso k H K g = (Tannaka.fgPointNatIsoHom k H K) g
A point is semisimple exactly when the natural semisimple factors of all its finitely generated comodule actions recover its original point action.