map_comp_comm_eq — Mathlib

English

A natural map from submodules to the full tensor product preserves the submodule structure via mapIncl.

Русский

Естественное отображение из подпространств в полное тензорное произведение сохраняет подмодуль через mapIncl.

LaTeX

$$$\\operatorname{range}(\\mathrm{mapIncl}\\ p\\ q) = \\mathrm{map_2}(\\mathrm{mk}\\ R\\ P\\ Q)\\ p\\ q$$$

Lean4

/-- Given linear maps `f : M → P`, `g : N → Q`, if we identify `M ⊗ N` with `N ⊗ M` and `P ⊗ Q`
with `Q ⊗ P`, then this lemma states that `f ⊗ g = g ⊗ f`. -/
theorem map_comp_comm_eq (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    map f g ∘ₗ TensorProduct.comm R N M = TensorProduct.comm R Q P ∘ₗ map g f :=
  ext rfl

Похожие утверждения