Transport invariance of matrix coefficients

This file records how the matrix coefficients of a right comodule behave under transport of a comodule structure across a linear equivalence. The general functoriality lemmas for comodule morphisms live with the coefficient span and adjoin API in TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient.Adjoin; this file keeps the transport-specific consequences behind the Comodule.Transport import.

These lemmas are bookkeeping for the reductive-groups roadmap's faithful-representation criterion: faithful representations are detected by whether their matrix coefficients generate the coordinate Hopf algebra.

Main declarations

• TauCeti.Comodule.matrixCoefficientSet_transport: the set of coefficients is invariant under transported coactions.
• TauCeti.Comodule.matrixCoefficientSubmodule_transport and TauCeti.Comodule.matrixCoefficientSubalgebra_transport: coefficient objects are invariant under transported coactions.

References

This is standard matrix-coefficient functoriality for comodules; see Sweedler, Hopf Algebras, Chapter 2. It supplies a prerequisite for ReductiveGroups/README.md in TauCetiRoadmap, Layer 1, "Faithfulness done right", where faithful representations are characterized by their matrix coefficients generating the coordinate Hopf algebra.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientSet_transport {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] {N₀ : Type x} [AddCommMonoid N₀] [Module R N₀] (e : M ≃ₗ[R] N₀) : matrixCoefficientSet = matrixCoefficientSet

Transporting a comodule structure across a linear equivalence does not change its coefficient set.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientSubmodule_transport {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] {N₀ : Type x} [AddCommMonoid N₀] [Module R N₀] (e : M ≃ₗ[R] N₀) : matrixCoefficientSubmodule = matrixCoefficientSubmodule

Transporting a comodule structure across a linear equivalence does not change its coefficient submodule.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientSubalgebra_transport {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] {N₀ : Type x} [AddCommMonoid N₀] [Module R N₀] (e : M ≃ₗ[R] N₀) : matrixCoefficientSubalgebra = matrixCoefficientSubalgebra

Transporting a comodule structure across a linear equivalence does not change its coefficient algebra.