ProCGroups/NormalSubgroups/MaximalIntersectionsAndSimpleRanks.lean
1import ProCGroups.NormalSubgroups.Framework
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/NormalSubgroups/MaximalIntersectionsAndSimpleRanks.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Closed normal subgroups and simple quotients
14Develops normal-subgroup frameworks, maximal intersections, simple quotient ranks, compactness arguments, and algebraic comparison theorems.
15-/
17noncomputable section
19open scoped Cardinal
21namespace ProCGroups.NormalSubgroups
23universe u
25/-- A maximal normal subgroup gives a simple quotient. -/
27 {G : Type u} [Group G] (M : Subgroup G) [M.Normal]
28 (hproper : M ≠ ⊤)
29 (hmax : ∀ N : Subgroup G, N.Normal → M < N → N = ⊤) :
30 IsSimpleGroup (G ⧸ M) := by
31 have hnotTopLe : ¬ (⊤ : Subgroup G) ≤ M := by
32 intro hle
33 exact hproper (le_antisymm le_top hle)
34 rcases SetLike.not_le_iff_exists.mp hnotTopLe with ⟨g, _hgTop, hgM⟩
35 refine
36 { exists_pair_ne := ⟨QuotientGroup.mk' M g, 1, ?_⟩
37 eq_bot_or_eq_top_of_normal := ?_ }
38 · intro hg
39 exact hgM ((QuotientGroup.eq_one_iff g).mp (by simpa using hg))
40 · intro H hH
41 let N : Subgroup G := Subgroup.comap (QuotientGroup.mk' M) H
42 have hMN : M ≤ N := by
43 dsimp [N]
44 exact QuotientGroup.le_comap_mk' M H
45 have hNnormal : N.Normal := by
46 dsimp [N]
47 infer_instance
48 by_cases hNM : N = M
49 · left
50 apply Subgroup.comap_injective (QuotientGroup.mk'_surjective M)
51 dsimp [N] at hNM
52 rw [hNM]
53 ext x
54 simp only [MonoidHom.comap_bot, QuotientGroup.ker_mk']
55 · right
56 have hMNlt : M < N := lt_of_le_of_ne hMN (by
57 intro hMN'
58 exact hNM hMN'.symm)
59 have hNtop : N = ⊤ := hmax N hNnormal hMNlt
60 apply Subgroup.comap_injective (QuotientGroup.mk'_surjective M)
61 dsimp [N] at hNtop
62 rw [hNtop, Subgroup.comap_top]
64end ProCGroups.NormalSubgroups