Matrix coefficients of product comodules

This file records how matrix coefficients behave for the direct-sum/product comodule. If M × N carries Comodule.Prod, a coefficient of a vector (m, n) is the sum of the corresponding left and right coefficients. Consequently the coefficient submodule, and in an algebra the coefficient subalgebra, generated by M × N is the supremum of the two objects generated by M and by N.

This is a small Layer 1 prerequisite for the reductive-groups roadmap: matrix coefficients are the coalgebra-side functions attached to representations, and the finite-dimensional representation category needs their behavior under finite direct sums.

Main results

• TauCeti.Comodule.matrixCoefficient_prod: coefficient formula for M × N.
• TauCeti.Comodule.matrixCoefficientSubmodule_prod: coefficient submodules of a product are the supremum of the coefficient submodules of the two factors.
• TauCeti.Comodule.matrixCoefficientSubalgebra_prod: the analogous statement for the subalgebra generated by coefficients.

References

This is the standard direct-sum behavior of matrix coefficients of comodules; see Sweedler, Hopf Algebras, Chapter 2. It builds on Tau Ceti's Comodule.Prod construction.

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_prod {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] (φ : M × N →ₗ[R] R) (x : M × N) : matrixCoefficient φ x = matrixCoefficient (φ ∘ₗ LinearMap.inl R M N) x.1 + matrixCoefficient (φ ∘ₗ LinearMap.inr R M N) x.2

Matrix coefficients of the product comodule split as the sum of the left and right matrix coefficients.

theorem TauCeti.Comodule.matrixCoefficient_prod_inl {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] (φ : M →ₗ[R] R) (m : M) : matrixCoefficient (φ ∘ₗ LinearMap.fst R M N) ((LinearMap.inl R M N) m) = matrixCoefficient φ m

Matrix coefficients of a left summand, viewed in the product comodule, are the original left matrix coefficients.

theorem TauCeti.Comodule.matrixCoefficient_prod_inr {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] (ψ : N →ₗ[R] R) (n : N) : matrixCoefficient (ψ ∘ₗ LinearMap.snd R M N) ((LinearMap.inr R M N) n) = matrixCoefficient ψ n

Matrix coefficients of a right summand, viewed in the product comodule, are the original right matrix coefficients.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientSubmodule_prod {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] : matrixCoefficientSubmodule = matrixCoefficientSubmodule ⊔ matrixCoefficientSubmodule

The coefficient submodule of the product comodule is the supremum of the coefficient submodules of the two factors.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientSubalgebra_prod {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : matrixCoefficientSubalgebra = matrixCoefficientSubalgebra ⊔ matrixCoefficientSubalgebra

The coefficient subalgebra of the product comodule is the supremum of the coefficient subalgebras of the two factors.