Finite matrix-coefficient submodules #
This file proves that the matrix-coefficient submodule of a finite projective right comodule over a commutative semiring is finite.
This is the first finite-dimensionality step toward the fundamental theorem of comodules in the reductive-groups roadmap. The next substantive step is to show that this finite submodule is closed under comultiplication, making it a coefficient subcoalgebra.
Main results #
TauCeti.Comodule.matrixCoefficientSubmodule_finite: a finite projective comodule has a finite matrix-coefficient submodule.
References #
The coefficient-space construction is standard; see Sweedler, Hopf Algebras, Chapter 2.
It advances ReductiveGroups/README.md in TauCetiRoadmap, Layer 1,
"Finite-dimensional subcoalgebras (the fundamental theorem of comodules)".
instance
TauCeti.Comodule.matrixCoefficientSubmodule_finite
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
[Module.Finite R M]
[Module.Projective R M]
:
The matrix-coefficient submodule of a finite projective comodule is finite.