range_map_eq_span_tmul — Mathlib

English

Canonical inclusion of submodule tensors into the full tensor product.

Русский

Каноническое вложение подмодулей в полное тензорное произведение.

LaTeX

$$$\\mathrm{mapIncl}\\ p\\ q : p \\otimes_R q \\to P \\otimes_R Q$$$

Lean4

theorem range_map_eq_span_tmul (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    range (map f g) = Submodule.span R {t | ∃ m n, f m ⊗ₜ g n = t} :=
  by
  simp only [← Submodule.map_top, ← span_tmul_eq_top, Submodule.map_span]
  congr; ext t
  simp

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