updates 6

Author: themathqueen

Monlib/LinearAlgebra/Coalgebra/FiniteDimensional.lean

@@ -140,9 +140,9 @@ by
 
 open Coalgebra LinearMap TensorProduct in
 theorem Coalgebra.rTensor_mul_comp_lTensor_comul
-  [RCLike R] [NormedAddCommGroupOfRing A] [Star A] [InnerProductSpace R A]
+  [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A]
   [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A]
-  (h : ∃ σ : A → A, ∀ x y z : A, ⟪x * y, z⟫_R = ⟪y, σ (star x) * z⟫_R) :
+  (h : ∃ σ : A → A, ∀ x y z : A, ⟪x * y, z⟫_R = ⟪y, σ x * z⟫_R) :
   (rT A (m A)) ∘ₗ (ϰ A A A).symm.toLinearMap ∘ₗ (lT A comul) = comul ∘ₗ (m A) :=
 by
   rw [TensorProduct.ext_iff']
@@ -158,9 +158,9 @@ by
 
 -- open scoped ofFiniteDimensionalHilbertAlgebra in
 theorem Coalgebra.rTensor_mul_comp_lTensor_mul_adjoint
-  [RCLike R] [NormedAddCommGroupOfRing A] [Star A] [InnerProductSpace R A]
+  [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A]
   [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A]
-  (h : ∃ σ : A → A, ∀ x y z : A, ⟪x * y, z⟫_R = ⟪y, σ (star x) * z⟫_R) :
+  (h : ∃ σ : A → A, ∀ x y z : A, ⟪x * y, z⟫_R = ⟪y, σ x * z⟫_R) :
   (rT A (m A)) ∘ₗ (ϰ A A A).symm.toLinearMap ∘ₗ (lT A (LinearMap.adjoint (m A))) = (LinearMap.adjoint (m A)) ∘ₗ (m A) :=
 Coalgebra.rTensor_mul_comp_lTensor_comul h
 
@@ -239,9 +239,9 @@ Coalgebra.rTensor_mul_comp_lTensor_comul h
 
 open Coalgebra LinearMap TensorProduct in
 theorem Coalgebra.lTensor_mul_comp_rTensor_comul_of
-  [RCLike R] [NormedAddCommGroupOfRing A] [Star A] [InnerProductSpace R A]
+  [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A]
   [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A]
-  (h : ∃ σ : A → A, ∀ x y z : A, ⟪x * y, z⟫_R = ⟪y, σ (star x) * z⟫_R) :
+  (h : ∃ σ : A → A, ∀ x y z : A, ⟪x * y, z⟫_R = ⟪y, σ x * z⟫_R) :
   (lT A (m A)) ∘ₗ (ϰ A A A).toLinearMap ∘ₗ (rT A comul) = comul ∘ₗ (m A) :=
 by
   apply_fun adjoint using LinearEquiv.injective _
@@ -255,16 +255,16 @@ by
 
 open Coalgebra LinearMap TensorProduct in
 theorem Coalgebra.lTensor_mul_comp_rTensor_mul_adjoint_of
-  [RCLike R] [NormedAddCommGroupOfRing A] [Star A] [InnerProductSpace R A]
+  [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A]
   [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A]
-  (h : ∃ σ : A → A, ∀ x y z : A, ⟪x * y, z⟫_R = ⟪y, σ (star x) * z⟫_R) :
+  (h : ∃ σ : A → A, ∀ x y z : A, ⟪x * y, z⟫_R = ⟪y, σ x * z⟫_R) :
   (lT A (m A)) ∘ₗ (ϰ A A A).toLinearMap ∘ₗ (rT A (LinearMap.adjoint (m A))) = LinearMap.adjoint (m A) ∘ₗ (m A) :=
 Coalgebra.lTensor_mul_comp_rTensor_comul_of h
 
 noncomputable def FiniteDimensionalCoAlgebra_isFrobeniusAlgebra_of
-  [RCLike R] [NormedAddCommGroupOfRing A] [Star A] [InnerProductSpace R A]
+  [RCLike R] [NormedAddCommGroupOfRing A] [InnerProductSpace R A]
   [SMulCommClass R A A] [IsScalarTower R A A] [FiniteDimensional R A]
-  (h : ∃ σ : A → A, ∀ x y z : A, ⟪x * y, z⟫_R = ⟪y, σ (star x) * z⟫_R) :
+  (h : ∃ σ : A → A, ∀ x y z : A, ⟪x * y, z⟫_R = ⟪y, σ x * z⟫_R) :
     FrobeniusAlgebra R A where
   lTensor_mul_comp_rTensor_comul_commute := by
     rw [Coalgebra.lTensor_mul_comp_rTensor_comul_of h, Coalgebra.rTensor_mul_comp_lTensor_comul h]

Monlib/LinearAlgebra/QuantumSet/Basic.lean

@@ -530,15 +530,16 @@ lemma _root_.QuantumSet.rTensor_mul_comp_lTensor_comul_eq_comul_comp_mul :
    = Coalgebra.comul ∘ₗ mul' ℂ A :=
 by
   rw [Coalgebra.comul_eq_mul_adjoint, Coalgebra.rTensor_mul_comp_lTensor_mul_adjoint]
-  exact ⟨modAut _, fun x y z ↦ inner_star_left x y z⟩
+  exact ⟨_, fun x y z ↦ inner_star_left x y z⟩
 open LinearMap in
 lemma _root_.QuantumSet.lTensor_mul_comp_rTensor_comul_eq_comul_comp_mul :
   lTensor A (mul' ℂ A) ∘ₗ (TensorProduct.assoc ℂ _ _ _).toLinearMap ∘ₗ rTensor A (Coalgebra.comul)
    = Coalgebra.comul ∘ₗ mul' ℂ A :=
 by
   rw [Coalgebra.comul_eq_mul_adjoint, Coalgebra.lTensor_mul_comp_rTensor_mul_adjoint_of]
-  exact ⟨modAut _, fun x y z ↦ inner_star_left x y z⟩
+  exact ⟨_, fun x y z ↦ inner_star_left x y z⟩
 
+@[instance]
 noncomputable def _root_.QuantumSet.isFrobeniusAlgebra :
     FrobeniusAlgebra ℂ A where
   lTensor_mul_comp_rTensor_comul_commute := by

Monlib/LinearAlgebra/QuantumSet/SchurMul.lean

@@ -36,8 +36,12 @@ open Coalgebra
   `x •ₛ y := m ∘ (x ⊗ y) ∘ comul`  -/
 @[simps]
 noncomputable def schurMul {B C : Type _}
-  [starAlgebra B] [starAlgebra C]
-  [hB : QuantumSet B] [hC : QuantumSet C] :
+  [AddCommMonoid B] [NonUnitalNonAssocSemiring C]
+  [Module ℂ B] [Module ℂ C]
+  [CoalgebraStruct ℂ B]
+  [SMulCommClass ℂ C C]
+  [IsScalarTower ℂ C C]
+   :
   (B →ₗ[ℂ] C) →ₗ[ℂ] (B →ₗ[ℂ] C) →ₗ[ℂ] (B →ₗ[ℂ] C)
     where
   toFun x :=
@@ -65,9 +69,15 @@ notation3:80 (name := schurMulNotation) x:81 " •ₛ " y:80 => schurMul x y
 -- open scoped schurMul
 
 variable {A B C : Type _}
-  [starAlgebra A] [starAlgebra B] [starAlgebra C]
-  [hA : QuantumSet A] [hB : QuantumSet B] [hC : QuantumSet C]
-
+  [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [NormedAddCommGroupOfRing C]
+  [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [InnerProductSpace ℂ C]
+  [SMulCommClass ℂ A A] [SMulCommClass ℂ B B]
+  [SMulCommClass ℂ C C] [IsScalarTower ℂ A A]
+  [IsScalarTower ℂ B B] [IsScalarTower ℂ C C]
+  [FiniteDimensional ℂ A] [FiniteDimensional ℂ B]
+  [FiniteDimensional ℂ C]
+
+omit [FiniteDimensional ℂ B] in
 theorem schurMul.apply_rankOne
   (a : B) (b : C) (c : B) (d : C) : (↑|a⟩⟨b|) •ₛ (↑|c⟩⟨d|) = (|a * c⟩⟨b * d| : C →ₗ[ℂ] B) :=
   by
@@ -83,6 +93,7 @@ theorem schurMul.apply_rankOne
     LinearMap.mul'_apply, smul_mul_smul_comm, ← TensorProduct.inner_tmul, ← Finset.sum_smul, ← inner_sum,
     h, comul_eq_mul_adjoint, LinearMap.adjoint_inner_right, LinearMap.mul'_apply]
 
+omit [FiniteDimensional ℂ B] in
 theorem schurMul.apply_ket
   (a b : B) :
   (ket ℂ a) •ₛ (ket ℂ b) = (ket ℂ (a * b)).toLinearMap :=
@@ -175,14 +186,15 @@ theorem mul_comp_lid_symm {R : Type*} [CommSemiring R] :
 by aesop
 
 theorem schurMul.apply_bra
-  (a b : B) :
+  (a b : C) :
   (bra ℂ a) •ₛ (bra ℂ b) = (bra ℂ (a * b)).toLinearMap :=
 by
   rw [schurMul_apply_apply, bra_map_bra, LinearMap.comp_assoc, bra_comp_linearMap,
     Coalgebra.comul_eq_mul_adjoint, LinearMap.adjoint_adjoint, LinearMap.mul'_apply,
     ← LinearMap.comp_assoc, mul_comp_lid_symm]
   rfl
 
+omit [FiniteDimensional ℂ B] in
 theorem schurMul.comp_apply_of
   (δ : ℂ)
   (hAδ : Coalgebra.comul ∘ₗ LinearMap.mul' ℂ A = δ • LinearMap.id)
@@ -218,7 +230,10 @@ theorem schurMul_adjoint (x y : B →ₗ[ℂ] C) :
   simp only [LinearMap.coe_mk, AddHom.coe_mk, LinearMap.adjoint_comp, LinearMap.adjoint_adjoint,
     TensorProduct.map_adjoint, LinearMap.comp_assoc]
 
-theorem schurMul_real (x y : A →ₗ[ℂ] B) :
+theorem schurMul_real
+  {A B : Type*} [starAlgebra A] [starAlgebra B]
+  [QuantumSet A] [QuantumSet B]
+  (x y : A →ₗ[ℂ] B) :
     LinearMap.real (x •ₛ y : A →ₗ[ℂ] B) = (LinearMap.real y) •ₛ (LinearMap.real x) :=
   by
   obtain ⟨α, β, rfl⟩ := x.exists_sum_rankOne
@@ -227,7 +242,9 @@ theorem schurMul_real (x y : A →ₗ[ℂ] B) :
   simp_rw [rankOne_real, schurMul.apply_rankOne, ← map_mul, ← StarMul.star_mul]
   rw [Finset.sum_comm]
 
-theorem schurMul_one_right_rankOne (a b : B) :
+theorem schurMul_one_right_rankOne
+  {B : Type*} [starAlgebra B] [hB : QuantumSet B]
+  (a b : B) :
     (↑|a⟩⟨b|) •ₛ 1 = lmul a * (LinearMap.adjoint (lmul b : l(B))) :=
   by
   simp_rw [LinearMap.ext_iff_inner_map]
@@ -239,7 +256,9 @@ theorem schurMul_one_right_rankOne (a b : B) :
     hB.inner_star_left,
     inner_conj_symm, OrthonormalBasis.sum_inner_mul_inner, lmul_adjoint, lmul_apply]
 
-theorem schurMul_one_left_rankOne (a b : B) :
+theorem schurMul_one_left_rankOne
+  {B : Type*} [starAlgebra B] [hB : QuantumSet B]
+  (a b : B) :
     (1 : l(B)) •ₛ (|a⟩⟨b|) = (rmul a : l(B)) * (LinearMap.adjoint (rmul b : l(B))) :=
   by
   simp_rw [← ext_inner_map]
@@ -252,7 +271,10 @@ theorem schurMul_one_left_rankOne (a b : B) :
     OrthonormalBasis.sum_inner_mul_inner, ← QuantumSet.inner_conj_left,
     rmul_adjoint, rmul_apply]
 
-theorem Psi.schurMul (r₁ r₂ : ℝ)
+theorem Psi.schurMul
+  {A B : Type*} [starAlgebra A] [starAlgebra B]
+  [hA : QuantumSet A] [QuantumSet B]
+  (r₁ r₂ : ℝ)
     (f g : A →ₗ[ℂ] B) :
     hA.Psi r₁ r₂ (f •ₛ g) = hA.Psi r₁ r₂ f * hA.Psi r₁ r₂ g :=
   by
@@ -268,7 +290,10 @@ theorem Psi.schurMul (r₁ r₂ : ℝ)
     hA.Psi_toFun_apply, Algebra.TensorProduct.tmul_mul_tmul,
     ← MulOpposite.op_mul, ← StarMul.star_mul, ← map_mul]
 
-theorem schurMul_assoc (f g h : A →ₗ[ℂ] B) :
+theorem schurMul_assoc {A B : Type*}
+  [starAlgebra A] [starAlgebra B]
+  [hA : QuantumSet A] [QuantumSet B]
+  (f g h : A →ₗ[ℂ] B) :
   (f •ₛ g) •ₛ h = f •ₛ (g •ₛ h) :=
 by
   apply_fun hA.Psi 0 0 using LinearEquiv.injective _
@@ -290,22 +315,27 @@ theorem algHom_comp_mul {R A B : Type*} [CommSemiring R] [Semiring A]
     f.toLinearMap ∘ₗ LinearMap.mul' R A = (LinearMap.mul' R B) ∘ₗ (f.toLinearMap ⊗ₘ f.toLinearMap) :=
 nonUnitalAlgHom_comp_mul f.toNonUnitalAlgHom
 
+attribute [local instance] Algebra.ofIsScalarTowerSmulCommClass
+
 set_option linter.deprecated false in
 theorem comul_comp_nonUnitalAlgHom_adjoint (f : A →ₙₐ[ℂ] B) :
     Coalgebra.comul ∘ₗ (LinearMap.adjoint f.toLinearMap)
       = ((LinearMap.adjoint f.toLinearMap) ⊗ₘ (LinearMap.adjoint f.toLinearMap)) ∘ₗ Coalgebra.comul :=
 by
   simp_rw [comul_eq_mul_adjoint, ← TensorProduct.map_adjoint, ← LinearMap.adjoint_comp,
-    nonUnitalAlgHom_comp_mul]
+    nonUnitalAlgHom_comp_mul f]
 
 theorem comul_comp_algHom_adjoint (f : A →ₐ[ℂ] B) :
   Coalgebra.comul ∘ₗ (LinearMap.adjoint f.toLinearMap)
     = ((LinearMap.adjoint f.toLinearMap) ⊗ₘ (LinearMap.adjoint f.toLinearMap)) ∘ₗ Coalgebra.comul :=
 comul_comp_nonUnitalAlgHom_adjoint f.toNonUnitalAlgHom
 
