map_le_iff_le_comap — Mathlib

English

For any submodules p ⊆ M and q ⊆ M₂, map f p ≤ q iff p ≤ comap f q (when σ₂₃ surjective).

Русский

Для любых подмодулей p ⊆ M и q ⊆ M₂ выполняется map f p ≤ q тогда и только тогда, когда p ≤ comap f q (при сюръективности).

LaTeX

$$$\\operatorname{map} f p \\le q \\ \\Leftrightarrow\\ p \\le \\operatorname{comap} f q$$$

Lean4

theorem map_le_iff_le_comap {f : F} {p : Submodule R M} {q : Submodule R₂ M₂} : map f p ≤ q ↔ p ≤ comap f q :=
  image_subset_iff

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