isCoatom_comap_iff — Mathlib

English

If f is surjective, IsCoatom (comap f p) is equivalent to IsCoatom p.

Русский

Если f сюръективно, то IsCoatom (comap f p) эквивалентно IsCoatom p.

LaTeX

$$$IsCoatom(\operatorname{comap}_f p) \iff IsCoatom(p)$$

Lean4

theorem isCoatom_comap_iff {f : F} (hf : Surjective f) {p : Submodule R₂ M₂} : IsCoatom (comap f p) ↔ IsCoatom p :=
  by
  have := comap_injective_of_surjective hf
  rw [IsCoatom, IsCoatom, ← comap_top f, this.ne_iff]
  refine and_congr_right fun _ ↦ ⟨fun h m hm ↦ this (h _ <| comap_strictMono_of_surjective hf hm), fun h m hm ↦ ?_⟩
  rw [← h _ (lt_map_of_comap_lt_of_surjective hf hm), comap_map_eq_self ((comap_mono bot_le).trans hm.le)]

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