map_le_map_iff — Mathlib

English

Let f be a semilinear map with a surjective ring hom. For submodules p, p' of the domain, the inclusion of images map f p ≤ map f p' is equivalent to p ≤ p' ⊔ ker f.

Русский

Пусть f — полилинейное отображение с сюръективным гомомом кольца. Для подмодулов p, p' выполняется: образ p содержится в образе p' тогда и только тогда, когда p ⊆ p' ⊔ ker f.

LaTeX

$$$\operatorname{map} f\,p \le \operatorname{map} f\,p' \iff p \le p' \sqcup \ker f$$$

Lean4

protected theorem map_le_map_iff (f : F) {p p'} : map f p ≤ map f p' ↔ p ≤ p' ⊔ ker f := by
  rw [map_le_iff_le_comap, Submodule.comap_map_eq]

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