Matrix coefficients of dual comodules

For a finite projective right comodule M over a Hopf algebra, this file identifies the matrix coefficients of Tau Ceti's explicit right dual with the antipode images of the coefficients of M. The pointwise formula uses evaluation to turn m : M into a functional on the dual:

c_(Mᵛ)(ev_m, φ) = S(c_M(φ, m)).

Finite projectivity identifies every functional on Mᵛ with evaluation at some m, so the coefficient sets satisfy CoeffSet(Mᵛ) = S '' CoeffSet(M). No inverse for the antipode is needed. When the Hopf algebra is commutative, this becomes an equality of coefficient subalgebras, and combining it with the product-comodule formula gives the coefficient algebra of M × Mᵛ.

Main results

• TauCeti.Comodule.matrixCoefficient_dual_eval: the pointwise dual-coefficient formula.
• TauCeti.Comodule.matrixCoefficientSet_dual: dual coefficients are exactly antipode images.
• TauCeti.Comodule.matrixCoefficientSubalgebra_dual: the coefficient algebra of the dual is the antipode image of the original coefficient algebra.
• TauCeti.Comodule.matrixCoefficientSubalgebra_prod_dual: adjoining a comodule and its dual adjoins the original coefficient algebra and its antipode image.

References

The dual-comodule formula is standard; see Sweedler, Hopf Algebras, Chapter 2. For the role of ordinary and dual matrix coefficients in faithful representations, see Milne, Algebraic Groups (2017), Remark 4.1, Example 4.2, and Theorems 4.9 and 4.14, and Milne, Reductive Groups, Sections 5.1 and 5.8--5.9.

@[simp]

theorem TauCeti.Comodule.matrixCoefficient_dual_eval {R : Type u} {H : Type v} {M : Type w} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] (φ : Module.Dual R M) (m : M) : matrixCoefficient ((Module.Dual.eval R M) m) φ = (HopfAlgebraStruct.antipode R) (matrixCoefficient φ m)

Evaluating against m gives a coefficient of the dual comodule equal to the antipode of the original coefficient indexed by the same functional and vector.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientSet_dual {R : Type u} {H : Type v} {M : Type w} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] : matrixCoefficientSet = ⇑(HopfAlgebraStruct.antipode R) '' matrixCoefficientSet

The coefficients of the explicit dual comodule are exactly the antipode images of the coefficients of the original finite projective comodule.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientSubalgebra_dual {R : Type u} {H : Type v} {M : Type w} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] : matrixCoefficientSubalgebra = Subalgebra.map (HopfAlgebra.antipodeAlgHom R H) matrixCoefficientSubalgebra

For a commutative Hopf algebra, the coefficient subalgebra of the dual comodule is the image of the original coefficient subalgebra under the antipode algebra endomorphism.

theorem TauCeti.Comodule.matrixCoefficientSubalgebra_prod_dual {R : Type u} {H : Type v} {M : Type w} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] : matrixCoefficientSubalgebra = matrixCoefficientSubalgebra ⊔ Subalgebra.map (HopfAlgebra.antipodeAlgHom R H) matrixCoefficientSubalgebra

The coefficient subalgebra of the product of a finite projective comodule and its dual is the supremum of the original coefficient subalgebra and its antipode image.