ProCGroups/NormalSubgroups/SimpleQuotients/FiniteIntersections.lean
1import ProCGroups.NormalSubgroups.SimpleQuotients.Algebraic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/NormalSubgroups/SimpleQuotients/FiniteIntersections.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/-- An arbitrary infimum of normal subgroups is normal, when normality is known for every
22subgroup in the indexing set. -/
23theorem sInf_normal_of_forall_normal
24 {G : Type u} [Group G] {S : Set (Subgroup G)}
25 (hSnormal : ∀ M ∈ S, M.Normal) :
26 (sInf S).Normal := by
27 rw [sInf_eq_iInf']
28 exact Subgroup.normal_iInf_normal (fun M : S => hSnormal M.1 M.2)
30/-- Finite-intersection step: in a noncommutative simple quotient, any finite intersection of
31normal subgroups whose product with `K` is all of `G` still has product `⊤` with `K`. -/
33 {G : Type u} [Group G] (K : Subgroup G) [K.Normal]
34 [IsSimpleGroup (G ⧸ K)]
35 (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
36 {S : Set (Subgroup G)} (hSfinite : S.Finite)
37 (hSnormal : ∀ M ∈ S, M.Normal)
38 (hStop : ∀ M ∈ S, M ⊔ K = ⊤) :
39 sInf S ⊔ K = ⊤ := by
40 induction S, hSfinite using Set.Finite.induction_on with
41 | empty =>
42 simp only [sInf_empty, le_top, sup_of_le_left]
43 | @insert a S ha hSfinite ih =>
44 have hSnormal' : ∀ M ∈ S, M.Normal := by
45 intro M hM
46 exact hSnormal M (by simp only [Set.mem_insert_iff, hM, or_true])
47 have hStop' : ∀ M ∈ S, M ⊔ K = ⊤ := by
48 intro M hM
49 exact hStop M (by simp only [Set.mem_insert_iff, hM, or_true])
50 haveI : a.Normal := hSnormal a (by simp only [Set.mem_insert_iff, true_or])
51 have hInfNormal : (sInf S).Normal := sInf_normal_of_forall_normal hSnormal'
52 haveI : (sInf S).Normal := hInfNormal
53 rw [sInf_insert]
54 exact inf_sup_eq_top_of_noncomm_simple_quotient K a (sInf S)
55 hquotNoncomm (hStop a (by simp only [Set.mem_insert_iff, true_or])) (ih hSnormal' hStop')
57end ProCGroups.NormalSubgroups