Documentation

Mathlib.LinearAlgebra.TensorProduct.Prod

Tensor products of products #

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

Main results #

Notes #

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

source
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.
Instances For
    source
    @[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)
    source
    @[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₃)
    source
    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.
    Instances For
      source
      @[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₃)
      source
      @[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₃