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 u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] : TensorProduct R M₁ (M₂ × M₃) ≃ₗ[S] 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 u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m : M₂ × M₃) : (prodRight R S M₁ M₂ M₃) (m₁ ⊗ₜ[R] m) = (m₁ ⊗ₜ[R] m.1, m₁ ⊗ₜ[R] m.2)

@[simp]

theorem TensorProduct.prodRight_symm_tmul (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (prodRight R S M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃) = m₁ ⊗ₜ[R] (m₂, m₃)

noncomputable def TensorProduct.prodLeft (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] [Module S M₂] [IsScalarTower R S M₂] : TensorProduct R (M₁ × M₂) M₃ ≃ₗ[S] TensorProduct R M₁ M₃ × TensorProduct R M₂ M₃

Tensor products distribute over a product on the left .

Equations

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

@[simp]

theorem TensorProduct.prodLeft_tmul (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] [Module S M₂] [IsScalarTower R S M₂] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (prodLeft R S M₁ M₂ M₃) ((m₁, m₂) ⊗ₜ[R] m₃) = (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃)

@[simp]

theorem TensorProduct.prodLeft_symm_tmul (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] [Module S M₂] [IsScalarTower R S M₂] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (prodLeft R S M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) = (m₁, m₂) ⊗ₜ[R] m₃