ProCGroups/NormalSubgroups/SimpleQuotients/Algebraic.lean
1import ProCGroups.NormalSubgroups.Framework
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/NormalSubgroups/SimpleQuotients/Algebraic.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-/
17namespace ProCGroups.NormalSubgroups
19universe u
21/-- If `G/K` is simple, every normal subgroup of `G` containing `K` is either `K` or
22all of `G`. This is the correspondence theorem form of the simple-quotient dichotomy. -/
24 {G : Type u} [Group G] (K L : Subgroup G) [K.Normal] (hL : L.Normal)
25 [IsSimpleGroup (G ⧸ K)] (hKL : K ≤ L) :
26 L = K ∨ L = ⊤ := by
27 haveI : L.Normal := hL
28 let qL : Subgroup (G ⧸ K) := Subgroup.map (QuotientGroup.mk' K) L
29 have hqLnormal : qL.Normal := inferInstance
30 rcases hqLnormal.eq_bot_or_eq_top with hbot | htop
31 · left
32 apply le_antisymm
33 · have hLK : L ≤ K := by
35 (Subgroup.map_eq_bot_iff L).mp hbot
36 simpa [QuotientGroup.ker_mk'] using hker
37 exact hLK
38 · exact hKL
39 · right
40 have hcomap : Subgroup.comap (QuotientGroup.mk' K) qL = L := by
41 dsimp [qL]
42 rw [QuotientGroup.comap_map_mk']
43 exact sup_of_le_right hKL
44 rw [← hcomap, htop]
45 simp only [Subgroup.comap_top]
47/-- Algebraic core of the simple-quotient intersection argument: if subgroups above `K` satisfy
48the two-point dichotomy induced by a simple quotient, and the quotient by `K` is noncommutative,
50intersection. -/
52 {G : Type u} [Group G] (K M N : Subgroup G) [K.Normal] [M.Normal] [N.Normal]
53 (hsimple : ∀ L : Subgroup G, L.Normal → K ≤ L → L = K ∨ L = ⊤)
54 (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
55 (hMK : M ⊔ K = ⊤) (hNK : N ⊔ K = ⊤) :
56 M ⊓ N ⊔ K = ⊤ := by
57 let L : Subgroup G := M ⊓ N ⊔ K
58 have hLnormal : L.Normal := inferInstance
59 have hKleL : K ≤ L := le_sup_right
60 rcases hsimple L hLnormal hKleL with hLK | hLtop
61 · exfalso
62 have hMNK : ⁅M, N⁆ ≤ K := by
63 exact (Subgroup.commutator_le_inf M N).trans ((le_sup_left : M ⊓ N ≤ L).trans_eq hLK)
64 have hmapK : Subgroup.map (QuotientGroup.mk' K) K = ⊥ := by
65 rw [Subgroup.map_eq_bot_iff, QuotientGroup.ker_mk']
66 have hmapM : Subgroup.map (QuotientGroup.mk' K) M = ⊤ := by
67 have hmapSup : Subgroup.map (QuotientGroup.mk' K) (M ⊔ K) = ⊤ := by
68 rw [hMK]
69 exact Subgroup.map_top_of_surjective (QuotientGroup.mk' K)
70 (QuotientGroup.mk'_surjective K)
71 rw [Subgroup.map_sup, hmapK, sup_bot_eq] at hmapSup
72 exact hmapSup
73 have hmapN : Subgroup.map (QuotientGroup.mk' K) N = ⊤ := by
74 have hmapSup : Subgroup.map (QuotientGroup.mk' K) (N ⊔ K) = ⊤ := by
75 rw [hNK]
76 exact Subgroup.map_top_of_surjective (QuotientGroup.mk' K)
77 (QuotientGroup.mk'_surjective K)
78 rw [Subgroup.map_sup, hmapK, sup_bot_eq] at hmapSup
79 exact hmapSup
80 have hcommBot : commutator (G ⧸ K) = ⊥ := by
81 rw [commutator_def]
82 nth_rewrite 1 [← hmapM]
83 nth_rewrite 1 [← hmapN]
84 rw [← Subgroup.map_commutator]
85 apply (Subgroup.map_eq_bot_iff ⁅M, N⁆).2
86 simpa [QuotientGroup.ker_mk'] using hMNK
87 exact hquotNoncomm hcommBot
88 · exact hLtop
90/-- Algebraic core with the simple quotient stated directly. -/
92 {G : Type u} [Group G] (K M N : Subgroup G) [K.Normal] [M.Normal] [N.Normal]
93 [IsSimpleGroup (G ⧸ K)]
94 (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
95 (hMK : M ⊔ K = ⊤) (hNK : N ⊔ K = ⊤) :
96 M ⊓ N ⊔ K = ⊤ :=
98 (fun L hL hKL => normal_subgroup_eq_kernel_or_top_of_simple_quotient K L hL hKL)
99 hquotNoncomm hMK hNK
101end ProCGroups.NormalSubgroups