noncomputable def Corollary_1_22_6_smul_map {k : Type u} [CommSemiring k] {H : Type v} [Semiring H] {V : Type v} [AddCommGroup V] [Module k V] [Module H V] [SMulCommClass k H V] (h : H) : V →ₗ[k] V

k-linear map given by scalar multiplication by an element h : H.

noncomputable def Corollary_1_22_6_right_dual_action {k : Type u} [CommSemiring k] {H : Type v} [Semiring H] [HopfAlgebra k H] {V : Type v} [AddCommGroup V] [Module k V] [Module H V] [SMulCommClass k H V] (a : H) (f : Module.Dual k V) : Module.Dual k V

The right-dual H-action on V^* from Corollary 1.22.6: (a · f)(v) = f(S(a) · v).

@[simp]

theorem Corollary_1_22_6_right_dual_action_one {k : Type u} [CommSemiring k] {H : Type v} [Semiring H] [HopfAlgebra k H] {V : Type v} [AddCommGroup V] [Module k V] [Module H V] [SMulCommClass k H V] (f : Module.Dual k V) : Corollary_1_22_6_right_dual_action 1 f = f

The unit of H acts trivially on the right-dual action.

theorem Corollary_1_22_6_right_dual_action_mul {k : Type u} [CommSemiring k] {H : Type v} [Semiring H] [HopfAlgebra k H] {V : Type v} [AddCommGroup V] [Module k V] [Module H V] [SMulCommClass k H V] (a b : H) (f : Module.Dual k V) : Corollary_1_22_6_right_dual_action (a * b) f = Corollary_1_22_6_right_dual_action a (Corollary_1_22_6_right_dual_action b f)

The right-dual action satisfies the multiplicative law (ab) · f = a · (b · f), using that the antipode is an antihomomorphism of algebras.

theorem Corollary_1_22_6_right_dual_action_add {k : Type u} [CommSemiring k] {H : Type v} [Semiring H] [HopfAlgebra k H] {V : Type v} [AddCommGroup V] [Module k V] [Module H V] [SMulCommClass k H V] (a b : H) (f : Module.Dual k V) : Corollary_1_22_6_right_dual_action (a + b) f = Corollary_1_22_6_right_dual_action a f + Corollary_1_22_6_right_dual_action b f

The right-dual action is additive in the acting element.