map_comap_of_surjective — Mathlib

English

If f is surjective, then map f (comap f I) = I for any ideal I.

Русский

Если f сюрьективна, то образ через map от прообраза I равен I.

LaTeX

$$$\\text{If } hf: \\text{Surjective } f,\\; \\operatorname{map} f(\\operatorname{comap} f I) = I$$$

Lean4

theorem map_comap_of_surjective (I : Ideal S) : map f (comap f I) = I :=
  le_antisymm (map_le_iff_le_comap.2 le_rfl) fun s hsi =>
    let ⟨r, hfrs⟩ := hf s
    hfrs ▸ (mem_map_of_mem f <| show f r ∈ I from hfrs.symm ▸ hsi)

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