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
def TensorProduct.directSum (R : Type u) [CommRing R] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] (M₁ : ι₁ → Type w₁) (M₂ : ι₂ → Type w₂) [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] :
TensorProduct R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂) ≃ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct R (M₁ i.fst) (M₂ i.snd)

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
    def TensorProduct.directSumLeft (R : Type u) [CommRing R] {ι₁ : Type v₁} [DecidableEq ι₁] (M₁ : ι₁ → Type w₁) (M₂' : Type w₂') [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [AddCommGroup M₂'] [(i₁ : ι₁) → Module R (M₁ i₁)] [Module R M₂'] :
    TensorProduct R (⨁ (i₁ : ι₁), M₁ i₁) M₂' ≃ₗ[R] ⨁ (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
      def TensorProduct.directSumRight (R : Type u) [CommRing R] {ι₂ : Type v₂} [DecidableEq ι₂] (M₁' : Type w₁') (M₂ : ι₂ → Type w₂) [AddCommGroup M₁'] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [Module R M₁'] [(i₂ : ι₂) → Module R (M₂ i₂)] :
      TensorProduct R M₁' (⨁ (i : ι₂), M₂ i) ≃ₗ[R] ⨁ (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) [CommRing R] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
        ↑(TensorProduct.directSum R M₁ M₂) (↑(DirectSum.lof R ι₁ M₁ i₁) m₁ ⊗ₜ[R] ↑(DirectSum.lof R ι₂ M₂ i₂) m₂) = ↑(DirectSum.lof R (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.fst) (M₂ i.snd)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)
        source
        @[simp]
        theorem TensorProduct.directSum_symm_lof_tmul (R : Type u) [CommRing R] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
        ↑(LinearEquiv.symm (TensorProduct.directSum R M₁ M₂)) (↑(DirectSum.lof R (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.fst) (M₂ i.snd)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)) = ↑(DirectSum.lof R ι₁ M₁ i₁) m₁ ⊗ₜ[R] ↑(DirectSum.lof R ι₂ M₂ i₂) m₂
        source
        @[simp]
        theorem TensorProduct.directSumLeft_tmul_lof (R : Type u) [CommRing R] {ι₁ : Type v₁} [DecidableEq ι₁] {M₁ : ι₁ → Type w₁} {M₂' : Type w₂'} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [AddCommGroup M₂'] [(i₁ : ι₁) → Module R (M₁ i₁)] [Module R M₂'] (i : ι₁) (x : M₁ i) (y : M₂') :
        ↑(TensorProduct.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) [CommRing R] {ι₁ : Type v₁} [DecidableEq ι₁] {M₁ : ι₁ → Type w₁} {M₂' : Type w₂'} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [AddCommGroup M₂'] [(i₁ : ι₁) → Module R (M₁ i₁)] [Module R M₂'] (i : ι₁) (x : M₁ i) (y : M₂') :
        ↑(LinearEquiv.symm (TensorProduct.directSumLeft R M₁ M₂')) (↑(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) [CommRing R] {ι₂ : Type v₂} [DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [AddCommGroup M₁'] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [Module R M₁'] [(i₂ : ι₂) → Module R (M₂ i₂)] (x : M₁') (i : ι₂) (y : M₂ i) :
        ↑(TensorProduct.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) [CommRing R] {ι₂ : Type v₂} [DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [AddCommGroup M₁'] [(i₂ : ι₂) → AddCommGroup (M₂ i₂)] [Module R M₁'] [(i₂ : ι₂) → Module R (M₂ i₂)] (x : M₁') (i : ι₂) (y : M₂ i) :
        ↑(LinearEquiv.symm (TensorProduct.directSumRight R M₁' M₂)) (↑(DirectSum.lof R ι₂ (fun i => TensorProduct R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] ↑(DirectSum.lof R ι₂ M₂ i) y