Simplicity of a quotient from a normal-subgroup dichotomy

Simplicity theorems for groups of Lie type, by Tits's criterion for a BN-pair or Iwasawa's criterion for a group action, first prove a dichotomy in the group itself: every normal subgroup either lies in a fixed proper normal subgroup N or is the whole group. The quotient G ⧸ N is then simple, since a normal subgroup of G ⧸ N is the image of its preimage, which is normal in G. Mathlib's Group.isSimpleGroup_of_isCoatom asks instead for N to be maximal among all subgroups, which these criteria do not give.

Main results

• QuotientGroup.isSimpleGroup_of_forall_normal: if every normal subgroup lies in the proper normal subgroup N or is the whole group, then G ⧸ N is simple.

theorem QuotientGroup.isSimpleGroup_of_forall_normal {G : Type u_1} [Group G] {N : Subgroup G} [N.Normal] (hN : N ≠ ⊤) (h : ∀ (K : Subgroup G) [K.Normal], K ≤ N ∨ K = ⊤) : IsSimpleGroup (G ⧸ N)

Simplicity of a quotient from a normal-subgroup dichotomy. If every normal subgroup of G lies in the proper normal subgroup N or is the whole group, then G ⧸ N is simple.