Matrix coefficients of the regular comodule

This file records that the regular right comodule has enough matrix coefficients to recover the whole coalgebra, and likewise that the coefficients of its restriction to a subcoalgebra recover that subcoalgebra. The key coefficient is the counit: for the regular comodule, the matrix coefficient attached to Coalgebra.counit and a vector c is exactly c.

This is a small Layer 1 prerequisite for the reductive-groups roadmap's faithful representation criterion, where faithfulness is detected by whether matrix coefficients generate the coordinate Hopf algebra. It proves that the regular representation satisfies that generated-coefficient condition.

Main declarations

• TauCeti.Comodule.regular_matrixCoefficientSet_eq_univ: every element of a coalgebra is a matrix coefficient of the regular comodule.
• TauCeti.Comodule.regular_matrixCoefficientSubmodule_eq_top: regular coefficients span the whole coalgebra.
• TauCeti.Comodule.regular_matrixCoefficientSubalgebra_eq_top: for a bialgebra or algebra coalgebra, regular coefficients generate the whole algebra.
• TauCeti.Subcoalgebra.le_matrixCoefficientSubalgebra_toRegularSubcomodule: a subcoalgebra is contained in the coefficient algebra of its restricted regular comodule.

References

This is the standard observation that the regular comodule's coefficient space is the whole coalgebra; see Sweedler, Hopf Algebras, Chapter 2. It uses the existing Tau Ceti matrix coefficient API and Mathlib's counit law for coalgebras.

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_counit_comp_subtype {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] (N : Subcomodule R C C) (n : ↥N) : matrixCoefficient (CoalgebraStruct.counit ∘ₗ SMulMemClass.subtype N) n = ↑n

Pairing a vector in a regular subcomodule with the restricted counit recovers its underlying element of the coalgebra.

theorem TauCeti.Comodule.mem_regular_matrixCoefficientSet {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (c : C) : c ∈ matrixCoefficientSet

Every element of a coalgebra is a matrix coefficient of the regular comodule.

The element c is obtained by pairing c with the counit functional.

@[simp]

theorem TauCeti.Comodule.regular_matrixCoefficientSet_eq_univ {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : matrixCoefficientSet = Set.univ

The matrix coefficient set of the regular comodule is the whole coalgebra.

theorem TauCeti.Comodule.regular_matrixCoefficientSubmodule_le_iff_eq_top {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {P : Submodule R C} : matrixCoefficientSubmodule ≤ P ↔ P = ⊤

A submodule contains all regular-comodule matrix coefficients iff it is top.

@[simp]

theorem TauCeti.Comodule.regular_matrixCoefficientSubmodule_eq_top {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : matrixCoefficientSubmodule = ⊤

The regular comodule's matrix coefficients span the whole coalgebra.

theorem TauCeti.Comodule.mem_regularObj_matrixCoefficientSet {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (c : ↑(ComoduleCat.regular R C).toSemimoduleCat) : c ∈ matrixCoefficientSet

Every element of the bundled regular comodule's coalgebra is a matrix coefficient.

theorem TauCeti.Comodule.regularObj_matrixCoefficientSet_eq_univ {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : matrixCoefficientSet = Set.univ

The bundled regular comodule's matrix coefficient set is the whole coalgebra.

theorem TauCeti.Comodule.regularObj_matrixCoefficientSubmodule_eq_top {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : matrixCoefficientSubmodule = ⊤

The bundled regular comodule's matrix coefficients span the whole coalgebra.

theorem TauCeti.Comodule.regular_matrixCoefficientSubalgebra_le_iff_eq_top {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] {S : Subalgebra R C} : matrixCoefficientSubalgebra ≤ S ↔ S = ⊤

A subalgebra contains all regular-comodule matrix coefficients iff it is top.

@[simp]

theorem TauCeti.Comodule.regular_matrixCoefficientSubalgebra_eq_top {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] : matrixCoefficientSubalgebra = ⊤

The regular comodule's matrix coefficients generate the whole ambient algebra.

theorem TauCeti.Comodule.regularObj_matrixCoefficientSubalgebra_eq_top {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] : matrixCoefficientSubalgebra = ⊤

The bundled regular comodule's matrix coefficients generate the whole ambient algebra.

theorem TauCeti.Subcoalgebra.le_matrixCoefficientSubalgebra_toRegularSubcomodule {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [Module.Flat R C] (D : Subcoalgebra R C) : D.toSubmodule ≤ Subalgebra.toSubmodule Comodule.matrixCoefficientSubalgebra

A subcoalgebra lies in the algebra generated by the matrix coefficients of its restricted regular comodule.

For c ∈ D, use c as a vector in D and restrict the coalgebra counit to D. The resulting matrix coefficient is c by the counit law for the regular comodule.