Contracting the combined coefficient of two coacted tensors

The diagonal coaction on a tensor product of comodules multiplies the coefficients of the two factors (TauCeti.Comodule.tensorCombine). This file records how contracting the product coefficient against a linear functional (LinearMap.tensorComponent) splits when the functional splits on products, as a counit does, ε (a * b) = ε a * ε b, or a tangent vector at the identity does, d (a * b) = d a * ε b + ε a * d b.

Main results

• TauCeti.Comodule.tensorComponent_tensorCombine: contracting against a functional which splits on products as θ (a * b) = φ a * ψ b + φ' a * ψ' b splits the contraction accordingly.

theorem TauCeti.Comodule.tensorComponent_tensorCombine {R : Type u_1} {C : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring R] [NonUnitalNonAssocSemiring C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] {θ φ ψ φ' ψ' : C →ₗ[R] R} (hθ : ∀ (a b : C), θ (a * b) = φ a * ψ b + φ' a * ψ' b) (x : TensorProduct R V C) (y : TensorProduct R W C) : (LinearMap.tensorComponent θ) (tensorCombine (x ⊗ₜ[R] y)) = (LinearMap.tensorComponent φ) x ⊗ₜ[R] (LinearMap.tensorComponent ψ) y + (LinearMap.tensorComponent φ') x ⊗ₜ[R] (LinearMap.tensorComponent ψ') y

Contracting the combined coefficient of two coacted tensors against a functional which splits on products as θ (a * b) = φ a * ψ b + φ' a * ψ' b splits the contraction accordingly.