Documentation

Mathlib.LinearAlgebra.TensorProduct.Prod

Tensor products of products #

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

Main results #

source
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.
Instances For
    source
    @[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₃)
    source
    @[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₃) :
    (LinearEquiv.symm (TensorProduct.prodRight R M₁ M₂ M₃)) (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃) = m₁ ⊗ₜ[R] (m₂, m₃)
    source
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[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₃)
      source
      @[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₃) :
      (LinearEquiv.symm (TensorProduct.prodLeft R M₁ M₂ M₃)) (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) = (m₁, m₂) ⊗ₜ[R] m₃