Schur Multiplication on Tensor Products

This file relates Schur multiplication on tensor-product coalgebras to the fourfold tensor shuffle used by the Monlib4 quantum-set tensor product.

theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq_swapMiddleTensor {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] : tensorTensorTensorComm R R R R A B C D = swapMiddleTensor R A B C D

The Mathlib tensor-product factor swap agrees with Monlib4's tensor shuffle.

theorem TensorProduct.map_schurMul {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [AddCommMonoid A] [Semiring B] [AddCommMonoid C] [Semiring D] [Module ℂ A] [Module ℂ B] [Module ℂ C] [Module ℂ D] [Coalgebra ℂ A] [Coalgebra ℂ C] [SMulCommClass ℂ B B] [SMulCommClass ℂ D D] [IsScalarTower ℂ B B] [IsScalarTower ℂ D D] {f h : A →ₗ[ℂ] B} {g k : C →ₗ[ℂ] D} : map f g •ₛ map h k = map (f •ₛ h) (g •ₛ k)

Schur multiplication commutes with tensoring linear maps.