range_le_iff_comap — Mathlib

English

Let f be a semilinear map with a surjective underlying ring hom. Then the image of f is contained in a submodule p if and only if the preimage of p under f is the whole domain; i.e., range f ≤ p ⇔ comap f p = ⊤.

Русский

Пусть f — полуправое линейное отображение, а соответствующее кольцевое отображение сюр'єктивно. Тогда образ f содержится в подмодуле p тогда и только тогда, когда прообраз p по f равен всему пространству: range f ≤ p ⇔ comap f p = ⊤.

LaTeX

$$$\operatorname{range} f \le p \;\;\Leftrightarrow\;\; \operatorname{comap} f p = \top$$$

Lean4

theorem range_le_iff_comap [RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂} : range f ≤ p ↔ comap f p = ⊤ := by
  rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]

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