+omit [FiniteDimensional ℂ C] in
 set_option linter.deprecated false in
-theorem schurMul_nonUnitalAlgHom_comp_coalgHom {D : Type*} [starAlgebra D]
-  [hD : QuantumSet D] (g : C →ₙₐ[ℂ] D) (f : A →ₗc[ℂ] B) (x y : B →ₗ[ℂ] C) :
+theorem schurMul_nonUnitalAlgHom_comp_coalgHom {D : Type*}
+  [Semiring D] [Module ℂ D]
+  [SMulCommClass ℂ D D] [IsScalarTower ℂ D D]
+  (g : C →ₙₐ[ℂ] D) (f : A →ₗc[ℂ] B) (x y : B →ₗ[ℂ] C) :
   (g.toLinearMap ∘ₗ x ∘ₗ f.toLinearMap) •ₛ (g.toLinearMap ∘ₗ y ∘ₗ f.toLinearMap)
     = g.toLinearMap ∘ₗ (x •ₛ y) ∘ₗ f.toLinearMap :=
 by
@@ -316,15 +346,21 @@ by
   congr 1
   simp_rw [TensorProduct.map_comp]
 
-theorem schurMul_algHom_comp_coalgHom {D : Type*} [starAlgebra D]
-  [hD : QuantumSet D] (g : C →ₐ[ℂ] D) (f : A →ₗc[ℂ] B) (x y : B →ₗ[ℂ] C) :
+omit [FiniteDimensional ℂ C] in
+theorem schurMul_algHom_comp_coalgHom {D : Type*}
+  [Semiring D] [Module ℂ D]
+  [SMulCommClass ℂ D D] [IsScalarTower ℂ D D]
+  (g : C →ₐ[ℂ] D) (f : A →ₗc[ℂ] B) (x y : B →ₗ[ℂ] C) :
   (g.toLinearMap ∘ₗ x ∘ₗ f.toLinearMap) •ₛ (g.toLinearMap ∘ₗ y ∘ₗ f.toLinearMap)
     = g.toLinearMap ∘ₗ (x •ₛ y) ∘ₗ f.toLinearMap :=
 schurMul_nonUnitalAlgHom_comp_coalgHom (g.toNonUnitalAlgHom) f x y
 
