Tensor products of products

This file shows that taking TensorProducts commutes with taking Prods in both arguments.

Main results

• TensorProduct.prodLeft
• TensorProduct.prodRight

Notes

See Mathlib.LinearAlgebra.TensorProduct.Pi for arbitrary products.

noncomputable def TensorProduct.prodRight (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] : TensorProduct R M₁ (M₂ × M₃) ≃ₗ[R] TensorProduct R M₁ M₂ × TensorProduct R M₁ M₃

Tensor products distribute over a product on the right.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TensorProduct.prodRight_tmul (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (TensorProduct.prodRight R M₁ M₂ M₃) (m₁ ⊗ₜ[R] (m₂, m₃)) = (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃)

@[simp]

theorem TensorProduct.prodRight_symm_tmul (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (TensorProduct.prodRight R M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃) = m₁ ⊗ₜ[R] (m₂, m₃)

noncomputable def TensorProduct.prodLeft (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] : TensorProduct R (M₁ × M₂) M₃ ≃ₗ[R] TensorProduct R M₁ M₃ × TensorProduct R M₂ M₃

Tensor products distribute over a product on the left .

Equations

• TensorProduct.prodLeft R M₁ M₂ M₃ = ((TensorProduct.comm R (M₁ × M₂) M₃).trans (TensorProduct.prodRight R M₃ M₁ M₂)).trans ((TensorProduct.comm R M₃ M₁).prod (TensorProduct.comm R M₃ M₂))

@[simp]

theorem TensorProduct.prodLeft_tmul (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (TensorProduct.prodLeft R M₁ M₂ M₃) ((m₁, m₂) ⊗ₜ[R] m₃) = (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃)

@[simp]

theorem TensorProduct.prodLeft_symm_tmul (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (TensorProduct.prodLeft R M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) = (m₁, m₂) ⊗ₜ[R] m₃