Theorems · Theorem · linear algebra

PiTensorProduct.map_comp_reindex_eq

∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11}
  [inst_3 : (i : ι) → AddCommMonoid (t i)] [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i)
  (e : ι ≃ ι₂),
  (PiTensorProduct.map fun i => f (e.symm i)) ∘ₗ ↑(PiTensorProduct.reindex R s e) =
    ↑(PiTensorProduct.reindex R t e) ∘ₗ PiTensorProduct.map f

Re-indexing the components of the tensor product by an equivalence e is compatible with PiTensorProduct.map.

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModule