feat(linear_algebra/tensor_product): define `tensor_tensor_tensor_com…

…m` (#7724)

The intended application is defining the bracket structure when extending the scalars of a Lie algebra.

src/linear_algebra/tensor_product.lean

@@ -843,6 +843,53 @@ rfl
   (congr f g).symm (p ⊗ₜ q) = f.symm p ⊗ₜ g.symm q :=
 rfl
 
+variables (R M N P Q)
+
+/-- A tensor product analogue of `mul_left_comm`. -/
+def left_comm : M ⊗[R] (N ⊗[R] P) ≃ₗ[R] N ⊗[R] (M ⊗[R] P) :=
+let e₁ := (tensor_product.assoc R M N P).symm,
+    e₂ := congr (tensor_product.comm R M N) (1 : P ≃ₗ[R] P),
+    e₃ := (tensor_product.assoc R N M P) in
+e₁.trans $ e₂.trans e₃
+
+variables {M N P Q}
+
+@[simp] lemma left_comm_tmul (m : M) (n : N) (p : P) :
+  left_comm R M N P (m ⊗ₜ (n ⊗ₜ p)) = n ⊗ₜ (m ⊗ₜ p) :=
+rfl
+
+@[simp] lemma left_comm_symm_tmul (m : M) (n : N) (p : P) :
+  (left_comm R M N P).symm (n ⊗ₜ (m ⊗ₜ p)) = m ⊗ₜ (n ⊗ₜ p) :=
+rfl
+
+variables (M N P Q)
+
+/-- This special case is worth defining explicitly since it is useful for defining multiplication
+on tensor products of modules carrying multiplications (e.g., associative rings, Lie rings, ...).
+
+E.g., suppose `M = P` and `N = Q` and that `M` and `N` carry bilinear multiplications:
+`M ⊗ M → M` and `N ⊗ N → N`. Using `map`, we can define `(M ⊗ M) ⊗ (N ⊗ N) → M ⊗ N` which, when
+combined with this definition, yields a bilinear multiplication on `M ⊗ N`:
+`(M ⊗ N) ⊗ (M ⊗ N) → M ⊗ N`. In particular we could use this to define the multiplication in
+the `tensor_product.semiring` instance (currently defined "by hand" using `tensor_product.mul`).
+
+See also `mul_mul_mul_comm`. -/
+def tensor_tensor_tensor_comm : (M ⊗[R] N) ⊗[R] (P ⊗[R] Q) ≃ₗ[R] (M ⊗[R] P) ⊗[R] (N ⊗[R] Q) :=
+let e₁ := tensor_product.assoc R M N (P ⊗[R] Q),
+    e₂ := congr (1 : M ≃ₗ[R] M) (left_comm R N P Q),
+    e₃ := (tensor_product.assoc R M P (N ⊗[R] Q)).symm in
+e₁.trans $ e₂.trans e₃
+
+variables {M N P Q}
+
+@[simp] lemma tensor_tensor_tensor_comm_tmul (m : M) (n : N) (p : P) (q : Q) :
+  tensor_tensor_tensor_comm R M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q) :=
+rfl
+
+@[simp] lemma tensor_tensor_tensor_comm_symm_tmul (m : M) (n : N) (p : P) (q : Q) :
+  (tensor_tensor_tensor_comm R M N P Q).symm ((m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q)) = (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) :=
+rfl
+
 end tensor_product
 
 namespace linear_map