Semisimple point actions on monoid-algebra comodules

The weight-space decomposition of a comodule over a monoid algebra diagonalizes the endomorphism induced by any algebra map from the monoid algebra to a commutative ring. This file proves the corresponding eigenspace spanning result and, when the target is a field, semisimplicity of the induced endomorphism.

Main declarations

• TauCeti.Comodule.baseChange_weightSpace_le_eigenspace: the base-changed x-weight space is contained in the corresponding eigenspace of the point-action endomorphism.
• TauCeti.Comodule.iSup_baseChange_weightSpace_eq_top: the base-changed weight submodules span the scalar extension.
• TauCeti.Comodule.iSup_eigenspace_endOfPoint_eq_top: the eigenspaces of the point action span the scalar extension.
• TauCeti.Comodule.isSemisimple_endOfPoint_monoidAlgebra: the point-action endomorphism on any comodule over a monoid algebra is semisimple.

References

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

This supplies generic comodule infrastructure used by the semisimple-points results for diagonalizable groups in Layer 4 of the ReductiveGroups roadmap.

theorem TauCeti.Comodule.baseChange_weightSpace_le_eigenspace {R : Type u} {X : Type v} {V : Type w} {K : Type x} [CommSemiring R] [Monoid X] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R X) V] [CommRing K] [Algebra R K] (f : MonoidAlgebra R X →ₐ[R] K) (x : X) : Submodule.baseChange K (weightSpace R X V x) ≤ Module.End.eigenspace (endOfPoint V f) (f (MonoidAlgebra.single x 1))

The base change to K of the x-weight submodule is contained in the eigenspace of Comodule.endOfPoint V f with eigenvalue f (MonoidAlgebra.single x 1).

theorem TauCeti.Comodule.iSup_baseChange_weightSpace_eq_top {R : Type u} {X : Type v} {V : Type w} {K : Type x} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R X) V] [CommSemiring K] [Algebra R K] : ⨆ (x : X), Submodule.baseChange K (weightSpace R X V x) = ⊤

The base-changed weight submodules of a monoid-algebra comodule span the scalar extension.

theorem TauCeti.Comodule.iSup_eigenspace_endOfPoint_eq_top {R : Type u} {X : Type v} {V : Type w} {K : Type x} [CommSemiring R] [Monoid X] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R X) V] [CommRing K] [Algebra R K] (f : MonoidAlgebra R X →ₐ[R] K) : ⨆ (μ : K), Module.End.eigenspace (endOfPoint V f) μ = ⊤

The eigenspaces of the point-action endomorphism Comodule.endOfPoint V f span the scalar extension K ⊗[R] V.

theorem TauCeti.Comodule.isSemisimple_endOfPoint_monoidAlgebra {R : Type u} {X : Type v} {V : Type w} {K : Type x} [CommSemiring R] [Monoid X] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R X) V] [Field K] [Algebra R K] (f : MonoidAlgebra R X →ₐ[R] K) : Module.End.IsSemisimple (endOfPoint V f)

The point-action endomorphism on any comodule over a monoid algebra is semisimple.