Weight decomposition of comodules over a group-like-spanned coalgebra

Let C be a torsion-free coalgebra over a domain k whose group-like elements span C. Over a field and for C a commutative Hopf algebra, this says that C is the coordinate algebra of a diagonalizable group. This file proves that every C-comodule is the sum of its group-like weight spaces, and, when it is torsion-free, their internal direct sum: every representation of a diagonalizable group is diagonalizable.

The proof expands the coaction in the basis Subcoalgebra.groupLikeBasis of C formed by the group-like elements. Writing ρ m = ∑_g m_g ⊗ g, the counit law gives m = ∑_g m_g, and coassociativity, read off by the coordinate functionals of the basis, shows that each m_g has weight g.

Main declarations

• TauCeti.Comodule.iSup_groupLikeWeightSpace_eq_top: a comodule over a group-like-spanned coalgebra is spanned by its group-like weight spaces.
• TauCeti.Comodule.isInternal_groupLikeWeightSpace: a torsion-free comodule over a group-like-spanned coalgebra is the internal direct sum of its group-like weight spaces.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.12.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Theorem 2.2.

theorem TauCeti.Comodule.coactComponent_groupLikeBasis_coord_mem_weightSpace {k : Type u} {C : Type v} {M : Type w} [CommRing k] [IsDomain k] [AddCommGroup C] [Module k C] [Module.IsTorsionFree k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (hC : Subcoalgebra.groupLikeSetSpan Set.univ = ⊤) (g : GroupLike k C) (m : M) : (coactComponent ((Subcoalgebra.groupLikeBasis hC).coord g)) m ∈ g.weightSpace

The coordinate of a coaction along a group-like basis vector has that group-like weight.

theorem TauCeti.Comodule.iSup_groupLikeWeightSpace_eq_top {k : Type u} {C : Type v} {M : Type w} [CommRing k] [IsDomain k] [AddCommGroup C] [Module k C] [Module.IsTorsionFree k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (hC : Subcoalgebra.groupLikeSetSpan Set.univ = ⊤) : ⨆ (g : GroupLike k C), g.weightSpace = ⊤

A comodule over a coalgebra spanned by its group-like elements is spanned by its group-like weight spaces.

theorem TauCeti.Comodule.isInternal_groupLikeWeightSpace {k : Type u} {C : Type v} {M : Type w} [CommRing k] [IsDomain k] [AddCommGroup C] [Module k C] [Module.IsTorsionFree k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] [Module.IsTorsionFree k M] (hC : Subcoalgebra.groupLikeSetSpan Set.univ = ⊤) : DirectSum.IsInternal GroupLike.weightSpace

A torsion-free comodule over a coalgebra spanned by its group-like elements is the internal direct sum of its group-like weight spaces. Over a field this says that every representation of a diagonalizable group is diagonalizable.