Yamaguchi Lean 4 Library
ProCGroups/Completion/SameFiniteQuotients.lean
ProCGroups/Completion/SameFiniteQuotients/Source

ProCGroups/Completion/SameFiniteQuotients.lean

1import Mathlib.GroupTheory.Finiteness
2import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
3import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/Completion/SameFiniteQuotients.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Pro-C completion and finite quotient systems
16Organizes finite quotient systems, completion maps, finite-target factorization, and the universal property of pro-C completion.
17-/
19open scoped Topology
21namespace ProCGroups.Completion
23universe u
25/-- Two abstract groups have the same finite quotients when they have exactly the same finite
26surjective homomorphic images.
27-/
29 (G₁ : Type u) [Group G₁]
30 (G₂ : Type u) [Group G₂] : Prop :=
31 ∀ (Q : Type u) [Group Q] [Finite Q],
32 (∃ φ : G₁ →* Q, Function.Surjective φ) ↔
33 (∃ ψ : G₂ →* Q, Function.Surjective ψ)
35/-- Topological finite quotient predicate using continuous maps to finite discrete groups. -/
37 (G₁ : Type u) [Group G₁] [TopologicalSpace G₁] [IsTopologicalGroup G₁]
38 (G₂ : Type u) [Group G₂] [TopologicalSpace G₂] [IsTopologicalGroup G₂] : Prop :=
39 ∀ (Q : Type u) [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
40 [Finite Q] [DiscreteTopology Q],
41 (∃ φ : G₁ →ₜ* Q, Function.Surjective φ) ↔
42 (∃ ψ : G₂ →ₜ* Q, Function.Surjective ψ)
44/-- Auxiliary strong-completeness input: every surjective homomorphism to a finite discrete group
45is continuous. This isolates the hypothesis needed to identify abstract finite quotients with
46continuous finite quotients. -/
48 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop where
49 continuous_of_surjective :
50 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
51 [Finite Q] [DiscreteTopology Q],
52 ∀ (φ : G →* Q), Function.Surjective φ → Continuous φ
54/-- A bundled profinite completion model for an abstract group, keeping only the finite-quotient
55universal property.
57Note: finite quotients are taken with their discrete topology, which is the standard profinite
58completion interface.
59-/
61 (G : Type u) [Group G] where
62 carrier : Type u
63 instGroup : Group carrier
64 instTopologicalSpace : TopologicalSpace carrier
65 instIsTopologicalGroup : IsTopologicalGroup carrier
66 instCompactSpace : CompactSpace carrier
67 instT2Space : T2Space carrier
68 instTotallyDisconnectedSpace : TotallyDisconnectedSpace carrier
69 map : G →* carrier
70 denseRange_map : DenseRange map
71 existsUnique_lift_finite :
72 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
73 [Finite Q] [DiscreteTopology Q],
74 ∀ (φ : G →* Q), Function.Surjective φ →
75 ∃! φbar : carrier →* Q, Continuous φbar ∧ φbar.comp map = φ
77attribute [instance] AbstractProfiniteCompletionData.instGroup
78attribute [instance] AbstractProfiniteCompletionData.instTopologicalSpace
79attribute [instance] AbstractProfiniteCompletionData.instIsTopologicalGroup
80attribute [instance] AbstractProfiniteCompletionData.instCompactSpace
81attribute [instance] AbstractProfiniteCompletionData.instT2Space
82attribute [instance] AbstractProfiniteCompletionData.instTotallyDisconnectedSpace
84/-- The dense image of a finite abstract generating set topologically generates the completion. -/
86 {G : Type u} [Group G] [Group.FG G]
88 FiniteGeneration.TopologicallyFinitelyGenerated Ghat.carrier := by
89 classical
90 rcases (Group.fg_iff' (G := G)).1 (inferInstance : Group.FG G) with
91 ⟨_n, s, _hscard, hsclosure⟩
92 let t : Finset Ghat.carrier := s.image Ghat.map
93 have htclosure :
94 Subgroup.closure (↑t : Set Ghat.carrier) = Ghat.map.range := by
95 calc
96 Subgroup.closure (↑t : Set Ghat.carrier)
97 = Subgroup.closure (Ghat.map '' (↑s : Set G)) := by
98 ext x
99 simp only [Finset.coe_image, t]
100 _ = (Subgroup.closure (↑s : Set G)).map Ghat.map := by
101 symm
102 simpa using (MonoidHom.map_closure Ghat.map (↑s : Set G))
103 _ = (⊤ : Subgroup G).map Ghat.map := by
104 simp only [hsclosure]
105 _ = Ghat.map.range := by
106 simp only [MonoidHom.range_eq_map]
107 have hdense :
108 Dense (((Subgroup.closure (↑t : Set Ghat.carrier)) : Subgroup Ghat.carrier) :
109 Set Ghat.carrier) := by
110 rw [htclosure, dense_iff_closure_eq]
111 simpa using Ghat.denseRange_map.closure_range
112 refine ⟨t, ?_⟩
113 exact
114 (Generation.topologicallyGenerates_iff_dense
115 (G := Ghat.carrier) (X := (↑t : Set Ghat.carrier))).2 hdense
117/-- A finite quotient of `G₂` yields, via the common finite quotient hypothesis and the universal
118property of `G₁hat`, a surjective continuous homomorphism from `G₁hat`. -/
120 {G₁ : Type u} [Group G₁]
121 {G₂ : Type u} [Group G₂]
122 (hquot : HasSameFiniteQuotients G₁ G₂)
125 {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
126 [Finite Q] [DiscreteTopology Q]
127 (ψ : G₂hat.carrier →* Q) (hψ : Continuous ψ) (hψsurj : Function.Surjective ψ) :
128 ∃ φ : ContinuousMonoidHom G₁hat.carrier Q, Function.Surjective φ := by
129 have hcompSurj : Function.Surjective (ψ.comp G₂hat.map) := by
130 have hDense : Dense (Set.range G₂hat.map) := by
131 simpa [DenseRange] using G₂hat.denseRange_map
132 rw [dense_iff_inter_open] at hDense
133 intro q
134 rcases hψsurj q with ⟨x, rfl⟩
135 let V : Set G₂hat.carrier := ψ ⁻¹' ({ψ x} : Set Q)
136 have hVopen : IsOpen V := by
137 have hsingle : IsOpen ({ψ x} : Set Q) := isOpen_discrete _
138 simpa [V] using hsingle.preimage hψ
139 have hVne : V.Nonempty := ⟨x, by simp only [Set.mem_preimage, Set.mem_singleton_iff, V]⟩
140 rcases hDense V hVopen hVne with ⟨y, hyV, hyRange⟩
141 let g : G₂ := Classical.choose hyRange
142 have hg : G₂hat.map g = y := Classical.choose_spec hyRange
143 refine ⟨g, ?_⟩
144 have hyEq : ψ y = ψ x := by
145 simpa [V] using hyV
146 simpa [MonoidHom.comp_apply, hg] using hyEq
147 rcases (hquot Q).2 ⟨ψ.comp G₂hat.map, hcompSurj⟩ with ⟨φ₀, hφ₀surj⟩
148 rcases G₁hat.existsUnique_lift_finite φ₀ hφ₀surj with ⟨φbar, hφbar, _huniq⟩
149 refine ⟨{ toMonoidHom := φbar, continuous_toFun := hφbar.1 }, ?_⟩
150 intro q
151 rcases hφ₀surj q with ⟨g, rfl⟩
152 refine ⟨G₁hat.map g, ?_⟩
153 have hfac := congrArg (fun f : G₁ →* Q => f g) hφbar.2
154 simpa [MonoidHom.comp_apply] using hfac
156/-- The common finite quotient hypothesis yields a surjective continuous homomorphism between the
157associated profinite completions. -/
159 {G₁ : Type u} [Group G₁]
160 {G₂ : Type u} [Group G₂]
161 [Group.FG G₁]
162 (hquot : HasSameFiniteQuotients G₁ G₂)
165 ∃ φ : ContinuousMonoidHom G₁hat.carrier G₂hat.carrier, Function.Surjective φ := by
166 classical
167 let H₁ := G₁hat.carrier
168 let H₂ := G₂hat.carrier
169 let C := FiniteGroupClass.allFinite
170 have hH₁fg : FiniteGeneration.TopologicallyFinitelyGenerated H₁ :=
172 have hH₂prof : IsProfiniteGroup H₂ := by
173 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
174 have hH₂proC : ProC.IsProCGroup C H₂ := by
175 exact (ProC.isProC_allFinite_iff_isProfiniteGroup (G := H₂)).2 hH₂prof
176 let S₂ : InverseSystems.InverseSystem
177 (I := OrderDual (ProC.OpenNormalSubgroupInClass C H₂)) :=
178 ProC.openNormalSubgroupInClassSystem C H₂
179 let SurjHom (U : OrderDual (ProC.OpenNormalSubgroupInClass C H₂)) :=
180 { φ : ContinuousMonoidHom H₁ (S₂.X U) // Function.Surjective φ }
181 letI : Nonempty (ProC.OpenNormalSubgroupInClass C H₂) :=
182 ProC.IsProCGroup.openNormalSubgroupInClass_nonempty hH₂proC
183 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C H₂),
184 Group (S₂.X U) := fun U => by
185 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
186 infer_instance
187 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C H₂),
188 IsTopologicalGroup (S₂.X U) := fun U => by
189 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
190 infer_instance
191 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C H₂),
192 Finite (S₂.X U) := fun U => by
193 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
194 exact (OrderDual.ofDual U).2
195 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C H₂),
196 DiscreteTopology (S₂.X U) := fun U => by
197 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
198 exact QuotientGroup.discreteTopology
200 ((OrderDual.ofDual U).1 : OpenNormalSubgroup H₂))
201 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C H₂),
202 Finite (ContinuousMonoidHom H₁ (S₂.X U)) := fun U => by
203 exact
204 FiniteGeneration.finite_continuousMonoidHom_to_finite_of_topologicallyFinitelyGenerated
205 (G := H₁) (R := S₂.X U) hH₁fg
206 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C H₂),
207 TopologicalSpace (SurjHom U) := fun _ => ⊥
208 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C H₂),
209 DiscreteTopology (SurjHom U) := fun _ => ⟨rfl⟩
210 let X₂ : InverseSystems.InverseSystem
211 (I := OrderDual (ProC.OpenNormalSubgroupInClass C H₂)) :=
212 { X := SurjHom
213 topologicalSpace := fun _ => ⊥
214 map := fun {U V} hUV φ => by
215 have hUV' : ((OrderDual.ofDual V).1 : Subgroup H₂) ≤ (OrderDual.ofDual U).1 := hUV
216 let qUV : ContinuousMonoidHom (S₂.X V) (S₂.X U) :=
217 { toMonoidHom := by
218 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
219 exact ProC.OpenNormalSubgroupInClass.map
220 (C := C) (G := H₂)
221 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV'
222 continuous_toFun := continuous_of_discreteTopology }
223 refine ⟨qUV.comp φ.1, ?_⟩
224 intro x
225 rcases (ProC.OpenNormalSubgroupInClass.map_surjective
226 (C := C) (G := H₂)
227 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV') x with ⟨y, hy⟩
228 rcases φ.2 y with ⟨z, hz⟩
229 refine ⟨z, ?_⟩
230 calc
231 (qUV.comp φ.1) z = qUV (φ.1 z) := rfl
232 _ = qUV y := by rw [hz]
233 _ = x := hy
234 continuous_map := by
235 intro U V hUV
236 exact continuous_of_discreteTopology
237 map_id := by
238 intro U
239 funext φ
240 apply Subtype.ext
241 apply ContinuousMonoidHom.ext
242 intro x
243 change ProC.OpenNormalSubgroupInClass.map
244 (C := C) (G := H₂)
245 (U := OrderDual.ofDual U) (V := OrderDual.ofDual U) (le_rfl)
246 (φ.1 x) = φ.1 x
247 exact congrFun
248 (congrArg DFunLike.coe
249 (ProC.OpenNormalSubgroupInClass.map_id
250 (C := C) (G := H₂) (U := OrderDual.ofDual U)))
251 (φ.1 x)
252 map_comp := by
253 intro U V W hUV hVW
254 have hUV' : ((OrderDual.ofDual V).1 : Subgroup H₂) ≤ (OrderDual.ofDual U).1 := hUV
255 have hVW' : ((OrderDual.ofDual W).1 : Subgroup H₂) ≤ (OrderDual.ofDual V).1 := hVW
256 funext φ
257 apply Subtype.ext
258 apply ContinuousMonoidHom.ext
259 intro x
260 change ProC.OpenNormalSubgroupInClass.map
261 (C := C) (G := H₂)
262 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV'
263 (ProC.OpenNormalSubgroupInClass.map
264 (C := C) (G := H₂)
265 (U := OrderDual.ofDual V) (V := OrderDual.ofDual W) hVW' (φ.1 x)) =
266 ProC.OpenNormalSubgroupInClass.map
267 (C := C) (G := H₂)
268 (U := OrderDual.ofDual U) (V := OrderDual.ofDual W) (hVW'.trans hUV')
269 (φ.1 x)
270 exact
271 congrArg
272 (fun f : H₂ ⧸ (((OrderDual.ofDual W).1 : OpenNormalSubgroup H₂) : Subgroup H₂) →*
273 H₂ ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup H₂) : Subgroup H₂) =>
274 f (φ.1 x))
275 (ProC.OpenNormalSubgroupInClass.map_comp
276 (C := C) (G := H₂)
277 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
278 hUV' hVW') }
279 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C H₂),
280 Nonempty (X₂.X U) := fun U => by
281 dsimp [X₂]
282 let qU : H₂ →* S₂.X U :=
283 ProC.openNormalSubgroupInClassProj
284 (C := C) (G := H₂) U
285 have hqUcont : Continuous qU := by
286 dsimp [qU, S₂, ProC.openNormalSubgroupInClassSystem]
287 simpa using
288 (continuous_quotient_mk' : Continuous
289 (QuotientGroup.mk'
290 (((OrderDual.ofDual U).1 : OpenNormalSubgroup H₂) : Subgroup H₂)))
291 have hqUsurj : Function.Surjective qU :=
292 ProC.openNormalSubgroupInClassProj_surjective
293 (C := C) (G := H₂) U
295 (G₁ := G₁) (G₂ := G₂) hquot G₁hat G₂hat qU hqUcont hqUsurj with
296 ⟨φ, hφsurj⟩
297 exact ⟨⟨φ, hφsurj⟩⟩
298 have hdir₂ :
299 Directed
300 (α := OrderDual (ProC.OpenNormalSubgroupInClass C H₂))
301 (· ≤ ·) (fun U => U) := by
302 intro U V
303 let W : ProC.OpenNormalSubgroupInClass C H₂ :=
304 ⟨(OrderDual.ofDual U).1 ⊓ (OrderDual.ofDual V).1,
305 FiniteGroupClass.Formation.quotient_inf_mem
306 (C := C) (G := H₂)
307 FiniteGroupClass.allFinite_formation
308 (OrderDual.ofDual U).1 (OrderDual.ofDual V).1
309 (OrderDual.ofDual U).2 (OrderDual.ofDual V).2⟩
310 refine ⟨OrderDual.toDual W, ?_, ?_⟩
311 · change ((W.1 : Subgroup H₂) ≤ ((OrderDual.ofDual U).1 : Subgroup H₂))
312 exact inf_le_left
313 · change ((W.1 : Subgroup H₂) ≤ ((OrderDual.ofDual V).1 : Subgroup H₂))
314 exact inf_le_right
315 rcases InverseSystems.InverseSystem.nonempty_inverseLimit_of_finite (S := X₂) hdir₂ with ⟨x₂⟩
316 let ψ₂ : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C H₂),
317 H₁ → S₂.X U := fun U => (x₂.1 U).1
318 have hψ₂cont : ∀ U, Continuous (ψ₂ U) := by
319 intro U
320 exact ((x₂.1 U).1).continuous_toFun
321 have hψ₂compat : S₂.CompatibleMaps ψ₂ := by
322 intro U V hUV
323 funext x
324 have hEq : X₂.map hUV (x₂.1 V) = x₂.1 U := x₂.2 U V hUV
325 have hEq' : (X₂.map hUV (x₂.1 V)).1 = (x₂.1 U).1 := congrArg Subtype.val hEq
326 exact congrArg (fun φ : ContinuousMonoidHom H₁ (S₂.X U) => φ x) hEq'
327 have hψ₂surj : ∀ U, Function.Surjective (ψ₂ U) := by
328 intro U
329 exact (x₂.1 U).2
330 let fToInv : ContinuousMonoidHom H₁ S₂.inverseLimit :=
331 { toMonoidHom :=
332 { toFun := S₂.inverseLimitLift ψ₂ hψ₂compat
333 map_one' := by
334 apply S₂.ext
335 intro U
336 calc
337 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat 1) = ψ₂ U 1 := by
338 simpa [Function.comp] using congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) (1 : H₁)
339 _ = 1 := by simp only [map_one, ψ₂]
340 map_mul' := by
341 intro x y
342 apply S₂.ext
343 intro U
344 calc
345 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat (x * y)) = ψ₂ U (x * y) := by
346 simpa [Function.comp] using
347 congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) (x * y)
348 _ = ψ₂ U x * ψ₂ U y := by simp only [map_mul, ψ₂]
349 _ = S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat x) *
350 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat y) := by
351 have hπx :
352 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat x) = ψ₂ U x := by
353 simpa [Function.comp] using
354 congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) x
355 have hπy :
356 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat y) = ψ₂ U y := by
357 simpa [Function.comp] using
358 congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) y
359 rw [← hπx, ← hπy] }
360 continuous_toFun := S₂.continuous_inverseLimitLift ψ₂ hψ₂cont hψ₂compat }
361 have hfToInv_surj : Function.Surjective (S₂.inverseLimitLift ψ₂ hψ₂compat) :=
362 S₂.surjective_inverseLimitLift ψ₂ hψ₂cont hψ₂compat hψ₂surj hdir₂
363 let e₂ : H₂ ≃ₜ* S₂.inverseLimit :=
364 ProC.IsProCGroup.openNormalSubgroupInClassMulEquivInverseLimit
365 (C := C) (G := H₂)
366 FiniteGroupClass.allFinite_formation hH₂proC
367 let e₂symmHom : ContinuousMonoidHom S₂.inverseLimit H₂ :=
368 { toMonoidHom := e₂.symm.toMonoidHom
369 continuous_toFun := e₂.symm.continuous_toFun }
370 refine ⟨e₂symmHom.comp fToInv, ?_⟩
371 intro y
372 rcases hfToInv_surj (e₂ y) with ⟨x, hx⟩
373 refine ⟨x, ?_⟩
374 change e₂.symm (S₂.inverseLimitLift ψ₂ hψ₂compat x) = y
375 rw [hx]
376 exact e₂.symm_apply_apply y
378/-- Finitely generated abstract groups with the same finite quotients have isomorphic profinite
379completion models. -/
381 {G₁ : Type u} [Group G₁]
382 {G₂ : Type u} [Group G₂]
383 [Group.FG G₁] [Group.FG G₂]
384 (hquot : HasSameFiniteQuotients G₁ G₂)
387 Nonempty (G₁hat.carrier ≃ₜ* G₂hat.carrier) := by
388 classical
389 let H₁ := G₁hat.carrier
390 let H₂ := G₂hat.carrier
391 have hH₁fg : FiniteGeneration.TopologicallyFinitelyGenerated H₁ :=
394 (G₁ := G₁) (G₂ := G₂) hquot G₁hat G₂hat with ⟨φ, hφsurj⟩
396 (G₁ := G₂) (G₂ := G₁) (by
397 intro Q _ _
398 exact (hquot Q).symm) G₂hat G₁hat with
399 ⟨ψ, hψsurj⟩
400 let ψφ : ContinuousMonoidHom H₁ H₁ := ψ.comp φ
401 have hψφsurj : Function.Surjective ψφ := by
402 simpa [ψφ] using hψsurj.comp hφsurj
403 rcases (FiniteGeneration.surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated
404 (G := H₁) hH₁fg ψφ hψφsurj) with ⟨e, he⟩
405 have hψφinj : Function.Injective ψφ := by
406 intro x y hxy
407 apply e.injective
408 calc
409 e x = ψφ x := he x
410 _ = ψφ y := hxy
411 _ = e y := (he y).symm
412 have hφinj : Function.Injective φ := by
413 intro x y hxy
414 apply hψφinj
415 change ψ (φ x) = ψ (φ y)
416 exact congrArg ψ hxy
417 exact ⟨ContinuousMulEquiv.ofBijectiveCompactToT2
418 φ.toMonoidHom φ.continuous_toFun ⟨hφinj, hφsurj⟩⟩
420/-- The continuous finite quotient hypothesis yields a surjective continuous homomorphism between
421topologically finitely generated profinite groups. -/
423 {G₁ : Type u} [Group G₁] [TopologicalSpace G₁] [IsTopologicalGroup G₁]
424 {G₂ : Type u} [Group G₂] [TopologicalSpace G₂] [IsTopologicalGroup G₂]
425 [CompactSpace G₁]
426 [CompactSpace G₂] [T2Space G₂] [TotallyDisconnectedSpace G₂]
427 (hG₁fg : FiniteGeneration.TopologicallyFinitelyGenerated G₁)
429 ∃ φ : ContinuousMonoidHom G₁ G₂, Function.Surjective φ := by
430 classical
431 let C := FiniteGroupClass.allFinite
432 have hG₂prof : IsProfiniteGroup G₂ := by
433 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
434 have hG₂proC : ProC.IsProCGroup C G₂ := by
435 exact (ProC.isProC_allFinite_iff_isProfiniteGroup (G := G₂)).2 hG₂prof
436 let S₂ : InverseSystems.InverseSystem
437 (I := OrderDual (ProC.OpenNormalSubgroupInClass C G₂)) :=
438 ProC.openNormalSubgroupInClassSystem C G₂
439 let SurjHom (U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂)) :=
440 { φ : ContinuousMonoidHom G₁ (S₂.X U) // Function.Surjective φ }
441 letI : Nonempty (ProC.OpenNormalSubgroupInClass C G₂) :=
442 ProC.IsProCGroup.openNormalSubgroupInClass_nonempty hG₂proC
443 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),
444 Group (S₂.X U) := fun U => by
445 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
446 infer_instance
447 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),
448 IsTopologicalGroup (S₂.X U) := fun U => by
449 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
450 infer_instance
451 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),
452 Finite (S₂.X U) := fun U => by
453 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
454 exact (OrderDual.ofDual U).2
455 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),
456 DiscreteTopology (S₂.X U) := fun U => by
457 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
458 exact QuotientGroup.discreteTopology
460 ((OrderDual.ofDual U).1 : OpenNormalSubgroup G₂))
461 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),
462 Finite (ContinuousMonoidHom G₁ (S₂.X U)) := fun U => by
463 exact
464 FiniteGeneration.finite_continuousMonoidHom_to_finite_of_topologicallyFinitelyGenerated
465 (G := G₁) (R := S₂.X U) hG₁fg
466 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),
467 TopologicalSpace (SurjHom U) := fun _ => ⊥
468 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),
469 DiscreteTopology (SurjHom U) := fun _ => ⟨rfl⟩
470 let X₂ : InverseSystems.InverseSystem
471 (I := OrderDual (ProC.OpenNormalSubgroupInClass C G₂)) :=
472 { X := SurjHom
473 topologicalSpace := fun _ => ⊥
474 map := fun {U V} hUV φ => by
475 have hUV' : ((OrderDual.ofDual V).1 : Subgroup G₂) ≤ (OrderDual.ofDual U).1 := hUV
476 let qUV : ContinuousMonoidHom (S₂.X V) (S₂.X U) :=
477 { toMonoidHom := by
478 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
479 exact ProC.OpenNormalSubgroupInClass.map
480 (C := C) (G := G₂)
481 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV'
482 continuous_toFun := continuous_of_discreteTopology }
483 refine ⟨qUV.comp φ.1, ?_⟩
484 intro x
485 rcases (ProC.OpenNormalSubgroupInClass.map_surjective
486 (C := C) (G := G₂)
487 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV') x with ⟨y, hy⟩
488 rcases φ.2 y with ⟨z, hz⟩
489 refine ⟨z, ?_⟩
490 calc
491 (qUV.comp φ.1) z = qUV (φ.1 z) := rfl
492 _ = qUV y := by rw [hz]
493 _ = x := hy
494 continuous_map := by
495 intro U V hUV
496 exact continuous_of_discreteTopology
497 map_id := by
498 intro U
499 funext φ
500 apply Subtype.ext
501 apply ContinuousMonoidHom.ext
502 intro x
503 change ProC.OpenNormalSubgroupInClass.map
504 (C := C) (G := G₂)
505 (U := OrderDual.ofDual U) (V := OrderDual.ofDual U) (le_rfl)
506 (φ.1 x) = φ.1 x
507 exact congrFun
508 (congrArg DFunLike.coe
509 (ProC.OpenNormalSubgroupInClass.map_id
510 (C := C) (G := G₂) (U := OrderDual.ofDual U)))
511 (φ.1 x)
512 map_comp := by
513 intro U V W hUV hVW
514 have hUV' : ((OrderDual.ofDual V).1 : Subgroup G₂) ≤ (OrderDual.ofDual U).1 := hUV
515 have hVW' : ((OrderDual.ofDual W).1 : Subgroup G₂) ≤ (OrderDual.ofDual V).1 := hVW
516 funext φ
517 apply Subtype.ext
518 apply ContinuousMonoidHom.ext
519 intro x
520 change ProC.OpenNormalSubgroupInClass.map
521 (C := C) (G := G₂)
522 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV'
523 (ProC.OpenNormalSubgroupInClass.map
524 (C := C) (G := G₂)
525 (U := OrderDual.ofDual V) (V := OrderDual.ofDual W) hVW' (φ.1 x)) =
526 ProC.OpenNormalSubgroupInClass.map
527 (C := C) (G := G₂)
528 (U := OrderDual.ofDual U) (V := OrderDual.ofDual W) (hVW'.trans hUV')
529 (φ.1 x)
530 exact
531 congrArg
532 (fun f : G₂ ⧸ (((OrderDual.ofDual W).1 : OpenNormalSubgroup G₂) : Subgroup G₂) →*
533 G₂ ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G₂) : Subgroup G₂) =>
534 f (φ.1 x))
535 (ProC.OpenNormalSubgroupInClass.map_comp
536 (C := C) (G := G₂)
537 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
538 hUV' hVW') }
539 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),
540 Nonempty (X₂.X U) := fun U => by
541 dsimp [X₂]
542 let qU : G₂ →ₜ* S₂.X U :=
543 { toMonoidHom := ProC.openNormalSubgroupInClassProj
544 (C := C) (G := G₂) U
545 continuous_toFun := by
546 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]
547 simpa using
548 (continuous_quotient_mk' : Continuous
549 (QuotientGroup.mk'
550 (((OrderDual.ofDual U).1 : OpenNormalSubgroup G₂) : Subgroup G₂))) }
551 have hqUsurj : Function.Surjective qU :=
552 ProC.openNormalSubgroupInClassProj_surjective
553 (C := C) (G := G₂) U
554 rcases (hquot (S₂.X U)).2 ⟨qU, hqUsurj⟩ with ⟨φ, hφsurj⟩
555 exact ⟨⟨φ, hφsurj⟩⟩
556 have hdir₂ :
557 Directed
558 (α := OrderDual (ProC.OpenNormalSubgroupInClass C G₂))
559 (· ≤ ·) (fun U => U) := by
560 intro U V
561 let W : ProC.OpenNormalSubgroupInClass C G₂ :=
562 ⟨(OrderDual.ofDual U).1 ⊓ (OrderDual.ofDual V).1,
563 FiniteGroupClass.Formation.quotient_inf_mem
564 (C := C) (G := G₂)
565 FiniteGroupClass.allFinite_formation
566 (OrderDual.ofDual U).1 (OrderDual.ofDual V).1
567 (OrderDual.ofDual U).2 (OrderDual.ofDual V).2⟩
568 refine ⟨OrderDual.toDual W, ?_, ?_⟩
569 · change ((W.1 : Subgroup G₂) ≤ ((OrderDual.ofDual U).1 : Subgroup G₂))
570 exact inf_le_left
571 · change ((W.1 : Subgroup G₂) ≤ ((OrderDual.ofDual V).1 : Subgroup G₂))
572 exact inf_le_right
573 rcases InverseSystems.InverseSystem.nonempty_inverseLimit_of_finite (S := X₂) hdir₂ with ⟨x₂⟩
574 let ψ₂ : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),
575 G₁ → S₂.X U := fun U => (x₂.1 U).1
576 have hψ₂cont : ∀ U, Continuous (ψ₂ U) := by
577 intro U
578 exact ((x₂.1 U).1).continuous_toFun
579 have hψ₂compat : S₂.CompatibleMaps ψ₂ := by
580 intro U V hUV
581 funext x
582 have hEq : X₂.map hUV (x₂.1 V) = x₂.1 U := x₂.2 U V hUV
583 have hEq' : (X₂.map hUV (x₂.1 V)).1 = (x₂.1 U).1 := congrArg Subtype.val hEq
584 exact congrArg (fun φ : ContinuousMonoidHom G₁ (S₂.X U) => φ x) hEq'
585 have hψ₂surj : ∀ U, Function.Surjective (ψ₂ U) := by
586 intro U
587 exact (x₂.1 U).2
588 let fToInv : ContinuousMonoidHom G₁ S₂.inverseLimit :=
589 { toMonoidHom :=
590 { toFun := S₂.inverseLimitLift ψ₂ hψ₂compat
591 map_one' := by
592 apply S₂.ext
593 intro U
594 calc
595 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat 1) = ψ₂ U 1 := by
596 simpa [Function.comp] using congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) (1 : G₁)
597 _ = 1 := by simp only [map_one, ψ₂]
598 map_mul' := by
599 intro x y
600 apply S₂.ext
601 intro U
602 calc
603 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat (x * y)) = ψ₂ U (x * y) := by
604 simpa [Function.comp] using
605 congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) (x * y)
606 _ = ψ₂ U x * ψ₂ U y := by simp only [map_mul, ψ₂]
607 _ = S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat x) *
608 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat y) := by
609 have hπx :
610 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat x) = ψ₂ U x := by
611 simpa [Function.comp] using
612 congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) x
613 have hπy :
614 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat y) = ψ₂ U y := by
615 simpa [Function.comp] using
616 congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) y
617 rw [← hπx, ← hπy] }
618 continuous_toFun := S₂.continuous_inverseLimitLift ψ₂ hψ₂cont hψ₂compat }
619 have hfToInv_surj : Function.Surjective (S₂.inverseLimitLift ψ₂ hψ₂compat) :=
620 S₂.surjective_inverseLimitLift ψ₂ hψ₂cont hψ₂compat hψ₂surj hdir₂
621 let e₂ : G₂ ≃ₜ* S₂.inverseLimit :=
622 ProC.IsProCGroup.openNormalSubgroupInClassMulEquivInverseLimit
623 (C := C) (G := G₂)
624 FiniteGroupClass.allFinite_formation hG₂proC
625 let e₂symmHom : ContinuousMonoidHom S₂.inverseLimit G₂ :=
626 { toMonoidHom := e₂.symm.toMonoidHom
627 continuous_toFun := e₂.symm.continuous_toFun }
628 refine ⟨e₂symmHom.comp fToInv, ?_⟩
629 intro y
630 rcases hfToInv_surj (e₂ y) with ⟨x, hx⟩
631 refine ⟨x, ?_⟩
632 change e₂.symm (S₂.inverseLimitLift ψ₂ hψ₂compat x) = y
633 rw [hx]
634 exact e₂.symm_apply_apply y
636/-- Topologically finitely generated profinite groups are determined by their continuous finite
637discrete quotients. -/
639 {G₁ : Type u} [Group G₁] [TopologicalSpace G₁] [IsTopologicalGroup G₁]
640 {G₂ : Type u} [Group G₂] [TopologicalSpace G₂] [IsTopologicalGroup G₂]
641 [CompactSpace G₁] [T2Space G₁] [TotallyDisconnectedSpace G₁]
642 [CompactSpace G₂] [T2Space G₂] [TotallyDisconnectedSpace G₂]
643 (hfg₁ : FiniteGeneration.TopologicallyFinitelyGenerated G₁)
644 (hfg₂ : FiniteGeneration.TopologicallyFinitelyGenerated G₂)
646 Nonempty (G₁ ≃ₜ* G₂) := by
647 classical
649 (G₁ := G₁) (G₂ := G₂) hfg₁ hquot with ⟨φ, hφsurj⟩
650 have hquot_symm : HasSameContinuousFiniteDiscreteQuotients G₂ G₁ := by
651 intro Q _ _ _ _ _
652 exact (hquot Q).symm
654 (G₁ := G₂) (G₂ := G₁) hfg₂ hquot_symm with ⟨ψ, hψsurj⟩
655 let ψφ : ContinuousMonoidHom G₁ G₁ := ψ.comp φ
656 have hψφsurj : Function.Surjective ψφ := by
657 simpa [ψφ] using hψsurj.comp hφsurj
658 rcases (FiniteGeneration.surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated
659 (G := G₁) hfg₁ ψφ hψφsurj) with ⟨e, he⟩
660 have hψφinj : Function.Injective ψφ := by
661 intro x y hxy
662 apply e.injective
663 calc
664 e x = ψφ x := he x
665 _ = ψφ y := hxy
666 _ = e y := (he y).symm
667 have hφinj : Function.Injective φ := by
668 intro x y hxy
669 apply hψφinj
670 change ψ (φ x) = ψ (φ y)
671 exact congrArg ψ hxy
672 exact ⟨ContinuousMulEquiv.ofBijectiveCompactToT2
673 φ.toMonoidHom φ.continuous_toFun ⟨hφinj, hφsurj⟩⟩
675/-- Topologically finitely generated profinite groups are determined by abstract finite
676quotients, provided strong completeness identifies abstract finite quotients with continuous
677finite discrete quotients. -/
679 {G₁ : Type u} [Group G₁] [TopologicalSpace G₁] [IsTopologicalGroup G₁]
680 {G₂ : Type u} [Group G₂] [TopologicalSpace G₂] [IsTopologicalGroup G₂]
681 [CompactSpace G₁] [T2Space G₁] [TotallyDisconnectedSpace G₁]
682 [CompactSpace G₂] [T2Space G₂] [TotallyDisconnectedSpace G₂]
685 (hfg₁ : FiniteGeneration.TopologicallyFinitelyGenerated G₁)
686 (hfg₂ : FiniteGeneration.TopologicallyFinitelyGenerated G₂)
687 (hquot : HasSameFiniteQuotients G₁ G₂) :
688 Nonempty (G₁ ≃ₜ* G₂) := by
690 (G₁ := G₁) (G₂ := G₂) hfg₁ hfg₂
691 intro Q _ _ _ _ _
692 constructor
693 · rintro ⟨φ, hφsurj⟩
694 rcases (hquot Q).1 ⟨φ.toMonoidHom, hφsurj⟩ with ⟨ψ, hψsurj⟩
695 exact
696 ⟨{ toMonoidHom := ψ
697 continuous_toFun :=
698 StronglyCompleteForFiniteDiscreteQuotients.continuous_of_surjective ψ hψsurj },
699 hψsurj⟩
700 · rintro ⟨ψ, hψsurj⟩
701 rcases (hquot Q).2 ⟨ψ.toMonoidHom, hψsurj⟩ with ⟨φ, hφsurj⟩
702 exact
703 ⟨{ toMonoidHom := φ
704 continuous_toFun :=
705 StronglyCompleteForFiniteDiscreteQuotients.continuous_of_surjective φ hφsurj },
706 hφsurj⟩
708end ProCGroups.Completion