+omit [FiniteDimensional ℂ C] in
 set_option linter.deprecated false in
-theorem schurMul_nonUnitalAlgHom_comp_nonUnitalAlgHom_adjoint {D : Type*} [starAlgebra D]
-  [hD : QuantumSet D] (g : C →ₙₐ[ℂ] D) (f : B →ₙₐ[ℂ] A) (x y : B →ₗ[ℂ] C) :
+theorem schurMul_nonUnitalAlgHom_comp_nonUnitalAlgHom_adjoint {D : Type*}
+  [Semiring D] [Module ℂ D]
+  [SMulCommClass ℂ D D] [IsScalarTower ℂ D D]
+  (g : C →ₙₐ[ℂ] D) (f : B →ₙₐ[ℂ] A) (x y : B →ₗ[ℂ] C) :
   (g.toLinearMap ∘ₗ x ∘ₗ (LinearMap.adjoint f.toLinearMap))
     •ₛ (g.toLinearMap ∘ₗ y ∘ₗ LinearMap.adjoint f.toLinearMap)
     = g.toLinearMap ∘ₗ (x •ₛ y) ∘ₗ LinearMap.adjoint f.toLinearMap :=
@@ -336,25 +372,35 @@ by
   congr 1
   simp_rw [TensorProduct.map_comp]
 
