mapIncl — Mathlib

English

Range equality for canonical inclusion map.

Русский

Равенство образа для канонического включения.

LaTeX

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

Lean4

/-- Given submodules `p ⊆ P` and `q ⊆ Q`, this is the natural map: `p ⊗ q → P ⊗ Q`. -/
@[simp]
def mapIncl (p : Submodule R P) (q : Submodule R Q) : p ⊗[R] q →ₗ[R] P ⊗[R] Q :=
  map p.subtype q.subtype

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