Duals of finite projective comodules

For a finite projective right comodule M over a Hopf algebra H, this file constructs the right-comodule structure on the linear dual Module.Dual R M. Its coaction is characterized basis-freely by

Σ φ₀(m) φ₁ = S(c(φ, m)),

where c(φ, m) is the matrix coefficient and S is the antipode. The canonical equivalence dualTensorHomEquiv turns this equation into a definition without requiring a basis or any finiteness condition on H.

Main declarations

• TauCeti.Comodule.dualCoact: the coaction map on the linear dual.
• TauCeti.Comodule.dualTensorHom_dualCoact: its characteristic linear-map equation.
• TauCeti.Comodule.dual: the explicit, non-global dual comodule structure.

References

This is the standard finite-projective dual-comodule construction; see Sweedler, Hopf Algebras, Chapter 2.

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

The basis-free coaction map on the linear dual of a finite projective right comodule.

Under dualTensorHomEquiv, the tensor dualCoact φ corresponds to the linear map m ↦ S(c(φ, m)).

Equations

• TauCeti.Comodule.dualCoact = ↑(dualTensorHomEquiv R M H).symm ∘ₗ LinearMap.compRight R (HopfAlgebraStruct.antipode R) ∘ₗ TauCeti.Comodule.matrixCoefficientBilinear

@[simp]

theorem TauCeti.Comodule.dualTensorHom_dualCoact {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) : (dualTensorHom R M H) (dualCoact φ) = HopfAlgebraStruct.antipode R ∘ₗ matrixCoefficientBilinear φ

The characteristic equation for the dual coaction, as an equality of linear maps in the vector argument.

theorem TauCeti.Comodule.dualTensorHom_dualCoact_apply {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) : ((dualTensorHom R M H) (dualCoact φ)) m = (HopfAlgebraStruct.antipode R) (matrixCoefficient φ m)

Pointwise characteristic equation for the dual coaction: Σ φ₀(m) φ₁ = S(c(φ, m)).

theorem TauCeti.Comodule.dualCoact_counit {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] : LinearMap.lTensor (Module.Dual R M) CoalgebraStruct.counit ∘ₗ dualCoact = (TensorProduct.mk R (Module.Dual R M) R).flip 1

Applying the counit to the coefficient leg of the dual coaction recovers the original functional.

theorem TauCeti.Comodule.dualCoact_coassoc {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] : ↑(TensorProduct.assoc R (Module.Dual R M) H H) ∘ₗ LinearMap.rTensor H dualCoact ∘ₗ dualCoact = LinearMap.lTensor (Module.Dual R M) CoalgebraStruct.comul ∘ₗ dualCoact

The dual coaction is coassociative.

@[instance_reducible]

noncomputable def TauCeti.Comodule.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] : Comodule R H (Module.Dual R M)

The right-comodule structure on the linear dual of a finite projective right comodule.

This is deliberately not a global instance: a module can carry multiple coactions. Downstream code should select it explicitly, typically as a local instance.

Equations

• TauCeti.Comodule.dual R H M = { coact := TauCeti.Comodule.dualCoact, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.dual_coact {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] : coact = dualCoact

The coaction of the explicit dual-comodule structure is dualCoact.