Yamaguchi Lean 4 Library
ProCGroups/FreeProC/Criteria/InverseLimitsAndFiniteSubsets.lean
ProCGroups/FreeProC/Criteria/InverseLimitsAndFiniteSubsets/Source

ProCGroups/FreeProC/Criteria/InverseLimitsAndFiniteSubsets.lean

1import ProCGroups.FreeProC.Basic
2import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/FreeProC/Criteria/InverseLimitsAndFiniteSubsets.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Free pro-C groups
15Develops free pro-C groups on spaces and pointed spaces, their universal properties, finite
16quotient characterizations, and standard comparison isomorphisms.
17-/
19open Set
20open scoped Topology
22namespace ProCGroups.FreeProC
24universe u v
26section InverseLimitsAndFiniteSubsets
29variable {I : Type u} [Preorder I]
31/-- A bundled inverse system of topological groups. -/
33 toInverseSystem : ProCGroups.InverseSystems.InverseSystem (I := I)
34 group : ∀ i, Group (toInverseSystem.X i)
36 isTopologicalGroup : ∀ i, IsTopologicalGroup (toInverseSystem.X i)
37 inverseLimit_isTopologicalGroup :
38 letI : ∀ i, Group (toInverseSystem.X i) := group
40 letI : ∀ i, IsTopologicalGroup (toInverseSystem.X i) := isTopologicalGroup
41 IsTopologicalGroup toInverseSystem.inverseLimit
43attribute [instance] TopologicalGroupInverseSystemData.group
44attribute [instance] TopologicalGroupInverseSystemData.isGroupSystem
45attribute [instance] TopologicalGroupInverseSystemData.isTopologicalGroup
49 IsTopologicalGroup S.toInverseSystem.inverseLimit := by
50 simpa using S.inverseLimit_isTopologicalGroup
52/-- A pointed inverse system of profinite spaces. -/
54 I : Type u
55 instPreorder : Preorder I
56 system : ProCGroups.InverseSystems.InverseSystem.{u, u} (I := I)
57 point : ∀ i, system.X i
58 map_point : ∀ {i j : I} (hij : i ≤ j), system.map hij (point j) = point i
59 profinite_stage : ∀ i, ProCGroups.InverseSystems.IsProfiniteSpace (system.X i)
61attribute [instance] PointedProfiniteInverseSystem.instPreorder
65/-- The compatible basepoint in the inverse limit of a pointed profinite system. -/
66def limitPoint (S : PointedProfiniteInverseSystem) : S.system.inverseLimit :=
67 ⟨fun i => S.point i, fun _i _j hij => S.map_point hij⟩
71/-- A presentation of a pointed profinite space as an inverse limit of pointed profinite spaces. -/
73 (X : Type u) [TopologicalSpace X] (x0 : X) where
75 homeomorph : X ≃ₜ inverseSystem.system.inverseLimit
76 map_base : homeomorph x0 = inverseSystem.limitPoint
78/-- The type of finite subsets of `X`, encoded without any decidable-equality assumption. -/
79abbrev FiniteSubset (X : Type u) := {Y : Set X // Y.Finite}
81/-- A continuous homomorphism from a profinite group onto a profinite target is surjective once
82its range contains a topological generating family of the target. -/
84 {α : Type u}
85 {G : Type u} [Group G] [TopologicalSpace G]
86 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
87 (hGprof : IsProfiniteGroup G)
88 (hHprof : IsProfiniteGroup H)
89 {ι : α → H}
90 (hgen : Generation.TopologicallyGenerates (G := H) (Set.range ι))
91 {σ : G →* H} (hσ : Continuous σ)
92 (hsub : Set.range ι ⊆ (σ.range : Set H)) :
93 Function.Surjective σ := by
94 letI : CompactSpace G := IsProfiniteGroup.compactSpace hGprof
95 letI : T2Space H := IsProfiniteGroup.t2Space hHprof
96 have hσgen : Generation.TopologicallyGenerates (G := H) ((σ.range : Set H)) :=
97 Generation.topologicallyGenerates_mono (G := H) hgen hsub
98 have hσclosed : IsClosed ((σ.range : Set H)) := by
99 simpa using (isCompact_range hσ).isClosed
100 have hσclosure_le : (σ.range : Subgroup H).topologicalClosure ≤ σ.range :=
101 Subgroup.topologicalClosure_minimal _ le_rfl hσclosed
102 have hσclosure_top : (σ.range : Subgroup H).topologicalClosure = ⊤ := by
103 have htop :
104 (Subgroup.closure (σ.range : Set H)).topologicalClosure = (⊤ : Subgroup H) := by
105 simpa [Generation.TopologicallyGenerates] using hσgen
106 have hclosure_eq : (σ.range : Subgroup H) = Subgroup.closure (σ.range : Set H) := by
107 simpa using (Subgroup.closure_eq (σ.range)).symm
108 rw [hclosure_eq]
109 exact htop
110 have hσrange_top : σ.range = ⊤ := by
111 apply top_unique
112 intro z hz
113 have hz' : z ∈ ((σ.range : Subgroup H).topologicalClosure : Set H) := by
114 rw [hσclosure_top]
115 simp only [Subgroup.coe_top, mem_univ]
116 exact hσclosure_le hz'
117 intro z
118 have hz : z ∈ (σ.range : Set H) := by
119 simp only [hσrange_top, Subgroup.coe_top, mem_univ]
120 simpa using hz
122/-- The kernel in a split exact sequence is the smallest closed normal subgroup containing
123a specified set. -/
125 {G : Type u} [Group G] [TopologicalSpace G]
126 (A : Set G) (N : Subgroup G) : Prop :=
127 N.Normal ∧
128 IsClosed ((N : Set G)) ∧
129 A ⊆ (N : Set G) ∧
130 ∀ M : Subgroup G, M.Normal → IsClosed ((M : Set G)) → A ⊆ (M : Set G) → N ≤ M
132/-- Pointed free pro-`C` groups on pointed profinite spaces preserve inverse-limit
133presentations by transporting the pointed free structure across the presenting homeomorphism. -/
135 {X : Type u} [TopologicalSpace X] {x0 : X}
137 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
138 {ι : X → F}
139 (hι : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι) :
140 ∃ ιlim : P.inverseSystem.system.inverseLimit → F,
141 Continuous ιlim ∧
142 ιlim P.inverseSystem.limitPoint = 1 ∧
143 (∀ x, ιlim (P.homeomorph x) = ι x) ∧
145 P.inverseSystem.system.inverseLimit P.inverseSystem.limitPoint F ιlim := by
146 let ιlim : P.inverseSystem.system.inverseLimit → F := ι ∘ P.homeomorph.symm
147 have hιlim : Continuous ιlim :=
148 hι.continuous_ι.comp P.homeomorph.symm.continuous_toFun
149 have hsymm_base : P.homeomorph.symm P.inverseSystem.limitPoint = x0 := by
150 simpa [P.map_base] using P.homeomorph.left_inv x0
151 refine ⟨ιlim, hιlim, ?_, ?_, ?_⟩
152 · simpa [ιlim, hsymm_base] using hι.map_base
153 · intro x
154 simp only [Function.comp_apply, Homeomorph.symm_apply_apply, ιlim]
155 · refine ⟨hι.isProC, hιlim, ?_, ?_, ?_⟩
156 · simpa [ιlim, hsymm_base] using hι.map_base
157 · have hsub : Set.range ι ⊆ Set.range ιlim := by
158 rintro z ⟨x, rfl⟩
159 exact ⟨P.homeomorph x, by simp only [Function.comp_apply, Homeomorph.symm_apply_apply, ιlim]⟩
160 exact Generation.topologicallyGenerates_mono (G := F) hι.generates_range hsub
161 · intro G _ _ _ hG φ hφ hφ0 hgen
162 let ψ : X → G := φ ∘ P.homeomorph
163 have hψ : Continuous ψ := hφ.comp P.homeomorph.continuous_toFun
164 have hψ0 : ψ x0 = 1 := by
165 simpa [ψ, Function.comp, P.map_base] using hφ0
166 have hψgen : Generation.TopologicallyGenerates (G := G) (Set.range ψ) := by
167 have hrange : Set.range ψ = Set.range φ := by
168 ext z
169 constructor
170 · rintro ⟨x, rfl⟩
171 exact ⟨P.homeomorph x, rfl⟩
172 · rintro ⟨y, rfl⟩
173 exact ⟨P.homeomorph.symm y, by simp only [Function.comp_apply, Homeomorph.apply_symm_apply, ψ]⟩
174 simpa [hrange] using hgen
175 rcases hι.existsUnique_lift hG ψ hψ hψ0 hψgen with ⟨f, hf, huniq⟩
176 refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
177 · intro y
178 rcases P.homeomorph.surjective y with ⟨x, rfl⟩
179 simpa [ιlim, ψ, Function.comp] using hf.2 x
180 · intro g hg
181 apply huniq g
182 refine ⟨hg.1, ?_⟩
183 intro x
184 simpa [ψ, ιlim, Function.comp] using hg.2 (P.homeomorph x)
186/-- Every pointed profinite space has a finite inverse-limit presentation. -/
188 {X : Type u} [TopologicalSpace X] (hX : ProCGroups.InverseSystems.IsProfiniteSpace X)
189 (x0 : X) :
190 ∃ P : PointedProfinitePresentation.{u, u} X x0,
191 ∀ i : P.inverseSystem.I, Finite (P.inverseSystem.system.X i) := by
192 letI : CompactSpace X := hX.1
193 letI : T2Space X := hX.2.1
194 letI : TotallyDisconnectedSpace X := hX.2.2
197 I := OrderDual (DiscreteQuotient X)
198 instPreorder := inferInstance
199 system := S
200 point := fun Q => (show DiscreteQuotient X from Q).proj x0
201 map_point := by
202 intro Q R hQR
203 exact DiscreteQuotient.ofLE_proj hQR x0
204 profinite_stage := by
205 intro Q
207 (Quotient (show DiscreteQuotient X from Q).toSetoid)
208 letI : Fintype (Quotient (show DiscreteQuotient X from Q).toSetoid) := by
209 have : Finite (show DiscreteQuotient X from Q) := inferInstance
210 exact Fintype.ofFinite _
211 exact
213 (Quotient (show DiscreteQuotient X from Q).toSetoid)
214 }
215 let e : X ≃ₜ Psys.system.inverseLimit :=
217 let P : PointedProfinitePresentation.{u, u} X x0 := {
220 map_base := by
221 ext Q
222 rfl
223 }
224 refine ⟨P, ?_⟩
225 intro Q
226 change Finite (Quotient (show DiscreteQuotient X from Q).toSetoid)
227 infer_instance
229/-- Every pointed profinite space admits a finite inverse-limit presentation, and a pointed
230free pro-`C` group on it transports to the inverse-limit space. -/
232 {X : Type u} [TopologicalSpace X] {x0 : X}
234 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
235 {ι : X → F}
236 (hι : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι) :
237 ∃ P : PointedProfinitePresentation.{u, u} X x0,
238 (∀ i : P.inverseSystem.I, Finite (P.inverseSystem.system.X i)) ∧
239 ∃ ιlim : P.inverseSystem.system.inverseLimit → F,
240 Continuous ιlim ∧
241 ιlim P.inverseSystem.limitPoint = 1 ∧
243 P.inverseSystem.system.inverseLimit P.inverseSystem.limitPoint F ιlim := by
245 rcases pointedFreeProCGroup_preserves_inverseLimits (ProC := ProC) P hι with
246 ⟨ιlim, hιlim, hbase, _hfac, hfree⟩
247 exact ⟨P, hfinite, ιlim, hιlim, hbase, hfree⟩
249/-- Raw finite-subset inverse-system construction for a free pro-`C` group on a basis converging
250to `1`. The result is intentionally unbundled; `FiniteSubsetSystem` in
251`ProCGroups.FreeProC.FinitelyGenerated` packages this data for ordinary use. -/
253 {X : Type u}
254 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
255 {ι : X → F}
256 (hProfinite :
257 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
258 @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
259 InverseSystems.IsProfiniteSpace G)
260 (hClosed :
261 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
262 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
263 (H : Subgroup G), IsClosed (H : Set G) →
264 @ProCGroups.ProC.ProCGroupPredicate.holds ProC H _ _ _)
265 (hFiniteQuot :
266 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
267 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
268 (U : OpenNormalSubgroup G),
269 @ProCGroups.ProC.ProCGroupPredicate.holds ProC (G ⧸ (U : Subgroup G)) _ _ _)
270 (hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι) :
272 ∃ basis : ∀ s : FiniteSubset X, ↥s.1 → S.toInverseSystem.X s,
273 (∀ s : FiniteSubset X,
275 ↥s.1 (S.toInverseSystem.X s) (basis s)) ∧
276 (∀ {s t : FiniteSubset X} (hst : s ≤ t) (x : ↥t.1),
277 S.toInverseSystem.map hst (basis t x) =
278 by
279 classical
280 exact if hx : x.1 ∈ s.1 then basis s ⟨x.1, hx⟩ else 1) ∧
281 (∀ s : FiniteSubset X,
282 ∃ e : S.toInverseSystem.X s →* F,
283 Continuous e ∧
284 Function.Injective e ∧
285 IsClosed (Set.range e) ∧
286 ∀ x : ↥s.1, e (basis s x) = ι x.1) ∧
287 Nonempty (F ≃ₜ* S.toInverseSystem.inverseLimit) := by
288 classical
289 let hFspace : InverseSystems.IsProfiniteSpace F := hProfinite hF.isProC
290 let hFprof :
292 IsProfiniteGroup.of_isProfiniteSpace hFspace
293 letI : CompactSpace F := IsProfiniteGroup.compactSpace hFprof
294 letI : T2Space F := IsProfiniteGroup.t2Space hFprof
295 letI : TotallyDisconnectedSpace F := IsProfiniteGroup.totallyDisconnectedSpace hFprof
296 let stage : FiniteSubset X → Subgroup F :=
297 fun s => (Subgroup.closure (Set.range fun x : ↥s.1 => ι x.1)).topologicalClosure
298 let stageBasis : ∀ s : FiniteSubset X, ↥s.1 → stage s :=
299 fun s x => ⟨ι x.1, Subgroup.le_topologicalClosure _ <| by
300 exact Subgroup.subset_closure ⟨x, rfl⟩⟩
301 have hstage_closed : ∀ s : FiniteSubset X, IsClosed ((stage s : Set F)) := by
302 intro s
303 exact Subgroup.isClosed_topologicalClosure _
304 have hstage_proC :
305 ∀ s : FiniteSubset X, @ProCGroups.ProC.ProCGroupPredicate.holds ProC (stage s) _ _ _ := by
306 intro s
307 exact hClosed hF.isProC (stage s) (hstage_closed s)
308 have hstage_space :
309 ∀ s : FiniteSubset X, InverseSystems.IsProfiniteSpace (stage s) := by
310 intro s
311 exact hProfinite (hstage_proC s)
312 have hstage_prof :
313 ∀ s : FiniteSubset X, IsProfiniteGroup (stage s) := by
314 intro s
315 exact IsProfiniteGroup.of_isProfiniteSpace (hstage_space s)
316 let stageSet : ∀ s : FiniteSubset X, Set (stage s) :=
317 fun s => Set.range (stageBasis s)
318 have hstage_generates :
319 ∀ s : FiniteSubset X,
320 Generation.TopologicallyGenerates (G := stage s) (stageSet s) := by
321 intro s
322 let H := stage s
323 let K : Subgroup H := Subgroup.closure (stageSet s)
324 have hclosedSubtype : IsClosedMap (H.subtype : H → F) :=
325 (hstage_closed s).isClosedMap_subtype_val
326 have hclosure :
327 closure (((fun y : H => (y : F)) '' ((K : Set H)))) =
328 (fun y : H => (y : F)) '' closure ((K : Set H)) :=
329 hclosedSubtype.closure_image_eq_of_continuous continuous_subtype_val _
330 have himg :
331 ((fun y : H => (y : F)) '' ((K : Set H))) =
332 (((Subgroup.closure (Set.range fun x : ↥s.1 => ι x.1)) : Subgroup F) : Set F) := by
333 have hstageRange :
334 ((fun y : H => (y : F)) '' stageSet s) =
335 Set.range (fun x : ↥s.1 => ι x.1) := by
336 ext z
337 constructor
338 · rintro ⟨x, hx, rfl⟩
339 rcases hx with ⟨y, rfl⟩
340 exact ⟨y, rfl⟩
341 · rintro ⟨x, rfl⟩
342 exact ⟨stageBasis s x, ⟨x, rfl⟩, rfl⟩
343 have hmap :
344 K.map H.subtype =
345 Subgroup.closure (((fun y : H => (y : F)) '' stageSet s)) := by
347 (H.subtype.map_closure (stageSet s))
348 simpa [hstageRange] using
349 congrArg (fun L : Subgroup F => (L : Set F)) hmap
350 rw [Generation.topologicallyGenerates_iff_dense, dense_iff_closure_eq]
351 ext y
352 constructor
353 · intro _hy
354 simp only [mem_univ]
355 · intro _hy
356 have hy' : (y : F) ∈ ((fun z : H => (z : F)) '' closure ((K : Set H))) := by
357 rw [← hclosure, himg]
358 simp only [Subtype.coe_prop, stage]
359 rcases hy' with ⟨w, hw, hwEq⟩
360 exact (Subtype.ext hwEq) ▸ hw
361 have hstage_free :
362 ∀ s : FiniteSubset X,
363 IsFreeProCGroupOnConvergingSet (ProC := ProC) ↥s.1 (stage s) (stageBasis s) := by
364 intro s
365 letI : Finite ↥s.1 := s.2.to_subtype
366 refine ⟨hstage_proC s, ?_, hstage_generates s, ?_⟩
367 · exact FamilyConvergesToOne.of_finite_domain (G := stage s) (stageBasis s)
368 · intro G _ _ _ hG φ hφconv hφgen
369 let hGspace : InverseSystems.IsProfiniteSpace G := hProfinite hG
370 let hGprof : IsProfiniteGroup G := by
371 exact IsProfiniteGroup.of_isProfiniteSpace hGspace
372 letI : T2Space G := IsProfiniteGroup.t2Space hGprof
373 let ψ : X → G := fun x => if hx : x ∈ s.1 then φ ⟨x, hx⟩ else 1
374 have hψsub :
375 Set.range ψ ⊆ Set.range φ ∪ ({1} : Set G) := by
376 intro z hz
377 rcases hz with ⟨x, rfl⟩
378 by_cases hx : x ∈ s.1
379 · left
380 exact ⟨⟨x, hx⟩, by simp only [hx, ↓reduceDIte, ψ]⟩
381 · right
382 simp only [hx, ↓reduceDIte, mem_singleton_iff, ψ]
383 have hψconv : FamilyConvergesToOne (G := G) ψ := by
384 intro U
385 have hsubset : {x : X | ψ x ∉ (U : Set G)} ⊆ s.1 := by
386 intro x hx
387 by_cases hxs : x ∈ s.1
388 · exact hxs
389 · exfalso
390 exact hx (by simp only [hxs, ↓reduceDIte, SetLike.mem_coe, one_mem, ψ])
391 exact s.2.subset hsubset
392 have hψgen : Generation.TopologicallyGenerates (G := G) (Set.range ψ) := by
393 have hsub : Set.range φ ⊆ Set.range ψ := by
394 intro z hz
395 rcases hz with ⟨x, rfl⟩
396 exact ⟨x.1, by simp only [x.2, ↓reduceDIte, Subtype.coe_eta, ψ]⟩
397 exact Generation.topologicallyGenerates_mono (G := G) hφgen hsub
398 rcases hF.existsUnique_lift hG ψ hψconv hψgen with ⟨f, hf, huniq⟩
399 let fs : stage s →* G := f.comp (stage s).subtype
400 refine ⟨fs, ⟨hf.1.comp continuous_subtype_val, ?_⟩, ?_⟩
401 · intro x
402 simpa [fs, ψ, stageBasis, x.2] using hf.2 x.1
403 · intro g hg
404 let K : Subgroup (stage s) := Subgroup.closure (stageSet s)
405 let E : Subgroup (stage s) := {
406 carrier := {x | g x = fs x}
407 one_mem' := by
408 change g 1 = fs 1
410 mul_mem' := by
411 intro a b ha hb
412 change g (a * b) = fs (a * b)
413 rw [map_mul, map_mul, ha, hb]
414 inv_mem' := by
415 intro a ha
416 change g a⁻¹ = fs a⁻¹
417 rw [map_inv, map_inv, ha] }
418 have hrangeE : stageSet s ⊆ (E : Set (stage s)) := by
419 rintro z ⟨x, rfl⟩
420 change g (stageBasis s x) = fs (stageBasis s x)
421 calc
422 g (stageBasis s x) = φ x := hg.2 x
423 _ = f (ι x.1) := by
424 simpa [ψ, x.2] using (hf.2 x.1).symm
425 _ = fs (stageBasis s x) := rfl
426 have hKle : K ≤ E := by
427 change Subgroup.closure (stageSet s) ≤ E
428 exact (Subgroup.closure_le (K := E)).2 hrangeE
429 have hKdense : DenseRange (K.subtype : K → stage s) := by
430 rw [DenseRange]
431 simpa [K, stageSet, Subgroup.range_subtype] using
432 (Generation.topologicallyGenerates_iff_dense (G := stage s) (X := stageSet s)).1 (hstage_generates s)
433 have hEqFun : (g : stage s → G) = fs := by
434 apply DenseRange.equalizer (f := K.subtype) hKdense
435 · exact hg.1
436 · exact hf.1.comp continuous_subtype_val
437 · funext z
438 exact hKle z.2
439 ext x
440 exact congrFun hEqFun x
441 let extendBasis : ∀ s : FiniteSubset X, X → stage s :=
442 fun s x => if hx : x ∈ s.1 then stageBasis s ⟨x, hx⟩ else 1
443 have hextendBasis_conv :
444 ∀ s : FiniteSubset X, FamilyConvergesToOne (G := stage s) (extendBasis s) := by
445 intro s
446 letI : Finite ↥s.1 := s.2.to_subtype
447 intro U
448 have hsubset : {x : X | extendBasis s x ∉ (U : Set (stage s))} ⊆ s.1 := by
449 intro x hx
450 by_cases hxs : x ∈ s.1
451 · exact hxs
452 · exfalso
453 exact hx (by simp only [hxs, ↓reduceDIte, SetLike.mem_coe, one_mem, extendBasis])
454 exact s.2.subset hsubset
455 have hextendBasis_gen :
456 ∀ s : FiniteSubset X,
457 Generation.TopologicallyGenerates (G := stage s) (Set.range (extendBasis s)) := by
458 intro s
459 have hsub : stageSet s ⊆ Set.range (extendBasis s) := by
460 intro z hz
461 rcases hz with ⟨x, rfl⟩
462 exact ⟨x.1, by simp only [x.2, ↓reduceDIte, extendBasis, stageBasis]⟩
463 exact Generation.topologicallyGenerates_mono (G := stage s) (hstage_generates s) hsub
464 let stageRetraction :
465 ∀ s : FiniteSubset X, F →* stage s := fun s =>
466 Classical.choose <| ExistsUnique.exists <|
467 hF.existsUnique_lift (hstage_proC s) (extendBasis s)
468 (hextendBasis_conv s) (hextendBasis_gen s)
469 have hstageRetraction_continuous :
470 ∀ s : FiniteSubset X, Continuous (stageRetraction s) := by
471 intro s
472 exact (Classical.choose_spec <| ExistsUnique.exists <|
473 hF.existsUnique_lift (hstage_proC s) (extendBasis s)
474 (hextendBasis_conv s) (hextendBasis_gen s)).1
475 have hstageRetraction_spec :
476 ∀ s : FiniteSubset X, ∀ x : X,
477 stageRetraction s (ι x) = extendBasis s x := by
478 intro s x
479 exact (Classical.choose_spec <| ExistsUnique.exists <|
480 hF.existsUnique_lift (hstage_proC s) (extendBasis s)
481 (hextendBasis_conv s) (hextendBasis_gen s)).2 x
482 have hstageRetraction_restrict :
483 ∀ s : FiniteSubset X,
484 (stageRetraction s).comp (stage s).subtype = MonoidHom.id (stage s) := by
485 intro s
486 let basis := stageBasis s
487 rcases (hstage_free s).existsUnique_lift (hstage_proC s) basis
488 (by simpa using (hstage_free s).convergesToOne)
489 (by simpa using (hstage_free s).generates_range) with
490 ⟨u, hu, huniq⟩
491 have hId :
492 Continuous (MonoidHom.id (stage s)) ∧
493 ∀ x : ↥s.1, (MonoidHom.id (stage s)) (basis x) = basis x := by
494 refine ⟨continuous_id, ?_⟩
495 intro x
496 rfl
497 have hRet :
498 Continuous ((stageRetraction s).comp (stage s).subtype) ∧
499 ∀ x : ↥s.1, ((stageRetraction s).comp (stage s).subtype) (basis x) = basis x := by
500 refine ⟨(hstageRetraction_continuous s).comp continuous_subtype_val, ?_⟩
501 intro x
502 simpa [basis, extendBasis, stageBasis, x.2, MonoidHom.comp_apply] using
503 hstageRetraction_spec s x.1
504 calc
505 (stageRetraction s).comp (stage s).subtype = u := huniq _ hRet
506 _ = MonoidHom.id (stage s) := (huniq _ hId).symm
507 have hstageRetraction_comp :
508 ∀ {s t : FiniteSubset X}, s ≤ t →
509 ((stageRetraction s).comp (stage t).subtype).comp (stageRetraction t) =
510 stageRetraction s := by
511 intro s t hst
512 rcases hF.existsUnique_lift (hstage_proC s) (extendBasis s)
513 (hextendBasis_conv s) (hextendBasis_gen s) with ⟨u, hu, huniq⟩
514 have hStage : stageRetraction s = u :=
515 huniq _ ⟨hstageRetraction_continuous s, hstageRetraction_spec s⟩
516 have hComp :
517 ((stageRetraction s).comp (stage t).subtype).comp (stageRetraction t) = u := by
518 refine huniq _ ⟨((hstageRetraction_continuous s).comp continuous_subtype_val).comp
519 (hstageRetraction_continuous t), ?_⟩
520 intro x
521 by_cases hx : x ∈ t.1
522 · calc
523 (((stageRetraction s).comp (stage t).subtype).comp (stageRetraction t)) (ι x)
524 = stageRetraction s ((stage t).subtype (stageBasis t ⟨x, hx⟩)) := by
525 simp only [MonoidHom.comp_apply, hstageRetraction_spec, hx, ↓reduceDIte, Subgroup.subtype_apply, extendBasis]
526 _ = stageRetraction s (ι x) := rfl
527 _ = extendBasis s x := hstageRetraction_spec s x
528 · have hsx : x ∉ s.1 := fun hsx => hx (hst hsx)
529 calc
530 (((stageRetraction s).comp (stage t).subtype).comp (stageRetraction t)) (ι x)
531 = stageRetraction s ((stage t).subtype (1 : stage t)) := by
532 simp only [MonoidHom.comp_apply, hstageRetraction_spec, hx, ↓reduceDIte, map_one,
533 extendBasis]
534 _ = stageRetraction s 1 := rfl
535 _ = 1 := map_one _
536 _ = extendBasis s x := by simp only [hsx, ↓reduceDIte, extendBasis]
537 exact hComp.trans hStage.symm
538 let stageMap :
539 ∀ {s t : FiniteSubset X}, s ≤ t → stage t →* stage s :=
540 fun {_s _t} _ => (stageRetraction _s).comp (stage _t).subtype
541 let Ssys : InverseSystems.InverseSystem (I := FiniteSubset X) := {
542 X := fun s => stage s
543 topologicalSpace := fun s => inferInstance
544 map := fun {_s _t} hst => stageMap hst
545 continuous_map := by
546 intro s t hst
547 exact (hstageRetraction_continuous s).comp continuous_subtype_val
548 map_id := by
549 intro s
550 funext x
551 simpa [stageMap] using congrArg (fun f : stage s →* stage s => f x)
552 (hstageRetraction_restrict s)
553 map_comp := by
554 intro s t u hst htu
555 funext x
556 change stageRetraction s ((stage t).subtype ((stageRetraction t) ((stage u).subtype x))) =
557 stageRetraction s ((stage u).subtype x)
558 simpa [stageMap, MonoidHom.comp_apply] using
559 congrArg (fun f : F →* stage s => f ((stage u).subtype x)) (hstageRetraction_comp hst)
560 }
562 toInverseSystem := Ssys
563 group := fun s => inferInstance
565 map_one := by
566 intro s t hst
567 exact (stageMap hst).map_one
568 map_mul := by
569 intro s t hst x y
570 exact (stageMap hst).map_mul x y
571 map_inv := by
572 intro s t hst x
573 exact (stageMap hst).map_inv x
574 }
575 isTopologicalGroup := fun s => inferInstance
576 inverseLimit_isTopologicalGroup := by infer_instance
577 }
578 letI : ∀ s, Group (Ssys.X s) := Sdata.group
579 letI : InverseSystems.IsGroupSystem Ssys := Sdata.isGroupSystem
580 letI : ∀ s, IsTopologicalGroup (Ssys.X s) := Sdata.isTopologicalGroup
581 let limitMap : F → Ssys.inverseLimit :=
582 Ssys.inverseLimitLift (fun s => stageRetraction s)
583 (by
584 intro s t hst
585 funext x
586 change stageRetraction s ((stage t).subtype (stageRetraction t x)) = stageRetraction s x
587 simpa [MonoidHom.comp_apply] using
588 congrArg (fun f : F →* stage s => f x) (hstageRetraction_comp hst))
589 have hlimitMap_continuous : Continuous limitMap :=
590 Ssys.continuous_inverseLimitLift (fun s => stageRetraction s) (fun s => hstageRetraction_continuous s)
591 (by
592 intro s t hst
593 funext x
594 change stageRetraction s ((stage t).subtype (stageRetraction t x)) = stageRetraction s x
595 simpa [MonoidHom.comp_apply] using
596 congrArg (fun f : F →* stage s => f x) (hstageRetraction_comp hst))
597 let limitHom : F →* Ssys.inverseLimit := {
598 toFun := limitMap
599 map_one' := by
600 apply Ssys.ext
601 intro s
602 change stageRetraction s 1 = 1
603 exact map_one _
604 map_mul' := by
605 intro x y
606 apply Ssys.ext
607 intro s
608 change stageRetraction s (x * y) = stageRetraction s x * stageRetraction s y
609 exact map_mul _ _ _
610 }
611 have hlimit_inj : Function.Injective limitHom := by
612 intro x y hxy
613 by_contra hne
614 have hxyne : x * y⁻¹ ≠ 1 := by
615 intro h1
616 apply hne
617 simpa using mul_inv_eq_one.mp h1
618 rcases ProCGroups.ProC.exists_openNormalSubgroup_not_mem (G := F) hFprof hxyne with ⟨U, hUxy⟩
619 let q : F →* F ⧸ (U : Subgroup F) := QuotientGroup.mk' (U : Subgroup F)
620 letI : Finite (F ⧸ (U : Subgroup F)) := by infer_instance
621 letI : DiscreteTopology (F ⧸ (U : Subgroup F)) := by infer_instance
622 have hquotProC :
623 @ProCGroups.ProC.ProCGroupPredicate.holds ProC (F ⧸ (U : Subgroup F)) _ _ _ := by
624 exact hFiniteQuot hF.isProC U
625 let Uone : OpenSubgroup (F ⧸ (U : Subgroup F)) :=
626 ⟨⊥, by
627 exact
628 isOpen_discrete
629 ((⊥ : Subgroup (F ⧸ (U : Subgroup F))) : Set (F ⧸ (U : Subgroup F)))⟩
630 have himg :
631 Generation.GeneratesAndConvergesToOne (G := F ⧸ (U : Subgroup F))
632 (q '' Set.range ι) := by
633 exact Generation.GeneratesAndConvergesToOne.image_of_continuousSurjective
634 (G := F) hFprof q continuous_quotient_mk'
635 (QuotientGroup.mk'_surjective (U : Subgroup F))
636 ⟨hF.generates_range, hF.convergesToOne.range⟩
637 have hnontriv :
638 {x : X | ι x ∉ (U : Set F)}.Finite := by
639 exact hF.convergesToOne U.toOpenSubgroup
640 let s0 : FiniteSubset X := ⟨{x : X | ι x ∉ (U : Set F)}, hnontriv⟩
641 letI : Finite ↥s0.1 := s0.2.to_subtype
642 let φ0 : ↥s0.1 → F ⧸ (U : Subgroup F) := fun x => q (ι x.1)
643 have hφ0conv : FamilyConvergesToOne (G := F ⧸ (U : Subgroup F)) φ0 := by
644 letI : Finite ↥s0.1 := s0.2.to_subtype
645 exact FamilyConvergesToOne.of_finite_domain (G := F ⧸ (U : Subgroup F)) φ0
646 have hgen0 : Generation.TopologicallyGenerates (G := F ⧸ (U : Subgroup F)) (Set.range φ0) := by
647 have hgen' :
648 Generation.TopologicallyGenerates (G := F ⧸ (U : Subgroup F))
649 (q '' Set.range ι) := by
650 simpa [Set.range_comp] using himg.1
651 have hsub :
652 q '' Set.range ι ⊆ Set.range φ0 ∪ ({1} : Set (F ⧸ (U : Subgroup F))) := by
653 rintro z ⟨w, ⟨x, rfl⟩, rfl⟩
654 by_cases hx : x ∈ s0.1
655 · left
656 exact ⟨⟨x, hx⟩, rfl⟩
657 · right
658 have hxU : ι x ∈ (U : Set F) := by
659 exact by
660 simp only [s0, Set.mem_setOf_eq, not_not] at hx
661 exact hx
662 have hq1 : q (ι x) = 1 := by
663 simpa [q] using
664 (QuotientGroup.eq_one_iff (N := (U : Subgroup F)) (ι x)).2 hxU
665 simp only [hq1, mem_singleton_iff]
666 have hgenUnion :
667 Generation.TopologicallyGenerates (G := F ⧸ (U : Subgroup F))
668 (Set.range φ0 ∪ ({1} : Set (F ⧸ (U : Subgroup F)))) := by
669 exact Generation.topologicallyGenerates_mono (G := F ⧸ (U : Subgroup F)) hgen' hsub
670 rw [Generation.topologicallyGenerates_union_one_iff] at hgenUnion
671 exact hgenUnion
672 rcases (hstage_free s0).existsUnique_lift hquotProC φ0 hφ0conv hgen0 with
673 ⟨fq, hfq, _⟩
674 have hqfac : fq.comp (stageRetraction s0) = q := by
675 let ψ0 : X → F ⧸ (U : Subgroup F) := fun x =>
676 if hx : x ∈ s0.1 then φ0 ⟨x, hx⟩ else 1
677 have hψ0sub :
678 Set.range ψ0 ⊆ Set.range φ0 ∪ ({1} : Set (F ⧸ (U : Subgroup F))) := by
679 intro z hz
680 rcases hz with ⟨x, rfl⟩
681 by_cases hx : x ∈ s0.1
682 · left
683 exact ⟨⟨x, hx⟩, by simp only [dite_eq_ite, hx, ↓reduceIte, φ0, ψ0]⟩
684 · right
685 simp only [hx, ↓reduceDIte, mem_singleton_iff, ψ0]
686 have hψ0conv : FamilyConvergesToOne (G := F ⧸ (U : Subgroup F)) ψ0 := by
687 intro V
688 have hsubset :
689 {x : X | ψ0 x ∉ (V : Set (F ⧸ (U : Subgroup F)))} ⊆ s0.1 := by
690 intro x hx
691 by_cases hxs : x ∈ s0.1
692 · exact hxs
693 · exfalso
694 exact hx (by simp only [hxs, ↓reduceDIte, SetLike.mem_coe, one_mem, ψ0])
695 exact s0.2.subset hsubset
696 have hψ0gen :
697 Generation.TopologicallyGenerates (G := F ⧸ (U : Subgroup F)) (Set.range ψ0) := by
698 have hsub : Set.range φ0 ⊆ Set.range ψ0 := by
699 intro z hz
700 rcases hz with ⟨x, rfl⟩
701 exact ⟨x.1, by simp only [dite_eq_ite, x.2, ↓reduceIte, ψ0, φ0]⟩
702 exact Generation.topologicallyGenerates_mono (G := F ⧸ (U : Subgroup F)) hgen0 hsub
703 rcases hF.existsUnique_lift hquotProC ψ0 hψ0conv hψ0gen with ⟨u, hu, huniq⟩
704 have hqeq : q = u := by
705 exact huniq _ ⟨continuous_quotient_mk', by
706 intro x
707 by_cases hx : x ∈ s0.1
708 · simp only [dite_eq_ite, hx, ↓reduceIte, ψ0, φ0]
709 · have hx1 : q (ι x) = 1 := by
710 have hxU : ι x ∈ (U : Set F) := by
711 simpa [s0] using hx
712 simpa [q] using (QuotientGroup.eq_one_iff (N := (U : Subgroup F)) (ι x)).2 hxU
713 simp only [hx1, hx, ↓reduceDIte, ψ0]⟩
714 have hcompEq : fq.comp (stageRetraction s0) = u := by
715 exact huniq _ ⟨hfq.1.comp (hstageRetraction_continuous s0), by
716 intro x
717 by_cases hx : x ∈ s0.1
718 · calc
719 (fq.comp (stageRetraction s0)) (ι x)
720 = fq (stageBasis s0 ⟨x, hx⟩) := by
721 simp only [MonoidHom.comp_apply, hstageRetraction_spec, hx, ↓reduceDIte, extendBasis]
722 _ = φ0 ⟨x, hx⟩ := hfq.2 ⟨x, hx⟩
723 _ = ψ0 x := by simp only [dite_eq_ite, hx, ↓reduceIte, φ0, ψ0]
724 · calc
725 (fq.comp (stageRetraction s0)) (ι x)
726 = fq (1 : stage s0) := by
727 simp only [MonoidHom.comp_apply, hstageRetraction_spec, hx, ↓reduceDIte, map_one, extendBasis]
728 _ = 1 := map_one _
729 _ = ψ0 x := by simp only [hx, ↓reduceDIte, ψ0]⟩
730 exact hcompEq.trans hqeq.symm
731 have hs0eq :
732 stageRetraction s0 x = stageRetraction s0 y := by
733 exact congrArg (fun z : Ssys.inverseLimit => Ssys.projection s0 z) hxy
734 have hqeq : q x = q y := by
735 calc
736 q x = fq (stageRetraction s0 x) := by
737 simpa [MonoidHom.comp_apply] using
738 (congrArg (fun f : F →* F ⧸ (U : Subgroup F) => f x) hqfac).symm
739 _ = fq (stageRetraction s0 y) := by rw [hs0eq]
740 _ = q y := by
741 simpa [MonoidHom.comp_apply] using
742 congrArg (fun f : F →* F ⧸ (U : Subgroup F) => f y) hqfac
743 have hcontr :
744 x * y⁻¹ ∈ (U : Subgroup F) := by
745 simpa [div_eq_mul_inv] using
746 (QuotientGroup.eq_iff_div_mem (N := (U : Subgroup F))).mp hqeq
747 exact hUxy hcontr
748 have hlimit_surj : Function.Surjective limitHom := by
749 intro z
750 let C : FiniteSubset X → Set F := fun s => {x | stageRetraction s x = Ssys.projection s z}
751 have hCclosed : ∀ s : FiniteSubset X, IsClosed (C s) := by
752 intro s
753 simpa [C] using isClosed_singleton.preimage (hstageRetraction_continuous s)
754 have hCdir : Directed (· ⊇ ·) C := by
755 intro s t
756 refine ⟨⟨s.1 ∪ t.1, s.2.union t.2⟩, ?_, ?_⟩
757 · intro x hx
758 change stageRetraction s x = Ssys.projection s z
759 let hsu : s ≤ ⟨s.1 ∪ t.1, s.2.union t.2⟩ := by
760 intro y hy
761 exact Or.inl hy
762 have hcomp := congrArg (fun f : F →* stage s => f x)
763 (hstageRetraction_comp hsu)
764 have hzcomp :
765 stageMap hsu
766 (Ssys.projection ⟨s.1 ∪ t.1, s.2.union t.2⟩ z) =
767 Ssys.projection s z := by
768 exact z.2 s ⟨s.1 ∪ t.1, s.2.union t.2⟩ hsu
769 calc
770 stageRetraction s x
771 = stageRetraction s
772 ((stage ⟨s.1 ∪ t.1, s.2.union t.2⟩).subtype
773 (stageRetraction ⟨s.1 ∪ t.1, s.2.union t.2⟩ x)) := by
774 simpa [MonoidHom.comp_apply] using hcomp.symm
775 _ = stageMap hsu (stageRetraction ⟨s.1 ∪ t.1, s.2.union t.2⟩ x) := by
776 rfl
777 _ = stageMap hsu (Ssys.projection ⟨s.1 ∪ t.1, s.2.union t.2⟩ z) := by
778 rw [hx]
779 _ = Ssys.projection s z := hzcomp
780 · intro x hx
781 change stageRetraction t x = Ssys.projection t z
782 let htu' : t ≤ ⟨s.1 ∪ t.1, s.2.union t.2⟩ := by
783 intro y hy
784 exact Or.inr hy
785 have hzcomp :
786 stageMap htu'
787 (Ssys.projection ⟨s.1 ∪ t.1, s.2.union t.2⟩ z) =
788 Ssys.projection t z := by
789 exact z.2 t ⟨s.1 ∪ t.1, s.2.union t.2⟩ htu'
790 calc
791 stageRetraction t x
792 = stageRetraction t
793 ((stage ⟨s.1 ∪ t.1, s.2.union t.2⟩).subtype
794 (stageRetraction ⟨s.1 ∪ t.1, s.2.union t.2⟩ x)) := by
795 simpa [MonoidHom.comp_apply] using
796 (congrArg (fun f : F →* stage t => f x) (hstageRetraction_comp htu')).symm
797 _ = stageMap htu' (stageRetraction ⟨s.1 ∪ t.1, s.2.union t.2⟩ x) := by
798 rfl
799 _ = stageMap htu' (Ssys.projection ⟨s.1 ∪ t.1, s.2.union t.2⟩ z) := by
800 rw [hx]
801 _ = Ssys.projection t z := hzcomp
802 letI : Nonempty (FiniteSubset X) := ⟨⟨∅, Set.finite_empty⟩⟩
803 have hCnonemptyEach : ∀ s : FiniteSubset X, (C s).Nonempty := by
804 intro s
805 refine ⟨(stage s).subtype (Ssys.projection s z), ?_⟩
806 simpa [C, MonoidHom.comp_apply] using
807 congrArg (fun f : stage s →* stage s => f (Ssys.projection s z)) (hstageRetraction_restrict s)
808 have hCcompact : ∀ s : FiniteSubset X, IsCompact (C s) := by
809 intro s
810 exact (hCclosed s).isCompact
811 have hCnonempty : (⋂ s, C s).Nonempty := by
812 exact IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
813 (t := C) hCdir hCnonemptyEach hCcompact hCclosed
814 rcases hCnonempty with ⟨x, hx⟩
815 refine ⟨x, ?_⟩
816 apply Ssys.ext
817 intro s
818 exact Set.mem_iInter.1 hx s
819 have hlimit_bij : Function.Bijective limitHom := ⟨hlimit_inj, hlimit_surj⟩
820 refine ⟨Sdata, stageBasis, hstage_free, ?_, ?_, ?_⟩
821 · intro s t hst x
822 by_cases hx : x.1 ∈ s.1
823 · calc
824 Sdata.toInverseSystem.map hst (stageBasis t x)
825 = stageRetraction s (ι x.1) := rfl
826 _ = stageBasis s ⟨x.1, hx⟩ := by
827 simpa [extendBasis, stageBasis, hx]
828 using (hstageRetraction_spec s x.1).trans (by simp only [hx, ↓reduceDIte, extendBasis, stageBasis])
829 _ = (if hx' : x.1 ∈ s.1 then stageBasis s ⟨x.1, hx'⟩ else 1) := by
830 simp only [hx, ↓reduceDIte]
831 · calc
832 Sdata.toInverseSystem.map hst (stageBasis t x)
833 = stageRetraction s (ι x.1) := rfl
834 _ = 1 := by
835 simpa [extendBasis, hx] using hstageRetraction_spec s x.1
836 _ = (if hx' : x.1 ∈ s.1 then stageBasis s ⟨x.1, hx'⟩ else 1) := by
837 simp only [hx, ↓reduceDIte]
838 · intro s
839 refine ⟨(stage s).subtype, continuous_subtype_val, ?_, ?_, ?_⟩
840 · exact Subtype.val_injective
841 · convert hstage_closed s using 1
842 ext y
843 constructor
844 · rintro ⟨x, rfl⟩
845 exact x.2
846 · intro hy
847 exact ⟨⟨y, hy⟩, rfl⟩
848 · intro x
849 rfl
850 · refine ⟨ContinuousMulEquiv.ofBijectiveCompactToT2 limitHom hlimitMap_continuous hlimit_bij⟩
852/-- 3.10(a). For each finite subset of a basis converging to `1`, the corresponding finite-stage
853free pro-`C` group embeds as a closed subgroup of the ambient free pro-`C` group. -/
855 {X : Type u}
856 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
857 {ι : X → F}
858 (hProfinite :
859 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
860 @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
861 InverseSystems.IsProfiniteSpace G)
862 (hClosed :
863 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
864 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
865 (H : Subgroup G), IsClosed (H : Set G) →
866 @ProCGroups.ProC.ProCGroupPredicate.holds ProC H _ _ _)
867 (hFiniteQuot :
868 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
869 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
870 (U : OpenNormalSubgroup G),
871 @ProCGroups.ProC.ProCGroupPredicate.holds ProC (G ⧸ (U : Subgroup G)) _ _ _)
872 (hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
873 (s : FiniteSubset X) :
874 ∃ (Fs : Type u) (_ : Group Fs) (_ : TopologicalSpace Fs) (_ : IsTopologicalGroup Fs)
875 (ιs : ↥s.1 → Fs),
876 IsFreeProCGroupOnConvergingSet (ProC := ProC) ↥s.1 Fs ιs ∧
877 ∃ e : Fs →* F,
878 Continuous e ∧ Function.Injective e ∧ IsClosed (Set.range e) ∧
879 ∀ x : ↥s.1, e (ιs x) = ι x.1 := by
881 (ProC := ProC) (X := X) (F := F) (ι := ι)
882 hProfinite hClosed hFiniteQuot hF with
883 ⟨S, basis, hbasis, _hmap, hembed, _hlimit⟩
884 rcases hembed s with ⟨e, he, hinj, hclosed, heq⟩
885 exact ⟨S.toInverseSystem.X s, inferInstance, inferInstance, inferInstance, basis s,
886 hbasis s, e, he, hinj, hclosed, heq⟩
888/-- 3.10(b). A free pro-`C` group on a basis converging to `1` is the inverse limit of the
889finite-stage free pro-`C` groups attached to its finite subsets. -/
891 {X : Type u}
892 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
893 {ι : X → F}
894 (hProfinite :
895 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
896 @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
897 InverseSystems.IsProfiniteSpace G)
898 (hClosed :
899 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
900 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
901 (H : Subgroup G), IsClosed (H : Set G) →
902 @ProCGroups.ProC.ProCGroupPredicate.holds ProC H _ _ _)
903 (hFiniteQuot :
904 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
905 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
906 (U : OpenNormalSubgroup G),
907 @ProCGroups.ProC.ProCGroupPredicate.holds ProC (G ⧸ (U : Subgroup G)) _ _ _)
908 (hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι) :
910 ∃ basis : ∀ s : FiniteSubset X, ↥s.1 → S.toInverseSystem.X s,
911 (∀ s : FiniteSubset X,
913 ↥s.1 (S.toInverseSystem.X s) (basis s)) ∧
914 (∀ {s t : FiniteSubset X} (hst : s ≤ t) (x : ↥t.1),
915 S.toInverseSystem.map hst (basis t x) =
916 by
917 classical
918 exact if hx : x.1 ∈ s.1 then basis s ⟨x.1, hx⟩ else 1) ∧
919 (∀ s : FiniteSubset X,
920 ∃ e : S.toInverseSystem.X s →* F,
921 Continuous e ∧
922 Function.Injective e ∧
923 IsClosed (Set.range e) ∧
924 ∀ x : ↥s.1, e (basis s x) = ι x.1) ∧
925 Nonempty (F ≃ₜ* S.toInverseSystem.inverseLimit) := by
926 simpa using
928 (ProC := ProC) (X := X) (F := F) (ι := ι) hProfinite hClosed hFiniteQuot hF
929/-- Restricting a free pro-`C` group from a basis `X` to a sub-basis `Y` gives a split quotient
930whose kernel is the smallest closed normal subgroup generated by the complementary basis
931elements. -/
933 (hProfinite :
934 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
935 @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
936 InverseSystems.IsProfiniteSpace G)
937 (hClosed :
938 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
939 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
940 (H : Subgroup G), IsClosed (H : Set G) →
941 @ProCGroups.ProC.ProCGroupPredicate.holds ProC H _ _ _)
942 {X : Type u} (Y : Set X)
943 {FX : Type u} [Group FX] [TopologicalSpace FX] [IsTopologicalGroup FX]
944 {FY : Type u} [Group FY] [TopologicalSpace FY] [IsTopologicalGroup FY]
945 {ιX : X → FX} {ιY : Y → FY}
946 (hX : IsFreeProCGroupOnConvergingSet (ProC := ProC) X FX ιX)
947 (hY : IsFreeProCGroupOnConvergingSet (ProC := ProC) Y FY ιY) :
948 by
949 classical
950 exact
951 ∃ φ : FX →* FY,
952 Continuous φ ∧
953 (∀ x, φ (ιX x) = if hx : x ∈ Y then ιY ⟨x, hx⟩ else 1) ∧
954 Function.Surjective φ ∧
955 ∃ σ : FY →* FX,
956 Continuous σ ∧
957 φ.comp σ = MonoidHom.id FY ∧
959 (Set.range fun x : {x : X // x ∉ Y} => ιX x.1) φ.ker := by
960 classical
961 let α : X → FY := fun x => if hx : x ∈ Y then ιY ⟨x, hx⟩ else 1
962 have hαsub :
963 Set.range α ⊆ Set.range ιY ∪ ({1} : Set FY) := by
964 rintro z ⟨x, rfl⟩
965 by_cases hx : x ∈ Y
966 · left
967 exact ⟨⟨x, hx⟩, by simp only [hx, ↓reduceDIte, α]⟩
968 · right
969 simp only [hx, ↓reduceDIte, mem_singleton_iff, α]
970 have hαgen :
971 Generation.TopologicallyGenerates (G := FY) (Set.range α) := by
972 have hsub : Set.range ιY ⊆ Set.range α := by
973 rintro z ⟨y, rfl⟩
974 exact ⟨y.1, by simp only [y.2, ↓reduceDIte, Subtype.coe_eta, α]⟩
975 exact Generation.topologicallyGenerates_mono (G := FY) hY.generates_range hsub
976 have hαconv :
977 FamilyConvergesToOne (G := FY) α := by
978 intro U
979 have hsubset :
980 {x : X | α x ∉ (U : Set FY)} ⊆
981 (fun y : Y => (y : X)) '' {y : Y | ιY y ∉ (U : Set FY)} := by
982 intro x hx
983 by_cases hxy : x ∈ Y
984 · exact ⟨⟨x, hxy⟩, by simpa [α, hxy] using hx, rfl⟩
985 · exfalso
986 exact hx (by simp only [hxy, ↓reduceDIte, SetLike.mem_coe, one_mem, α])
987 exact (hY.convergesToOne U).image (fun y : Y => (y : X)) |>.subset hsubset
988 rcases hX.existsUnique_lift hY.isProC α hαconv hαgen with ⟨φ, hφ, hφuniq⟩
989 let K : Subgroup FX :=
990 (Subgroup.closure (Set.range fun y : Y => ιX y.1)).topologicalClosure
991 let βK : Y → K := fun y => ⟨ιX y.1, Subgroup.le_topologicalClosure _ <|
992 Subgroup.subset_closure ⟨y, rfl⟩⟩
993 have hKclosed : IsClosed ((K : Set FX)) := by
994 exact Subgroup.isClosed_topologicalClosure _
995 have hKproC :
996 @ProCGroups.ProC.ProCGroupPredicate.holds ProC K _ _ _ := by
997 exact hClosed hX.isProC K hKclosed
998 have hFXspace : InverseSystems.IsProfiniteSpace FX := hProfinite hX.isProC
999 have hFXprof : IsProfiniteGroup FX := by
1000 exact IsProfiniteGroup.of_isProfiniteSpace hFXspace
1001 have hβKgen :
1002 Generation.TopologicallyGenerates (G := K) (Set.range βK) := by
1003 let L : Subgroup K := Subgroup.closure (Set.range βK)
1004 have hclosedSubtype : IsClosedMap (K.subtype : K → FX) :=
1005 hKclosed.isClosedMap_subtype_val
1006 have hclosure :
1007 closure (((fun z : K => (z : FX)) '' ((L : Set K)))) =
1008 (fun z : K => (z : FX)) '' closure ((L : Set K)) :=
1009 hclosedSubtype.closure_image_eq_of_continuous continuous_subtype_val _
1010 have himg :
1011 ((fun z : K => (z : FX)) '' ((L : Set K))) =
1012 (((Subgroup.closure (Set.range fun y : Y => ιX y.1)) : Subgroup FX) : Set FX) := by
1013 have hβRange :
1014 ((fun z : K => (z : FX)) '' Set.range βK) =
1015 Set.range (fun y : Y => ιX y.1) := by
1016 ext z
1017 constructor
1018 · rintro ⟨x, hx, rfl⟩
1019 rcases hx with ⟨y, rfl⟩
1020 exact ⟨y, rfl⟩
1021 · rintro ⟨y, rfl⟩
1022 exact ⟨βK y, ⟨y, rfl⟩, rfl⟩
1023 have hmap :
1024 L.map K.subtype =
1025 Subgroup.closure (((fun z : K => (z : FX)) '' Set.range βK)) := by
1027 (K.subtype.map_closure (Set.range βK))
1028 simpa [hβRange] using
1029 congrArg (fun J : Subgroup FX => (J : Set FX)) hmap
1030 rw [Generation.topologicallyGenerates_iff_dense, dense_iff_closure_eq]
1031 ext z
1032 constructor
1033 · intro _hz
1034 simp only [mem_univ]
1035 · intro _hz
1036 have hz' : (z : FX) ∈ ((fun w : K => (w : FX)) '' closure ((L : Set K))) := by
1037 rw [← hclosure, himg]
1038 simp only [Subtype.coe_prop, K]
1039 rcases hz' with ⟨w, hw, hwz⟩
1040 simpa [L] using ((Subtype.ext hwz) ▸ hw)
1041 have hβKconv :
1042 FamilyConvergesToOne (G := K) βK := by
1043 intro U
1044 letI : CompactSpace FX := IsProfiniteGroup.compactSpace hFXprof
1045 letI : TotallyDisconnectedSpace FX := IsProfiniteGroup.totallyDisconnectedSpace hFXprof
1046 have hUopen : IsOpen (U : Set K) := openSubgroup_isOpen (G := K) U
1047 rcases isOpen_induced_iff.mp hUopen with ⟨W, hWopen, hWeq⟩
1048 have h1W : (1 : FX) ∈ W := by
1049 have h1U : (1 : K) ∈ (U : Set K) := U.one_mem
1050 have : (⟨1, K.one_mem⟩ : K) ∈ Subtype.val ⁻¹' W := by
1051 exact hWeq.symm ▸ h1U
1052 simpa using this
1054 (G := FX) hWopen h1W with
1055 ⟨V, hVW⟩
1056 have hbadFinite :
1057 {y : Y | ιX y.1 ∉ (V.toOpenSubgroup : Set FX)}.Finite := by
1058 let e : Y ↪ X := ⟨fun y => y.1, Subtype.val_injective⟩
1059 have hfinite : {x : X | ιX x ∉ (V.toOpenSubgroup : Set FX)}.Finite :=
1060 hX.convergesToOne V.toOpenSubgroup
1061 simpa [Set.preimage, e] using hfinite.preimage_embedding e
1062 have hsubset :
1063 {y : Y | βK y ∉ (U : Set K)} ⊆
1064 {y : Y | ιX y.1 ∉ (V.toOpenSubgroup : Set FX)} := by
1065 intro y hy hyV
1066 have hyW : ιX y.1 ∈ W := hVW hyV
1067 have hyPre : βK y ∈ Subtype.val ⁻¹' W := by
1068 simpa [βK] using hyW
1069 have hyU : βK y ∈ (U : Set K) := by
1070 exact hWeq ▸ hyPre
1071 exact hy hyU
1072 exact hbadFinite.subset hsubset
1073 rcases hY.existsUnique_lift hKproC βK hβKconv hβKgen with ⟨σK, hσK, _hσKuniq⟩
1074 let σ : FY →* FX := K.subtype.comp σK
1075 have hσcont : Continuous σ := continuous_subtype_val.comp hσK.1
1076 have hσbasis : ∀ y : Y, σ (ιY y) = ιX y.1 := by
1077 intro y
1078 change K.subtype (σK (ιY y)) = ιX y.1
1079 exact congrArg Subtype.val (hσK.2 y)
1080 have hsection : φ.comp σ = MonoidHom.id FY := by
1081 rcases hY.existsUnique_lift hY.isProC ιY hY.convergesToOne hY.generates_range with
1082 ⟨u, _hu, huniq⟩
1083 have huId : MonoidHom.id FY = u := by
1084 exact huniq _ ⟨continuous_id, fun y => rfl⟩
1085 have huSect : φ.comp σ = u := by
1086 refine huniq _ ⟨hφ.1.comp hσcont, ?_⟩
1087 intro y
1088 change φ (σ (ιY y)) = ιY y
1089 calc
1090 φ (σ (ιY y)) = φ (ιX y.1) := congrArg φ (hσbasis y)
1091 _ = ιY y := by
1092 simpa [α, y.2] using hφ.2 y.1
1093 exact huSect.trans huId.symm
1094 have hφsurj : Function.Surjective φ := by
1095 intro y
1096 refine ⟨σ y, ?_⟩
1097 have hsec := congrArg (fun f : FY →* FY => f y) hsection
1098 simpa [MonoidHom.comp_apply] using hsec
1099 have hFYspace : InverseSystems.IsProfiniteSpace FY := hProfinite hY.isProC
1100 letI : T2Space FY :=
1101 IsProfiniteGroup.t2Space (IsProfiniteGroup.of_isProfiniteSpace hFYspace)
1102 have hkerClosed : IsClosed ((φ.ker : Set FX)) := by
1103 change IsClosed (φ ⁻¹' ({1} : Set FY))
1104 simpa using isClosed_singleton.preimage hφ.1
1105 refine ⟨φ, hφ.1, hφ.2, hφsurj, σ, hσcont, hsection, ?_⟩
1106 refine ⟨by infer_instance, hkerClosed, ?_, ?_⟩
1107 · rintro z ⟨x, rfl⟩
1108 change φ (ιX x.1) = 1
1109 simpa [α, x.2] using hφ.2 x.1
1110 · intro M hMnorm hMclosed hMgen
1111 let ρ : FX →* FX := σ.comp φ
1112 let E : Subgroup FX := {
1113 carrier := {g : FX | ρ g * g⁻¹ ∈ M}
1114 one_mem' := by
1115 simp only [MonoidHom.coe_comp, Function.comp_apply, mem_setOf_eq, map_one, inv_one, mul_one, one_mem, ρ]
1116 mul_mem' := by
1117 intro a b ha hb
1118 have hbconj : a * (ρ b * b⁻¹) * a⁻¹ ∈ M := hMnorm.conj_mem (ρ b * b⁻¹) hb a
1119 have hprod : (ρ a * a⁻¹) * (a * (ρ b * b⁻¹) * a⁻¹) ∈ M :=
1120 M.mul_mem ha hbconj
1121 simpa [ρ, map_mul, mul_assoc] using hprod
1122 inv_mem' := by
1123 intro a ha
1124 have ha' : (ρ a * a⁻¹)⁻¹ ∈ M := M.inv_mem ha
1125 simpa [ρ, map_inv, mul_assoc] using
1126 hMnorm.conj_mem ((ρ a * a⁻¹)⁻¹) ha' a⁻¹ }
1127 have hEclosed : IsClosed ((E : Set FX)) := by
1128 let δ : FX → FX := fun g => ρ g * g⁻¹
1129 have hδ : Continuous δ := (hσcont.comp hφ.1).mul continuous_inv
1130 simpa [E, δ] using hMclosed.preimage hδ
1131 have hιXsub : Set.range ιX ⊆ (E : Set FX) := by
1132 rintro z ⟨x, rfl⟩
1133 by_cases hx : x ∈ Y
1134 · change ρ (ιX x) * (ιX x)⁻¹ ∈ M
1135 have hEq : ρ (ιX x) * (ιX x)⁻¹ = 1 := by
1136 change σ (φ (ιX x)) * (ιX x)⁻¹ = 1
1137 rw [hφ.2 x]
1138 simp only [hx, ↓reduceDIte, hσbasis, mul_inv_cancel, α]
1139 rw [hEq]
1140 exact M.one_mem
1141 · change ρ (ιX x) * (ιX x)⁻¹ ∈ M
1142 have hxM : ιX x ∈ M := hMgen ⟨⟨x, hx⟩, rfl⟩
1143 have hEq : ρ (ιX x) * (ιX x)⁻¹ = (ιX x)⁻¹ := by
1144 change σ (φ (ιX x)) * (ιX x)⁻¹ = (ιX x)⁻¹
1145 rw [hφ.2 x]
1146 simp only [hx, ↓reduceDIte, map_one, one_mul, α]
1147 rw [hEq]
1148 exact M.inv_mem hxM
1149 have hEtop : E = ⊤ := by
1150 have hclosureLe : Subgroup.closure (Set.range ιX) ≤ E := by
1151 show Subgroup.closure (Set.range ιX) ≤ E
1152 exact (Subgroup.closure_le (K := E)).2 hιXsub
1153 have htopLe : (⊤ : Subgroup FX) ≤ E := by
1154 rw [← hX.generates_range]
1155 exact Subgroup.topologicalClosure_minimal _ hclosureLe hEclosed
1156 exact top_unique htopLe
1157 intro x hx
1158 have hxE : x ∈ E := by
1159 simp only [hEtop, Subgroup.mem_top]
1160 change ρ x * x⁻¹ ∈ M at hxE
1161 have hρx : ρ x = 1 := by
1162 have hxφ : φ x = 1 := by
1163 simpa [MonoidHom.mem_ker] using hx
1164 simp only [MonoidHom.comp_apply, hxφ, map_one, ρ]
1165 have hxinv : x⁻¹ ∈ M := by
1166 simpa [hρx] using hxE
1167 simpa using M.inv_mem hxinv
1169/-- For an open subgroup of a free pro-`C` group on a basis converging to `1`, there is a cofinal
1170finite-subset subsystem whose stage indices agree with the original open subgroup, under the same
1171explicit profiniteness, closed-subgroup permanence, finite-quotient permanence, and injectivity
1172hypotheses used in the finite-subset approximation theorem. -/
1174 {X : Type u}
1175 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1176 {ι : X → F}
1177 (hProfinite :
1178 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
1179 @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
1180 InverseSystems.IsProfiniteSpace G)
1181 (hClosed :
1182 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1183 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
1184 (K : Subgroup G), IsClosed (K : Set G) →
1185 @ProCGroups.ProC.ProCGroupPredicate.holds ProC K _ _ _)
1186 (hFiniteQuot :
1187 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1188 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
1189 (U : OpenNormalSubgroup G),
1190 @ProCGroups.ProC.ProCGroupPredicate.holds ProC (G ⧸ (U : Subgroup G)) _ _ _)
1191 (hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1192 (H : Subgroup F) (hH : IsOpen ((H : Set F))) :
1194 ∃ basis : ∀ s : FiniteSubset X, ↥s.1 → S.toInverseSystem.X s,
1195 (∀ s : FiniteSubset X,
1197 ↥s.1 (S.toInverseSystem.X s) (basis s)) ∧
1198 (∀ {s t : FiniteSubset X} (hst : s ≤ t) (x : ↥t.1),
1199 S.toInverseSystem.map hst (basis t x) =
1200 by
1201 classical
1202 exact if hx : x.1 ∈ s.1 then basis s ⟨x.1, hx⟩ else 1) ∧
1203 ∃ _limitIso : F ≃ₜ* S.toInverseSystem.inverseLimit,
1204 ∃ cofinalSubsets : Set (FiniteSubset X),
1205 (∀ s : FiniteSubset X, ∃ t, t ∈ cofinalSubsets ∧ s ≤ t) ∧
1206 ∃ stageSubgroup :
1207 ∀ {t : FiniteSubset X},
1208 t ∈ cofinalSubsets → Subgroup (S.toInverseSystem.X t),
1209 (∀ {t : FiniteSubset X} (ht : t ∈ cofinalSubsets),
1210 IsOpen ((stageSubgroup ht : Set (S.toInverseSystem.X t)))) ∧
1211 (∀ {t : FiniteSubset X} (ht : t ∈ cofinalSubsets),
1212 (stageSubgroup ht).index = H.index) := by
1213 classical
1215 (ProC := ProC) (X := X) (F := F) (ι := ι)
1216 hProfinite hClosed hFiniteQuot hF with
1217 ⟨S, basis, hbasis, hmap, _hembed, hlimit⟩
1218 let hFspace : InverseSystems.IsProfiniteSpace F := hProfinite hF.isProC
1219 let hFprof : IsProfiniteGroup F :=
1220 IsProfiniteGroup.of_isProfiniteSpace hFspace
1221 letI : CompactSpace F := IsProfiniteGroup.compactSpace hFprof
1222 letI : T2Space F := IsProfiniteGroup.t2Space hFprof
1223 letI : TotallyDisconnectedSpace F := IsProfiniteGroup.totallyDisconnectedSpace hFprof
1224 let Hopen : OpenSubgroup F := ⟨H, hH⟩
1225 letI : Finite (F ⧸ H) := openSubgroup_finiteQuotient (G := F) Hopen
1226 letI : H.FiniteIndex := Subgroup.finiteIndex_of_finite_quotient (H := H)
1227 let U : OpenNormalSubgroup F :=
1228 { toSubgroup := H.normalCore
1229 isOpen' := by
1230 exact H.normalCore.isOpen_of_isClosed_of_finiteIndex
1231 (H.normalCore_isClosed (Subgroup.isClosed_of_isOpen H hH))
1232 isNormal' := by infer_instance }
1233 have hUleH : (U : Subgroup F) ≤ H := Subgroup.normalCore_le H
1234 let q : F →* F ⧸ (U : Subgroup F) := QuotientGroup.mk' (U : Subgroup F)
1235 letI : Finite (F ⧸ (U : Subgroup F)) := openNormalSubgroup_finiteQuotient (G := F) U
1236 letI : DiscreteTopology (F ⧸ (U : Subgroup F)) :=
1237 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := F) U)
1238 let Q := F ⧸ (U : Subgroup F)
1239 have hquotProC :
1240 @ProCGroups.ProC.ProCGroupPredicate.holds ProC Q _ _ _ := by
1241 exact hFiniteQuot hF.isProC U
1242 have hQspace : InverseSystems.IsProfiniteSpace Q := hProfinite hquotProC
1243 have hQprof : IsProfiniteGroup Q :=
1244 IsProfiniteGroup.of_isProfiniteSpace hQspace
1245 let Hbar : Subgroup Q := H.map q
1246 have hHbar_index : Hbar.index = H.index := by
1247 simpa [Hbar, q] using
1248 (Subgroup.index_map_eq (H := H) (f := q)
1249 (QuotientGroup.mk'_surjective (U : Subgroup F)) (by simpa [q] using hUleH))
1250 let HbarOpen : OpenSubgroup Q :=
1251 { toSubgroup := Hbar
1252 isOpen' := by
1253 exact isOpen_discrete (Hbar : Set Q) }
1254 have himg :
1255 Generation.GeneratesAndConvergesToOne (G := Q) (q '' Set.range ι) := by
1256 exact Generation.GeneratesAndConvergesToOne.image_of_continuousSurjective
1257 (G := F) hFprof q continuous_quotient_mk'
1258 (QuotientGroup.mk'_surjective (U : Subgroup F))
1259 ⟨hF.generates_range, hF.convergesToOne.range⟩
1260 have hnontriv :
1261 {x : X | ι x ∉ (U : Set F)}.Finite := by
1262 exact hF.convergesToOne U.toOpenSubgroup
1263 let s0 : FiniteSubset X := ⟨{x : X | ι x ∉ (U : Set F)}, hnontriv⟩
1264 let cofinalSubsets : Set (FiniteSubset X) := {t : FiniteSubset X | s0 ≤ t}
1265 have hcofinal :
1266 ∀ s : FiniteSubset X, ∃ t, t ∈ cofinalSubsets ∧ s ≤ t := by
1267 intro s
1268 refine ⟨⟨s.1 ∪ s0.1, s.2.union s0.2⟩, ?_, ?_⟩
1269 · intro x hx
1270 exact Or.inr hx
1271 · intro x hx
1272 exact Or.inl hx
1273 have stageQuotMap_exists :
1274 ∀ {t : FiniteSubset X} (ht : t ∈ cofinalSubsets),
1275 ∃ u : S.toInverseSystem.X t →* Q,
1276 Continuous u ∧ Function.Surjective u := by
1277 intro t ht
1278 let φt : ↥t.1 → Q := fun x => q (ι x.1)
1279 have hφtconv : FamilyConvergesToOne (G := Q) φt := by
1280 letI : Finite ↥t.1 := t.2.to_subtype
1281 exact FamilyConvergesToOne.of_finite_domain (G := Q) φt
1282 have hφtgen : Generation.TopologicallyGenerates (G := Q) (Set.range φt) := by
1283 have hgen' : Generation.TopologicallyGenerates (G := Q) (q '' Set.range ι) := by
1284 simpa [Set.range_comp] using himg.1
1285 have hsub :
1286 q '' Set.range ι ⊆ Set.range φt ∪ ({1} : Set Q) := by
1287 rintro z ⟨w, ⟨x, rfl⟩, rfl⟩
1288 by_cases hx : x ∈ t.1
1289 · left
1290 exact ⟨⟨x, hx⟩, rfl⟩
1291 · right
1292 have hx0 : x ∉ s0.1 := by
1293 intro hx0
1294 exact hx (ht hx0)
1295 have hxU : ι x ∈ (U : Set F) := by
1296 simp only [s0, Set.mem_setOf_eq, not_not] at hx0
1297 exact hx0
1298 have hq1 : q (ι x) = 1 := by
1299 simpa [q] using
1300 (QuotientGroup.eq_one_iff (N := (U : Subgroup F)) (ι x)).2 hxU
1301 simp only [hq1, mem_singleton_iff]
1302 have hgenUnion :
1303 Generation.TopologicallyGenerates (G := Q)
1304 (Set.range φt ∪ ({1} : Set Q)) := by
1305 exact Generation.topologicallyGenerates_mono (G := Q) hgen' hsub
1306 rw [Generation.topologicallyGenerates_union_one_iff] at hgenUnion
1307 exact hgenUnion
1308 rcases (hbasis t).existsUnique_lift hquotProC φt hφtconv hφtgen with ⟨u, hu, _⟩
1309 have hSspace : InverseSystems.IsProfiniteSpace (S.toInverseSystem.X t) := by
1310 exact hProfinite (hbasis t).isProC
1311 have hSprof : IsProfiniteGroup (S.toInverseSystem.X t) := by
1312 exact
1313 IsProfiniteGroup.of_isProfiniteSpace hSspace
1314 have husub : Set.range φt ⊆ (u.range : Set Q) := by
1315 rintro z ⟨x, rfl⟩
1316 exact ⟨basis t x, hu.2 x⟩
1317 have husurj : Function.Surjective u :=
1319 (G := S.toInverseSystem.X t) (H := Q) hSprof hQprof hφtgen hu.1 husub
1320 exact ⟨u, hu.1, husurj⟩
1321 let stageQuotMap :
1322 ∀ {t : FiniteSubset X}, t ∈ cofinalSubsets → S.toInverseSystem.X t →* Q :=
1323 fun {t} ht => Classical.choose (stageQuotMap_exists (t := t) ht)
1324 let stageSubgroup :
1325 ∀ {t : FiniteSubset X}, t ∈ cofinalSubsets → Subgroup (S.toInverseSystem.X t) :=
1326 fun {t} ht => Subgroup.comap (stageQuotMap ht) Hbar
1327 have hstageOpen :
1328 ∀ {t : FiniteSubset X} (ht : t ∈ cofinalSubsets),
1329 IsOpen ((stageSubgroup ht : Set (S.toInverseSystem.X t))) := by
1330 intro t ht
1331 change IsOpen
1332 ((stageQuotMap ht) ⁻¹' ((Hbar : Subgroup Q) : Set Q))
1333 simpa using
1334 HbarOpen.isOpen'.preimage (Classical.choose_spec (stageQuotMap_exists (t := t) ht)).1
1335 have hstageIndex :
1336 ∀ {t : FiniteSubset X} (ht : t ∈ cofinalSubsets),
1337 (stageSubgroup ht).index = H.index := by
1338 intro t ht
1339 have hsurj : Function.Surjective (stageQuotMap ht) :=
1340 (Classical.choose_spec (stageQuotMap_exists (t := t) ht)).2
1341 calc
1342 (stageSubgroup ht).index = Hbar.index := by
1343 simpa [stageSubgroup] using
1344 (Subgroup.index_comap_of_surjective
1345 (H := Hbar) (f := stageQuotMap ht) hsurj)
1346 _ = H.index := hHbar_index
1347 refine ⟨S, basis, hbasis, hmap, ?_⟩
1348 rcases hlimit with ⟨limitIso⟩
1349 exact ⟨limitIso, cofinalSubsets, hcofinal, stageSubgroup, hstageOpen, hstageIndex⟩
1351end InverseLimitsAndFiniteSubsets
1352end ProCGroups.FreeProC