Matrix coefficients of a tensor product of comodules

For two right comodules M and N over a bialgebra C, the tensor product M ⊗[R] N carries the diagonal coaction m ⊗ n ↦ (m₀ ⊗ n₀) ⊗ m₁ n₁ of TauCeti.Algebra.Coalgebra.Comodule.TensorProduct (Comodule.tensor), which multiplies the two coefficient factors in C. This file records the corresponding fact about matrix coefficients: the coefficient of the product functional φ ⊗ ψ on a decomposable vector m ⊗ n is the product of the two coefficients,

c_{φ ⊗ ψ, m ⊗ n} = c_{φ, m} · c_{ψ, n}.

Here φ ⊗ ψ is the functional on M ⊗[R] N given by Mathlib's TensorProduct.dualDistrib, m ⊗ n ↦ φ m · ψ n. This multiplicativity is the algebra-side reflection of the monoidal (tensor-product) structure on comodules: multiplying one coefficient of M by one coefficient of N produces a coefficient of M ⊗[R] N, so the coefficient submodules multiply into the coefficient submodule of the tensor product.

This is Layer 1 infrastructure for the reductive-groups roadmap (ReductiveGroups/README.md in TauCetiRoadmap), whose Layer 1 asks for the representation/comodule dictionary with matrix coefficients and for the tensor product of comodules; the faithful-representation criterion is stated in terms of the subalgebra generated by matrix coefficients, and multiplicativity on tensor products is the key structural fact relating that subalgebra to the tensor product of representations.

Main declarations

• TauCeti.Comodule.matrixCoefficient_tensor: the coefficient of φ ⊗ ψ on m ⊗ n is the product c_{φ, m} · c_{ψ, n}.
• TauCeti.Comodule.matrixCoefficientSet_mul_subset: a product of a coefficient of M and a coefficient of N is a coefficient of M ⊗[R] N.
• TauCeti.Comodule.matrixCoefficientSubmodule_mul_le: the coefficient submodules multiply into the coefficient submodule of the tensor product.

References

This is the standard multiplicativity of matrix coefficients under the tensor product of comodules; see Sweedler, Hopf Algebras, Chapter 2. It builds on the tensor-product comodule TauCeti.Comodule.tensor and the matrix-coefficient API of TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient, and uses Mathlib's TensorProduct.dualDistrib.

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_tensor {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (φ : M →ₗ[R] R) (ψ : N →ₗ[R] R) (m : M) (n : N) : matrixCoefficient ((TensorProduct.dualDistrib R M N) (φ ⊗ₜ[R] ψ)) (m ⊗ₜ[R] n) = matrixCoefficient φ m * matrixCoefficient ψ n

Matrix coefficients multiply on a tensor product of comodules. For the diagonal coaction on M ⊗[R] N, the matrix coefficient of the product functional TensorProduct.dualDistrib R M N (φ ⊗ₜ ψ) (which sends m ⊗ n ↦ φ m · ψ n) evaluated at m ⊗ n is the product of the matrix coefficients of φ at m and of ψ at n.

theorem TauCeti.Comodule.mul_matrixCoefficient_mem_set_tensor {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (φ : M →ₗ[R] R) (ψ : N →ₗ[R] R) (m : M) (n : N) : matrixCoefficient φ m * matrixCoefficient ψ n ∈ matrixCoefficientSet

The product of a matrix coefficient of M and a matrix coefficient of N is a matrix coefficient of the tensor product M ⊗[R] N, realized on the product functional and the decomposable vector.

theorem TauCeti.Comodule.matrixCoefficientSet_mul_subset {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : matrixCoefficientSet * matrixCoefficientSet ⊆ matrixCoefficientSet

Products of coefficients are coefficients of the tensor product. The pointwise product of the coefficient sets of M and of N is contained in the coefficient set of M ⊗[R] N.

theorem TauCeti.Comodule.matrixCoefficientSubmodule_mul_le {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Bialgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : matrixCoefficientSubmodule * matrixCoefficientSubmodule ≤ matrixCoefficientSubmodule

The coefficient submodules multiply into the tensor product's. The product of the matrix coefficient submodules of M and of N is contained in the matrix coefficient submodule of M ⊗[R] N.