isCoatom_comap_of_surjective — Mathlib

English

If φ: G →* H is surjective and M ⊆ H is a coatom, then the preimage M.comap φ is a coatom in G.

Русский

Если φ: G →* H сюръективно и M ⊆ H является коатомом, то его прообраз M.comap φ является коатомом в G.

LaTeX

$$IsCoatom M → IsCoatom (M.comap φ) for surjective φ$$

Lean4

theorem isCoatom_comap_of_surjective {H : Type*} [Group H] {φ : G →* H} (hφ : Function.Surjective φ) {M : Subgroup H}
    (hM : IsCoatom M) : IsCoatom (M.comap φ) :=
  by
  refine And.imp (fun hM ↦ ?_) (fun hM ↦ ?_) hM
  · rwa [← (comap_injective hφ).ne_iff, comap_top] at hM
  · intro K hK
    specialize hM (K.map φ)
    rw [← comap_lt_comap_of_surjective hφ, ← (comap_injective hφ).eq_iff] at hM
    rw [comap_map_eq_self ((M.ker_le_comap φ).trans hK.le), comap_top] at hM
    exact hM hK

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