Comultiplication of matrix coefficients

The comultiplication of a matrix coefficient is controlled by the coaction:

Δ(c(φ, m)) = (c(φ, ·) ⊗ id)(ρ(m)).

For a finite basis (eᵢ), expanding the coaction in that basis gives the familiar formula

Δ(c(φ, m)) = ∑ i, c(φ, eᵢ) ⊗ c(eⁱ, m).

Both formulas are basic facts about matrix coefficients; the finite-basis expansion is what makes the coefficient submodule of a finite free comodule stable under comultiplication in TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient.Subcoalgebra.

Main declarations

• TauCeti.Comodule.comul_matrixCoefficient: the basis-free comultiplication formula.
• TauCeti.Comodule.comul_matrixCoefficient_eq_sum: its expansion in a finite basis.
• TauCeti.Comodule.coact_eq_sum_basis_matrixCoefficient: the expansion of the coaction itself in a finite basis.

References

This is the standard coefficient-coalgebra computation; see Sweedler, Hopf Algebras, Chapter 2. It supplies a prerequisite for ReductiveGroups/README.md in TauCetiRoadmap, Layer 1, "Finite-dimensional subcoalgebras".

@[simp]

theorem TauCeti.Comodule.comul_matrixCoefficient {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.Dual R M) (m : M) : CoalgebraStruct.comul (matrixCoefficient φ m) = (TensorProduct.map (matrixCoefficientLinear φ) LinearMap.id) (coact m)

Comultiplication of a matrix coefficient is obtained by applying its coefficient map to the vector factor of the coaction.

theorem TauCeti.Comodule.coact_eq_sum_basis_matrixCoefficient {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] {ι : Type x} [Fintype ι] (b : Module.Basis ι R M) (m : M) : coact m = ∑ i : ι, b i ⊗ₜ[R] matrixCoefficient (b.coord i) m

The coaction of a comodule with a finite basis (eᵢ) expands as ρ(m) = ∑ i, eᵢ ⊗ c(eⁱ, m) in matrix coefficients.

theorem TauCeti.Comodule.comul_matrixCoefficient_eq_sum {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] {ι : Type x} [Fintype ι] (b : Module.Basis ι R M) (φ : Module.Dual R M) (m : M) : CoalgebraStruct.comul (matrixCoefficient φ m) = ∑ i : ι, matrixCoefficient φ (b i) ⊗ₜ[R] matrixCoefficient (b.coord i) m

The comultiplication of a matrix coefficient, expanded in a finite basis.