Source: ProCGroups.NormalSubgroups.MaximalIntersectionsAndSimpleRanks
1import ProCGroups.NormalSubgroups.Framework
3/-!
4# Maximal normal subgroups and simple quotients
6This module proves that a proper normal subgroup maximal among normal subgroups yields a simple
7quotient.
8-/
10noncomputable section
12open scoped Cardinal
14namespace ProCGroups.NormalSubgroups
16universe u
18/-- A maximal normal subgroup gives a simple quotient. -/
19theorem maximal_normal_intersection_simple_quotient
20 {G : Type u} [Group G] (M : Subgroup G) [M.Normal]
21 (hproper : M ≠ ⊤)
22 (hmax : ∀ N : Subgroup G, N.Normal → M < N → N = ⊤) :
23 IsSimpleGroup (G ⧸ M) := by
24 have hnotTopLe : ¬ (⊤ : Subgroup G) ≤ M := by
25 intro hle
26 exact hproper (le_antisymm le_top hle)
27 rcases SetLike.not_le_iff_exists.mp hnotTopLe with ⟨g, _hgTop, hgM⟩
28 refine
29 { exists_pair_ne := ⟨QuotientGroup.mk' M g, 1, ?_⟩
30 eq_bot_or_eq_top_of_normal := ?_ }
31 · intro hg
32 exact hgM ((QuotientGroup.eq_one_iff g).mp (by simpa using hg))
33 · intro H hH
34 let N : Subgroup G := Subgroup.comap (QuotientGroup.mk' M) H
35 have hMN : M ≤ N := by
36 dsimp [N]
37 exact QuotientGroup.le_comap_mk' M H
38 have hNnormal : N.Normal := by
39 dsimp [N]
40 infer_instance
41 by_cases hNM : N = M
42 · left
43 apply Subgroup.comap_injective (QuotientGroup.mk'_surjective M)
44 dsimp [N] at hNM
45 rw [hNM]
46 ext x
47 simp only [MonoidHom.comap_bot, QuotientGroup.ker_mk']
48 · right
49 have hMNlt : M < N := lt_of_le_of_ne hMN (by
50 intro hMN'
51 exact hNM hMN'.symm)
52 have hNtop : N = ⊤ := hmax N hNnormal hMNlt
53 apply Subgroup.comap_injective (QuotientGroup.mk'_surjective M)
54 dsimp [N] at hNtop
55 rw [hNtop, Subgroup.comap_top]
57end ProCGroups.NormalSubgroups