comap_map_eq — Mathlib

English

For any f and submodule p, the preimage of the image equals the join of p with the kernel of f: comap f (map f p) = p ⊔ ker f.

Русский

Для любого отображения f и подмодуля p предобраз образа равен сумме p и ядра f: comap f (map f p) = p ⊔ ker f.

LaTeX

$$$\operatorname{comap}_f(\operatorname{map}_f p) = p \;⊔\; \ker f$$$

Lean4

theorem comap_map_eq (f : F) (p : Submodule R M) : comap f (map f p) = p ⊔ LinearMap.ker f :=
  by
  refine le_antisymm ?_ (sup_le (le_comap_map _ _) (comap_mono bot_le))
  rintro x ⟨y, hy, e⟩
  exact mem_sup.2 ⟨y, hy, x - y, by simpa using sub_eq_zero.2 e.symm, by simp⟩

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