isSimpleGroup_of_surjective — Mathlib

English

If there is a surjective homomorphism from a simple group G to a nontrivial group H, then H is simple.

Русский

Если существует сюръективный гомоморфизм от простой группы G к нетривиальной группе H, то H простая.

LaTeX

$$IsSimpleGroup H$$

Lean4

@[to_additive]
theorem isSimpleGroup_of_surjective {H : Type*} [Group H] [IsSimpleGroup G] [Nontrivial H] (f : G →* H)
    (hf : Function.Surjective f) : IsSimpleGroup H :=
  ⟨fun H iH => by
    refine (iH.comap f).eq_bot_or_eq_top.imp (fun h => ?_) fun h => ?_
    · rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]
    · rw [← comap_top f] at h
      exact comap_injective hf h⟩

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