comap_map_of_surjective — Mathlib

English

If f is surjective, then comap f (map f I) equals I ⊔ comap f ⊥ for any ideal I.

Русский

Если f сюръективен, то comap f (map f I) = I ⊔ comap f ⊥ для любого идеала I.

LaTeX

$$comap f (map f I) = I ⊔ comap f ⊥$$

Lean4

theorem comap_map_of_surjective (hf : Function.Surjective f) (I : Ideal R) : comap f (map f I) = I ⊔ comap f ⊥ :=
  le_antisymm
    (fun r h =>
      let ⟨s, hsi, hfsr⟩ := mem_image_of_mem_map_of_surjective f hf h
      Submodule.mem_sup.2
        ⟨s, hsi, r - s, (Submodule.mem_bot S).2 <| by rw [map_sub, hfsr, sub_self], add_sub_cancel s r⟩)
    (sup_le (map_le_iff_le_comap.1 le_rfl) (comap_mono bot_le))

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