Theorems · Definition · linear algebra

PiTensorProduct.equivPiTensorComplSingletonTensor

(R : Type u_1) →
  {ι : Type u_2} →
    [DecidableEq ι] →
      (M : ι → Type u_3) →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              (i₀ : ι) → (PiTensorProduct R fun i => M i) ≃ₗ[R] TensorProduct R (PiTensorProduct R fun i => M ↑i) (M i₀)

The linear equivalence between ⨂[R] i, M i and the tensor product of the pi tensor product indexed by the complement of {i₀} and M i₀.

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Generators

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidableEqCommSemiringAddCommMonoidModule