Theorems · Definition · linear algebra

TensorProduct.directSum

(R : Type u) →
  [inst : CommSemiring R] →
    (S : Type u_1) →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {ι₁ : Type v₁} →
            {ι₂ : Type v₂} →
              [DecidableEq ι₁] →
                [DecidableEq ι₂] →
                  (M₁ : ι₁ → Type w₁) →
                    (M₂ : ι₂ → Type w₂) →
                      [inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)] →
                        [inst_6 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] →
                          [inst_7 : (i₁ : ι₁) → Module R (M₁ i₁)] →
                            [inst_8 : (i₂ : ι₂) → Module R (M₂ i₂)] →
                              [inst_9 : (i₁ : ι₁) → Module S (M₁ i₁)] →
                                [inst_10 : ∀ (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".

Defined in

Mathlib.LinearAlgebra.DirectSum.TensorProduct

Cited by

6 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringSemiringAlgebraDecidableEqDecidableEqAddCommMonoidAddCommMonoidModuleModuleModuleIsScalarTower