-theorem schurMul_algHom_comp_algHom_adjoint {D : Type*} [starAlgebra D]
-  [hD : QuantumSet D] (g : C →ₐ[ℂ] D) (f : B →ₐ[ℂ] A) (x y : B →ₗ[ℂ] C) :
+omit [FiniteDimensional ℂ C] in
+theorem schurMul_algHom_comp_algHom_adjoint {D : Type*}
+  [Semiring D] [Module ℂ D]
+  [SMulCommClass ℂ D D] [IsScalarTower ℂ D D]
+  (g : C →ₐ[ℂ] D) (f : B →ₐ[ℂ] A) (x y : B →ₗ[ℂ] C) :
   (g.toLinearMap ∘ₗ x ∘ₗ (LinearMap.adjoint f.toLinearMap))
     •ₛ (g.toLinearMap ∘ₗ y ∘ₗ LinearMap.adjoint f.toLinearMap)
     = g.toLinearMap ∘ₗ (x •ₛ y) ∘ₗ LinearMap.adjoint f.toLinearMap :=
 schurMul_nonUnitalAlgHom_comp_nonUnitalAlgHom_adjoint g.toNonUnitalAlgHom f.toNonUnitalAlgHom x y
 
-theorem schurMul_one_iff_one_schurMul_of_isReal {x y z : A →ₗ[ℂ] B}
+theorem schurMul_one_iff_one_schurMul_of_isReal
+  {A B : Type*} [starAlgebra A] [starAlgebra B]
+  [QuantumSet A] [QuantumSet B]
+  {x y z : A →ₗ[ℂ] B}
   (hx : LinearMap.IsReal x) (hy : LinearMap.IsReal y) (hz : LinearMap.IsReal z) :
     x •ₛ y = z ↔ y •ₛ x = z :=
 by
   rw [LinearMap.real_inj_eq, schurMul_real, x.isReal_iff.mp hx, y.isReal_iff.mp hy,
     z.isReal_iff.mp hz]
 
