Documentation

Mathlib.LinearAlgebra.DirectSum.TensorProduct

Tensor products of direct sums #

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

Main results #

source
noncomputable def TensorProduct.directSum (R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] (M₁ : ι₁ → Type w₁) (M₂ : ι₂ → Type w₂) [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] :
TensorProduct R (DirectSum ι₁ fun (i₁ : ι₁) => M₁ i₁) (DirectSum ι₂ fun (i₂ : ι₂) => M₂ i₂) ≃ₗ[S] DirectSum (ι₁ × ι₂) fun (i : ι₁ × ι₂) => TensorProduct R (M₁ i.1) (M₂ i.2)

The linear equivalence (⨁ i₁, M₁ i₁) ⊗ (⨁ i₂, M₂ i₂) ≃ (⨁ i₁, ⨁ i₂, M₁ i₁ ⊗ M₂ i₂), i.e. "tensor product distributes over direct sum".

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def TensorProduct.directSumLeft (R : Type u) [CommSemiring R] {ι₁ : Type v₁} [DecidableEq ι₁] (M₁ : ι₁ → Type w₁) (M₂' : Type w₂') [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [AddCommMonoid M₂'] [(i₁ : ι₁) → Module R (M₁ i₁)] [Module R M₂'] :
    TensorProduct R (DirectSum ι₁ fun (i₁ : ι₁) => M₁ i₁) M₂' ≃ₗ[R] DirectSum ι₁ fun (i : ι₁) => TensorProduct R (M₁ i) M₂'

    Tensor products distribute over a direct sum on the left .

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def TensorProduct.directSumRight (R : Type u) [CommSemiring R] {ι₂ : Type v₂} [DecidableEq ι₂] (M₁' : Type w₁') (M₂ : ι₂ → Type w₂) [AddCommMonoid M₁'] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [Module R M₁'] [(i₂ : ι₂) → Module R (M₂ i₂)] :
      TensorProduct R M₁' (DirectSum ι₂ fun (i : ι₂) => M₂ i) ≃ₗ[R] DirectSum ι₂ fun (i : ι₂) => TensorProduct R M₁' (M₂ i)

      Tensor products distribute over a direct sum on the right.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TensorProduct.directSum_lof_tmul_lof (R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
        (TensorProduct.directSum R S M₁ M₂) ((DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂) = (DirectSum.lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)
        source
        @[simp]
        theorem TensorProduct.directSum_symm_lof_tmul (R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
        (TensorProduct.directSum R S M₁ M₂).symm ((DirectSum.lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)) = (DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂
        source
        @[simp]
        theorem TensorProduct.directSumLeft_tmul_lof (R : Type u) [CommSemiring R] {ι₁ : Type v₁} [DecidableEq ι₁] {M₁ : ι₁ → Type w₁} {M₂' : Type w₂'} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [AddCommMonoid M₂'] [(i₁ : ι₁) → Module R (M₁ i₁)] [Module R M₂'] (i : ι₁) (x : M₁ i) (y : M₂') :
        (directSumLeft R M₁ M₂') ((DirectSum.lof R ι₁ M₁ i) x ⊗ₜ[R] y) = (DirectSum.lof R ι₁ (fun (i : ι₁) => TensorProduct R (M₁ i) M₂') i) (x ⊗ₜ[R] y)
        source
        @[simp]
        theorem TensorProduct.directSumLeft_symm_lof_tmul (R : Type u) [CommSemiring R] {ι₁ : Type v₁} [DecidableEq ι₁] {M₁ : ι₁ → Type w₁} {M₂' : Type w₂'} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [AddCommMonoid M₂'] [(i₁ : ι₁) → Module R (M₁ i₁)] [Module R M₂'] (i : ι₁) (x : M₁ i) (y : M₂') :
        (directSumLeft R M₁ M₂').symm ((DirectSum.lof R ι₁ (fun (i : ι₁) => TensorProduct R (M₁ i) M₂') i) (x ⊗ₜ[R] y)) = (DirectSum.lof R ι₁ M₁ i) x ⊗ₜ[R] y
        source
        @[simp]
        theorem TensorProduct.directSumRight_tmul_lof (R : Type u) [CommSemiring R] {ι₂ : Type v₂} [DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [AddCommMonoid M₁'] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [Module R M₁'] [(i₂ : ι₂) → Module R (M₂ i₂)] (x : M₁') (i : ι₂) (y : M₂ i) :
        (directSumRight R M₁' M₂) (x ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i) y) = (DirectSum.lof R ι₂ (fun (i : ι₂) => TensorProduct R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)
        source
        @[simp]
        theorem TensorProduct.directSumRight_symm_lof_tmul (R : Type u) [CommSemiring R] {ι₂ : Type v₂} [DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [AddCommMonoid M₁'] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [Module R M₁'] [(i₂ : ι₂) → Module R (M₂ i₂)] (x : M₁') (i : ι₂) (y : M₂ i) :
        (directSumRight R M₁' M₂).symm ((DirectSum.lof R ι₂ (fun (i : ι₂) => TensorProduct R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i) y
        source
        theorem TensorProduct.directSumRight_comp_rTensor (R : Type u) [CommSemiring R] {ι₁ : Type v₁} [DecidableEq ι₁] {M₁ : ι₁ → Type w₁} {M₁' : Type w₁'} {M₂' : Type w₂'} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [(i₁ : ι₁) → Module R (M₁ i₁)] [Module R M₁'] [Module R M₂'] (f : M₁' →ₗ[R] M₂') :
        ↑(directSumRight R M₂' M₁) ∘ₗ LinearMap.rTensor (DirectSum ι₁ fun (i : ι₁) => M₁ i) f = (DirectSum.lmap fun (x : ι₁) => LinearMap.rTensor (M₁ x) f) ∘ₗ ↑(directSumRight R M₁' M₁)