Points and tangent vectors acting on a tensor product of comodules

The tensor product M ⊗ N of two comodules over a bialgebra H carries the diagonal coaction m ⊗ n ↦ m₀ ⊗ n₀ ⊗ m₁ n₁ (TauCeti.Comodule.tensor). This file computes the two actions that a comodule representation induces on it:

• a base-valued point g of H acts diagonally, g • (m ⊗ n) = g • m ⊗ g • n, because g is multiplicative;
• a tangent vector d at the identity acts by the Leibniz rule, d • (m ⊗ n) = d • m ⊗ n + m ⊗ d • n, because d is a derivation into the counit coefficients.

The first is the statement that the comodule tensor product integrates the tensor product of group representations; the second, that differentiating a representation turns tensor products of representations of the group into tensor products of representations of its Lie algebra.

Main results

• TauCeti.Comodule.basePointsRepresentation_tensor_tmul: a base-valued point acts diagonally on the tensor product comodule.
• TauCeti.Comodule.differential_tensor_tmul: a tangent vector acts on the tensor product comodule by the Leibniz rule.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.7 and I.7.11.
• J. S. Milne, Algebraic Groups (2017), §§4.5 and 10.

theorem TauCeti.Comodule.basePointsRepresentation_tensor_tmul {R : Type u_1} {H : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [AddCommMonoid W] [Module R W] [Comodule R H W] (g : WithConv (H →ₐ[R] R)) (v : V) (w : W) : ((basePointsRepresentation (TensorProduct R V W)) g) (v ⊗ₜ[R] w) = ((basePointsRepresentation V) g) v ⊗ₜ[R] ((basePointsRepresentation W) g) w

A point acts diagonally on a tensor product of comodules: a base-valued point g of the Hopf algebra H acts on the diagonal tensor product comodule V ⊗ W by g • (v ⊗ w) = g • v ⊗ g • w.

theorem TauCeti.Comodule.differential_tensor_tmul {R : Type u_1} {H : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing R] [CommRing H] [Bialgebra R H] [AddCommGroup V] [Module R V] [Comodule R H V] [AddCommGroup W] [Module R W] [Comodule R H W] (d : Derivation R H (Bialgebra.CounitAlgebra R H R)) (v : V) (w : W) : (differential d) (v ⊗ₜ[R] w) = (differential d) v ⊗ₜ[R] w + v ⊗ₜ[R] (differential d) w

The Leibniz rule for a tensor product of comodules: a tangent vector d at the identity acts on the diagonal tensor product comodule V ⊗ W by d • (v ⊗ w) = d • v ⊗ w + v ⊗ d • w.

theorem TauCeti.Comodule.differential_tensor {R : Type u_1} {H : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing R] [CommRing H] [Bialgebra R H] [AddCommGroup V] [Module R V] [Comodule R H V] [AddCommGroup W] [Module R W] [Comodule R H W] (d : Derivation R H (Bialgebra.CounitAlgebra R H R)) : differential d = LinearMap.rTensor W (differential d) + LinearMap.lTensor V (differential d)

The Leibniz rule for a tensor product of comodules, as an identity of linear maps: a tangent vector acts on V ⊗ W by d ⊗ 1 + 1 ⊗ d.