-theorem schurMul_reflexive_of_isReal {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) :
+theorem schurMul_reflexive_of_isReal
+  {A : Type*} [starAlgebra A] [QuantumSet A]
+  {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) :
   x •ₛ 1 = 1 ↔ 1 •ₛ x = 1 :=
 schurMul_one_iff_one_schurMul_of_isReal hx LinearMap.isRealOne LinearMap.isRealOne
 
-theorem schurMul_irreflexive_of_isReal {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) :
+theorem schurMul_irreflexive_of_isReal
+  {A : Type*} [starAlgebra A] [QuantumSet A]
+  {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) :
   x •ₛ 1 = 0 ↔ 1 •ₛ x = 0 :=
 schurMul_one_iff_one_schurMul_of_isReal hx LinearMap.isRealOne LinearMap.isRealZero
 

Monlib/LinearAlgebra/QuantumSet/Symm.lean

@@ -293,14 +293,14 @@ by
 theorem commute_real_real {R A : Type _} [Semiring R] [StarRing R] [AddCommMonoid A] [Module R A]
     [StarAddMonoid A] [StarModule R A] (f g : A →ₗ[R] A) :
     Commute (f.real : A →ₗ[R] A) (g.real : A →ₗ[R] A) ↔ Commute f g := by
-  simp_rw [Commute, SemiconjBy, LinearMap.mul_eq_comp, ← LinearMap.real_comp, ←
+  simp_rw [Commute, SemiconjBy, Module.End.mul_eq_comp, ← LinearMap.real_comp, ←
     LinearMap.real_inj_eq]
 
 theorem linearMap_commute_modAut_pos_neg (r : ℝ) (x : B →ₗ[ℂ] B) :
     Commute x (hb.modAut r).toLinearMap ↔
       Commute x (hb.modAut (-r)).toLinearMap :=
   by
-  simp_rw [Commute, SemiconjBy, LinearMap.mul_eq_comp]
+  simp_rw [Commute, SemiconjBy, Module.End.mul_eq_comp]
   rw [AlgEquiv.linearMap_comp_eq_iff, ← starAlgebra.modAut_symm]
   nth_rw 1 [← AlgEquiv.comp_linearMap_eq_iff]
   rw [eq_comm]

Monlib/LinearAlgebra/QuantumSet/schurMulTensor.lean

@@ -0,0 +1,38 @@
+import Monlib.LinearAlgebra.QuantumSet.SchurMul
+import Monlib.LinearAlgebra.QuantumSet.TensorProduct
+import Mathlib.RingTheory.Coalgebra.TensorProduct
+
+open scoped TensorProduct
+
+lemma TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq_swap_middle_tensor
+  {R A B C D : Type*} [CommSemiring R]
+  [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
+  [Module R A] [Module R B] [Module R C] [Module R D] :
+  (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A B C D) = swap_middle_tensor R A B C D :=
+by
+  rw [← LinearEquiv.toLinearMap_inj]
+  apply TensorProduct.ext_fourfold'
+  simp
+
+theorem TensorProduct.map_schurMul {A B C D : Type*}
+  [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) :=
+by
+  rw [schurMul_apply_apply, TensorProduct.comul_def, LinearMap.mul'_tensorProduct,
+    TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq_swap_middle_tensor]
+  simp only [LinearMap.comp_assoc]
+  rw [← LinearMap.comp_assoc _ _ (swap_middle_tensor _ _ _ _ _).toLinearMap]
+  nth_rw 2 [← LinearMap.comp_assoc, LinearMap.comp_assoc, ← swap_middle_tensor_symm]
+  rw [swap_middle_tensor_map_conj]
+  simp only [← LinearMap.comp_assoc, ← TensorProduct.map_comp,
+    TensorProduct.AlgebraTensorModule.map_eq]
+  rfl