noncomputable def dualCoactUncurried (k : Type u) [CommSemiring k] (H : Type v) [Semiring H] [HopfAlgebra k H] (X : Type v) [AddCommGroup X] [Module k X] (π : X →ₗ[k] TensorProduct k X H) : TensorProduct k (Module.Dual k X) X →ₗ[k] H

Uncurried form of the dual coaction map: given a coaction π : X → X ⊗ H, produces the linear map X* ⊗ X → H obtained by combining the antipode, the original coaction, and the evaluation pairing.

noncomputable def dualCoactCurried (k : Type u) [CommSemiring k] (H : Type v) [Semiring H] [HopfAlgebra k H] (X : Type v) [AddCommGroup X] [Module k X] (π : X →ₗ[k] TensorProduct k X H) : Module.Dual k X →ₗ[k] X →ₗ[k] H

Curried version of dualCoactUncurried: a map X* → (X → H).

noncomputable def dualCoaction (k : Type u) [CommSemiring k] (H : Type v) [Semiring H] [HopfAlgebra k H] (X : Type v) [AddCommGroup X] [Module k X] [Module.Free k X] [Module.Finite k X] (π : X →ₗ[k] TensorProduct k X H) : Module.Dual k X →ₗ[k] TensorProduct k (Module.Dual k X) H

The dual coaction X* → X* ⊗ H on the linear dual of an H-comodule, used in Corollary 1.22.6 to equip X* with a right H-comodule structure via the antipode.

theorem lid_contractLeft_rTensor_assoc_eq_lid_rTensor (k : Type u) [CommSemiring k] (H : Type v) [Semiring H] [HopfAlgebra k H] (X : Type v) [AddCommGroup X] [Module k X] (f : Module.Dual k X) : ↑(TensorProduct.lid k H) ∘ₗ LinearMap.rTensor H (contractLeft k X) ∘ₗ ↑(TensorProduct.assoc k (Module.Dual k X) X H).symm ∘ₗ (TensorProduct.mk k (Module.Dual k X) (TensorProduct k X H)) f = ↑(TensorProduct.lid k H) ∘ₗ LinearMap.rTensor H f

A naturality identity reducing a composite of left-id, contraction, associator inverse, and mk to lid composed with rTensor.

theorem dualTensorHom_lTensor_comp (k : Type u) [CommSemiring k] (X : Type v) [AddCommGroup X] [Module k X] {N : Type u_1} {P : Type u_2} [AddCommMonoid N] [Module k N] [AddCommMonoid P] [Module k P] (g : N →ₗ[k] P) (t : TensorProduct k (Module.Dual k X) N) (m : X) : ((dualTensorHom k X P) ((LinearMap.lTensor (Module.Dual k X) g) t)) m = g (((dualTensorHom k X N) t) m)

Compatibility of dualTensorHom with lTensor: postcomposing with g on the target commutes with applying dualTensorHom.

theorem counit_comp_dualCoactCurried (k : Type u) [CommSemiring k] (H : Type v) [Semiring H] [HopfAlgebra k H] (X : Type v) [AddCommGroup X] [Module k X] (π : X →ₗ[k] TensorProduct k X H) (hcounit : LinearMap.lTensor X CoalgebraStruct.counit ∘ₗ π = (TensorProduct.mk k X k).flip 1) (f : Module.Dual k X) : CoalgebraStruct.counit ∘ₗ (dualCoactCurried k H X π) f = f

Counit compatibility for the curried dual coaction: composing Coalgebra.counit with dualCoactCurried returns the original functional f.

theorem dualCoaction_coassoc (k : Type u) [CommSemiring k] (H : Type v) [Semiring H] [HopfAlgebra k H] (X : Type v) [AddCommGroup X] [Module k X] [Module.Free k X] [Module.Finite k X] (hπ : RightComodule k H X) : ↑(TensorProduct.assoc k (Module.Dual k X) H H) ∘ₗ LinearMap.rTensor H (dualCoaction k H X RightComodule.coact) ∘ₗ dualCoaction k H X RightComodule.coact = LinearMap.lTensor (Module.Dual k X) CoalgebraStruct.comul ∘ₗ dualCoaction k H X RightComodule.coact

The dual coaction on X* is coassociative, one of the two comodule axioms needed to make X* a right H-comodule.

theorem dualCoaction_counit (k : Type u) [CommSemiring k] (H : Type v) [Semiring H] [HopfAlgebra k H] (X : Type v) [AddCommGroup X] [Module k X] [Module.Free k X] [Module.Finite k X] (hπ : RightComodule k H X) : LinearMap.lTensor (Module.Dual k X) CoalgebraStruct.counit ∘ₗ dualCoaction k H X RightComodule.coact = (TensorProduct.mk k (Module.Dual k X) k).flip 1

The counit axiom for the dual coaction on X*: applying the counit recovers the canonical embedding of X* into X* ⊗ k.

@[reducible]

noncomputable def rmk_1_22_7_right_dual_comodule (k : Type u) [CommSemiring k] (H : Type v) [Semiring H] [HopfAlgebra k H] (X : Type v) [AddCommGroup X] [Module k X] [Module.Free k X] [Module.Finite k X] [hrc : RightComodule k H X] : RightComodule k H (Module.Dual k X)

Remark 1.22.7 / Corollary 1.22.6: The linear dual of a finite-dimensional right H-comodule carries a natural right H-comodule structure via the antipode.