map_eq_top_iff — Mathlib

English

If ker f = ⊥, then the map p ↦ map f p is injective on submodules of M.

Русский

Если ядро отображения f равно нулю, отображение подмодулов p ↦ map f p инъективно.

LaTeX

$$Injective (\,p \mapsto \operatorname{map} f\,p\,) under ker f = ⊥$$

Lean4

theorem map_eq_top_iff {f : F} (hf : range f = ⊤) {p : Submodule R M} : p.map f = ⊤ ↔ p ⊔ LinearMap.ker f = ⊤ := by
  simp_rw [← top_le_iff, ← hf, range_eq_map, LinearMap.map_le_map_iff]

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