Matrix coefficients under corestriction #
Corestriction along a coalgebra morphism applies that morphism to each matrix coefficient. This gives the coordinate formula for restricting a representation along a morphism of affine group schemes, without requiring a finite basis.
The calculation follows Comodule.coefficientMatrix_corestrict, using the same
tensor-product naturality identity for an arbitrary functional and vector.
References #
- M. E. Sweedler, Hopf Algebras, Chapter 2.
@[simp]
theorem
CoalgHom.matrixCoefficient_corestrict
{R : Type u_1}
{C : Type u_2}
{D : Type u_3}
{M : Type u_4}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid D]
[Module R D]
[Coalgebra R D]
[AddCommMonoid M]
[Module R M]
[TauCeti.Comodule R C M]
(f : C →ₗc[R] D)
(φ : Module.Dual R M)
(m : M)
:
Corestriction applies the coalgebra morphism to each matrix coefficient.