ProCGroups/FreeProC/Basic.lean
1import Mathlib.GroupTheory.SpecificGroups.Cyclic
2import ProCGroups.Completion.UniversalProperty
3import ProCGroups.FiniteGroups.StandardClasses
4import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
5import ProCGroups.ProC.Category.Basic
6import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
8/-
9PUBLIC_PAGE_SNAPSHOT
10generated_at: 2026-05-27T09:47:29+09:00
11lean_source: lean4/ProCGroups/FreeProC/Basic.lean
12translation_root: data/translation
13purpose: identifies the local data snapshot used to build pages/
14placement: after imports, never before imports
15-/
16/-!
17# Free pro-C groups
19Develops free pro-C groups on spaces and pointed spaces, their universal properties, finite quotient characterizations, and standard comparison isomorphisms.
20-/
22open Set
23open scoped Topology
25namespace ProCGroups.FreeProC
27universe u v w
29open ProCGroups
31section
33variable {ProC : ProCGroups.ProC.ProCGroupPredicate}
35/-- Free pro-`C` groups via a strengthened universal property.
37maps whose image generates the target. -/
38structure IsFreeProCGroup
39 {X : Type u} [TopologicalSpace X]
40 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
41 (ι : X → F) : Prop where
43 continuous_ι : Continuous ι
44 generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
46 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
47 ProC (G := G) →
48 ∀ (φ : X → G), Continuous φ →
49 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x
51/-- A free pro-`C` group of rank `κ`, stated with the existing universal-property
52interface. -/
54 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
55 (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
56 (κ : Cardinal.{u}) : Prop :=
57 ∃ X : Type u, ∃ _ : TopologicalSpace X,
58 Cardinal.mk X = κ ∧
59 ∃ ι : X → F, IsFreeProCGroup (ProC := ProC) ι
61/-- Concrete finite-class specialization of `IsFreeProCGroupOfRank`. -/
63 (C : ProCGroups.FiniteGroupClass.{u})
64 (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
65 (κ : Cardinal.{u}) : Prop :=
67 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) F κ
69namespace IsFreeProCGroup
71variable {X : Type u} [TopologicalSpace X]
72variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
73variable {ι : X → F}
75/-- The lift supplied by the corresponding free pro-`C` universal property. -/
76noncomputable def lift (hι : IsFreeProCGroup (ProC := ProC) ι)
77 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
78 (hG : ProC (G := G)) (φ : X → G)
79 (hφ : Continuous φ) : F →* G :=
80 Classical.choose (ExistsUnique.exists (hι.existsUnique_lift hG φ hφ))
82/-- The universal-property lift has the prescribed values on the chosen generators. -/
83theorem lift_spec (hι : IsFreeProCGroup (ProC := ProC) ι)
84 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
85 (hG : ProC (G := G)) (φ : X → G)
86 (hφ : Continuous φ) :
87 Continuous (hι.lift hG φ hφ) ∧ ∀ x, hι.lift hG φ hφ (ι x) = φ x :=
88 Classical.choose_spec (ExistsUnique.exists (hι.existsUnique_lift hG φ hφ))
90/-- The universal-property lift is unique among continuous maps with the prescribed values. -/
91theorem lift_unique (hι : IsFreeProCGroup (ProC := ProC) ι)
92 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
93 (hG : ProC (G := G)) (φ : X → G)
94 (hφ : Continuous φ)
95 {f : F →* G} (hf : Continuous f) (hfac : ∀ x, f (ι x) = φ x) :
96 f = hι.lift hG φ hφ := by
97 rcases hι.existsUnique_lift hG φ hφ with ⟨g, _hg, huniq⟩
98 have hchosen : hι.lift hG φ hφ = g := huniq _ (hι.lift_spec hG φ hφ)
99 exact (huniq _ ⟨hf, hfac⟩).trans hchosen.symm
101/-- The lift as a continuous monoid homomorphism. -/
102noncomputable def liftHom (hι : IsFreeProCGroup (ProC := ProC) ι)
103 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
104 (hG : ProC (G := G)) (φ : X → G)
105 (hφ : Continuous φ) : F →ₜ* G where
106 toMonoidHom := hι.lift hG φ hφ
107 continuous_toFun := (hι.lift_spec hG φ hφ).1
109/-- Forgetting continuity from `liftHom` gives the underlying universal-property lift. -/
110@[simp] theorem liftHom_toMonoidHom (hι : IsFreeProCGroup (ProC := ProC) ι)
111 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
112 (hG : ProC (G := G)) (φ : X → G)
113 (hφ : Continuous φ) :
114 (hι.liftHom hG φ hφ).toMonoidHom = hι.lift hG φ hφ :=
115 rfl
117/-- `liftHom` has the prescribed value on each generator. -/
118@[simp] theorem liftHom_apply (hι : IsFreeProCGroup (ProC := ProC) ι)
119 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
120 (hG : ProC (G := G)) (φ : X → G)
121 (hφ : Continuous φ) (x : X) :
122 hι.liftHom hG φ hφ (ι x) = φ x :=
123 (hι.lift_spec hG φ hφ).2 x
125/-- `liftHom` is uniquely determined by its values on the generators. -/
126theorem liftHom_unique (hι : IsFreeProCGroup (ProC := ProC) ι)
127 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
128 (hG : ProC (G := G)) (φ : X → G)
129 (hφ : Continuous φ)
130 {f : F →ₜ* G} (hfac : ∀ x, f (ι x) = φ x) :
131 f = hι.liftHom hG φ hφ := by
132 ext y
133 exact congrArg (fun g : F →* G => g y)
134 (hι.lift_unique hG φ hφ f.continuous_toFun hfac)
136/-- Continuous homomorphisms out of a free pro-`C` group are determined by the basis. -/
137theorem hom_ext (hι : IsFreeProCGroup (ProC := ProC) ι)
138 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
139 (hG : ProC (G := G))
140 {f g : F →* G} (hf : Continuous f) (hg : Continuous g)
141 (hfg : ∀ x, f (ι x) = g (ι x)) :
142 f = g := by
143 let φ : X → G := fun x => f (ι x)
144 have hφ : Continuous φ := hf.comp hι.continuous_ι
145 have hf_lift : f = hι.lift hG φ hφ := hι.lift_unique hG φ hφ hf (by intro x; rfl)
146 have hg_lift : g = hι.lift hG φ hφ :=
147 hι.lift_unique hG φ hφ hg (by intro x; exact (hfg x).symm)
148 exact hf_lift.trans hg_lift.symm
150/-- Two universal-property lifts are equal when they agree on all generators. -/
151theorem lift_eq_of_forall (hι : IsFreeProCGroup (ProC := ProC) ι)
152 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
153 (hG : ProC (G := G))
154 {φ ψ : X → G} (hφ : Continuous φ) (hψ : Continuous ψ)
155 (h : ∀ x, φ x = ψ x) :
156 hι.lift hG φ hφ = hι.lift hG ψ hψ := by
157 apply hι.hom_ext hG
158 (hι.lift_spec hG φ hφ).1
159 (hι.lift_spec hG ψ hψ).1
160 intro x
161 calc
162 hι.lift hG φ hφ (ι x) = φ x := (hι.lift_spec hG φ hφ).2 x
163 _ = ψ x := h x
164 _ = hι.lift hG ψ hψ (ι x) := ((hι.lift_spec hG ψ hψ).2 x).symm
166/-- The lift of the canonical generator map to the same free pro-`C` group is the identity. -/
167@[simp] theorem lift_id (hι : IsFreeProCGroup (ProC := ProC) ι) :
168 hι.lift hι.isProC ι hι.continuous_ι = MonoidHom.id F := by
169 symm
170 exact hι.lift_unique hι.isProC ι hι.continuous_ι continuous_id (by intro x; rfl)
172/-- An endomorphism of a free pro-`C` group fixing the generators is the identity. -/
173theorem endomorphism_eq_id (hι : IsFreeProCGroup (ProC := ProC) ι)
174 {f : F →* F} (hf : Continuous f) (hfac : ∀ x, f (ι x) = ι x) :
175 f = MonoidHom.id F := by
176 exact hι.hom_ext hι.isProC hf continuous_id hfac
178/-- Composition of free pro-`C` lifts is again the lift of the composed generator map. -/
179theorem lift_comp (hι : IsFreeProCGroup (ProC := ProC) ι)
180 {G H : Type u}
181 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
182 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
183 (hG : ProC (G := G))
184 (hH : ProC (G := H))
185 (φ : X → G) (hφ : Continuous φ)
186 (ψ : G →* H) (hψ : Continuous ψ) :
187 ψ.comp (hι.lift hG φ hφ) =
188 hι.lift hH (fun x => ψ (φ x)) (hψ.comp hφ) := by
189 apply hι.lift_unique hH (fun x => ψ (φ x)) (hψ.comp hφ)
190 (hψ.comp (hι.lift_spec hG φ hφ).1)
191 intro x
192 simp only [MonoidHom.coe_comp, Function.comp_apply, (hι.lift_spec hG φ hφ).2 x]
194/-- The lift as a morphism in the bundled category `ProCGrp`. -/
195noncomputable def liftMorphism (hι : IsFreeProCGroup (ProC := ProC) ι)
196 [ProCGroups.ProC.ProCGroup ProC F]
198 ProCGrp.of ProC F ⟶ G :=
199 CategoryTheory.ConcreteCategory.ofHom
201 (hι.liftHom (inferInstanceAs (ProCGroups.ProC.ProCGroup ProC G)).isProC φ hφ)
203/-- The categorical lift morphism has the prescribed value on each generator. -/
204@[simp] theorem liftMorphism_apply (hι : IsFreeProCGroup (ProC := ProC) ι)
205 [ProCGroups.ProC.ProCGroup ProC F]
207 hι.liftMorphism G φ hφ (ι x) = φ x :=
208 hι.liftHom_apply (inferInstanceAs (ProCGroups.ProC.ProCGroup ProC G)).isProC φ hφ x
210/-- The categorical lift morphism is uniquely determined by its values on the generators. -/
211theorem liftMorphism_unique (hι : IsFreeProCGroup (ProC := ProC) ι)
212 [ProCGroups.ProC.ProCGroup ProC F]
214 {f : ProCGrp.of ProC F ⟶ G} (hfac : ∀ x, f (ι x) = φ x) :
215 f = hι.liftMorphism G φ hφ := by
216 apply ProCGrp.hom_ext
217 apply ContinuousMonoidHom.toMonoidHom_injective
218 exact congrArg (fun h : F →ₜ* G => h.toMonoidHom)
219 (hι.liftHom_unique (inferInstanceAs (ProCGroups.ProC.ProCGroup ProC G)).isProC φ hφ
220 (f := f.hom) hfac)
222/-- Extensionality for morphisms out of a free pro-`C` group by checking generators. -/
223theorem morphism_ext (hι : IsFreeProCGroup (ProC := ProC) ι)
224 [ProCGroups.ProC.ProCGroup ProC F]
225 {G : ProCGrp ProC} {f g : ProCGrp.of ProC F ⟶ G}
226 (hfg : ∀ x, f (ι x) = g (ι x)) :
227 f = g := by
228 apply ProCGrp.hom_ext
229 apply ContinuousMonoidHom.toMonoidHom_injective
230 exact hι.hom_ext (inferInstanceAs (ProCGroups.ProC.ProCGroup ProC G)).isProC
231 f.hom.continuous_toFun g.hom.continuous_toFun hfg
233/-- Precomposing the basis by a homeomorphism preserves the free pro-`C` universal property. -/
234theorem precompHomeomorph
235 {X' : Type u} [TopologicalSpace X']
236 (hι : IsFreeProCGroup (ProC := ProC) ι) (e : X' ≃ₜ X) :
237 IsFreeProCGroup (ProC := ProC) (fun x : X' => ι (e x)) := by
238 have hrange : Set.range (fun x : X' => ι (e x)) = Set.range ι := by
239 ext y
240 constructor
241 · rintro ⟨x, rfl⟩
242 exact ⟨e x, rfl⟩
243 · rintro ⟨x, rfl⟩
244 exact ⟨e.symm x, by simp only [Homeomorph.apply_symm_apply]⟩
245 refine
247 continuous_ι := hι.continuous_ι.comp e.continuous
248 generates_range := by simpa [hrange] using hι.generates_range
249 existsUnique_lift := ?_ }
250 intro G _ _ _ hG φ hφ
251 let φ' : X → G := fun x => φ (e.symm x)
252 have hφ' : Continuous φ' := hφ.comp e.symm.continuous
253 rcases hι.existsUnique_lift hG φ' hφ' with ⟨f, hf, huniq⟩
254 refine ⟨f, ?_, ?_⟩
255 · refine ⟨hf.1, ?_⟩
256 intro x
257 simpa [φ'] using hf.2 (e x)
258 · intro g hg
259 apply huniq
260 refine ⟨hg.1, ?_⟩
261 intro x
262 simpa [φ'] using hg.2 (e.symm x)
264/-- The canonical multiplicative homeomorphism between two free pro-`C` groups on the same
265basis. -/
266noncomputable def continuousMulEquivOfSameBasis
267 {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
268 {κ : X → F'}
269 (hι : IsFreeProCGroup (ProC := ProC) ι)
270 (hκ : IsFreeProCGroup (ProC := ProC) κ) :
271 F ≃ₜ* F' :=
272 let f : F →* F' := hι.lift hκ.isProC κ hκ.continuous_ι
273 let g : F' →* F := hκ.lift hι.isProC ι hι.continuous_ι
274 let hf : Continuous f := (hι.lift_spec hκ.isProC κ hκ.continuous_ι).1
275 let hg : Continuous g := (hκ.lift_spec hι.isProC ι hι.continuous_ι).1
276 { toMulEquiv :=
277 { toFun := f
278 invFun := g
279 left_inv := by
280 intro y
281 have hgf : g.comp f = MonoidHom.id F := by
282 apply hι.endomorphism_eq_id (hg.comp hf)
283 intro x
284 dsimp [f, g]
285 rw [(hι.lift_spec hκ.isProC κ hκ.continuous_ι).2 x]
286 exact (hκ.lift_spec hι.isProC ι hι.continuous_ι).2 x
287 exact congrArg (fun h : F →* F => h y) hgf
288 right_inv := by
289 intro y
290 have hfg : f.comp g = MonoidHom.id F' := by
291 apply hκ.endomorphism_eq_id (hf.comp hg)
292 intro x
293 dsimp [f, g]
294 rw [(hκ.lift_spec hι.isProC ι hι.continuous_ι).2 x]
295 exact (hι.lift_spec hκ.isProC κ hκ.continuous_ι).2 x
296 exact congrArg (fun h : F' →* F' => h y) hfg
297 map_mul' := f.map_mul }
298 continuous_toFun := hf
299 continuous_invFun := hg }
301/-- The canonical equivalence between free pro-`C` groups with the same basis fixes each generator. -/
302@[simp 900] theorem continuousMulEquivOfSameBasis_apply
303 {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
304 {κ : X → F'}
305 (hι : IsFreeProCGroup (ProC := ProC) ι)
306 (hκ : IsFreeProCGroup (ProC := ProC) κ) (x : X) :
307 hι.continuousMulEquivOfSameBasis hκ (ι x) = κ x := by
308 simpa [continuousMulEquivOfSameBasis] using
309 (hι.lift_spec hκ.isProC κ hκ.continuous_ι).2 x
311/-- The inverse canonical equivalence between free pro-`C` groups with the same basis fixes each generator. -/
312@[simp 900] theorem continuousMulEquivOfSameBasis_symm_apply
313 {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
314 {κ : X → F'}
315 (hι : IsFreeProCGroup (ProC := ProC) ι)
316 (hκ : IsFreeProCGroup (ProC := ProC) κ) (x : X) :
317 (hι.continuousMulEquivOfSameBasis hκ).symm (κ x) = ι x := by
318 simpa [continuousMulEquivOfSameBasis] using
319 (hκ.lift_spec hι.isProC ι hι.continuous_ι).2 x
321/-- A homeomorphism of the basis extends to a continuous multiplicative automorphism of the
322free pro-`C` group. This is the homeomorphism-valued core used in
323Ribes--Zalesskii, Exercise 5.6.2(d). -/
324noncomputable def continuousMulEquivOfBasisHomeomorph
325 (hι : IsFreeProCGroup (ProC := ProC) ι) (e : X ≃ₜ X) :
326 F ≃ₜ* F :=
327 hι.continuousMulEquivOfSameBasis (hι.precompHomeomorph e)
329@[simp 900] theorem continuousMulEquivOfBasisHomeomorph_apply
330 (hι : IsFreeProCGroup (ProC := ProC) ι) (e : X ≃ₜ X) (x : X) :
331 hι.continuousMulEquivOfBasisHomeomorph e (ι x) = ι (e x) := by
332 simp only [continuousMulEquivOfBasisHomeomorph, continuousMulEquivOfSameBasis_apply]
334@[simp 900] theorem continuousMulEquivOfBasisHomeomorph_symm_apply
335 (hι : IsFreeProCGroup (ProC := ProC) ι) (e : X ≃ₜ X) (x : X) :
336 (hι.continuousMulEquivOfBasisHomeomorph e).symm (ι x) = ι (e.symm x) := by
337 simpa [continuousMulEquivOfBasisHomeomorph] using
338 (hι.continuousMulEquivOfSameBasis_symm_apply (hι.precompHomeomorph e) (e.symm x))
342/-- The homeomorphism of a topological `A`-space induced by one group element. -/
344 (A : Type v) (X : Type u) [Group A] [TopologicalSpace A] [TopologicalSpace X]
345 [MulAction A X] [ContinuousSMul A X] (a : A) : X ≃ₜ X where
346 toEquiv :=
347 { toFun := fun x => a • x
348 invFun := fun x => a⁻¹ • x
349 left_inv := by
350 intro x
351 calc
352 a⁻¹ • (a • x) = (a⁻¹ * a) • x := by rw [mul_smul]
353 _ = x := by simp only [inv_mul_cancel, one_smul]
354 right_inv := by
355 intro x
356 calc
357 a • (a⁻¹ • x) = (a * a⁻¹) • x := by rw [mul_smul]
358 _ = x := by simp only [mul_inv_cancel, one_smul]}
359 continuous_toFun := (continuous_const : Continuous fun _ : X => a).smul continuous_id
360 continuous_invFun := (continuous_const : Continuous fun _ : X => a⁻¹).smul continuous_id
362@[simp 900] theorem mulActionHomeomorph_apply
363 (A : Type v) (X : Type u) [Group A] [TopologicalSpace A] [TopologicalSpace X]
364 [MulAction A X] [ContinuousSMul A X] (a : A) (x : X) :
365 mulActionHomeomorph A X a x = a • x :=
366 rfl
368@[simp 900] theorem mulActionHomeomorph_symm_apply
369 (A : Type v) (X : Type u) [Group A] [TopologicalSpace A] [TopologicalSpace X]
370 [MulAction A X] [ContinuousSMul A X] (a : A) (x : X) :
371 (mulActionHomeomorph A X a).symm x = a⁻¹ • x :=
372 rfl
374namespace IsFreeProCGroup
376variable {ProC : ProCGroups.ProC.ProCGroupPredicate}
377variable {X : Type u} [TopologicalSpace X]
378variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
379variable {ι : X → F}
381/-- A continuous action on the basis extends elementwise to continuous multiplicative
382automorphisms of the free pro-`C` group. This packages the automorphism-valued part of
383Ribes--Zalesskii, Exercise 5.6.2(d); the joint continuity of the resulting action is a separate
385noncomputable def basisActionContinuousMulEquiv
386 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
387 (hι : IsFreeProCGroup (ProC := ProC) ι) (a : A) :
388 F ≃ₜ* F :=
389 hι.continuousMulEquivOfBasisHomeomorph (mulActionHomeomorph A X a)
391@[simp 900] theorem basisActionContinuousMulEquiv_apply
392 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
393 (hι : IsFreeProCGroup (ProC := ProC) ι) (a : A) (x : X) :
394 hι.basisActionContinuousMulEquiv a (ι x) = ι (a • x) := by
395 simp only [basisActionContinuousMulEquiv, continuousMulEquivOfBasisHomeomorph_apply,
398@[simp 900] theorem basisActionContinuousMulEquiv_symm_apply
399 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
400 (hι : IsFreeProCGroup (ProC := ProC) ι) (a : A) (x : X) :
401 (hι.basisActionContinuousMulEquiv a).symm (ι x) = ι (a⁻¹ • x) := by
402 simp only [basisActionContinuousMulEquiv, continuousMulEquivOfBasisHomeomorph_symm_apply,
405/-- The automorphism-valued homomorphism extending a continuous action on the basis of a free
406pro-`C` group. -/
407noncomputable def basisActionMulAutHom
408 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
409 (hι : IsFreeProCGroup (ProC := ProC) ι) :
410 A →* MulAut F where
411 toFun a := (hι.basisActionContinuousMulEquiv a).toMulEquiv
412 map_one' := by
413 ext y
414 have hhom :
415 (hι.basisActionContinuousMulEquiv (1 : A)).toMulEquiv.toMonoidHom =
416 MonoidHom.id F := by
417 apply hι.hom_ext hι.isProC
418 (hι.basisActionContinuousMulEquiv (1 : A)).continuous_toFun
419 continuous_id
420 intro x
421 simp only [mulActionHomeomorph_apply, one_smul, lift_id, MonoidHom.id_apply]
422 exact congrArg (fun f : F →* F => f y) hhom
423 map_mul' := by
424 intro a b
425 ext y
426 have hcontComp :
427 Continuous fun y : F =>
428 hι.basisActionContinuousMulEquiv a (hι.basisActionContinuousMulEquiv b y) :=
429 (hι.basisActionContinuousMulEquiv a).continuous_toFun.comp
430 (hι.basisActionContinuousMulEquiv b).continuous_toFun
431 have hhom :
432 (hι.basisActionContinuousMulEquiv (a * b)).toMulEquiv.toMonoidHom =
433 ((hι.basisActionContinuousMulEquiv a).toMulEquiv.toMonoidHom).comp
434 ((hι.basisActionContinuousMulEquiv b).toMulEquiv.toMonoidHom) := by
435 apply hι.hom_ext hι.isProC
436 (hι.basisActionContinuousMulEquiv (a * b)).continuous_toFun
437 hcontComp
438 intro x
439 calc
440 hι.basisActionContinuousMulEquiv (a * b) (ι x) = ι ((a * b) • x) :=
441 hι.basisActionContinuousMulEquiv_apply (a * b) x
442 _ = ι (a • b • x) := by rw [mul_smul]
443 _ = hι.basisActionContinuousMulEquiv a (ι (b • x)) := by
444 exact (hι.basisActionContinuousMulEquiv_apply a (b • x)).symm
445 _ = hι.basisActionContinuousMulEquiv a
446 (hι.basisActionContinuousMulEquiv b (ι x)) := by
447 rw [hι.basisActionContinuousMulEquiv_apply b x]
448 exact congrArg (fun f : F →* F => f y) hhom
450@[simp 900] theorem basisActionMulAutHom_apply
451 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
452 (hι : IsFreeProCGroup (ProC := ProC) ι) (a : A) (x : X) :
453 hι.basisActionMulAutHom a (ι x) = ι (a • x) := by
454 exact hι.basisActionContinuousMulEquiv_apply a x
456/-- The algebraic action on a free pro-`C` group induced by a continuous action on its basis. -/
457noncomputable def basisMulDistribMulAction
458 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
459 (hι : IsFreeProCGroup (ProC := ProC) ι) :
460 MulDistribMulAction A F where
461 smul a y := hι.basisActionMulAutHom a y
462 one_smul y := by
463 change hι.basisActionMulAutHom (1 : A) y = y
465 mul_smul a b y := by
466 change hι.basisActionMulAutHom (a * b) y =
467 hι.basisActionMulAutHom a (hι.basisActionMulAutHom b y)
469 smul_one a := by
471 smul_mul a y z := by
474@[simp 900] theorem basisMulDistribMulAction_smul_generator
475 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
476 (hι : IsFreeProCGroup (ProC := ProC) ι) (a : A) (x : X) :
477 letI : MulDistribMulAction A F := hι.basisMulDistribMulAction
478 a • ι x = ι (a • x) := by
479 letI : MulDistribMulAction A F := hι.basisMulDistribMulAction
480 exact hι.basisActionMulAutHom_apply a x
482/-- Tube-lemma form of the continuity input for Exercise 5.6.2(d): after composing with any
483discrete pro-`C` target, the automorphisms induced by nearby basis-action parameters agree on a
484neighborhood of the chosen parameter. -/
485theorem basisActionContinuousMulEquiv_eventually_eq_of_discreteTarget
486 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
487 [CompactSpace X]
488 {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [DiscreteTopology Q]
489 (hι : IsFreeProCGroup (ProC := ProC) ι)
490 (hQ : ProC (G := Q)) (φ : F →* Q) (hφ : Continuous φ) (a₀ : A) :
491 ∃ U : Set A, IsOpen U ∧ a₀ ∈ U ∧
492 ∀ a ∈ U,
493 φ.comp (hι.basisActionContinuousMulEquiv a).toMulEquiv.toMonoidHom =
494 φ.comp (hι.basisActionContinuousMulEquiv a₀).toMulEquiv.toMonoidHom := by
495 let T : Set (A × X) := {p | φ (ι (p.1 • p.2)) = φ (ι (a₀ • p.2))}
496 have hleft : Continuous fun p : A × X => φ (ι (p.1 • p.2)) := by
497 exact hφ.comp (hι.continuous_ι.comp (continuous_fst.smul continuous_snd))
498 have hright : Continuous fun p : A × X => φ (ι (a₀ • p.2)) := by
499 exact hφ.comp
500 (hι.continuous_ι.comp
501 ((continuous_const : Continuous fun _ : A × X => a₀).smul continuous_snd))
502 have hTopen : IsOpen T := by
503 change IsOpen
504 ((fun p : A × X => (φ (ι (p.1 • p.2)), φ (ι (a₀ • p.2)))) ⁻¹'
505 {q : Q × Q | q.1 = q.2})
506 exact (isOpen_discrete {q : Q × Q | q.1 = q.2}).preimage (hleft.prodMk hright)
507 have hcontains : ({a₀} : Set A) ×ˢ (Set.univ : Set X) ⊆ T := by
508 rintro ⟨a, x⟩ ⟨ha, _hx⟩
509 change φ (ι (a • x)) = φ (ι (a₀ • x))
510 rw [Set.mem_singleton_iff] at ha
511 have ha' : a = a₀ := by simpa using ha
512 rw [ha']
513 rcases generalized_tube_lemma (s := ({a₀} : Set A)) isCompact_singleton
514 (t := (Set.univ : Set X)) isCompact_univ hTopen hcontains with
515 ⟨U, V, hUopen, _hVopen, hsingleU, hXV, hUV⟩
516 refine ⟨U, hUopen, hsingleU (by simp only [mem_singleton_iff]), ?_⟩
517 intro a ha
518 have hcontinuous_a :
519 Continuous (φ.comp (hι.basisActionContinuousMulEquiv a).toMulEquiv.toMonoidHom) := by
520 simpa [MonoidHom.comp_apply] using
521 hφ.comp (hι.basisActionContinuousMulEquiv a).continuous_toFun
522 have hcontinuous_a₀ :
523 Continuous (φ.comp (hι.basisActionContinuousMulEquiv a₀).toMulEquiv.toMonoidHom) := by
524 simpa [MonoidHom.comp_apply] using
525 hφ.comp (hι.basisActionContinuousMulEquiv a₀).continuous_toFun
526 apply hι.hom_ext hQ hcontinuous_a hcontinuous_a₀
527 intro x
528 have hx : (a, x) ∈ T := hUV ⟨ha, hXV trivial⟩
529 change φ (ι (a • x)) = φ (ι (a₀ • x)) at hx
530 calc
531 (φ.comp (hι.basisActionContinuousMulEquiv a).toMulEquiv.toMonoidHom) (ι x) =
532 φ (ι (a • x)) := by
533 exact congrArg φ (hι.basisActionContinuousMulEquiv_apply a x)
534 _ = φ (ι (a₀ • x)) := hx
535 _ = (φ.comp (hι.basisActionContinuousMulEquiv a₀).toMulEquiv.toMonoidHom) (ι x) := by
536 exact (congrArg φ (hι.basisActionContinuousMulEquiv_apply a₀ x)).symm
538/-- Composing the induced basis action on a free pro-`C` group with a discrete pro-`C` target is
540joint-continuity part of Exercise 5.6.2(d). -/
541theorem continuous_discreteTarget_comp_basisActionContinuousMulEquiv
542 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
543 [CompactSpace X]
544 {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [DiscreteTopology Q]
545 (hι : IsFreeProCGroup (ProC := ProC) ι)
546 (hQ : ProC (G := Q)) (φ : F →* Q) (hφ : Continuous φ) :
547 Continuous fun p : A × F => φ (hι.basisActionContinuousMulEquiv p.1 p.2) := by
548 rw [continuous_iff_continuousAt]
549 intro p
550 rcases hι.basisActionContinuousMulEquiv_eventually_eq_of_discreteTarget
551 (A := A) hQ φ hφ p.1 with
552 ⟨U, hUopen, hpU, hUeq⟩
553 let f : A × F → Q := fun q => φ (hι.basisActionContinuousMulEquiv p.1 q.2)
554 have hf : ContinuousAt f p := by
555 have hfcont : Continuous f :=
556 (hφ.comp (hι.basisActionContinuousMulEquiv p.1).continuous_toFun).comp continuous_snd
557 exact hfcont.continuousAt
558 have hUprod : Prod.fst ⁻¹' U ∈ 𝓝 p :=
559 (hUopen.preimage continuous_fst).mem_nhds hpU
560 have hev :
561 (fun q : A × F => φ (hι.basisActionContinuousMulEquiv q.1 q.2)) =ᶠ[𝓝 p] f := by
562 filter_upwards [hUprod] with q hq
563 exact congrArg (fun η : F →* Q => η q.2) (hUeq q.1 hq)
564 exact hf.congr_of_eventuallyEq hev
566/-- Exercise 5.6.2(d), concrete finite-class form: a continuous action on the profinite basis of
567a free pro-`C` group extends to a jointly continuous action on the free group. The proof checks
569the pro-`C` group. -/
570theorem basisMulDistribMulAction_continuousSMul_of_finiteGroupClass
571 (C : ProCGroups.FiniteGroupClass.{u}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
572 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
573 [CompactSpace X]
574 (hι : IsFreeProCGroup
575 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι) :
576 letI : MulDistribMulAction A F := hι.basisMulDistribMulAction
577 ContinuousSMul A F := by
578 letI : MulDistribMulAction A F := hι.basisMulDistribMulAction
579 refine ContinuousSMul.mk ?_
580 let S := ProCGroups.ProC.openNormalSubgroupInClassSystem C F
581 let e :=
583 (C := C) (G := F) hForm hι.isProC
584 let act : A × F → F := fun p => p.1 • p.2
585 let ψ : ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C F),
586 A × F → S.X U :=
587 fun U p => ProCGroups.ProC.openNormalSubgroupInClassProj (C := C) (G := F) U (act p)
588 have hψcont : ∀ U, Continuous (ψ U) := by
589 intro U
590 letI : DiscreteTopology (S.X U) := by
592 exact QuotientGroup.discreteTopology
593 (openNormalSubgroup_isOpen (G := F)
594 ((OrderDual.ofDual U).1 : OpenNormalSubgroup F))
595 letI : IsTopologicalGroup (S.X U) := by infer_instance
596 have hQ : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := S.X U) := by
597 letI : Finite (S.X U) := by
599 exact hForm.finiteOnly (OrderDual.ofDual U).2
601 (C := C) (G := S.X U) hForm.quotientClosed (by
602 simpa [S, ProCGroups.ProC.openNormalSubgroupInClassSystem] using
603 (OrderDual.ofDual U).2)
604 have hφcont :
605 Continuous (ProCGroups.ProC.openNormalSubgroupInClassProj (C := C) (G := F) U) :=
606 continuous_quotient_mk'
607 simpa [ψ, act] using
608 hι.continuous_discreteTarget_comp_basisActionContinuousMulEquiv
609 (A := A) hQ
610 (ProCGroups.ProC.openNormalSubgroupInClassProj (C := C) (G := F) U) hφcont
611 have hψcompat : S.CompatibleMaps ψ := by
612 intro U V hUV
613 funext p
614 exact congrFun
615 (ProCGroups.ProC.openNormalSubgroupInClassProj_compatible (C := C) (G := F) U V hUV)
616 (act p)
617 have hcontinuous_lift : Continuous (S.inverseLimitLift ψ hψcompat) :=
618 S.continuous_inverseLimitLift ψ hψcont hψcompat
619 have heq : (fun p : A × F => e (act p)) = S.inverseLimitLift ψ hψcompat := by
620 funext p
621 apply S.ext
622 intro U
623 change S.projection U (e (act p)) = ψ U p
624 simpa [e, ψ, act, S] using
626 (C := C) (G := F) hForm hι.isProC U (act p)
627 have hcontinuous_eact : Continuous fun p : A × F => e (act p) := by
628 simpa [heq] using hcontinuous_lift
629 have hcontinuous_act : Continuous act := by
630 have hcomp : Continuous fun p : A × F => e.symm (e (act p)) :=
631 e.continuous_invFun.comp hcontinuous_eact
632 convert hcomp using 1
633 funext p
634 simp only [ContinuousMulEquiv.symm_apply_apply, act]
635 simpa [act] using hcontinuous_act
639/-- Pointed free pro-`C` groups via a strengthened universal property. -/
640structure IsPointedFreeProCGroup
641 {X : Type u} [TopologicalSpace X] (x0 : X)
642 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
643 (ι : X → F) : Prop where
645 continuous_ι : Continuous ι
646 map_base : ι x0 = 1
647 generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
649 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
650 ProC (G := G) →
651 ∀ (φ : X → G), Continuous φ →
652 φ x0 = 1 →
653 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x
655namespace IsPointedFreeProCGroup
657variable {X : Type u} [TopologicalSpace X] {x0 : X}
658variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
659variable {ι : X → F}
661/-- The lift supplied by the corresponding free pro-`C` universal property. -/
662noncomputable def lift (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
663 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
664 (hG : ProC (G := G)) (φ : X → G)
665 (hφ : Continuous φ)
666 (hφ0 : φ x0 = 1) :
667 F →* G :=
668 Classical.choose (ExistsUnique.exists (hι.existsUnique_lift hG φ hφ hφ0))
670/-- The universal-property lift has the prescribed values on the chosen generators. -/
671theorem lift_spec (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
672 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
673 (hG : ProC (G := G)) (φ : X → G)
674 (hφ : Continuous φ)
675 (hφ0 : φ x0 = 1) :
676 Continuous (hι.lift hG φ hφ hφ0) ∧ ∀ x, hι.lift hG φ hφ hφ0 (ι x) = φ x :=
677 Classical.choose_spec (ExistsUnique.exists (hι.existsUnique_lift hG φ hφ hφ0))
679/-- The universal-property lift is unique among continuous maps with the prescribed values. -/
680theorem lift_unique (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
681 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
682 (hG : ProC (G := G)) (φ : X → G)
683 (hφ : Continuous φ)
684 (hφ0 : φ x0 = 1)
685 {f : F →* G} (hf : Continuous f) (hfac : ∀ x, f (ι x) = φ x) :
686 f = hι.lift hG φ hφ hφ0 := by
687 rcases hι.existsUnique_lift hG φ hφ hφ0 with ⟨g, _hg, huniq⟩
688 have hchosen : hι.lift hG φ hφ hφ0 = g := huniq _ (hι.lift_spec hG φ hφ hφ0)
689 exact (huniq _ ⟨hf, hfac⟩).trans hchosen.symm
691/-- The pointed lift as a continuous monoid homomorphism. -/
692noncomputable def liftHom (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
693 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
694 (hG : ProC (G := G)) (φ : X → G)
695 (hφ : Continuous φ)
696 (hφ0 : φ x0 = 1) :
697 F →ₜ* G where
698 toMonoidHom := hι.lift hG φ hφ hφ0
699 continuous_toFun := (hι.lift_spec hG φ hφ hφ0).1
701/-- `liftHom` has the prescribed value on each generator. -/
702@[simp] theorem liftHom_apply (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
703 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
704 (hG : ProC (G := G)) (φ : X → G)
705 (hφ : Continuous φ)
706 (hφ0 : φ x0 = 1) (x : X) :
707 hι.liftHom hG φ hφ hφ0 (ι x) = φ x :=
708 (hι.lift_spec hG φ hφ hφ0).2 x
710/-- Extensionality for homomorphisms out of a free pro-`C` group by checking generators. -/
711theorem hom_ext (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
712 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
713 (hG : ProC (G := G))
714 {f g : F →* G} (hf : Continuous f) (hg : Continuous g)
715 (hfg : ∀ x, f (ι x) = g (ι x)) :
716 f = g := by
717 let φ : X → G := fun x => f (ι x)
718 have hφ : Continuous φ := hf.comp hι.continuous_ι
720 have hf_lift : f = hι.lift hG φ hφ hφ0 :=
721 hι.lift_unique hG φ hφ hφ0 hf (by intro x; rfl)
722 have hg_lift : g = hι.lift hG φ hφ hφ0 :=
723 hι.lift_unique hG φ hφ hφ0 hg (by intro x; exact (hfg x).symm)
724 exact hf_lift.trans hg_lift.symm
726/-- The lift of the canonical generator map to the same free pro-`C` group is the identity. -/
727@[simp] theorem lift_id (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι) :
728 hι.lift hι.isProC ι hι.continuous_ι hι.map_base = MonoidHom.id F := by
729 symm
730 exact hι.lift_unique hι.isProC ι hι.continuous_ι hι.map_base continuous_id
731 (by intro x; rfl)
733/-- An endomorphism of a free pro-`C` group fixing the generators is the identity. -/
734theorem endomorphism_eq_id (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
735 {f : F →* F} (hf : Continuous f) (hfac : ∀ x, f (ι x) = ι x) :
736 f = MonoidHom.id F := by
737 exact hι.hom_ext hι.isProC hf continuous_id hfac
739/-- Composition of free pro-`C` lifts is again the lift of the composed generator map. -/
740theorem lift_comp (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
741 {G H : Type u}
742 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
743 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
744 (hG : ProC (G := G))
745 (hH : ProC (G := H))
746 (φ : X → G) (hφ : Continuous φ) (hφ0 : φ x0 = 1)
747 (ψ : G →* H) (hψ : Continuous ψ) :
748 ψ.comp (hι.lift hG φ hφ hφ0) =
751 (hψ.comp (hι.lift_spec hG φ hφ hφ0).1)
752 intro x
753 simp only [MonoidHom.coe_comp, Function.comp_apply, (hι.lift_spec hG φ hφ hφ0).2 x]
755/-- A basepoint-preserving continuous action on the pointed basis extends elementwise to
756continuous multiplicative automorphisms of the pointed free pro-`C` group. -/
757noncomputable def basisActionContinuousMulEquiv
758 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
759 (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
760 (hbase : ∀ a : A, a • x0 = x0) (a : A) :
761 F ≃ₜ* F := by
762 let φ : X → F := fun x => ι (a • x)
763 have hφ : Continuous φ := hι.continuous_ι.comp
764 ((continuous_const : Continuous fun _ : X => a).smul continuous_id)
765 have hφ0 : φ x0 = 1 := by
766 dsimp [φ]
767 rw [hbase a, hι.map_base]
768 let ψ : X → F := fun x => ι (a⁻¹ • x)
769 have hψ : Continuous ψ := hι.continuous_ι.comp
770 ((continuous_const : Continuous fun _ : X => a⁻¹).smul continuous_id)
771 have hψ0 : ψ x0 = 1 := by
772 dsimp [ψ]
773 rw [hbase a⁻¹, hι.map_base]
774 let f : F →* F := hι.lift hι.isProC φ hφ hφ0
775 let g : F →* F := hι.lift hι.isProC ψ hψ hψ0
776 have hfcont : Continuous f := (hι.lift_spec hι.isProC φ hφ hφ0).1
777 have hgcont : Continuous g := (hι.lift_spec hι.isProC ψ hψ hψ0).1
778 have hfg : g.comp f = MonoidHom.id F := by
779 refine hι.hom_ext hι.isProC (f := g.comp f) (g := MonoidHom.id F)
780 (hgcont.comp hfcont) continuous_id ?_
781 intro x
782 calc
783 (g.comp f) (ι x) = g (f (ι x)) := rfl
784 _ = g (ι (a • x)) := by
785 rw [(hι.lift_spec hι.isProC φ hφ hφ0).2 x]
786 _ = ι (a⁻¹ • (a • x)) := by
787 rw [(hι.lift_spec hι.isProC ψ hψ hψ0).2 (a • x)]
788 _ = ι x := by
789 rw [inv_smul_smul]
790 _ = MonoidHom.id F (ι x) := rfl
791 have hgf : f.comp g = MonoidHom.id F := by
792 refine hι.hom_ext hι.isProC (f := f.comp g) (g := MonoidHom.id F)
793 (hfcont.comp hgcont) continuous_id ?_
794 intro x
795 calc
796 (f.comp g) (ι x) = f (g (ι x)) := rfl
797 _ = f (ι (a⁻¹ • x)) := by
798 rw [(hι.lift_spec hι.isProC ψ hψ hψ0).2 x]
799 _ = ι (a • (a⁻¹ • x)) := by
800 rw [(hι.lift_spec hι.isProC φ hφ hφ0).2 (a⁻¹ • x)]
801 _ = ι x := by
802 rw [smul_inv_smul]
803 _ = MonoidHom.id F (ι x) := rfl
804 exact
805 { toMulEquiv :=
806 { toFun := f
807 invFun := g
808 left_inv := by
809 intro y
810 exact congrArg (fun h : F →* F => h y) hfg
811 right_inv := by
812 intro y
813 exact congrArg (fun h : F →* F => h y) hgf
814 map_mul' := f.map_mul }
815 continuous_toFun := hfcont
816 continuous_invFun := hgcont }
818@[simp 900] theorem basisActionContinuousMulEquiv_apply
819 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
820 (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
821 (hbase : ∀ a : A, a • x0 = x0) (a : A) (x : X) :
822 hι.basisActionContinuousMulEquiv hbase a (ι x) = ι (a • x) := by
823 let φ : X → F := fun x => ι (a • x)
824 have hφ : Continuous φ := hι.continuous_ι.comp
825 ((continuous_const : Continuous fun _ : X => a).smul continuous_id)
826 have hφ0 : φ x0 = 1 := by
827 dsimp [φ]
828 rw [hbase a, hι.map_base]
829 unfold basisActionContinuousMulEquiv
830 dsimp [φ]
831 exact (hι.lift_spec hι.isProC φ hφ hφ0).2 x
833@[simp 900] theorem basisActionContinuousMulEquiv_symm_apply
834 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
835 (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
836 (hbase : ∀ a : A, a • x0 = x0) (a : A) (x : X) :
837 (hι.basisActionContinuousMulEquiv hbase a).symm (ι x) = ι (a⁻¹ • x) := by
838 let ψ : X → F := fun x => ι (a⁻¹ • x)
839 have hψ : Continuous ψ := hι.continuous_ι.comp
840 ((continuous_const : Continuous fun _ : X => a⁻¹).smul continuous_id)
841 have hψ0 : ψ x0 = 1 := by
842 dsimp [ψ]
843 rw [hbase a⁻¹, hι.map_base]
844 unfold basisActionContinuousMulEquiv
845 dsimp [ψ]
846 exact (hι.lift_spec hι.isProC ψ hψ hψ0).2 x
848/-- The automorphism-valued homomorphism extending a basepoint-preserving action on the pointed
849basis of a free pro-`C` group. -/
850noncomputable def basisActionMulAutHom
851 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
852 (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
853 (hbase : ∀ a : A, a • x0 = x0) :
854 A →* MulAut F where
855 toFun a := (hι.basisActionContinuousMulEquiv hbase a).toMulEquiv
856 map_one' := by
857 ext y
858 have hhom :
859 (hι.basisActionContinuousMulEquiv hbase (1 : A)).toMulEquiv.toMonoidHom =
860 MonoidHom.id F := by
861 refine hι.hom_ext hι.isProC
862 (f := (hι.basisActionContinuousMulEquiv hbase (1 : A)).toMulEquiv.toMonoidHom)
863 (g := MonoidHom.id F)
864 (hι.basisActionContinuousMulEquiv hbase (1 : A)).continuous_toFun
865 continuous_id ?_
866 intro x
867 change hι.basisActionContinuousMulEquiv hbase (1 : A) (ι x) =
868 MonoidHom.id F (ι x)
869 rw [hι.basisActionContinuousMulEquiv_apply hbase (1 : A) x, one_smul]
870 rfl
871 exact congrArg (fun f : F →* F => f y) hhom
872 map_mul' := by
873 intro a b
874 ext y
875 have hcontComp :
876 Continuous fun y : F =>
877 hι.basisActionContinuousMulEquiv hbase a
878 (hι.basisActionContinuousMulEquiv hbase b y) :=
879 (hι.basisActionContinuousMulEquiv hbase a).continuous_toFun.comp
880 (hι.basisActionContinuousMulEquiv hbase b).continuous_toFun
881 have hhom :
882 (hι.basisActionContinuousMulEquiv hbase (a * b)).toMulEquiv.toMonoidHom =
883 ((hι.basisActionContinuousMulEquiv hbase a).toMulEquiv.toMonoidHom).comp
884 ((hι.basisActionContinuousMulEquiv hbase b).toMulEquiv.toMonoidHom) := by
885 refine hι.hom_ext hι.isProC
886 (f := (hι.basisActionContinuousMulEquiv hbase (a * b)).toMulEquiv.toMonoidHom)
887 (g :=
888 ((hι.basisActionContinuousMulEquiv hbase a).toMulEquiv.toMonoidHom).comp
889 ((hι.basisActionContinuousMulEquiv hbase b).toMulEquiv.toMonoidHom))
890 (hι.basisActionContinuousMulEquiv hbase (a * b)).continuous_toFun
891 hcontComp ?_
892 intro x
893 calc
894 hι.basisActionContinuousMulEquiv hbase (a * b) (ι x) = ι ((a * b) • x) :=
895 hι.basisActionContinuousMulEquiv_apply hbase (a * b) x
896 _ = ι (a • b • x) := by rw [mul_smul]
897 _ = hι.basisActionContinuousMulEquiv hbase a (ι (b • x)) := by
898 exact (hι.basisActionContinuousMulEquiv_apply hbase a (b • x)).symm
899 _ = hι.basisActionContinuousMulEquiv hbase a
900 (hι.basisActionContinuousMulEquiv hbase b (ι x)) := by
901 rw [hι.basisActionContinuousMulEquiv_apply hbase b x]
902 exact congrArg (fun f : F →* F => f y) hhom
904@[simp 900] theorem basisActionMulAutHom_apply
905 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
906 (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
907 (hbase : ∀ a : A, a • x0 = x0) (a : A) (x : X) :
908 hι.basisActionMulAutHom hbase a (ι x) = ι (a • x) :=
909 hι.basisActionContinuousMulEquiv_apply hbase a x
911/-- The algebraic action on a pointed free pro-`C` group induced by a basepoint-preserving
912continuous action on its pointed basis. -/
913noncomputable def basisMulDistribMulAction
914 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
915 (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
916 (hbase : ∀ a : A, a • x0 = x0) :
917 MulDistribMulAction A F where
918 smul a y := hι.basisActionMulAutHom hbase a y
919 one_smul y := by
920 change hι.basisActionMulAutHom hbase (1 : A) y = y
922 mul_smul a b y := by
923 change hι.basisActionMulAutHom hbase (a * b) y =
924 hι.basisActionMulAutHom hbase a (hι.basisActionMulAutHom hbase b y)
926 smul_one a := by
928 smul_mul a y z := by
931@[simp 900] theorem basisMulDistribMulAction_smul_generator
932 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
933 (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
934 (hbase : ∀ a : A, a • x0 = x0) (a : A) (x : X) :
935 letI : MulDistribMulAction A F := hι.basisMulDistribMulAction hbase
936 a • ι x = ι (a • x) := by
937 letI : MulDistribMulAction A F := hι.basisMulDistribMulAction hbase
938 exact hι.basisActionMulAutHom_apply hbase a x
940/-- Pointed tube-lemma continuity input for Exercise 5.6.2(d). -/
941theorem basisActionContinuousMulEquiv_eventually_eq_of_discreteTarget
942 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
943 [CompactSpace X]
944 {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [DiscreteTopology Q]
945 (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
946 (hbase : ∀ a : A, a • x0 = x0)
947 (hQ : ProC (G := Q)) (φ : F →* Q) (hφ : Continuous φ) (a₀ : A) :
948 ∃ U : Set A, IsOpen U ∧ a₀ ∈ U ∧
949 ∀ a ∈ U,
950 φ.comp (hι.basisActionContinuousMulEquiv hbase a).toMulEquiv.toMonoidHom =
951 φ.comp (hι.basisActionContinuousMulEquiv hbase a₀).toMulEquiv.toMonoidHom := by
952 let T : Set (A × X) := {p | φ (ι (p.1 • p.2)) = φ (ι (a₀ • p.2))}
953 have hleft : Continuous fun p : A × X => φ (ι (p.1 • p.2)) := by
954 exact hφ.comp (hι.continuous_ι.comp (continuous_fst.smul continuous_snd))
955 have hright : Continuous fun p : A × X => φ (ι (a₀ • p.2)) := by
956 exact hφ.comp
957 (hι.continuous_ι.comp
958 ((continuous_const : Continuous fun _ : A × X => a₀).smul continuous_snd))
959 have hTopen : IsOpen T := by
960 change IsOpen
961 ((fun p : A × X => (φ (ι (p.1 • p.2)), φ (ι (a₀ • p.2)))) ⁻¹'
962 {q : Q × Q | q.1 = q.2})
963 exact (isOpen_discrete {q : Q × Q | q.1 = q.2}).preimage (hleft.prodMk hright)
964 have hcontains : ({a₀} : Set A) ×ˢ (Set.univ : Set X) ⊆ T := by
965 rintro ⟨a, x⟩ ⟨ha, _hx⟩
966 change φ (ι (a • x)) = φ (ι (a₀ • x))
967 rw [Set.mem_singleton_iff] at ha
968 have ha' : a = a₀ := by simpa using ha
969 rw [ha']
970 rcases generalized_tube_lemma (s := ({a₀} : Set A)) isCompact_singleton
971 (t := (Set.univ : Set X)) isCompact_univ hTopen hcontains with
972 ⟨U, V, hUopen, _hVopen, hsingleU, hXV, hUV⟩
973 refine ⟨U, hUopen, hsingleU (by simp only [mem_singleton_iff]), ?_⟩
974 intro a ha
975 have hcontinuous_a :
976 Continuous (φ.comp (hι.basisActionContinuousMulEquiv hbase a).toMulEquiv.toMonoidHom) := by
977 simpa [MonoidHom.comp_apply] using
978 hφ.comp (hι.basisActionContinuousMulEquiv hbase a).continuous_toFun
979 have hcontinuous_a₀ :
980 Continuous (φ.comp (hι.basisActionContinuousMulEquiv hbase a₀).toMulEquiv.toMonoidHom) := by
981 simpa [MonoidHom.comp_apply] using
982 hφ.comp (hι.basisActionContinuousMulEquiv hbase a₀).continuous_toFun
983 apply hι.hom_ext hQ hcontinuous_a hcontinuous_a₀
984 intro x
985 have hx : (a, x) ∈ T := hUV ⟨ha, hXV trivial⟩
986 change φ (ι (a • x)) = φ (ι (a₀ • x)) at hx
987 calc
988 (φ.comp (hι.basisActionContinuousMulEquiv hbase a).toMulEquiv.toMonoidHom) (ι x) =
989 φ (ι (a • x)) := by
990 exact congrArg φ (hι.basisActionContinuousMulEquiv_apply hbase a x)
991 _ = φ (ι (a₀ • x)) := hx
992 _ = (φ.comp (hι.basisActionContinuousMulEquiv hbase a₀).toMulEquiv.toMonoidHom) (ι x) := by
993 exact (congrArg φ (hι.basisActionContinuousMulEquiv_apply hbase a₀ x)).symm
995/-- Composing the pointed induced basis action with a discrete pro-`C` target is jointly
996continuous. -/
997theorem continuous_discreteTarget_comp_basisActionContinuousMulEquiv
998 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
999 [CompactSpace X]
1000 {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [DiscreteTopology Q]
1001 (hι : IsPointedFreeProCGroup (ProC := ProC) x0 ι)
1002 (hbase : ∀ a : A, a • x0 = x0)
1003 (hQ : ProC (G := Q)) (φ : F →* Q) (hφ : Continuous φ) :
1004 Continuous fun p : A × F => φ (hι.basisActionContinuousMulEquiv hbase p.1 p.2) := by
1005 rw [continuous_iff_continuousAt]
1006 intro p
1007 rcases hι.basisActionContinuousMulEquiv_eventually_eq_of_discreteTarget
1008 (A := A) hbase hQ φ hφ p.1 with
1009 ⟨U, hUopen, hpU, hUeq⟩
1010 let f : A × F → Q := fun q => φ (hι.basisActionContinuousMulEquiv hbase p.1 q.2)
1011 have hf : ContinuousAt f p := by
1012 have hfcont : Continuous f :=
1013 (hφ.comp (hι.basisActionContinuousMulEquiv hbase p.1).continuous_toFun).comp continuous_snd
1014 exact hfcont.continuousAt
1015 have hUprod : Prod.fst ⁻¹' U ∈ 𝓝 p :=
1016 (hUopen.preimage continuous_fst).mem_nhds hpU
1017 have hev :
1018 (fun q : A × F => φ (hι.basisActionContinuousMulEquiv hbase q.1 q.2)) =ᶠ[𝓝 p] f := by
1019 filter_upwards [hUprod] with q hq
1020 exact congrArg (fun η : F →* Q => η q.2) (hUeq q.1 hq)
1021 exact hf.congr_of_eventuallyEq hev
1023/-- Pointed form of Exercise 5.6.2(d) for a finite-group class: a basepoint-preserving continuous
1024action on the pointed profinite basis extends to a jointly continuous action on the pointed free
1025pro-`C` group. -/
1026theorem basisMulDistribMulAction_continuousSMul_of_finiteGroupClass
1027 (C : ProCGroups.FiniteGroupClass.{u}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
1028 {A : Type v} [Group A] [TopologicalSpace A] [MulAction A X] [ContinuousSMul A X]
1029 [CompactSpace X]
1030 (hι : IsPointedFreeProCGroup
1031 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) x0 ι)
1032 (hbase : ∀ a : A, a • x0 = x0) :
1033 letI : MulDistribMulAction A F := hι.basisMulDistribMulAction hbase
1034 ContinuousSMul A F := by
1035 letI : MulDistribMulAction A F := hι.basisMulDistribMulAction hbase
1036 refine ContinuousSMul.mk ?_
1037 let S := ProCGroups.ProC.openNormalSubgroupInClassSystem C F
1038 let e :=
1040 (C := C) (G := F) hForm hι.isProC
1041 let act : A × F → F := fun p => p.1 • p.2
1042 let ψ : ∀ U : OrderDual (ProCGroups.ProC.OpenNormalSubgroupInClass C F),
1043 A × F → S.X U :=
1044 fun U p => ProCGroups.ProC.openNormalSubgroupInClassProj (C := C) (G := F) U (act p)
1045 have hψcont : ∀ U, Continuous (ψ U) := by
1046 intro U
1047 letI : DiscreteTopology (S.X U) := by
1049 exact QuotientGroup.discreteTopology
1050 (openNormalSubgroup_isOpen (G := F)
1051 ((OrderDual.ofDual U).1 : OpenNormalSubgroup F))
1052 letI : IsTopologicalGroup (S.X U) := by infer_instance
1053 have hQ : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := S.X U) := by
1054 letI : Finite (S.X U) := by
1056 exact hForm.finiteOnly (OrderDual.ofDual U).2
1058 (C := C) (G := S.X U) hForm.quotientClosed (by
1059 simpa [S, ProCGroups.ProC.openNormalSubgroupInClassSystem] using
1060 (OrderDual.ofDual U).2)
1061 have hφcont :
1062 Continuous (ProCGroups.ProC.openNormalSubgroupInClassProj (C := C) (G := F) U) :=
1063 continuous_quotient_mk'
1064 simpa [ψ, act] using
1065 hι.continuous_discreteTarget_comp_basisActionContinuousMulEquiv
1066 (A := A) hbase hQ
1067 (ProCGroups.ProC.openNormalSubgroupInClassProj (C := C) (G := F) U) hφcont
1068 have hψcompat : S.CompatibleMaps ψ := by
1069 intro U V hUV
1070 funext p
1071 exact congrFun
1072 (ProCGroups.ProC.openNormalSubgroupInClassProj_compatible (C := C) (G := F) U V hUV)
1073 (act p)
1074 have hcontinuous_lift : Continuous (S.inverseLimitLift ψ hψcompat) :=
1075 S.continuous_inverseLimitLift ψ hψcont hψcompat
1076 have heq : (fun p : A × F => e (act p)) = S.inverseLimitLift ψ hψcompat := by
1077 funext p
1078 apply S.ext
1079 intro U
1080 change S.projection U (e (act p)) = ψ U p
1081 simpa [e, ψ, act, S] using
1083 (C := C) (G := F) hForm hι.isProC U (act p)
1084 have hcontinuous_eact : Continuous fun p : A × F => e (act p) := by
1085 simpa [heq] using hcontinuous_lift
1086 have hcontinuous_act : Continuous act := by
1087 have hcomp : Continuous fun p : A × F => e.symm (e (act p)) :=
1088 e.continuous_invFun.comp hcontinuous_eact
1089 convert hcomp using 1
1090 funext p
1091 simp only [ContinuousMulEquiv.symm_apply_apply, act]
1092 simpa [act] using hcontinuous_act
1096end
1098section
1100variable {ProC : ProCGroups.ProC.ProCGroupPredicate}
1102/-- A family in a topological group converges to `1` when every open subgroup contains all but
1103finitely many indexed terms. -/
1105 {X : Type v}
1106 {G : Type u} [Group G] [TopologicalSpace G]
1107 (μ : X → G) : Prop :=
1108 ∀ U : OpenSubgroup G, {x : X | μ x ∉ (U : Set G)}.Finite
1110namespace FamilyConvergesToOne
1112variable {X : Type v}
1113variable {G : Type u} [Group G] [TopologicalSpace G]
1115/-- A family converging to `1` has range converging to `1` as a set. -/
1116theorem range {μ : X → G} (hμ : FamilyConvergesToOne (G := G) μ) :
1117 Generation.ConvergesToOne (G := G) (Set.range μ) := by
1118 intro U
1119 have hsubset :
1120 Set.range μ \ (U : Set G) ⊆ μ '' {x : X | μ x ∉ (U : Set G)} := by
1121 rintro y ⟨⟨x, rfl⟩, hxU⟩
1122 exact ⟨x, hxU, rfl⟩
1123 exact (hμ U).image μ |>.subset hsubset
1125/-- Convergence to `1` is preserved by a continuous homomorphism. -/
1126theorem comp
1127 {H : Type*} [TopologicalSpace H] [Group H]
1128 {μ : X → G}
1129 (hμ : FamilyConvergesToOne (G := G) μ) (f : G →ₜ* H) :
1130 FamilyConvergesToOne (G := H) (fun x => f (μ x)) := by
1131 intro U
1132 simpa using hμ (OpenSubgroup.comap (f := (f : G →* H)) f.continuous U)
1134/-- Range convergence implies family convergence for injectively indexed families. -/
1135theorem of_set_of_injective {μ : X → G}
1136 (hμ : Generation.ConvergesToOne (G := G) (Set.range μ))
1137 (hinj : Function.Injective μ) :
1138 FamilyConvergesToOne (G := G) μ := by
1139 intro U
1140 have himage :
1141 μ '' {x : X | μ x ∉ (U : Set G)} = Set.range μ \ (U : Set G) := by
1142 ext y
1143 constructor
1144 · rintro ⟨x, hxU, rfl⟩
1145 exact ⟨⟨x, rfl⟩, hxU⟩
1146 · rintro ⟨⟨x, rfl⟩, hxU⟩
1147 exact ⟨x, hxU, rfl⟩
1148 letI : Finite (μ '' {x : X | μ x ∉ (U : Set G)}) := by
1149 rw [himage]
1150 exact (hμ U).to_subtype
1151 exact Finite.Set.finite_of_finite_image {x : X | μ x ∉ (U : Set G)} (by
1152 intro a _ b _ hab
1153 exact hinj hab)
1155/-- Families indexed by a finite type converge to `1`. -/
1156theorem of_finite_domain [Finite X] (μ : X → G) :
1157 FamilyConvergesToOne (G := G) μ := by
1158 intro U
1159 exact Set.finite_univ.subset (by intro x _; trivial)
1163/-- A family which both converges to `1` and topologically generates the target. -/
1164structure ConvergingGeneratingMap
1165 (X : Type v)
1166 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
1167 toFun : X → G
1168 convergesToOne : FamilyConvergesToOne (G := G) toFun
1169 generates : Generation.TopologicallyGenerates (G := G) (Set.range toFun)
1171namespace ConvergingGeneratingMap
1173variable {X Y : Type v}
1174variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1176instance instCoeFunConvergingGeneratingMap :
1177 CoeFun (ConvergingGeneratingMap X G) (fun _ => X → G) where
1178 coe φ := φ.toFun
1180@[simp] theorem toFun_eq_coe (φ : ConvergingGeneratingMap X G) :
1181 φ.toFun = (φ : X → G) := rfl
1183/-- Reindexing along an equivalence preserves family convergence and generation. -/
1184def reindex (φ : ConvergingGeneratingMap X G) (e : Y ≃ X) :
1185 ConvergingGeneratingMap Y G where
1186 toFun := fun y => φ (e y)
1187 convergesToOne := by
1188 intro U
1189 have hsubset :
1190 {y : Y | φ (e y) ∉ (U : Set G)} ⊆
1191 e.symm '' {x : X | φ x ∉ (U : Set G)} := by
1192 intro y hy
1193 exact ⟨e y, hy, by simp only [Equiv.symm_apply_apply]⟩
1194 exact (φ.convergesToOne U).image e.symm |>.subset hsubset
1195 generates := by
1196 have hrange : Set.range (fun y : Y => φ (e y)) = Set.range (φ : X → G) := by
1197 ext z
1198 constructor
1199 · rintro ⟨y, rfl⟩
1200 exact ⟨e y, rfl⟩
1201 · rintro ⟨x, rfl⟩
1202 exact ⟨e.symm x, by simp only [Equiv.apply_symm_apply]⟩
1203 simpa [hrange] using φ.generates
1205theorem generatesAndConvergesToOne (φ : ConvergingGeneratingMap X G) :
1206 Generation.GeneratesAndConvergesToOne (G := G) (Set.range (φ : X → G)) :=
1207 ⟨φ.generates, φ.convergesToOne.range⟩
1211/-- Generated-target extension property for a pro-`C` group on a topological space.
1214generated by the chosen map. -/
1216 (X : Type u) [TopologicalSpace X]
1217 (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1218 (ι : X → F) : Prop where
1220 continuous_ι : Continuous ι
1221 generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
1223 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
1224 ProC (G := G) →
1225 ∀ (φ : X → G), Continuous φ →
1226 Generation.TopologicallyGenerates (G := G) (Set.range φ) →
1227 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x
1229/-- The true free pro-`C` universal property implies the generated-target extension property. -/
1231 {X : Type u} [TopologicalSpace X]
1232 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1233 {ι : X → F}
1234 (hι : IsFreeProCGroup (ProC := ProC) ι) :
1235 HasGeneratingTargetExtensionProperty (ProC := ProC) X F ι := by
1236 refine
1238 continuous_ι := hι.continuous_ι
1239 generates_range := hι.generates_range
1240 existsUnique_lift := ?_ }
1241 intro G _ _ _ hG φ hφ _hgen
1242 exact hι.existsUnique_lift hG φ hφ
1244namespace HasGeneratingTargetExtensionProperty
1246variable {X : Type u} [TopologicalSpace X]
1247variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1248variable {ι : X → F}
1250/-- Recover the usual free pro-`C` universal property from the older generated-target interface,
1251provided the pro-`C` predicate is stable under closed subgroups.
1253The proof corestricts an arbitrary target map to the closed subgroup it topologically generates,
1255theorem toFreeProperty
1256 (hι : HasGeneratingTargetExtensionProperty (ProC := ProC) X F ι)
1257 (hClosedSubgroups :
1258 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
1259 ProC (G := G) → (H : ClosedSubgroup G) →
1260 ProC (G := ↥(H : Subgroup G))) :
1261 IsFreeProCGroup (ProC := ProC) ι := by
1262 refine
1264 continuous_ι := hι.continuous_ι
1265 generates_range := hι.generates_range
1266 existsUnique_lift := ?_ }
1267 intro G _ _ _ hG φ hφ
1268 let K : ClosedSubgroup G := Generation.closedSubgroupGenerated (G := G) (Set.range φ)
1269 let φK : X → ↥(K : Subgroup G) := Generation.closedSubgroupGeneratedMap (G := G) φ
1270 have hφKcont : Continuous φK := by
1271 exact Continuous.subtype_mk hφ (fun x => (φK x).2)
1272 have hφKgen :
1273 Generation.TopologicallyGenerates (G := ↥(K : Subgroup G)) (Set.range φK) := by
1274 simpa [φK] using
1275 (Generation.closedSubgroupGeneratedMap_topologicallyGenerates (G := G) φ)
1276 have hK : ProC (G := ↥(K : Subgroup G)) := hClosedSubgroups hG K
1277 rcases hι.existsUnique_lift hK φK hφKcont hφKgen with
1278 ⟨fK, hfK, huniqK⟩
1280 let f : F →* G := incl.comp fK
1281 refine ⟨f, ⟨?_, ?_⟩, ?_⟩
1282 · exact continuous_subtype_val.comp hfK.1
1283 · intro x
1284 exact congrArg Subtype.val (hfK.2 x)
1285 · intro g hg
1286 have hg_mem : ∀ y : F, g y ∈ (K : Subgroup G) := by
1287 let L : Subgroup F := Subgroup.comap g (K : Subgroup G)
1288 have hLclosed : IsClosed ((L : Subgroup F) : Set F) := by
1289 change IsClosed (g ⁻¹' ((K : Subgroup G) : Set G))
1290 exact K.isClosed'.preimage hg.1
1291 have hsub : Subgroup.closure (Set.range ι) ≤ L := by
1292 rw [Subgroup.closure_le]
1293 rintro y ⟨x, rfl⟩
1294 change g (ι x) ∈ (K : Subgroup G)
1295 simpa [K, hg.2 x] using
1296 (Subgroup.le_topologicalClosure (Subgroup.closure (Set.range φ))
1297 (Subgroup.subset_closure ⟨x, rfl⟩))
1298 have htop : (⊤ : Subgroup F) ≤ L := by
1299 have hcl : (Subgroup.closure (Set.range ι)).topologicalClosure ≤ L :=
1300 Subgroup.topologicalClosure_minimal _ hsub hLclosed
1301 have hgen : (Subgroup.closure (Set.range ι)).topologicalClosure = ⊤ := hι.generates_range
1302 simpa [hgen] using hcl
1303 intro y
1304 exact htop trivial
1305 let gK : F →* ↥(K : Subgroup G) :=
1306 { toFun := fun y => ⟨g y, hg_mem y⟩
1307 map_one' := by
1308 apply Subtype.ext
1310 map_mul' := by
1311 intro a b
1312 apply Subtype.ext
1314 have hgKcont : Continuous gK :=
1315 Continuous.subtype_mk hg.1 hg_mem
1316 have hgKfac : ∀ x, gK (ι x) = φK x := by
1317 intro x
1318 apply Subtype.ext
1319 exact hg.2 x
1320 have hgK_eq : gK = fK := huniqK gK ⟨hgKcont, hgKfac⟩
1321 apply MonoidHom.ext
1322 intro y
1323 change g y = fK y
1324 calc
1325 g y = (gK y : G) := rfl
1326 _ = (fK y : G) := by rw [hgK_eq]
1327 _ = f y := rfl
1331/-- The generated-target extension property is the true free pro-`C` universal property when the
1332class of pro-`C` groups is stable under closed subgroups. -/
1334 {X : Type u} [TopologicalSpace X]
1335 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1336 {ι : X → F}
1337 (hι : HasGeneratingTargetExtensionProperty (ProC := ProC) X F ι)
1338 (hClosedSubgroups :
1339 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
1340 ProC (G := G) → (H : ClosedSubgroup G) →
1341 ProC (G := ↥(H : Subgroup G))) :
1342 IsFreeProCGroup (ProC := ProC) ι :=
1343 hι.toFreeProperty hClosedSubgroups
1345/-- Pointed free pro-`C` group on a pointed topological space. -/
1347 (X : Type u) [TopologicalSpace X] (x0 : X)
1348 (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1349 (ι : X → F) : Prop where
1351 continuous_ι : Continuous ι
1352 map_base : ι x0 = 1
1353 generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
1355 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
1356 ProC (G := G) →
1357 ∀ (φ : X → G), Continuous φ → φ x0 = 1 →
1358 Generation.TopologicallyGenerates (G := G) (Set.range φ) →
1359 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x
1361/-- Free pro-`C` group on a set converging to `1`. -/
1363 (X : Type v)
1364 (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1365 (ι : X → F) : Prop where
1367 convergesToOne : FamilyConvergesToOne (G := F) ι
1368 generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
1370 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
1371 ProC (G := G) →
1372 ∀ (φ : X → G), FamilyConvergesToOne (G := G) φ →
1373 Generation.TopologicallyGenerates (G := G) (Set.range φ) →
1374 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x
1376/-- The canonical map of a free pro-`C` group on a topological space is injective whenever the
1377predicate supplies enough separating pro-`C` targets. -/
1378theorem freeProCGroupOn_injective
1379 {X : Type u} [TopologicalSpace X]
1380 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1381 {ι : X → F}
1382 (hι : IsFreeProCGroup (ProC := ProC) ι)
1383 (hsep :
1384 ∀ ⦃x y : X⦄, x ≠ y →
1385 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A),
1386 ProC (G := A) ∧
1387 ∃ φ : X → A, Continuous φ ∧
1388 Generation.TopologicallyGenerates (G := A) (Set.range φ) ∧ φ x ≠ φ y) :
1389 Function.Injective ι := by
1390 intro x y hEq
1391 by_contra hxy
1392 rcases hsep hxy with ⟨A, _instGroupA, _instTopA, _instTopGroupA, hA, φ, hφ, hgenφ, hφxy⟩
1393 rcases hι.existsUnique_lift hA φ hφ with ⟨f, hf, _huniq⟩
1394 have hcontr : φ x = φ y := by
1395 simpa [hf.2 x, hf.2 y] using congrArg f hEq
1396 exact hφxy hcontr
1398/-- Under an explicit nontrivial cyclic pro-`C` target hypothesis, the identity does not lie in
1399the image of the topological basis of a free pro-`C` group. -/
1401 {X : Type u} [TopologicalSpace X] [Nonempty X]
1402 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1403 {ι : X → F}
1404 (hι : IsFreeProCGroup (ProC := ProC) ι)
1405 (hnontrivial :
1406 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A),
1407 ProC (G := A) ∧ ∃ a : A, a ≠ 1 ∧
1408 Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
1409 (1 : F) ∉ Set.range ι := by
1410 intro h1
1411 rcases h1 with ⟨x, hx⟩
1412 rcases hnontrivial with ⟨A, _instGroupA, _instTopA, _instTopGroupA, hA, a, ha1, hgena⟩
1413 let φ : X → A := fun _ => a
1414 have hφ : Continuous φ := continuous_const
1415 have hrange : Set.range φ = ({a} : Set A) := by
1416 ext b
1417 constructor
1418 · rintro ⟨y, rfl⟩
1419 simp only [mem_singleton_iff, φ]
1420 · intro hb
1421 rw [Set.mem_singleton_iff] at hb
1422 subst b
1423 exact ⟨Classical.choice ‹Nonempty X›, rfl⟩
1424 have hgenφ : Generation.TopologicallyGenerates (G := A) (Set.range φ) := by
1425 simpa [hrange] using hgena
1426 rcases hι.existsUnique_lift hA φ hφ with ⟨f, hf, _huniq⟩
1427 have haeq : a = 1 := by
1428 simpa [φ, hx] using (hf.2 x).symm
1429 exact ha1 haeq
1431/-- Under an explicit nontrivial cyclic pro-`C` target hypothesis, the identity does not lie in a
1432basis converging to `1`. -/
1434 {X : Type u}
1435 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1436 {ι : X → F}
1437 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1438 (hnontrivial :
1439 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A),
1440 ProC (G := A) ∧ ∃ a : A, a ≠ 1 ∧
1441 Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
1442 (1 : F) ∉ Set.range ι := by
1443 classical
1444 intro h1
1445 rcases h1 with ⟨x, hx⟩
1446 rcases hnontrivial with ⟨A, _instGroupA, _instTopA, _instTopGroupA, hA, a, ha1, hgena⟩
1447 let φ : X → A := fun z => if z = x then a else 1
1448 have hφconv : FamilyConvergesToOne (G := A) φ := by
1449 intro U
1450 have hsubset : {z : X | φ z ∉ (U : Set A)} ⊆ ({x} : Set X) := by
1451 intro z hz
1452 by_cases hzx : z = x
1453 · simp only [hzx, mem_singleton_iff]
1454 · exfalso
1455 exact hz (by simp only [hzx, ↓reduceIte, SetLike.mem_coe, one_mem, φ])
1456 exact (Set.finite_singleton x).subset hsubset
1457 have hφgen : Generation.TopologicallyGenerates (G := A) (Set.range φ) := by
1458 have hsub : ({a} : Set A) ⊆ Set.range φ := by
1459 intro z hz
1460 rw [Set.mem_singleton_iff] at hz
1461 subst z
1462 exact ⟨x, by simp only [↓reduceIte, φ]⟩
1463 exact Generation.topologicallyGenerates_mono (G := A) hgena hsub
1464 rcases hι.existsUnique_lift hA φ hφconv hφgen with ⟨f, hf, _⟩
1465 have haeq : a = 1 := by
1466 simpa [φ, hx] using (hf.2 x).symm
1467 exact ha1 haeq
1469/-- Under the same nontrivial cyclic-target hypothesis, the basis map for a free pro-`C` group on
1470a set converging to `1` is injective. -/
1472 {X : Type u}
1473 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1474 {ι : X → F}
1475 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1476 (hnontrivial :
1477 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A),
1478 ProC (G := A) ∧ ∃ a : A, a ≠ 1 ∧
1479 Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
1480 Function.Injective ι := by
1481 classical
1482 intro x y hEq
1483 by_contra hxy
1484 rcases hnontrivial with ⟨A, _instGroupA, _instTopA, _instTopGroupA, hA, a, ha1, hgena⟩
1485 have hyx : y ≠ x := by
1486 intro hyx'
1487 exact hxy hyx'.symm
1488 let φ : X → A := fun z => if z = x then a else 1
1489 have hφconv : FamilyConvergesToOne (G := A) φ := by
1490 intro U
1491 have hsubset : {z : X | φ z ∉ (U : Set A)} ⊆ ({x} : Set X) := by
1492 intro z hz
1493 by_cases hzx : z = x
1494 · simp only [hzx, mem_singleton_iff]
1495 · exfalso
1496 exact hz (by simp only [hzx, ↓reduceIte, SetLike.mem_coe, one_mem, φ])
1497 exact (Set.finite_singleton x).subset hsubset
1498 have hφgen : Generation.TopologicallyGenerates (G := A) (Set.range φ) := by
1499 have hsub : ({a} : Set A) ⊆ Set.range φ := by
1500 intro z hz
1501 rw [Set.mem_singleton_iff] at hz
1502 subst z
1503 exact ⟨x, by simp only [↓reduceIte, φ]⟩
1504 exact Generation.topologicallyGenerates_mono (G := A) hgena hsub
1505 rcases hι.existsUnique_lift hA φ hφconv hφgen with ⟨f, hf, _⟩
1506 have hfa : f (ι x) = a := by
1507 simpa [φ] using hf.2 x
1508 have hf1 : f (ι y) = 1 := by
1509 simpa [φ, hyx] using hf.2 y
1510 have haeq : a = 1 := by
1511 rw [← hfa, ← hf1]
1512 exact congrArg f hEq
1513 exact ha1 haeq
1515/-- A nontrivial cyclic topological group has a nontrivial singleton topological generator. -/
1517 {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
1518 [IsCyclic A] [Nontrivial A] :
1519 ∃ a : A, a ≠ 1 ∧ Generation.TopologicallyGenerates (G := A) ({a} : Set A) := by
1520 obtain ⟨a, ha⟩ := IsCyclic.exists_generator (α := A)
1521 have ha1 : a ≠ 1 := by
1522 intro hEq
1523 have hallOne : ∀ x : A, x = 1 := by
1524 intro x
1525 obtain ⟨n, hn⟩ := Subgroup.mem_zpowers_iff.mp (ha x)
1526 simpa [hEq] using hn.symm
1527 exact not_subsingleton A ⟨fun x y => by rw [hallOne x, hallOne y]⟩
1528 refine ⟨a, ha1, ?_⟩
1529 rw [Generation.TopologicallyGenerates]
1530 apply top_unique
1531 intro x _
1532 exact Subgroup.le_topologicalClosure _ <| by
1533 simpa [Subgroup.zpowers_eq_closure] using ha x
1535/-- A concrete finite-group class containing a nontrivial finite cyclic group admits a
1538 (C : ProCGroups.FiniteGroupClass.{u})
1539 (hquot : ProCGroups.FiniteGroupClass.QuotientClosed C)
1540 (hcyc :
1541 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
1542 C A ∧ IsCyclic A ∧ Nontrivial A) :
1543 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A),
1544 (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := A) ∧
1545 ∃ a : A, a ≠ 1 ∧ Generation.TopologicallyGenerates (G := A) ({a} : Set A) := by
1546 rcases hcyc with ⟨A, _instGroupA, _instFiniteA, hCA, hAcyc, hAnontriv⟩
1547 let _ : TopologicalSpace A := ⊥
1548 let _ : DiscreteTopology A := ⟨rfl⟩
1549 let _ : IsTopologicalGroup A := by infer_instance
1550 letI : IsCyclic A := hAcyc
1551 letI : Nontrivial A := hAnontriv
1552 have hAProC : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := A) := by
1554 (C := C) (G := A) hquot hCA
1555 rcases exists_nontrivial_singleton_topologicalGenerator (A := A) with ⟨a, ha1, hgena⟩
1556 exact ⟨A, inferInstance, inferInstance, inferInstance, hAProC, a, ha1, hgena⟩
1558/-- For a finite-rank free pro-`C` group, any generating family with the same finite cardinality
1559is again a converging-set basis. -/
1561 {X : Type u} {Y : Type u}
1562 [Finite X] [Finite Y]
1563 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1564 {ι : X → F} {μ : Y → F}
1565 (hF : ProCGroups.IsProfiniteGroup F)
1566 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1567 (hcard : Cardinal.mk X = Cardinal.mk Y)
1568 (hgen : Generation.TopologicallyGenerates (G := F) (Set.range μ)) :
1569 IsFreeProCGroupOnConvergingSet (ProC := ProC) Y F μ := by
1570 classical
1571 letI : CompactSpace F := ProCGroups.IsProfiniteGroup.compactSpace hF
1572 letI : T2Space F := ProCGroups.IsProfiniteGroup.t2Space hF
1573 letI : TotallyDisconnectedSpace F := ProCGroups.IsProfiniteGroup.totallyDisconnectedSpace hF
1574 have hXY : Nonempty (X ≃ Y) := by
1575 simpa [← Cardinal.eq] using hcard
1576 let eXY : X ≃ Y := Classical.choice hXY
1577 let ψ : X → F := fun x => μ (eXY x)
1578 have hψconv : FamilyConvergesToOne (G := F) ψ := by
1579 exact FamilyConvergesToOne.of_finite_domain (G := F) ψ
1580 have hψgen : Generation.TopologicallyGenerates (G := F) (Set.range ψ) := by
1581 have hrange : Set.range ψ = Set.range μ := by
1582 ext z
1583 constructor
1584 · rintro ⟨x, rfl⟩
1585 exact ⟨eXY x, rfl⟩
1586 · rintro ⟨y, rfl⟩
1587 exact ⟨eXY.symm y, by simp only [Equiv.apply_symm_apply, ψ]⟩
1588 simpa [hrange] using hgen
1589 rcases hι.existsUnique_lift hι.isProC ψ hψconv hψgen with ⟨σ, hσ, hσuniq⟩
1590 have hrangeμ : Set.range μ ⊆ (σ.range : Set F) := by
1591 rintro z ⟨y, rfl⟩
1592 exact ⟨ι (eXY.symm y), by simpa [ψ] using hσ.2 (eXY.symm y)⟩
1593 have hσgen : Generation.TopologicallyGenerates (G := F) ((σ.range : Set F)) :=
1594 Generation.topologicallyGenerates_mono (G := F) hgen hrangeμ
1595 have hσclosed : IsClosed ((σ.range : Set F)) := by
1596 simpa using (isCompact_range hσ.1).isClosed
1597 have hσclosure_le : (σ.range : Subgroup F).topologicalClosure ≤ σ.range :=
1598 Subgroup.topologicalClosure_minimal _ le_rfl hσclosed
1599 have hσclosure_top : (σ.range : Subgroup F).topologicalClosure = ⊤ := by
1600 have htop :
1601 (Subgroup.closure (σ.range : Set F)).topologicalClosure = (⊤ : Subgroup F) := by
1602 simpa [Generation.TopologicallyGenerates] using hσgen
1603 have hclosure_eq : (σ.range : Subgroup F) = Subgroup.closure (σ.range : Set F) := by
1604 simpa using (Subgroup.closure_eq (σ.range)).symm
1605 rw [hclosure_eq]
1606 exact htop
1607 have hσrange_top : σ.range = ⊤ := by
1608 apply top_unique
1609 intro z hz
1610 have hz' : z ∈ ((σ.range : Subgroup F).topologicalClosure : Set F) := by
1611 rw [hσclosure_top]
1612 simp only [Subgroup.coe_top, mem_univ]
1613 exact hσclosure_le hz'
1614 have hσsurj : Function.Surjective σ := by
1615 intro z
1616 have hz : z ∈ (σ.range : Set F) := by
1617 simp only [hσrange_top, Subgroup.coe_top, mem_univ]
1618 simpa using hz
1619 let σc : ContinuousMonoidHom F F :=
1620 { toMonoidHom := σ
1621 continuous_toFun := hσ.1 }
1622 have hFG : _root_.ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated F := by
1623 letI : Fintype Y := Fintype.ofFinite Y
1624 refine ⟨Finset.univ.image μ, ?_⟩
1625 simpa [Finset.coe_image] using hgen
1626 rcases
1627 (_root_.ProCGroups.FiniteGeneration.surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated
1628 (G := F)) hFG σc hσsurj with
1629 ⟨e, he⟩
1630 refine ⟨hι.isProC, ?_, hgen, ?_⟩
1631 · exact FamilyConvergesToOne.of_finite_domain (G := F) μ
1632 · intro G _ _ _ hG φ hφ hgenφ
1633 let φX : X → G := fun x => φ (eXY x)
1634 have hφXconv : FamilyConvergesToOne (G := G) φX := by
1635 exact FamilyConvergesToOne.of_finite_domain (G := G) φX
1636 have hφXgen : Generation.TopologicallyGenerates (G := G) (Set.range φX) := by
1637 have hrange : Set.range φX = Set.range φ := by
1638 ext z
1639 constructor
1640 · rintro ⟨x, rfl⟩
1641 exact ⟨eXY x, rfl⟩
1642 · rintro ⟨y, rfl⟩
1643 exact ⟨eXY.symm y, by simp only [Equiv.apply_symm_apply, φX]⟩
1644 simpa [hrange] using hgenφ
1645 rcases hι.existsUnique_lift hG φX hφXconv hφXgen with ⟨fX, hfX, hfXuniq⟩
1646 let fY : F →* G := fX.comp e.symm.toMonoidHom
1647 refine ⟨fY, ⟨hfX.1.comp e.symm.continuous, ?_⟩, ?_⟩
1648 · intro y
1649 have hpre : e.symm (μ y) = ι (eXY.symm y) := by
1650 apply e.injective
1651 calc
1652 e (e.symm (μ y)) = μ y := by simp only [ContinuousMulEquiv.apply_symm_apply]
1653 _ = σ (ι (eXY.symm y)) := by
1654 symm
1655 simpa [ψ] using hσ.2 (eXY.symm y)
1656 _ = e (ι (eXY.symm y)) := by simpa [σc] using (he (ι (eXY.symm y))).symm
1657 calc
1658 fY (μ y) = fX (e.symm (μ y)) := rfl
1659 _ = fX (ι (eXY.symm y)) := by rw [hpre]
1660 _ = φX (eXY.symm y) := hfX.2 (eXY.symm y)
1661 _ = φ y := by simp only [Equiv.apply_symm_apply, φX]
1662 · intro g hg
1663 have hcomp : g.comp e.toMonoidHom = fX := by
1664 apply hfXuniq
1665 refine ⟨hg.1.comp e.continuous, ?_⟩
1666 intro x
1667 calc
1668 (g.comp e.toMonoidHom) (ι x) = g (e (ι x)) := rfl
1669 _ = g (σ (ι x)) := by
1670 exact congrArg g (by simpa [σc] using he (ι x))
1671 _ = g (μ (eXY x)) := by
1672 exact congrArg g (by simpa [ψ] using hσ.2 x)
1673 _ = φ (eXY x) := hg.2 (eXY x)
1674 _ = φX x := rfl
1675 ext z
1676 have hz := congrArg (fun k : F →* G => k (e.symm z)) hcomp
1677 have hz' : g (e (e.symm z)) = fX (e.symm z) := by
1678 change (g.comp e.toMonoidHom) (e.symm z) = fX (e.symm z)
1679 exact hz
1680 calc
1681 g z = g (e (e.symm z)) := by
1682 exact congrArg g (e.apply_symm_apply z).symm
1683 _ = fX (e.symm z) := hz'
1684 _ = fY z := rfl
1686/-- Concrete finite-group-class specialization of `finite_generatingFamily_is_basis`. -/
1688 (C : ProCGroups.FiniteGroupClass.{u})
1689 {X : Type u} {Y : Type u}
1690 [Finite X] [Finite Y]
1691 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1692 {ι : X → F} {μ : Y → F}
1693 (hι :
1695 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
1696 (hcard : Cardinal.mk X = Cardinal.mk Y)
1697 (hgen : Generation.TopologicallyGenerates (G := F) (Set.range μ)) :
1699 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) Y F μ := by
1701 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
1702 (hF := ProCGroups.ProC.isProfiniteGroup_of_finiteGroupClassProCPredicate C hι.isProC)
1703 hι hcard hgen
1705/-- Concrete finite-group-class specialization when a nontrivial cyclic target is available. -/
1707 (C : ProCGroups.FiniteGroupClass.{u})
1708 (hquot : ProCGroups.FiniteGroupClass.QuotientClosed C)
1709 (hcyc :
1710 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
1711 C A ∧ IsCyclic A ∧ Nontrivial A)
1712 {X : Type u} {Y : Type u}
1713 [Finite X] [Finite Y]
1714 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1715 {ι : X → F} {μ : Y → F}
1716 (hι :
1718 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
1719 (hcard : Cardinal.mk X = Cardinal.mk Y)
1720 (hgen : Generation.TopologicallyGenerates (G := F) (Set.range μ)) :
1722 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) Y F μ := by
1723 rcases exists_nontrivial_topologicallyCyclic_proC_of_finiteGroupClass C hquot hcyc with
1724 ⟨A, _instGroupA, _instTopA, _instTopGroupA, hA, a, ha1, hgena⟩
1726 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
1727 (hF := ProCGroups.ProC.isProfiniteGroup_of_finiteGroupClassProCPredicate C hι.isProC)
1728 hι hcard hgen
1730/-- If a continuous homomorphism has range containing a topological generating set, then it is
1731surjective between profinite groups. -/
1733 {X : Type u}
1734 {F : Type u} [Group F] [TopologicalSpace F]
1735 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1736 (hF : ProCGroups.IsProfiniteGroup F)
1737 (hG : ProCGroups.IsProfiniteGroup G)
1738 {ι : X → G}
1739 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range ι))
1740 {σ : F →* G} (hσ : Continuous σ)
1741 (hsub : Set.range ι ⊆ (σ.range : Set G)) :
1742 Function.Surjective σ := by
1743 letI : CompactSpace F := ProCGroups.IsProfiniteGroup.compactSpace hF
1744 letI : T2Space G := ProCGroups.IsProfiniteGroup.t2Space hG
1745 have hσgen : Generation.TopologicallyGenerates (G := G) ((σ.range : Set G)) :=
1746 Generation.topologicallyGenerates_mono (G := G) hgen hsub
1747 have hσclosed : IsClosed ((σ.range : Set G)) := by
1748 simpa using (isCompact_range hσ).isClosed
1749 have hσclosure_le : (σ.range : Subgroup G).topologicalClosure ≤ σ.range :=
1750 Subgroup.topologicalClosure_minimal _ le_rfl hσclosed
1751 have hσclosure_top : (σ.range : Subgroup G).topologicalClosure = ⊤ := by
1752 have htop :
1753 (Subgroup.closure (σ.range : Set G)).topologicalClosure = (⊤ : Subgroup G) := by
1754 simpa [Generation.TopologicallyGenerates] using hσgen
1755 have hclosure_eq : (σ.range : Subgroup G) = Subgroup.closure (σ.range : Set G) := by
1756 simpa using (Subgroup.closure_eq (σ.range)).symm
1757 rw [hclosure_eq]
1758 exact htop
1759 have hσrange_top : σ.range = ⊤ := by
1760 apply top_unique
1761 intro z hz
1762 have hz' : z ∈ ((σ.range : Subgroup G).topologicalClosure : Set G) := by
1763 rw [hσclosure_top]
1764 simp only [Subgroup.coe_top, mem_univ]
1765 exact hσclosure_le hz'
1766 intro z
1767 have hz : z ∈ (σ.range : Set G) := by
1768 simp only [hσrange_top, Subgroup.coe_top, mem_univ]
1769 simpa using hz
1771/-- A topologically finitely generated free pro-`C` group on a converging set has finite basis,
1774 {X : Type u}
1775 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1776 {ι : X → F}
1777 (hFprof : ProCGroups.IsProfiniteGroup F)
1778 (hfg : FiniteGeneration.TopologicallyFinitelyGenerated F)
1779 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1780 (hnontrivial :
1781 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A),
1782 ProC (G := A) ∧ ∃ a : A, a ≠ 1 ∧
1783 Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
1784 Finite X := by
1785 classical
1786 by_cases hXfin : Finite X
1787 · exact hXfin
1788 · have hXinf : Infinite X := by
1789 by_contra hXnotinf
1790 exact hXfin (not_infinite_iff_finite.mp hXnotinf)
1791 letI : Infinite X := hXinf
1792 letI : Nonempty X := Infinite.nonempty (α := X)
1793 letI : CompactSpace F := ProCGroups.IsProfiniteGroup.compactSpace hFprof
1794 letI : T2Space F := ProCGroups.IsProfiniteGroup.t2Space hFprof
1795 letI : TotallyDisconnectedSpace F := ProCGroups.IsProfiniteGroup.totallyDisconnectedSpace hFprof
1796 have hFspace : InverseSystems.IsProfiniteSpace F :=
1797 (InverseSystems.isProfiniteSpace_iff_compact_t2_totallyDisconnected (X := F)).2
1798 ⟨inferInstance, inferInstance, inferInstance⟩
1799 rcases
1800 (FiniteGeneration.topologicallyFinitelyGenerated_iff_exists_topologicallyGeneratedByAtMost
1801 (G := F)).mp hfg with
1802 ⟨_n, s, _hsle, hgen⟩
1803 have hsle : Cardinal.mk ↥s ≤ Cardinal.mk X := by
1804 exact (show Cardinal.mk ↥s < Cardinal.mk X from calc
1805 Cardinal.mk ↥s < Cardinal.aleph0 := by
1806 exact (Cardinal.mk_lt_aleph0_iff).2 (Finite.of_fintype ↥s)
1807 _ ≤ Cardinal.mk X := Cardinal.aleph0_le_mk X).le
1808 have hsle' : Cardinal.mk ↥s ≤ Cardinal.mk (Set.univ : Set X) := by
1809 simpa using hsle
1810 obtain ⟨p, _hpSub, hpCard⟩ := (Cardinal.le_mk_iff_exists_subset
1811 (c := Cardinal.mk ↥s) (s := (Set.univ : Set X))).1 hsle'
1812 have hpEquiv : Nonempty (p ≃ ↥s) := by
1813 simpa [← Cardinal.eq] using hpCard
1814 let e : p ≃ ↥s := Classical.choice hpEquiv
1815 have hpfinite : p.Finite :=
1816 Set.finite_coe_iff.mp (Finite.of_equiv (↥s) e.symm)
1817 let φ : X → F := fun x => if hx : x ∈ p then (e ⟨x, hx⟩ : F) else 1
1818 have hφconv : FamilyConvergesToOne (G := F) φ := by
1819 intro U
1820 have hsubset : {x : X | φ x ∉ (U : Set F)} ⊆ p := by
1821 intro x hx
1822 by_cases hxp : x ∈ p
1823 · exact hxp
1824 · exfalso
1825 exact hx (by simp only [hxp, ↓reduceDIte, SetLike.mem_coe, one_mem, φ])
1826 exact hpfinite.subset hsubset
1827 have hφgen : Generation.TopologicallyGenerates (G := F) (Set.range φ) := by
1828 have hsub : (s : Set F) ⊆ Set.range φ := by
1829 intro z hz
1830 let a : ↥s := ⟨z, hz⟩
1831 refine ⟨(e.symm a).1, ?_⟩
1832 have hp : (e.symm a).1 ∈ p := (e.symm a).2
1833 simp only [hp, ↓reduceDIte, Subtype.coe_eta, Equiv.apply_symm_apply, φ, a]
1834 exact Generation.topologicallyGenerates_mono (G := F) hgen hsub
1835 rcases hι.existsUnique_lift hι.isProC φ hφconv hφgen with ⟨σ, hσ, _⟩
1836 have hφsubσ : Set.range φ ⊆ (σ.range : Set F) := by
1837 rintro z ⟨x, rfl⟩
1838 exact ⟨ι x, hσ.2 x⟩
1839 have hσsurj : Function.Surjective σ :=
1841 (hF := hFprof) (hG := hFprof) hφgen hσ.1 hφsubσ
1842 let σc : ContinuousMonoidHom F F := {
1843 toMonoidHom := σ
1844 continuous_toFun := hσ.1
1845 }
1846 rcases
1847 (FiniteGeneration.surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated
1848 (G := F))
1849 hfg σc hσsurj with
1850 ⟨eσ, heσ⟩
1851 have hσinj : Function.Injective σ := by
1852 intro a b hab
1853 have h' : eσ a = eσ b := by
1854 calc
1855 eσ a = σ a := by simpa [σc] using heσ a
1856 _ = σ b := hab
1857 _ = eσ b := by simpa [σc] using (heσ b).symm
1858 exact eσ.injective h'
1859 have hιinj : Function.Injective ι :=
1860 freeProCGroupOnConvergingSet_injective (hι := hι) hnontrivial
1861 have hφinj : Function.Injective φ := by
1862 intro x y hxy
1863 apply hιinj
1864 apply hσinj
1865 calc
1866 σ (ι x) = φ x := hσ.2 x
1867 _ = φ y := hxy
1868 _ = σ (ι y) := (hσ.2 y).symm
1869 have hφsub : Set.range φ ⊆ (s : Set F) ∪ ({1} : Set F) := by
1870 rintro z ⟨x, rfl⟩
1871 by_cases hxp : x ∈ p
1872 · left
1873 simp only [hxp, ↓reduceDIte, Subtype.coe_prop, φ]
1874 · right
1875 simp only [hxp, ↓reduceDIte, mem_singleton_iff, φ]
1876 have hφfin : (Set.range φ).Finite :=
1877 (s.finite_toSet.union (Set.finite_singleton (1 : F))).subset hφsub
1878 have hXlt : Cardinal.mk X < Cardinal.aleph0 := by
1879 calc
1880 Cardinal.mk X = Cardinal.mk (Set.range φ) := by
1881 simpa using (Cardinal.mk_range_eq φ hφinj).symm
1882 _ < Cardinal.aleph0 := by
1883 exact (Cardinal.mk_lt_aleph0_iff).2 hφfin.to_subtype
1884 exact False.elim (hXfin ((Cardinal.mk_lt_aleph0_iff).1 hXlt))
1886/-- A fixed free pro-`C` group on a set converging to `1` admits a continuous epimorphism onto any
1887profinite pro-`C` target generated by the image of its basis. -/
1889 {X : Type u}
1890 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1891 {ι : X → F}
1892 (hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1893 (hFprof : ProCGroups.IsProfiniteGroup F)
1894 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1895 (hG : ProC (G := G))
1896 (hGprof : ProCGroups.IsProfiniteGroup G)
1897 (φ : X → G)
1898 (hφ : FamilyConvergesToOne (G := G) φ)
1899 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
1900 ∃ ψ : F →* G, Continuous ψ ∧ Function.Surjective ψ ∧ ∀ x, ψ (ι x) = φ x := by
1901 rcases hF.existsUnique_lift hG φ hφ hgen with ⟨ψ, hψ, _⟩
1902 have hsub : Set.range φ ⊆ (ψ.range : Set G) := by
1903 rintro z ⟨x, rfl⟩
1904 exact ⟨ι x, hψ.2 x⟩
1905 have hψsurj : Function.Surjective ψ :=
1907 (hF := hFprof) (hG := hGprof) hgen hψ.1 hsub
1908 exact ⟨ψ, hψ.1, hψsurj, hψ.2⟩
1910/-- The pro-`C` completion of the abstract free group on a finite basis is free pro-`C` on that
1911basis. -/
1913 {X : Type u} [Finite X]
1914 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
1915 [DiscreteTopology (FreeGroup X)]
1916 {Fhat : Type u} [Group Fhat] [TopologicalSpace Fhat] [IsTopologicalGroup Fhat]
1917 {ι : FreeGroup X →ₜ* Fhat}
1918 (hι : ProCGroups.Completion.IsProCCompletion ProC (FreeGroup X) Fhat ι) :
1919 IsFreeProCGroupOnConvergingSet (ProC := ProC) X Fhat
1920 (fun x => ι (FreeGroup.of x)) := by
1921 refine ⟨hι.isProC, ?_, ?_, ?_⟩
1922 · exact FamilyConvergesToOne.of_finite_domain (G := Fhat)
1923 (fun x : X => ι (FreeGroup.of x))
1924 · have himage :
1925 ι '' Set.range (FreeGroup.of : X → FreeGroup X) =
1926 Set.range (fun x : X => ι (FreeGroup.of x)) := by
1927 simpa [Function.comp] using
1928 (Set.range_comp ι (FreeGroup.of : X → FreeGroup X)).symm
1929 have hclosure :
1930 Subgroup.closure (Set.range fun x : X => ι (FreeGroup.of x)) =
1931 ι.toMonoidHom.range := by
1932 calc
1933 Subgroup.closure (Set.range fun x : X => ι (FreeGroup.of x))
1934 = Subgroup.map ι.toMonoidHom
1935 (Subgroup.closure (Set.range (FreeGroup.of : X → FreeGroup X))) := by
1936 simpa [himage] using
1937 (ι.toMonoidHom.map_closure (Set.range (FreeGroup.of : X → FreeGroup X))).symm
1938 _ = ι.toMonoidHom.range := by
1939 rw [FreeGroup.closure_range_of X, MonoidHom.range_eq_map]
1940 rw [Generation.TopologicallyGenerates, hclosure]
1941 rw [SetLike.ext'_iff, Subgroup.topologicalClosure_coe, Subgroup.coe_top]
1942 simpa [DenseRange, MonoidHom.coe_range, dense_iff_closure_eq] using hι.denseRange
1943 · intro G _ _ _ hG φ _hφ hgen
1944 let φfree : FreeGroup X →ₜ* G :=
1945 { toMonoidHom := FreeGroup.lift φ
1946 continuous_toFun := by
1947 simpa using (continuous_of_discreteTopology : Continuous (FreeGroup.lift φ)) }
1948 let φhat : Fhat →ₜ* G := hι.lift hG φfree
1949 refine ⟨φhat.toMonoidHom, ?_, ?_⟩
1950 · refine ⟨φhat.continuous_toFun, ?_⟩
1951 intro x
1952 have hfac := congrArg (fun ψ : FreeGroup X →ₜ* G => ψ (FreeGroup.of x))
1953 (hι.lift_spec hG φfree)
1954 have hfree : φfree (FreeGroup.of x) = φ x := by
1955 change FreeGroup.lift φ (FreeGroup.of x) = φ x
1956 simp only [FreeGroup.lift_apply_of]
1957 exact hfac.trans hfree
1958 · intro g hg
1959 let gCont : Fhat →ₜ* G := { toMonoidHom := g, continuous_toFun := hg.1 }
1960 have hfac' : gCont.comp ι = φfree := by
1961 apply ContinuousMonoidHom.toMonoidHom_injective
1962 ext x
1963 change g (ι (FreeGroup.of x)) = FreeGroup.lift φ (FreeGroup.of x)
1964 exact (hg.2 x).trans (by simp only [FreeGroup.lift_apply_of])
1965 exact congrArg ContinuousMonoidHom.toMonoidHom (hι.lift_unique hG φfree hfac')
1967namespace IsFreeProCGroupOnConvergingSet
1969variable {X : Type v}
1970variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1971variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
1972variable {ι : X → F}
1974/-- The lift supplied by the corresponding free pro-`C` universal property. -/
1975noncomputable def lift
1976 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1977 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1978 (hG : ProC (G := G)) (φ : X → G)
1979 (hφ : FamilyConvergesToOne (G := G) φ)
1980 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
1981 F →* G :=
1982 Classical.choose (ExistsUnique.exists (hι.existsUnique_lift hG φ hφ hgen))
1984/-- The universal-property lift has the prescribed values on the chosen generators. -/
1985theorem lift_spec
1986 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1987 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1988 (hG : ProC (G := G)) (φ : X → G)
1989 (hφ : FamilyConvergesToOne (G := G) φ)
1990 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
1991 Continuous (hι.lift hG φ hφ hgen) ∧
1992 ∀ x, hι.lift hG φ hφ hgen (ι x) = φ x :=
1993 Classical.choose_spec (ExistsUnique.exists (hι.existsUnique_lift hG φ hφ hgen))
1995/-- The universal-property lift is unique among continuous maps with the prescribed values. -/
1996theorem lift_unique
1997 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1998 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1999 (hG : ProC (G := G)) (φ : X → G)
2000 (hφ : FamilyConvergesToOne (G := G) φ)
2001 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ))
2002 {f : F →* G} (hf : Continuous f) (hfac : ∀ x, f (ι x) = φ x) :
2003 f = hι.lift hG φ hφ hgen := by
2004 rcases hι.existsUnique_lift hG φ hφ hgen with ⟨g, _hg, huniq⟩
2005 have hchosen : hι.lift hG φ hφ hgen = g := huniq _ (hι.lift_spec hG φ hφ hgen)
2006 exact (huniq _ ⟨hf, hfac⟩).trans hchosen.symm
2008/-- For a concrete finite-group class, the generated-target universal property of a free
2009pro-`C` group on a converging set extends any target map that converges to `1`.
2011The proof corestricts the target map to the closed subgroup it topologically generates. This is
2012the form needed for retractions that collapse all but finitely many basis elements. -/
2014 (C : ProCGroups.FiniteGroupClass.{u})
2015 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
2016 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
2017 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
2018 (hι :
2020 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2021 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
2022 (hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
2023 (φ : X → G) (hφ : FamilyConvergesToOne (G := G) φ) :
2024 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x := by
2025 classical
2026 let K : ClosedSubgroup G := Generation.closedSubgroupGenerated (G := G) (Set.range φ)
2027 let φK : X → ↥(K : Subgroup G) := Generation.closedSubgroupGeneratedMap (G := G) φ
2028 have hφKconv : FamilyConvergesToOne (G := ↥(K : Subgroup G)) φK := by
2029 intro U
2030 have hU_nhds : ((U : Subgroup ↥(K : Subgroup G)) : Set ↥(K : Subgroup G)) ∈
2031 𝓝 (1 : ↥(K : Subgroup G)) :=
2032 U.isOpen'.mem_nhds U.one_mem'
2033 rcases
2034 (mem_nhds_subtype ((K : Subgroup G) : Set G) (1 : ↥(K : Subgroup G))
2035 ((U : Subgroup ↥(K : Subgroup G)) : Set ↥(K : Subgroup G))).1 hU_nhds with
2036 ⟨W₀, hW₀_nhds, hW₀U⟩
2037 rcases mem_nhds_iff.mp hW₀_nhds with ⟨W, hWU₀, hWopen, h1W⟩
2038 rcases hG.hasOpenNormalBasisInClass W hWopen h1W with ⟨V, hVW, _hCV⟩
2039 have hsub :
2040 {x : X | φK x ∉ (U : Set ↥(K : Subgroup G))} ⊆
2041 {x : X | φ x ∉ ((V.toOpenSubgroup : OpenSubgroup G) : Set G)} := by
2042 intro x hx hxV
2043 exact hx (hW₀U (by
2044 change φ x ∈ W₀
2045 exact hWU₀ (hVW hxV)))
2046 exact (hφ V.toOpenSubgroup).subset hsub
2047 have hφKgen :
2048 Generation.TopologicallyGenerates (G := ↥(K : Subgroup G)) (Set.range φK) := by
2049 simpa [φK] using
2050 (Generation.closedSubgroupGeneratedMap_topologicallyGenerates (G := G) φ)
2051 have hK :
2053 (G := ↥(K : Subgroup G)) :=
2054 ProCGroups.ProC.IsProCGroup.of_closedSubgroup hIso hSub hQuot hG K
2055 rcases hι.existsUnique_lift hK φK hφKconv hφKgen with ⟨fK, hfK, huniqK⟩
2057 let f : F →* G := incl.comp fK
2058 refine ⟨f, ⟨?_, ?_⟩, ?_⟩
2059 · exact continuous_subtype_val.comp hfK.1
2060 · intro x
2061 exact congrArg Subtype.val (hfK.2 x)
2062 · intro g hg
2063 have hgK_mem : ∀ y : F, g y ∈ (K : Subgroup G) := by
2064 intro y
2065 have hy :
2066 y ∈ (Generation.closedSubgroupGenerated (G := F) (Set.range ι) : Subgroup F) := by
2067 change y ∈ ((Subgroup.closure (Set.range ι)).topologicalClosure : Subgroup F)
2068 rw [hι.generates_range]
2069 simp only [Subgroup.mem_top]
2070 have hgy :=
2071 Generation.map_mem_closedSubgroupGenerated_image
2072 (G := F) (H := G)
2073 ({ toMonoidHom := g, continuous_toFun := hg.1 } : F →ₜ* G)
2074 (X := Set.range ι) hy
2075 have himage :
2076 (({ toMonoidHom := g, continuous_toFun := hg.1 } : F →ₜ* G) ''
2077 Set.range ι) = Set.range φ := by
2078 ext z
2079 constructor
2080 · rintro ⟨y, ⟨x, rfl⟩, rfl⟩
2081 exact ⟨x, (hg.2 x).symm⟩
2082 · rintro ⟨x, rfl⟩
2083 exact ⟨ι x, ⟨x, rfl⟩, hg.2 x⟩
2084 simpa [K, himage] using hgy
2085 let gK : F →* ↥(K : Subgroup G) :=
2086 { toFun := fun y => ⟨g y, hgK_mem y⟩
2087 map_one' := by
2088 apply Subtype.ext
2090 map_mul' := by
2091 intro a b
2092 apply Subtype.ext
2094 have hgKcont : Continuous gK := by
2095 exact Continuous.subtype_mk hg.1 (fun y => (gK y).2)
2096 have hgKfac : ∀ x, gK (ι x) = φK x := by
2097 intro x
2098 apply Subtype.ext
2099 exact hg.2 x
2100 have hgK_eq : gK = fK := huniqK gK ⟨hgKcont, hgKfac⟩
2101 ext y
2102 exact congrArg Subtype.val (congrArg (fun f : F →* ↥(K : Subgroup G) => f y) hgK_eq)
2104/-- Continuous-homomorphism form of
2107 (C : ProCGroups.FiniteGroupClass.{u})
2108 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
2109 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
2110 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
2111 (hι :
2113 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2114 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
2115 (hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
2116 (φ : X → G) (hφ : FamilyConvergesToOne (G := G) φ) :
2117 ∃! f : F →ₜ* G, ∀ x, f (ι x) = φ x := by
2119 C hIso hSub hQuot hι hG φ hφ with
2120 ⟨f, hf, huniq⟩
2121 let fc : F →ₜ* G :=
2122 { toMonoidHom := f
2123 continuous_toFun := hf.1 }
2124 refine ⟨fc, hf.2, ?_⟩
2125 intro g hg
2126 apply ContinuousMonoidHom.toMonoidHom_injective
2127 exact huniq g.toMonoidHom ⟨g.continuous, hg⟩
2129/-- In a free pro-`Σ` group with nonempty `Σ`, a free generator has no positive torsion. -/
2131 {σ : Set ℕ} (hσ : ∃ p, p ∈ σ ∧ Nat.Prime p)
2132 (hι :
2135 (ProCGroups.FiniteGroupClass.sigmaGroup σ)) X F ι)
2136 (i : X) (N : ℕ) (hN : 0 < N) :
2137 (ι i) ^ N ≠ 1 := by
2138 classical
2139 rcases hσ with ⟨p, hpσ, hp⟩
2140 let M := p ^ (N + 1)
2141 have hMpos : 0 < M := pow_pos hp.pos (N + 1)
2142 have hsigmaM : ProCGroups.FiniteGroupClass.IsSigmaNumber σ M :=
2144 (sigma := σ) (p := p) (k := N + 1) hpσ hp
2145 let T := ULift.{u} (Multiplicative (ZMod M))
2146 letI : NeZero M := ⟨Nat.ne_of_gt hMpos⟩
2147 letI : Finite T := by
2148 let e : T ≃ Multiplicative (ZMod M) := Equiv.ulift
2149 exact Finite.of_equiv (Multiplicative (ZMod M)) e.symm
2150 letI : TopologicalSpace T := ⊥
2151 letI : DiscreteTopology T := ⟨rfl⟩
2152 letI : IsTopologicalGroup T := by infer_instance
2153 let φ : X → T :=
2154 fun j => if j = i then ULift.up (Multiplicative.ofAdd (1 : ZMod M)) else 1
2155 have hφconv : FamilyConvergesToOne (G := T) φ := by
2156 intro U
2157 refine (Set.finite_singleton i).subset ?_
2158 intro j hj
2159 by_cases hji : j = i
2160 · simp only [hji, Set.mem_singleton_iff]
2161 · have hφj : φ j = 1 := by simp only [hji, ↓reduceIte, φ]
2162 have hmem : φ j ∈ (U : Set T) := by simp only [hφj, SetLike.mem_coe, one_mem]
2163 exact False.elim (hj hmem)
2164 have hTclass : ProCGroups.FiniteGroupClass.sigmaGroup σ T :=
2165 ProCGroups.FiniteGroupClass.sigmaGroup_cyclicZMod (sigma := σ) hMpos hsigmaM
2166 have hT :
2168 (ProCGroups.FiniteGroupClass.sigmaGroup σ)) (G := T) :=
2171 (G := T)
2172 (ProCGroups.FiniteGroupClass.sigmaGroup_quotientClosed σ)
2173 hTclass
2174 rcases hι.existsUnique_liftHom_of_convergesToOne_of_finiteGroupClass
2176 (ProCGroups.FiniteGroupClass.sigmaGroup_isomClosed σ)
2177 (ProCGroups.FiniteGroupClass.sigmaGroup_subgroupClosed σ)
2178 (ProCGroups.FiniteGroupClass.sigmaGroup_quotientClosed σ)
2179 hT φ hφconv with
2180 ⟨f, hf, _⟩
2181 intro hpow
2183 have hcalc : f ((ι i) ^ N) = ULift.up (Multiplicative.ofAdd (N : ZMod M)) := by
2184 calc
2185 f ((ι i) ^ N) = (f (ι i)) ^ N := by simp only [map_pow]
2186 _ = (φ i) ^ N := by rw [hf i]
2187 _ = (ULift.up (Multiplicative.ofAdd (1 : ZMod M))) ^ N := by simp only [↓reduceIte, φ]
2188 _ = ULift.up (Multiplicative.ofAdd (N : ZMod M)) := by
2189 apply ULift.ext
2190 change (Multiplicative.ofAdd (1 : ZMod M)) ^ N =
2191 Multiplicative.ofAdd (N : ZMod M)
2192 change Multiplicative.ofAdd ((N : ℕ) • (1 : ZMod M)) =
2193 Multiplicative.ofAdd (N : ZMod M)
2194 simp only [nsmul_eq_mul, mul_one]
2195 have hlt_pow : N < p ^ (N + 1) :=
2196 lt_of_lt_of_le
2197 (Nat.lt_pow_self (n := N) (a := p) hp.one_lt)
2198 (Nat.pow_le_pow_right hp.pos (Nat.le_succ N))
2199 have hNmod : (N : ZMod M) ≠ 0 := by
2200 intro hzero
2201 have hdiv : M ∣ N := (ZMod.natCast_eq_zero_iff N M).mp hzero
2202 exact (Nat.not_dvd_of_pos_of_lt hN hlt_pow) hdiv
2203 have hofAdd_ne : ULift.up (Multiplicative.ofAdd (N : ZMod M)) ≠ (1 : T) := by
2204 intro h
2205 have hdown : Multiplicative.ofAdd (N : ZMod M) = 1 := congrArg ULift.down h
2206 have hz : (N : ZMod M) = 0 := by
2207 change Multiplicative.ofAdd (N : ZMod M) =
2208 Multiplicative.ofAdd (0 : ZMod M) at hdown
2209 exact Multiplicative.ofAdd.injective hdown
2210 exact hNmod hz
2211 exact hofAdd_ne (hcalc.symm.trans hf_pow)
2213/-- Integer-power form of `generator_pow_ne_one_of_sigma`. -/
2215 {σ : Set ℕ} (hσ : ∃ p, p ∈ σ ∧ Nat.Prime p)
2216 (hι :
2219 (ProCGroups.FiniteGroupClass.sigmaGroup σ)) X F ι)
2220 (i : X) (n : ℤ) (hn : n ≠ 0) :
2221 (ι i) ^ n ≠ 1 := by
2222 intro hzn
2223 have hnat_pos : 0 < n.natAbs := Int.natAbs_pos.mpr hn
2224 have hnat_ne :
2225 (ι i) ^ n.natAbs ≠ 1 :=
2226 hι.generator_pow_ne_one_of_sigma hσ i n.natAbs hnat_pos
2227 apply hnat_ne
2228 by_cases hnonneg : 0 ≤ n
2229 · have hnat : (n.natAbs : ℤ) = n := Int.natAbs_of_nonneg hnonneg
2230 simpa [zpow_natCast, hnat] using hzn
2231 · have hneg : n < 0 := lt_of_not_ge hnonneg
2232 have hnat : (n.natAbs : ℤ) = -n := Int.ofNat_natAbs_of_nonpos hneg.le
2233 have hzn' : (ι i) ^ (-n) = 1 := by
2234 calc
2235 (ι i) ^ (-n) = ((ι i) ^ n)⁻¹ := by rw [zpow_neg]
2236 _ = 1 := by simp only [hzn, inv_one]
2237 simpa [zpow_natCast, hnat] using hzn'
2239/-- The continuous homomorphism supplied by the free pro-`C` universal property. -/
2240noncomputable def liftHom
2241 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
2242 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
2243 (hG : ProC (G := G)) (φ : X → G)
2244 (hφ : FamilyConvergesToOne (G := G) φ)
2245 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
2246 F →ₜ* G where
2247 toMonoidHom := hι.lift hG φ hφ hgen
2248 continuous_toFun := (hι.lift_spec hG φ hφ hgen).1
2250/-- Bundled version of `liftHom`, taking a converging generating map as a single argument. -/
2251noncomputable def liftConvergingGeneratingMap
2252 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
2253 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
2254 (hG : ProC (G := G)) (φ : ConvergingGeneratingMap X G) :
2255 F →ₜ* G :=
2256 hι.liftHom hG φ φ.convergesToOne φ.generates
2258/-- The bundled lift has the prescribed value on each generator. -/
2259@[simp] theorem liftConvergingGeneratingMap_apply
2260 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
2261 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
2262 (hG : ProC (G := G)) (φ : ConvergingGeneratingMap X G) (x : X) :
2263 hι.liftConvergingGeneratingMap hG φ (ι x) = φ x := by
2264 change hι.lift hG φ φ.convergesToOne φ.generates (ι x) = φ x
2265 exact (hι.lift_spec hG φ φ.convergesToOne φ.generates).2 x
2267/-- `liftHom` has the prescribed value on each generator. -/
2268@[simp] theorem liftHom_apply
2269 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
2270 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
2271 (hG : ProC (G := G)) (φ : X → G)
2272 (hφ : FamilyConvergesToOne (G := G) φ)
2273 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) (x : X) :
2274 hι.liftHom hG φ hφ hgen (ι x) = φ x :=
2275 (hι.lift_spec hG φ hφ hgen).2 x
2277section FiniteSupportRetracts
2279variable {C : ProCGroups.FiniteGroupClass.{u}}
2280variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
2281variable [hIso : Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
2282variable {X : Type v} [DecidableEq X]
2283variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
2284variable {ι : X → F}
2286/-- The unique continuous endomorphism of a free pro-`C` group that keeps the finite set `S`
2287of basis elements and sends the remaining basis elements to `1`. -/
2289 (hι :
2291 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2292 (S : Finset X) :
2293 ∃! φ : F →ₜ* F, ∀ x, φ (ι x) = if x ∈ S then ι x else 1 := by
2294 have hconv :
2295 FamilyConvergesToOne (G := F) (fun x => if x ∈ S then ι x else 1) := by
2296 intro U
2297 classical
2298 refine S.finite_toSet.subset ?_
2299 intro x hx
2300 by_cases hxS : x ∈ S
2301 · exact hxS
2302 · exfalso
2303 exact hx (by simp only [hxS, ↓reduceIte, SetLike.mem_coe, one_mem])
2304 exact
2305 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet.existsUnique_liftHom_of_convergesToOne_of_finiteGroupClass
2306 C hIso.out hVar.out.subgroupClosed hVar.out.quotientClosed
2307 hι hι.isProC (fun x => if x ∈ S then ι x else 1) hconv
2309/-- The finite-support retraction of a free pro-`C` group onto the closed subgroup generated by a
2311noncomputable def collapseToFinset
2312 (hι :
2314 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2315 (S : Finset X) :
2316 F →ₜ* F :=
2317 Classical.choose (ExistsUnique.exists (hι.existsUnique_collapseToFinset_of_finiteGroupClass S))
2319@[simp] theorem collapseToFinset_apply_mem
2320 (hι :
2322 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2323 {S : Finset X} {x : X} (hx : x ∈ S) :
2324 hι.collapseToFinset S (ι x) = ι x := by
2325 simpa [hx, collapseToFinset] using
2326 (Classical.choose_spec
2327 (ExistsUnique.exists (hι.existsUnique_collapseToFinset_of_finiteGroupClass S)) x)
2329@[simp] theorem collapseToFinset_apply_not_mem
2330 (hι :
2332 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2333 {S : Finset X} {x : X} (hx : x ∉ S) :
2334 hι.collapseToFinset S (ι x) = 1 := by
2335 simpa [hx, collapseToFinset] using
2336 (Classical.choose_spec
2337 (ExistsUnique.exists (hι.existsUnique_collapseToFinset_of_finiteGroupClass S)) x)
2339@[simp] theorem collapseToFinset_idempotent
2340 (hι :
2342 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2343 (S : Finset X) :
2344 (hι.collapseToFinset S).comp (hι.collapseToFinset S) =
2345 hι.collapseToFinset S := by
2346 let hFprof : ProCGroups.IsProfiniteGroup F :=
2348 letI : T2Space F := hFprof.t2Space
2349 apply Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
2350 rintro _ ⟨x, rfl⟩
2351 by_cases hx : x ∈ S
2352 · simp only [ContinuousMonoidHom.comp_toFun, hx, collapseToFinset_apply_mem]
2353 · simp only [ContinuousMonoidHom.comp_toFun, hx, not_false_eq_true, collapseToFinset_apply_not_mem, map_one]
2355/-- A homomorphism that kills every basis element outside `S` is unchanged after precomposition
2358 (hι :
2360 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2361 {G : Type w} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
2362 (φ : F →ₜ* G) (S : Finset X)
2363 (hφ : ∀ x, x ∉ S → φ (ι x) = 1) :
2364 φ.comp (hι.collapseToFinset S) = φ := by
2365 apply Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
2366 rintro _ ⟨x, rfl⟩
2367 by_cases hx : x ∈ S
2368 · simp only [ContinuousMonoidHom.comp_toFun, hx, collapseToFinset_apply_mem]
2369 · simp only [ContinuousMonoidHom.comp_toFun, hx, not_false_eq_true, collapseToFinset_apply_not_mem, map_one,
2370 hφ x hx]
2372/-- The map from the free pro-`C` group onto the range of its finite-support retraction. -/
2373noncomputable def collapseToFinsetRange
2374 (hι :
2376 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2377 (S : Finset X) :
2378 F →ₜ* ↥((hι.collapseToFinset S : F →* F).range) :=
2379 { toMonoidHom := (hι.collapseToFinset S : F →* F).rangeRestrict
2380 continuous_toFun :=
2381 (hι.collapseToFinset S).continuous.subtype_mk (fun x => ⟨x, rfl⟩) }
2383/-- The inclusion of the range of a finite-support retraction back into the ambient free group. -/
2384noncomputable def collapseToFinsetInclusion
2385 (hι :
2387 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2388 (S : Finset X) :
2389 ↥((hι.collapseToFinset S : F →* F).range) →ₜ* F :=
2391 continuous_toFun := continuous_subtype_val }
2393/-- The range of the finite-support retraction, viewed as the finite-basis retract. -/
2394abbrev FinsetSupportRetract
2395 (hι :
2397 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2398 (S : Finset X) : Type u :=
2399 ↥((hι.collapseToFinset S : F →* F).range)
2401/-- The finite basis of the finite-support retract. -/
2402noncomputable def finsetSupportBasis
2403 (hι :
2405 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2406 (S : Finset X) :
2407 S → hι.FinsetSupportRetract S := by
2408 intro x
2409 refine ⟨ι x.1, ?_⟩
2410 exact ⟨ι x.1, hι.collapseToFinset_apply_mem x.2⟩
2412/-- The range of the finite-support retraction is closed. -/
2414 (hι :
2416 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2417 (S : Finset X) :
2418 IsClosed (((hι.collapseToFinset S : F →* F).range : Set F)) := by
2419 let hFprof : ProCGroups.IsProfiniteGroup F :=
2421 letI : T2Space F := hFprof.t2Space
2422 let r : F →ₜ* F := hι.collapseToFinset S
2423 let Fix : Subgroup F := (r : F →* F).eqLocus (MonoidHom.id F)
2424 have hFixClosed : IsClosed (Fix : Set F) := by
2425 change IsClosed {x : F | r x = x}
2426 exact isClosed_eq r.continuous continuous_id
2427 have hFixEq : Fix = (r : F →* F).range := by
2428 ext x
2429 constructor
2430 · intro hx
2431 exact ⟨x, by simpa using hx⟩
2432 · rintro ⟨y, rfl⟩
2433 change r (r y) = r y
2434 exact congrArg (fun ψ : F →ₜ* F => ψ y) (hι.collapseToFinset_idempotent S)
2435 simpa [r, Fix, hFixEq] using hFixClosed
2437/-- The finite-support retract is again a pro-`C` group. -/
2439 (hι :
2441 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2442 (S : Finset X) :
2444 (G := hι.FinsetSupportRetract S) := by
2445 exact
2447 hIso.out hVar.out.subgroupClosed hVar.out.quotientClosed
2448 hι.isProC ((hι.collapseToFinset S : F →* F).range)
2449 (hι.isClosed_range_collapseToFinset S)
2451/-- The finite-support retract is free pro-`C` on its retained finite basis. -/
2453 (hι :
2455 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2456 (S : Finset X) :
2458 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
2459 S (hι.FinsetSupportRetract S) (hι.finsetSupportBasis S) := by
2460 let R : Type u := hι.FinsetSupportRetract S
2461 let B : S → R := hι.finsetSupportBasis S
2462 let rRange : F →ₜ* R := hι.collapseToFinsetRange S
2463 let rIncl : R →ₜ* F := hι.collapseToFinsetInclusion S
2464 refine ⟨hι.isProCGroup_finsetSupportRetract S, ?_, ?_, ?_⟩
2465 · simpa [B] using FamilyConvergesToOne.of_finite_domain (G := R) B
2466 ·
2467 have hgen :
2468 Generation.TopologicallyGenerates (G := R) (Set.range B) := by
2469 let Img : Set R := rRange '' Set.range ι
2470 have hsurj : Function.Surjective rRange := by
2471 exact MonoidHom.rangeRestrict_surjective (hι.collapseToFinset S : F →* F)
2472 have hImgGen : Generation.TopologicallyGenerates (G := R) Img := by
2473 exact
2474 Generation.topologicallyGenerates_image_of_continuousSurjective
2475 (f := rRange.toMonoidHom) rRange.continuous hsurj hι.generates_range
2476 have hBsub : Set.range B ⊆ Img := by
2477 intro y hy
2478 rcases hy with ⟨x, rfl⟩
2479 refine ⟨ι x.1, ⟨x.1, rfl⟩, ?_⟩
2480 apply Subtype.ext
2481 change (hι.collapseToFinset S (ι x.1) : F) = ι x.1
2482 exact hι.collapseToFinset_apply_mem x.2
2483 have hImgSub : Img ⊆ ((Subgroup.closure (Set.range B) : Subgroup R) : Set R) := by
2484 intro y hy
2485 rcases hy with ⟨x, ⟨j, rfl⟩, rfl⟩
2486 by_cases hj : j ∈ S
2487 · exact
2488 Subgroup.subset_closure ⟨⟨j, hj⟩, by
2489 apply Subtype.ext
2490 change ι j = (hι.collapseToFinset S (ι j) : F)
2491 exact (hι.collapseToFinset_apply_mem hj).symm⟩
2492 · have hy1 : rRange (ι j) = 1 := by
2493 apply Subtype.ext
2494 change (hι.collapseToFinset S (ι j) : F) = 1
2495 exact hι.collapseToFinset_apply_not_mem hj
2496 rw [hy1]
2497 exact (Subgroup.closure (Set.range B)).one_mem
2498 have hclosureEq :
2499 Subgroup.closure Img = Subgroup.closure (Set.range B) := by
2500 apply le_antisymm
2501 · exact (Subgroup.closure_le (K := Subgroup.closure (Set.range B))).2 hImgSub
2502 · exact Subgroup.closure_mono hBsub
2503 change (Subgroup.closure (Set.range B)).topologicalClosure = ⊤
2504 change (Subgroup.closure Img).topologicalClosure = ⊤ at hImgGen
2505 rw [← hclosureEq]
2506 exact hImgGen
2507 simpa [B] using hgen
2508 · intro G _ _ _ hG φ hφ hgen
2509 let φext : X → G := fun x => if hx : x ∈ S then φ ⟨x, hx⟩ else 1
2510 have hφext : FamilyConvergesToOne (G := G) φext := by
2511 intro U
2512 refine S.finite_toSet.subset ?_
2513 intro x hx
2514 by_cases hxS : x ∈ S
2515 · exact hxS
2516 · exfalso
2517 exact hx (by simp only [hxS, ↓reduceDIte, SetLike.mem_coe, one_mem, φext])
2518 have hφextgen : Generation.TopologicallyGenerates (G := G) (Set.range φext) := by
2519 have hsub : Set.range φ ⊆ Set.range φext := by
2520 intro y hy
2521 rcases hy with ⟨x, rfl⟩
2522 exact ⟨x.1, by simp only [x.2, ↓reduceDIte, Subtype.coe_eta, φext]⟩
2523 exact Generation.topologicallyGenerates_mono (G := G) hgen hsub
2524 let Φ : F →ₜ* G := hι.liftHom hG φext hφext hφextgen
2525 have hΦspec : ∀ x, Φ (ι x) = φext x := by
2526 intro x
2527 exact hι.liftHom_apply hG φext hφext hφextgen x
2528 let Φbar : R →ₜ* G :=
2529 { toMonoidHom := Φ.toMonoidHom.comp rIncl.toMonoidHom
2530 continuous_toFun := Φ.continuous.comp rIncl.continuous }
2531 have hΦbar : ∀ x : S, Φbar (B x) = φ x := by
2532 intro x
2533 change Φ (ι x.1) = φ x
2534 simpa [φext, B, Φbar, rIncl, collapseToFinsetInclusion, finsetSupportBasis] using
2535 hΦspec x.1
2536 refine ⟨Φbar.toMonoidHom, ⟨Φbar.continuous, hΦbar⟩, ?_⟩
2537 intro ψ hψ
2538 let ψc : R →ₜ* G :=
2539 { toMonoidHom := ψ
2540 continuous_toFun := hψ.1 }
2541 have hψcomp : ψc.comp rRange = Φ := by
2542 let hGprof : ProCGroups.IsProfiniteGroup G :=
2544 letI : T2Space G := hGprof.t2Space
2545 apply Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
2546 rintro _ ⟨x, rfl⟩
2547 by_cases hx : x ∈ S
2548 · have hψx : ψc (rRange (ι x)) = φ ⟨x, hx⟩ := by
2549 have hBasis : rRange (ι x) = B ⟨x, hx⟩ := by
2550 apply Subtype.ext
2551 change (hι.collapseToFinset S (ι x) : F) = ι x
2552 exact hι.collapseToFinset_apply_mem hx
2553 exact hBasis ▸ hψ.2 ⟨x, hx⟩
2554 have hΦx : Φ (ι x) = φ ⟨x, hx⟩ := by
2555 simpa [φext, hx] using hΦspec x
2556 exact hψx.trans hΦx.symm
2557 · have hrx : rRange (ι x) = 1 := by
2558 apply Subtype.ext
2559 change (hι.collapseToFinset S (ι x) : F) = 1
2560 exact hι.collapseToFinset_apply_not_mem hx
2561 have hΦx : Φ (ι x) = 1 := by
2562 simpa [φext, hx] using hΦspec x
2563 calc
2564 ψc (rRange (ι x)) = ψc 1 := by rw [hrx]
2566 _ = Φ (ι x) := hΦx.symm
2567 have hΦbarcomp : Φbar.comp rRange = Φ := by
2568 let hGprof : ProCGroups.IsProfiniteGroup G :=
2570 letI : T2Space G := hGprof.t2Space
2571 ext y
2572 change Φ (hι.collapseToFinset S y) = Φ y
2573 have hfix :
2574 Φ.comp (hι.collapseToFinset S) = Φ := by
2575 exact hι.comp_collapseToFinset_eq_of_eq_one_outside Φ S (by
2576 intro x hx
2577 simpa [φext, hx] using hΦspec x)
2578 exact congrArg (fun f : F →ₜ* G => f y) hfix
2579 have hsurj : Function.Surjective rRange := by
2580 exact MonoidHom.rangeRestrict_surjective (hι.collapseToFinset S : F →* F)
2581 ext z
2582 rcases hsurj z with ⟨y, rfl⟩
2583 have hEq : ψc.comp rRange = Φbar.comp rRange := hψcomp.trans hΦbarcomp.symm
2584 exact congrArg (fun f : F →ₜ* G => f y) hEq
2586 /-- If `S ⊆ T`, then collapsing first to `T` and then to `S` is the same as
2588 projections. -/
2590 (hι :
2592 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2593 {S T : Finset X} (hST : S ⊆ T) :
2594 (hι.collapseToFinset S).comp (hι.collapseToFinset T) =
2595 hι.collapseToFinset S := by
2596 let hFprof : ProCGroups.IsProfiniteGroup F :=
2598 letI : T2Space F := hFprof.t2Space
2599 apply Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
2600 rintro _ ⟨x, rfl⟩
2601 by_cases hxS : x ∈ S
2602 · have hxT : x ∈ T := hST hxS
2603 simp only [ContinuousMonoidHom.comp_toFun, hxT, collapseToFinset_apply_mem, hxS]
2604 · by_cases hxT : x ∈ T
2605 · simp only [ContinuousMonoidHom.comp_toFun, hxT, collapseToFinset_apply_mem, hxS, not_false_eq_true,
2607 · simp only [ContinuousMonoidHom.comp_toFun, hxT, not_false_eq_true, collapseToFinset_apply_not_mem, map_one,
2608 hxS]
2610 /-- If `S ⊆ T`, then collapsing to `S` and then to `T` is again the collapse to `S`.
2612 projection. -/
2614 (hι :
2616 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2617 {S T : Finset X} (hST : S ⊆ T) :
2618 (hι.collapseToFinset T).comp (hι.collapseToFinset S) =
2619 hι.collapseToFinset S := by
2620 let hFprof : ProCGroups.IsProfiniteGroup F :=
2622 letI : T2Space F := hFprof.t2Space
2623 apply Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
2624 rintro _ ⟨x, rfl⟩
2625 by_cases hxS : x ∈ S
2626 · have hxT : x ∈ T := hST hxS
2627 simp only [ContinuousMonoidHom.comp_toFun, hxS, collapseToFinset_apply_mem, hxT]
2628 · simp only [ContinuousMonoidHom.comp_toFun, hxS, not_false_eq_true, collapseToFinset_apply_not_mem, map_one]
2630 /-- The transition map from the finite-support retract for `T` to the one for `S`, for
2631 `S ⊆ T`. It is the projection obtained by including the `T`-retract into the ambient free
2632 pro-`C` group and then collapsing to `S`. -/
2633 noncomputable def finsetSupportTransition
2634 (hι :
2636 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2637 {S T : Finset X} (_hST : S ⊆ T) :
2638 hι.FinsetSupportRetract T →ₜ* hι.FinsetSupportRetract S :=
2639 { toMonoidHom := (hι.collapseToFinsetRange S).toMonoidHom.comp
2640 (hι.collapseToFinsetInclusion T).toMonoidHom
2641 continuous_toFun :=
2642 (hι.collapseToFinsetRange S).continuous.comp
2643 (hι.collapseToFinsetInclusion T).continuous }
2645 @[simp] theorem finsetSupportTransition_apply_basis
2646 (hι :
2648 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2649 {S T : Finset X} (hST : S ⊆ T) (x : S) :
2650 hι.finsetSupportTransition hST
2651 (hι.finsetSupportBasis T ⟨x.1, hST x.2⟩) =
2652 hι.finsetSupportBasis S x := by
2653 apply Subtype.ext
2654 change hι.collapseToFinset S (ι x.1) = ι x.1
2655 exact hι.collapseToFinset_apply_mem x.2
2657 /-- Compatibility of the ambient projection `F → R_T` with the transition
2658 `R_T → R_S`. -/
2660 (hι :
2662 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
2663 {S T : Finset X} (hST : S ⊆ T) :
2664 (hι.finsetSupportTransition hST).comp (hι.collapseToFinsetRange T) =
2665 hι.collapseToFinsetRange S := by
2666 ext x
2667 change hι.collapseToFinset S (hι.collapseToFinset T x) =
2668 hι.collapseToFinset S x
2669 exact congrArg (fun f : F →ₜ* F => f x)
2670 (hι.collapseToFinset_small_comp_large_of_subset hST)
2672 end FiniteSupportRetracts
2674/-- Continuous homomorphisms out of a free pro-`C` group on a converging generating set are
2675determined by their values on the chosen generators. -/
2676theorem hom_ext
2677 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
2678 {G : Type u} [Group G] [TopologicalSpace G] [T2Space G]
2679 {f g : F →ₜ* G} (hfg : ∀ x, f (ι x) = g (ι x)) :
2680 f = g := by
2681 exact Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
2682 (by
2683 intro y hy
2684 rcases hy with ⟨x, rfl⟩
2685 exact hfg x)
2687/-- The lift of the canonical generator map to the same free pro-`C` group is the identity. -/
2688@[simp 900] theorem lift_id
2689 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι) :
2690 hι.lift hι.isProC ι hι.convergesToOne hι.generates_range = MonoidHom.id F := by
2691 symm
2692 exact hι.lift_unique hι.isProC ι hι.convergesToOne hι.generates_range continuous_id
2693 (by intro x; rfl)
2695/-- Precomposing the converging generating set by an equivalence preserves the free pro-`C` universal property. -/
2696theorem precompEquiv
2697 {X' : Type w}
2698 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι) (e : X' ≃ X) :
2699 IsFreeProCGroupOnConvergingSet (ProC := ProC) X' F (fun x : X' => ι (e x)) := by
2700 have hrange : Set.range (fun x : X' => ι (e x)) = Set.range ι := by
2701 ext y
2702 constructor
2703 · rintro ⟨x, rfl⟩
2704 exact ⟨e x, rfl⟩
2705 · rintro ⟨x, rfl⟩
2706 exact ⟨e.symm x, by simp only [Equiv.apply_symm_apply]⟩
2707 refine
2709 convergesToOne := by
2710 intro U
2711 have hsubset :
2712 {x : X' | ι (e x) ∉ (U : Set F)} ⊆
2713 e.symm '' {x : X | ι x ∉ (U : Set F)} := by
2714 intro x hx
2715 exact ⟨e x, hx, by simp only [Equiv.symm_apply_apply]⟩
2716 exact (hι.convergesToOne U).image e.symm |>.subset hsubset
2717 generates_range := by simpa [hrange] using hι.generates_range
2718 existsUnique_lift := ?_ }
2719 intro G _ _ _ hG φ hφ hgen
2720 let φ' : X → G := fun x => φ (e.symm x)
2721 have hrangeφ : Set.range φ' = Set.range φ := by
2722 ext y
2723 constructor
2724 · rintro ⟨x, rfl⟩
2725 exact ⟨e.symm x, rfl⟩
2726 · rintro ⟨x, rfl⟩
2727 exact ⟨e x, by simp only [Equiv.symm_apply_apply, φ']⟩
2728 have hφ' : FamilyConvergesToOne (G := G) φ' := by
2729 intro U
2730 have hsubset :
2731 {x : X | φ (e.symm x) ∉ (U : Set G)} ⊆
2732 e '' {x : X' | φ x ∉ (U : Set G)} := by
2733 intro x hx
2734 exact ⟨e.symm x, hx, by simp only [Equiv.apply_symm_apply]⟩
2735 exact (hφ U).image e |>.subset hsubset
2736 have hgen' : Generation.TopologicallyGenerates (G := G) (Set.range φ') := by
2737 simpa [hrangeφ] using hgen
2738 rcases hι.existsUnique_lift hG φ' hφ' hgen' with ⟨f, hf, huniq⟩
2739 refine ⟨f, ?_, ?_⟩
2740 · refine ⟨hf.1, ?_⟩
2741 intro x
2742 simpa [φ'] using hf.2 (e x)
2743 · intro g hg
2744 apply huniq
2745 refine ⟨hg.1, ?_⟩
2746 intro x
2747 simpa [φ'] using hg.2 (e.symm x)
2749/-- An endomorphism of a free pro-`C` group fixing the generators is the identity. -/
2750theorem endomorphism_eq_id
2751 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
2752 {f : F →* F} (hf : Continuous f) (hfac : ∀ x, f (ι x) = ι x) :
2753 f = MonoidHom.id F := by
2754 exact (hι.lift_unique hι.isProC ι hι.convergesToOne hι.generates_range hf hfac).trans
2755 hι.lift_id
2757/-- The canonical multiplicative homeomorphism between two free pro-`C` groups on the same
2758converging basis. -/
2759noncomputable def continuousMulEquivOfSameBasis
2760 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
2761 {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
2762 {κ : X → F'}
2763 (hκ : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F' κ) :
2764 F ≃ₜ* F' :=
2765 let f : F →* F' := hι.lift hκ.isProC κ hκ.convergesToOne hκ.generates_range
2766 let g : F' →* F := hκ.lift hι.isProC ι hι.convergesToOne hι.generates_range
2767 let hf : Continuous f := (hι.lift_spec hκ.isProC κ hκ.convergesToOne hκ.generates_range).1
2768 let hg : Continuous g := (hκ.lift_spec hι.isProC ι hι.convergesToOne hι.generates_range).1
2769 { toMulEquiv :=
2770 { toFun := f
2771 invFun := g
2772 left_inv := by
2773 intro y
2774 have hgf : g.comp f = MonoidHom.id F := by
2775 apply hι.endomorphism_eq_id (hg.comp hf)
2776 intro x
2777 dsimp [f, g]
2778 rw [(hι.lift_spec hκ.isProC κ hκ.convergesToOne hκ.generates_range).2 x]
2779 exact (hκ.lift_spec hι.isProC ι hι.convergesToOne hι.generates_range).2 x
2780 exact congrArg (fun h : F →* F => h y) hgf
2781 right_inv := by
2782 intro y
2783 have hfg : f.comp g = MonoidHom.id F' := by
2784 apply hκ.endomorphism_eq_id (hf.comp hg)
2785 intro x
2786 dsimp [f, g]
2787 rw [(hκ.lift_spec hι.isProC ι hι.convergesToOne hι.generates_range).2 x]
2788 exact (hι.lift_spec hκ.isProC κ hκ.convergesToOne hκ.generates_range).2 x
2789 exact congrArg (fun h : F' →* F' => h y) hfg
2790 map_mul' := f.map_mul }
2791 continuous_toFun := hf
2792 continuous_invFun := hg }
2794/-- The canonical equivalence between free pro-`C` groups with the same basis fixes each generator. -/
2795@[simp 900] theorem continuousMulEquivOfSameBasis_apply
2796 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
2797 {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
2798 {κ : X → F'}
2799 (hκ : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F' κ) (x : X) :
2800 hι.continuousMulEquivOfSameBasis hκ (ι x) = κ x := by
2801 simpa [continuousMulEquivOfSameBasis] using
2802 (hι.lift_spec hκ.isProC κ hκ.convergesToOne hκ.generates_range).2 x
2804/-- The inverse canonical equivalence between free pro-`C` groups with the same basis fixes each generator. -/
2805@[simp 900] theorem continuousMulEquivOfSameBasis_symm_apply
2806 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
2807 {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
2808 {κ : X → F'}
2809 (hκ : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F' κ) (x : X) :
2810 (hι.continuousMulEquivOfSameBasis hκ).symm (κ x) = ι x := by
2811 simpa [continuousMulEquivOfSameBasis] using
2812 (hκ.lift_spec hι.isProC ι hι.convergesToOne hι.generates_range).2 x
2814/-- Transport the free pro-`C` structure on a converging set across a continuous multiplicative
2815equivalence of ambient groups. -/
2816theorem ofContinuousMulEquiv
2817 (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
2818 (e : F ≃ₜ* F')
2819 (hF' : ProC (G := F')) :
2820 IsFreeProCGroupOnConvergingSet (ProC := ProC) X F' (fun x => e (ι x)) := by
2821 have hrange : Set.range (fun x : X => e (ι x)) = e '' Set.range ι := by
2822 ext y
2823 constructor
2824 · rintro ⟨x, rfl⟩
2825 exact ⟨ι x, ⟨x, rfl⟩, rfl⟩
2826 · rintro ⟨z, ⟨x, rfl⟩, rfl⟩
2827 exact ⟨x, rfl⟩
2828 refine
2830 convergesToOne := ?_
2831 generates_range := ?_
2832 existsUnique_lift := ?_ }
2833 ·
2834 intro U
2835 let V : OpenSubgroup F := OpenSubgroup.comap e.toMonoidHom e.continuous U
2836 have hsubset :
2837 {x : X | e (ι x) ∉ (U : Set F')} ⊆ {x : X | ι x ∉ (V : Set F)} := by
2838 intro x hx hxV
2839 exact hx (by simpa [V] using hxV)
2840 exact (hι.convergesToOne V).subset hsubset
2841 · rw [hrange]
2843 (G := F) (H := F') e hι.generates_range
2844 · intro G _ _ _ hG φ hφ hgen
2845 rcases hι.existsUnique_lift hG φ hφ hgen with ⟨f, hf, huniq⟩
2846 let f' : F' →* G := f.comp e.symm.toMonoidHom
2847 refine ⟨f', ?_, ?_⟩
2848 · refine ⟨hf.1.comp e.symm.continuous, ?_⟩
2849 intro x
2850 change f (e.symm (e (ι x))) = φ x
2851 rw [e.symm_apply_apply]
2852 exact hf.2 x
2853 · intro g hg
2854 have hgcomp : g.comp e.toMonoidHom = f := by
2855 apply huniq
2856 refine ⟨hg.1.comp e.continuous, ?_⟩
2857 intro x
2858 simpa using hg.2 x
2859 ext y
2860 rcases e.surjective y with ⟨x, rfl⟩
2861 change g (e x) = f (e.symm (e x))
2862 rw [e.symm_apply_apply]
2863 exact congrArg (fun h : F →* G => h x) hgcomp
2867/-- Packaged carrier for a free pro-`C` group on a set converging to `1`. -/
2868structure FreeProCGroupOnConvergingSetData
2869 (ProC : ProCGroups.ProC.ProCGroupPredicate) where
2870 basis : Type u
2871 carrier : Type u
2873 instTopologicalSpace : TopologicalSpace carrier
2874 instIsTopologicalGroup : IsTopologicalGroup carrier
2875 inclusion : basis → carrier
2876 isFree : IsFreeProCGroupOnConvergingSet (ProC := ProC) basis carrier inclusion
2878attribute [instance] FreeProCGroupOnConvergingSetData.instGroup
2879attribute [instance] FreeProCGroupOnConvergingSetData.instTopologicalSpace
2880attribute [instance] FreeProCGroupOnConvergingSetData.instIsTopologicalGroup
2882/-- The cardinality of a finite converging-set basis is the topological rank of the free
2885 (C : ProCGroups.FiniteGroupClass.{u})
2886 (hquot : ProCGroups.FiniteGroupClass.QuotientClosed C)
2887 (hcyc :
2888 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
2889 C A ∧ IsCyclic A ∧ Nontrivial A)
2890 (Fdata : FreeProCGroupOnConvergingSetData
2891 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C))
2892 [Finite Fdata.basis] :
2893 Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier := by
2894 classical
2895 let hFprof : ProCGroups.IsProfiniteGroup Fdata.carrier :=
2896 ProCGroups.ProC.isProfiniteGroup_of_finiteGroupClassProCPredicate C Fdata.isFree.isProC
2897 letI : Fintype Fdata.basis := Fintype.ofFinite Fdata.basis
2898 rcases exists_nontrivial_topologicallyCyclic_proC_of_finiteGroupClass C hquot hcyc with
2899 ⟨A, _instGroupA, _instTopA, _instTopGroupA, hA, a, ha1, hgena⟩
2900 have hnontrivial :
2901 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A),
2902 (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := A) ∧
2903 ∃ a : A, a ≠ 1 ∧ Generation.TopologicallyGenerates (G := A) ({a} : Set A) :=
2904 ⟨A, inferInstance, inferInstance, inferInstance, hA, a, ha1, hgena⟩
2905 have hιinj : Function.Injective Fdata.inclusion :=
2906 freeProCGroupOnConvergingSet_injective Fdata.isFree hnontrivial
2907 have hfg : _root_.ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated Fdata.carrier := by
2908 refine ⟨Finset.univ.image Fdata.inclusion, ?_⟩
2909 simpa [Finset.coe_image] using Fdata.isFree.generates_range
2910 have hdle :
2911 Generation.topologicalRank Fdata.carrier ≤ (Fintype.card Fdata.basis : Cardinal) := by
2912 calc
2913 Generation.topologicalRank Fdata.carrier ≤ Cardinal.mk (Set.range Fdata.inclusion) := by
2914 change sInf {κ : Cardinal |
2915 ∃ X : Set Fdata.carrier,
2916 Generation.GeneratesAndConvergesToOne (G := Fdata.carrier) X ∧
2917 Cardinal.mk X = κ} ≤ Cardinal.mk (Set.range Fdata.inclusion)
2918 exact csInf_le' ⟨Set.range Fdata.inclusion,
2919 ⟨Fdata.isFree.generates_range, Fdata.isFree.convergesToOne.range⟩,
2920 rfl⟩
2921 _ = Cardinal.mk Fdata.basis := by
2922 simpa using (Cardinal.mk_range_eq Fdata.inclusion hιinj)
2923 _ = (Fintype.card Fdata.basis : Cardinal) := by simp only [Cardinal.mk_fintype]
2924 have hdlt : Generation.topologicalRank Fdata.carrier < Cardinal.aleph0 := by
2925 exact lt_of_le_of_lt hdle (Cardinal.natCast_lt_aleph0 (n := Fintype.card Fdata.basis))
2926 let d : ℕ := Cardinal.toNat (Generation.topologicalRank Fdata.carrier)
2927 have hdEq : Generation.topologicalRank Fdata.carrier = d := by
2928 symm
2929 exact Cardinal.cast_toNat_of_lt_aleph0 hdlt
2930 have hdleNat : d ≤ Fintype.card Fdata.basis := by
2931 simpa [d, Nat.card_eq_fintype_card] using
2932 Cardinal.toNat_le_toNat hdle
2933 (Cardinal.natCast_lt_aleph0 (n := Fintype.card Fdata.basis))
2934 by_cases hd0 : d = 0
2935 · have hdEq0 : Generation.topologicalRank Fdata.carrier = 0 := by simpa [d, hd0] using hdEq
2936 letI : CompactSpace Fdata.carrier := ProCGroups.IsProfiniteGroup.compactSpace hFprof
2937 letI : T2Space Fdata.carrier := ProCGroups.IsProfiniteGroup.t2Space hFprof
2938 letI : TotallyDisconnectedSpace Fdata.carrier :=
2940 have hgen0 :
2941 _root_.ProCGroups.FiniteGeneration.TopologicallyGeneratedByAtMost
2942 (G := Fdata.carrier) 0 :=
2943 _root_.ProCGroups.FiniteGeneration.topologicallyGeneratedByAtMost_of_topologicalRank_eq_nat
2944 (G := Fdata.carrier) hFprof hdEq0
2945 rcases hgen0 with ⟨s, hs, hsgen⟩
2946 have hs0 : s.card = 0 := Nat.eq_zero_of_le_zero hs
2947 have hsempty : s = ∅ := Finset.card_eq_zero.mp hs0
2948 have htriv : ∀ x : Fdata.carrier, x = 1 := by
2949 intro x
2950 have hxmem :
2951 x ∈
2952 ((Subgroup.closure
2953 (((s : Finset Fdata.carrier) : Set Fdata.carrier))).topologicalClosure :
2954 Set Fdata.carrier) := by
2955 rw [Generation.TopologicallyGenerates] at hsgen
2956 rw [hsgen]
2957 simp only [Subgroup.coe_top, mem_univ]
2958 simpa [hsempty, Subgroup.coe_topologicalClosure_bot, closure_singleton] using hxmem
2959 have hEmpty : IsEmpty Fdata.basis := by
2960 refine ⟨fun b => ?_⟩
2961 have hb1 : Fdata.inclusion b = 1 := htriv (Fdata.inclusion b)
2962 exact
2964 (hι := Fdata.isFree) hnontrivial) ⟨b, hb1⟩
2965 letI : IsEmpty Fdata.basis := hEmpty
2966 have hcard0 : Cardinal.mk Fdata.basis = 0 := by simp only [Cardinal.mk_eq_zero]
2967 rw [hdEq0]
2968 exact hcard0
2969 · have hdPos : 0 < d := Nat.pos_of_ne_zero hd0
2970 rcases _root_.ProCGroups.FiniteGeneration.exists_generatingTuple_of_topologicalRank_le_of_finite
2971 (G := Fdata.carrier) hfg
2972 (show Generation.topologicalRank Fdata.carrier ≤ d by simp only [hdEq, le_refl]) with
2973 ⟨φ, hφgen⟩
2974 let i0 : Fin d := ⟨0, hdPos⟩
2975 have hdleNat' : Fintype.card (Fin d) ≤ Fintype.card Fdata.basis := by
2976 simpa using hdleNat
2977 have hEmb : Nonempty (Fin d ↪ Fdata.basis) := by
2978 exact Function.Embedding.nonempty_of_card_le (α := Fin d) (β := Fdata.basis) hdleNat'
2979 have hConst : Nonempty (Fdata.basis → Fin d) := ⟨fun _ => i0⟩
2980 rcases (Function.exists_surjective_iff).2 ⟨hConst, hEmb⟩ with ⟨q, hqsurj⟩
2981 let ψ : Fdata.basis → Fdata.carrier := fun b => φ (q b)
2982 have hψconv : FamilyConvergesToOne (G := Fdata.carrier) ψ := by
2983 exact FamilyConvergesToOne.of_finite_domain (G := Fdata.carrier) ψ
2984 have hψrange : Set.range ψ = Set.range φ := by
2985 ext x
2986 constructor
2987 · rintro ⟨b, rfl⟩
2988 exact ⟨q b, rfl⟩
2989 · rintro ⟨i, rfl⟩
2990 rcases hqsurj i with ⟨b, rfl⟩
2991 exact ⟨b, rfl⟩
2992 have hψgen : Generation.TopologicallyGenerates (G := Fdata.carrier) (Set.range ψ) := by
2993 simpa [hψrange] using hφgen
2994 rcases Fdata.isFree.existsUnique_lift Fdata.isFree.isProC ψ hψconv hψgen with
2995 ⟨σ, hσ, _⟩
2996 letI : CompactSpace Fdata.carrier := ProCGroups.IsProfiniteGroup.compactSpace hFprof
2997 letI : T2Space Fdata.carrier := ProCGroups.IsProfiniteGroup.t2Space hFprof
2998 have hσsub : Set.range φ ⊆ (σ.range : Set Fdata.carrier) := by
2999 rintro z ⟨i, rfl⟩
3000 rcases hqsurj i with ⟨b, hb⟩
3001 refine ⟨Fdata.inclusion b, ?_⟩
3002 simpa [ψ, hb] using hσ.2 b
3003 have hσsurj : Function.Surjective σ := by
3004 have hσgen :
3005 Generation.TopologicallyGenerates (G := Fdata.carrier)
3006 ((σ.range : Set Fdata.carrier)) :=
3007 Generation.topologicallyGenerates_mono (G := Fdata.carrier) hφgen hσsub
3008 have hσclosed : IsClosed ((σ.range : Set Fdata.carrier)) := by
3009 simpa using (isCompact_range hσ.1).isClosed
3010 have hσclosure_le : (σ.range : Subgroup Fdata.carrier).topologicalClosure ≤ σ.range :=
3011 Subgroup.topologicalClosure_minimal _ le_rfl hσclosed
3012 have hσclosure_top : (σ.range : Subgroup Fdata.carrier).topologicalClosure = ⊤ := by
3013 have htop :
3014 (Subgroup.closure (σ.range : Set Fdata.carrier)).topologicalClosure =
3015 (⊤ : Subgroup Fdata.carrier) := by
3016 simpa [Generation.TopologicallyGenerates] using hσgen
3017 have hclosure_eq :
3018 (σ.range : Subgroup Fdata.carrier) =
3019 Subgroup.closure (σ.range : Set Fdata.carrier) := by
3020 simpa using (Subgroup.closure_eq (σ.range)).symm
3021 rw [hclosure_eq]
3022 exact htop
3023 have hσrange_top : σ.range = ⊤ := by
3024 apply top_unique
3025 intro z hz
3026 have hz' :
3027 z ∈
3028 ((σ.range : Subgroup Fdata.carrier).topologicalClosure :
3029 Set Fdata.carrier) := by
3030 rw [hσclosure_top]
3031 simp only [Subgroup.coe_top, mem_univ]
3032 exact hσclosure_le hz'
3033 intro z
3034 have hz : z ∈ (σ.range : Set Fdata.carrier) := by
3035 simp only [hσrange_top, Subgroup.coe_top, mem_univ]
3036 simpa using hz
3037 let σc : ContinuousMonoidHom Fdata.carrier Fdata.carrier :=
3038 { toMonoidHom := σ
3039 continuous_toFun := hσ.1 }
3040 letI : TotallyDisconnectedSpace Fdata.carrier :=
3042 rcases
3043 (_root_.ProCGroups.FiniteGeneration.surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated
3044 (G := Fdata.carrier) hfg σc hσsurj) with
3045 ⟨eσ, heσ⟩
3046 have hσinj : Function.Injective σ := by
3047 intro a b hab
3048 have h' : eσ a = eσ b := by
3049 calc
3050 eσ a = σ a := by simpa [σc] using heσ a
3051 _ = σ b := hab
3052 _ = eσ b := by simpa [σc] using (heσ b).symm
3053 exact eσ.injective h'
3054 have hqinj : Function.Injective q := by
3055 intro b₁ b₂ hb
3056 apply hιinj
3057 apply hσinj
3058 calc
3059 σ (Fdata.inclusion b₁) = ψ b₁ := hσ.2 b₁
3060 _ = φ (q b₁) := rfl
3061 _ = φ (q b₂) := by simp only [hb]
3062 _ = ψ b₂ := rfl
3063 _ = σ (Fdata.inclusion b₂) := (hσ.2 b₂).symm
3064 have hcardEq : Fintype.card Fdata.basis = d := by
3065 have hcardLe : Fintype.card Fdata.basis ≤ d := by
3066 simpa using Fintype.card_le_of_injective q hqinj
3067 exact le_antisymm hcardLe hdleNat
3068 calc
3069 Cardinal.mk Fdata.basis = (Fintype.card Fdata.basis : Cardinal) := by simp only [Cardinal.mk_fintype]
3070 _ = d := by exact_mod_cast hcardEq
3071 _ = Generation.topologicalRank Fdata.carrier := hdEq.symm
3073/-- A pointed free pro-`C` object can be replaced by a free pro-`C` model on a set converging to
3074`1`.
3076This is the explicit bridge between pointed hypotheses and a Reidemeister-Schreier basis output
3077phrased as a converging-set basis model. -/
3079 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u}) : Prop :=
3080 ∀ {X : Type u} [TopologicalSpace X] {x0 : X}
3081 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
3082 {ι : X → F},
3083 IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι →
3084 ∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
3085 Nonempty (Fdata.carrier ≃ₜ* F)
3087/-- Apply a `PointedToConvergingSetBasisBridge` to a pointed free pro-`C` object. -/
3089 (hBridge : PointedToConvergingSetBasisBridge ProC)
3090 {X : Type u} [TopologicalSpace X] {x0 : X}
3091 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
3092 {ι : X → F}
3093 (hι : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι) :
3094 ∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
3095 Nonempty (Fdata.carrier ≃ₜ* F) :=
3096 hBridge hι
3098/-- Finite discrete pointed case of the pointed-to-converging-set bridge: remove the basepoint
3099from the pointed generating family. -/
3101 {X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X] {x0 : X}
3102 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
3103 {ι : X → F}
3104 (hι : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι) :
3106 (ProC := ProC) {x : X // x ≠ x0} F (fun x => ι x) := by
3107 classical
3108 let μ : {x : X // x ≠ x0} → F := fun x => ι x
3109 refine ⟨hι.isProC, ?_, ?_, ?_⟩
3110 · exact FamilyConvergesToOne.of_finite_domain (G := F) μ
3111 · have hrange : Set.range ι = Set.range μ ∪ ({1} : Set F) := by
3112 ext z
3113 constructor
3114 · rintro ⟨x, rfl⟩
3115 by_cases hx : x = x0
3116 · right
3117 simpa [hx] using hι.map_base
3118 · left
3119 exact ⟨⟨x, hx⟩, rfl⟩
3120 · intro hz
3121 rcases hz with hz | hz
3122 · rcases hz with ⟨x, rfl⟩
3123 exact ⟨x, rfl⟩
3124 · exact ⟨x0, hι.map_base.trans (by simpa using hz.symm)⟩
3125 have hgen' :
3126 Generation.TopologicallyGenerates (G := F) (Set.range μ ∪ ({1} : Set F)) := by
3127 simpa [μ, hrange] using hι.generates_range
3128 exact (Generation.topologicallyGenerates_union_one_iff (G := F) (X := Set.range μ)).1 hgen'
3129 · intro G _ _ _ hG φ _hφconv hgenφ
3130 let φhat : X → G := fun x => if h : x = x0 then 1 else φ ⟨x, h⟩
3131 have hφhat : Continuous φhat := continuous_of_discreteTopology
3132 have hφhat0 : φhat x0 = 1 := by
3133 simp only [ne_eq, ↓reduceDIte, φhat]
3134 have hrange : Set.range φhat = Set.range φ ∪ ({1} : Set G) := by
3135 ext z
3136 constructor
3137 · rintro ⟨x, rfl⟩
3138 by_cases hx : x = x0
3139 · right
3140 simp only [ne_eq, hx, ↓reduceDIte, mem_singleton_iff, φhat]
3141 · left
3142 exact ⟨⟨x, hx⟩, by simp only [ne_eq, hx, ↓reduceDIte, φhat]⟩
3143 · intro hz
3144 rcases hz with hz | hz
3145 · rcases hz with ⟨x, rfl⟩
3146 exact ⟨x, by simp only [ne_eq, x.2, ↓reduceDIte, Subtype.coe_eta, φhat]⟩
3147 · exact ⟨x0, by simpa [φhat] using hz.symm⟩
3148 have hφhatgen :
3149 Generation.TopologicallyGenerates (G := G) (Set.range φhat) := by
3150 have hgen' :
3151 Generation.TopologicallyGenerates (G := G) (Set.range φ ∪ ({1} : Set G)) := by
3152 exact (Generation.topologicallyGenerates_union_one_iff (G := G) (X := Set.range φ)).2 hgenφ
3153 simpa [φhat, hrange] using hgen'
3154 rcases hι.existsUnique_lift hG φhat hφhat hφhat0 hφhatgen with ⟨f, hf, huniq⟩
3155 refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
3156 · intro x
3157 simpa [μ, φhat, x.2] using hf.2 (x : X)
3158 · intro g hg
3159 apply huniq g
3160 refine ⟨hg.1, ?_⟩
3161 intro x
3162 by_cases hx : x = x0
3163 · calc
3164 g (ι x) = g (ι x0) := by rw [hx]
3165 _ = g 1 := by rw [hι.map_base]
3167 _ = φhat x := by simp only [ne_eq, hx, ↓reduceDIte, φhat]
3168 · simpa [μ, φhat, hx] using hg.2 ⟨x, hx⟩
3170/-- Finite discrete pointed case, bundled as a finite converging-set basis model. -/
3172 {X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X] {x0 : X}
3173 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
3174 {ι : X → F}
3175 (hι : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι) :
3176 ∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
3177 Nonempty (Fdata.carrier ≃ₜ* F) ∧ Finite Fdata.basis := by
3178 let B : Type u := {x : X // x ≠ x0}
3179 let Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC) :=
3180 { basis := B
3181 carrier := F
3183 instTopologicalSpace := inferInstance
3184 instIsTopologicalGroup := inferInstance
3185 inclusion := fun x => ι x
3186 isFree :=
3188 (ProC := ProC) (X := X) (x0 := x0) (F := F) (ι := ι) hι }
3189 refine ⟨Fdata, ⟨ContinuousMulEquiv.refl F⟩, ?_⟩
3190 dsimp [Fdata, B]
3191 infer_instance
3193end
3195end ProCGroups.FreeProC