ProCGroups/NormalSubgroups/SimpleQuotients/Compactness.lean
1import ProCGroups.NormalSubgroups.SimpleQuotients.FiniteIntersections
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/NormalSubgroups/SimpleQuotients/Compactness.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/-- Compactness step: if the closed normal subgroups satisfying `M โ K = โค`
23intersections. -/
25 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
26 (K : Subgroup G) [K.Normal] (hKclosed : IsClosed (K : Set G))
27 (๐ : Set (Subgroup G))
28 (hMclosed : โ M โ ๐, IsClosed (M : Set G))
29 (hfinite :
30 โ S : Set (Subgroup G), S.Finite โ S โ ๐ โ sInf S โ K = โค) :
31 sInf ๐ โ K = โค := by
32 rw [eq_top_iff]
33 intro g _
34 by_cases h๐ : ๐.Nonempty
35 ยท rcases h๐ with โจMโ, hMโโฉ
36 let coset : Set G := {x | gโปยน * x โ K}
37 let I := {M : Subgroup G // M โ ๐}
38 let F : I โ Set G := fun i => (i.1 : Set G) โฉ coset
39 have hcosetClosed : IsClosed coset := by
40 simpa [coset] using hKclosed.preimage (continuous_mul_left gโปยน)
41 have hclosed : โ i : I, IsClosed (F i) := by
42 intro i
43 exact (hMclosed i.1 i.2).inter hcosetClosed
44 have hfiniteNonempty : โ s : Finset I, (โ i โ s, F i).Nonempty := by
45 intro s
46 let S : Set (Subgroup G) := (fun i : I => i.1) '' (s : Set _)
47 have hSfinite : S.Finite := s.finite_toSet.image _
48 have hSsub : S โ ๐ := by
49 rintro M โจi, _hi, rflโฉ
50 exact i.2
51 have htop : sInf S โ K = โค := hfinite S hSfinite hSsub
52 have hgmem : g โ sInf S โ K := by
53 rw [htop]
54 exact Subgroup.mem_top g
55 rcases (Subgroup.mem_sup_of_normal_right (s := sInf S) (t := K) (x := g)).1 hgmem with
56 โจl, hlS, k, hk, hlkโฉ
57 refine โจl, ?_โฉ
58 simp only [Set.mem_iInter]
59 intro i hi
60 constructor
61 ยท exact (Subgroup.mem_sInf.mp hlS) i.1 โจi, hi, rflโฉ
62 ยท have hg : g = l * k := hlk.symm
63 have : gโปยน * l = kโปยน := by
64 rw [hg]
65 simp only [mul_inv_rev, mul_assoc, inv_mul_cancel, mul_one]
66 change gโปยน * l โ K
67 rw [this]
68 exact K.inv_mem hk
69 rcases CompactSpace.iInter_nonempty (t := F) hclosed hfiniteNonempty with โจx, hxโฉ
70 have hxall : โ i : I, x โ F i := by
71 simpa [F] using hx
72 have hxL : x โ sInf ๐ := by
73 rw [Subgroup.mem_sInf]
74 intro M hM
75 exact (hxall โจM, hMโฉ).1
76 have hxK : gโปยน * x โ K := (hxall โจMโ, hMโโฉ).2
77 have hxmem : x * (gโปยน * x)โปยน โ sInf ๐ โ K :=
78 Subgroup.mul_mem_sup hxL (K.inv_mem hxK)
79 simpa [mul_assoc] using hxmem
80 ยท have h๐_empty : ๐ = โ
:= Set.not_nonempty_iff_eq_empty.mp h๐
81 have htop : sInf ๐ = โค := by
82 rw [h๐_empty, sInf_empty]
83 simp only [htop, le_top, sup_of_le_left, Subgroup.mem_top]
85/-- Maximal open normal subgroups with a fixed nonabelian simple quotient are
86closed under arbitrary intersections. -/
88 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
89 (K : Subgroup G) [K.Normal] [IsSimpleGroup (G โงธ K)]
90 (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G โงธ K))
91 (hKclosed : IsClosed (K : Set G))
92 (๐ : Set (Subgroup G))
93 (hMnormal : โ M โ ๐, M.Normal)
94 (hMclosed : โ M โ ๐, IsClosed (M : Set G))
95 (hMtop : โ M โ ๐, M โ K = โค) :
96 sInf ๐ โ K = โค :=
97 maximal_open_normal_intersections_compactness_step K hKclosed ๐ hMclosed
98 (fun _S hSfinite hSsub =>
99 finite_sInf_sup_eq_top_of_noncomm_simple_quotient K hquotNoncomm hSfinite
100 (fun M hM => hMnormal M (hSsub hM))
101 (fun M hM => hMtop M (hSsub hM)))
103end ProCGroups.NormalSubgroups