comap_map_eq — Mathlib

English

If the image of I under f equals its image under f as a submodule, then comap f (map f I) = I ⊔ ker f.

Русский

Если образ I через f совпадает с образом I через f как подмодуль, то comap f (map f I) = I ⊔ ker f.

LaTeX

$$$(\,\text{hf}: \uparrow(\operatorname{map} f I) = f '' I) \Rightarrow \operatorname{comap} f (\operatorname{map} f I) = I \sqcup \ker f$$$

Lean4

@[simp]
theorem comap_map_eq (h : ↑(map f I) = f '' I) : comap f (map f I) = I ⊔ f.ker := by
  rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule, I.map_toSubmodule f h, LieSubmodule.sup_toSubmodule,
    f.ker_toSubmodule, Submodule.comap_map_eq]

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