feat(linear_algebra/tensor_product): define tensor_tensor_tensor_assoc (

#13864)

src/linear_algebra/tensor_product.lean

@@ -723,6 +723,29 @@ rfl
   (tensor_tensor_tensor_comm R M N P Q).symm ((m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q)) = (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) :=
 rfl
 
+variables (M N P Q)
+
+/-- This special case is useful for describing the interplay between `dual_tensor_hom_equiv` and
+composition of linear maps.
+
+E.g., composition of linear maps gives a map `(M → N) ⊗ (N → P) → (M → P)`, and applying
+`dual_tensor_hom_equiv.symm` to the three hom-modules gives a map
+`(M.dual ⊗ N) ⊗ (N.dual ⊗ P) → (M.dual ⊗ P)`, which agrees with the application of `contract_right`
+on `N ⊗ N.dual` after the suitable rebracketting.
+-/
+def tensor_tensor_tensor_assoc : (M ⊗[R] N) ⊗[R] (P ⊗[R] Q) ≃ₗ[R] M ⊗[R] (N ⊗[R] P) ⊗[R] Q :=
+(tensor_product.assoc R (M ⊗[R] N) P Q).symm ≪≫ₗ
+congr (tensor_product.assoc R M N P) (1 : Q ≃ₗ[R] Q)
+
+variables {M N P Q}
+
+@[simp] lemma tensor_tensor_tensor_assoc_tmul (m : M) (n : N) (p : P) (q : Q) :
+  tensor_tensor_tensor_assoc R M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q := rfl
+
+@[simp] lemma tensor_tensor_tensor_assoc_symm_tmul (m : M) (n : N) (p : P) (q : Q) :
+  (tensor_tensor_tensor_assoc R M N P Q).symm (m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q) = (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) :=
+rfl
+
 end tensor_product
 
 namespace linear_map