Matrix coefficients of comodules

For a right comodule M over a coalgebra C, a linear functional φ : M →ₗ[R] R and a vector m : M define a coefficient element of C by applying φ to the vector component of the coaction:

cᵩ,ₘ = (R ⊗ C ≃ C) ((φ ⊗ id) (ρ m)).

These coefficients are the coalgebra-side functions attached to a representation. They are the named ingredient in the reductive-groups roadmap's representation/comodule dictionary, and later faithful-representation criteria ask for the subalgebra generated by such matrix coefficients.

Main definitions

• TauCeti.Comodule.matrixCoefficientLinear: the linear map M →ₗ[R] C attached to a functional φ : M →ₗ[R] R.
• TauCeti.Comodule.matrixCoefficient: the coefficient element attached to φ and m.
• TauCeti.Comodule.matrixCoefficientBilinear: bilinearity in the functional and vector.
• TauCeti.Comodule.matrixCoefficientTensor: the induced linear map Module.Dual R M ⊗[R] M →ₗ[R] C.

Implementation notes

The coalgebra C is a phantom parameter of matrixCoefficient and its relatives throughout this family of files: it occurs in the return type and in the [Comodule R C M] instance, but not in the types of the explicit arguments φ : M →ₗ[R] R and m : M. A module M can be a comodule over more than one coalgebra, so C is genuinely not inferable from φ and m. Unless the expected result type already pins C down, call sites must pass it explicitly, as in matrixCoefficient (C := C) φ m (and likewise (R := R) when R is not otherwise determined) — and statements, simp lemmas, and Set.range-style expressions usually have no such expected type. These named arguments are required for elaboration there, not removable noise.

References

This is standard coalgebra/comodule terminology; see Sweedler, Hopf Algebras, Chapter 2. It supplies the "matrix coefficients" prerequisite in ReductiveGroups/README.md in TauCetiRoadmap, Layer 1, "The dictionary: representation of G ⇆ A-comodule; matrix coefficients."

def TauCeti.Comodule.matrixCoefficientLinear {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] (φ : M →ₗ[R] R) : M →ₗ[R] C

The linear map of matrix coefficients associated to a functional on a right comodule.

It sends m : M to (φ ⊗ id) (ρ m), with the canonical identification R ⊗ C ≃ C.

Equations

• TauCeti.Comodule.matrixCoefficientLinear φ = ↑(TensorProduct.lid R C) ∘ₗ TensorProduct.map φ LinearMap.id ∘ₗ TauCeti.Comodule.coact

def TauCeti.Comodule.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] (φ : M →ₗ[R] R) (m : M) : C

The matrix coefficient attached to a functional and a vector in a right comodule.

Equations

• TauCeti.Comodule.matrixCoefficient φ m = (TauCeti.Comodule.matrixCoefficientLinear φ) m

@[simp]

theorem TauCeti.Comodule.matrixCoefficientLinear_apply {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] (φ : M →ₗ[R] R) (m : M) : (matrixCoefficientLinear φ) m = matrixCoefficient φ m

theorem TauCeti.Comodule.matrixCoefficient_def {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] (φ : M →ₗ[R] R) (m : M) : matrixCoefficient φ m = (TensorProduct.lid R C) ((TensorProduct.map φ LinearMap.id) (coact m))

Matrix coefficients are obtained by applying φ ⊗ id to the coaction.

@[deprecated TauCeti.Comodule.matrixCoefficient_def (since := "2026-06-19")]

theorem TauCeti.Comodule.matrixCoefficient_eq_lid_map_coact {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] (φ : M →ₗ[R] R) (m : M) : matrixCoefficient φ m = (TensorProduct.lid R C) ((TensorProduct.map φ LinearMap.id) (coact m))

Alias of TauCeti.Comodule.matrixCoefficient_def.

---

Matrix coefficients are obtained by applying φ ⊗ id to the coaction.

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_zero {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] (φ : M →ₗ[R] R) : matrixCoefficient φ 0 = 0

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_add {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] (φ : M →ₗ[R] R) (m n : M) : matrixCoefficient φ (m + n) = matrixCoefficient φ m + matrixCoefficient φ n

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_smul {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] (φ : M →ₗ[R] R) (r : R) (m : M) : matrixCoefficient φ (r • m) = r • matrixCoefficient φ m

def TauCeti.Comodule.matrixCoefficientBilinear {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] : (M →ₗ[R] R) →ₗ[R] M →ₗ[R] C

Matrix coefficients as a linear map from the dual module to linear maps M →ₗ[R] C.

Equations

• TauCeti.Comodule.matrixCoefficientBilinear = { toFun := TauCeti.Comodule.matrixCoefficientLinear, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.Comodule.matrixCoefficientBilinear_apply {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] (φ : M →ₗ[R] R) : matrixCoefficientBilinear φ = matrixCoefficientLinear φ

@[simp]

theorem TauCeti.Comodule.matrixCoefficientBilinear_apply_apply {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] (φ : M →ₗ[R] R) (m : M) : (matrixCoefficientBilinear φ) m = matrixCoefficient φ m

def TauCeti.Comodule.matrixCoefficientTensor {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] : TensorProduct R (Module.Dual R M) M →ₗ[R] C

The linear map from the tensor product of the dual and a right comodule to the ambient coalgebra, whose pure tensors give the matrix coefficients.

Equations

• TauCeti.Comodule.matrixCoefficientTensor = TensorProduct.lift TauCeti.Comodule.matrixCoefficientBilinear

@[simp]

theorem TauCeti.Comodule.matrixCoefficientTensor_tmul {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) : matrixCoefficientTensor (φ ⊗ₜ[R] m) = matrixCoefficient φ m

On a pure tensor, matrixCoefficientTensor is the corresponding matrix coefficient.

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_zero_functional {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] (m : M) : matrixCoefficient 0 m = 0

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_add_functional {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] (φ ψ : M →ₗ[R] R) (m : M) : matrixCoefficient (φ + ψ) m = matrixCoefficient φ m + matrixCoefficient ψ m

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_smul_functional {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] (r : R) (φ : M →ₗ[R] R) (m : M) : matrixCoefficient (r • φ) m = r • matrixCoefficient φ m

@[simp]

theorem TauCeti.Comodule.counit_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.counit (matrixCoefficient φ m) = φ m

Applying the coalgebra counit to a matrix coefficient recovers evaluation of the functional on the vector.

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_map {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (φ : N →ₗ[R] R) (m : M) : matrixCoefficient φ (f m) = matrixCoefficient (φ ∘ₗ f.toLinearMap) m

Matrix coefficients are natural in comodule morphisms: pushing the vector forward is the same as pulling the functional back.

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_counit_self {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (c : C) : matrixCoefficient CoalgebraStruct.counit c = c

For the regular comodule, the coefficient attached to the counit is the identity map.

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_groupLike {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] (g : GroupLike R C) (φ : M →ₗ[R] R) (m : M) : matrixCoefficient φ m = φ m • ↑g

Matrix coefficients of a group-like comodule are scalar multiples of the group-like element.

theorem TauCeti.Comodule.matrixCoefficient_trivial {R : Type u} [CommSemiring R] {C : Type v} [Semiring C] [Bialgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] R) (m : M) : matrixCoefficient φ m = φ m • 1

Matrix coefficients of the trivial comodule are scalar multiples of 1.