Yamaguchi Lean 4 Library
Source: ProCGroups.FreeProC.Basic
ProCGroups/FreeProC/Basic/Source

Source: ProCGroups.FreeProC.Basic

1import Mathlib.GroupTheory.SpecificGroups.Cyclic
2import Mathlib.Topology.Algebra.Nonarchimedean.Basic
3import ProCGroups.Completion.UniversalProperty
4import ProCGroups.FiniteGroups.StandardClasses
5import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
6import ProCGroups.ProC.Category.Basic
7import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
9/-!
10# Pro C Groups / Free pro-C / Basic
12This module defines the free and pointed free pro-\(C\) universal properties,
13their converging-set form, and the bundled canonical source data used by later
14constructions.
15-/
17open Set
18open scoped Topology
20namespace ProCGroups.FreeProC
22universe u v w
24open ProCGroups
25open ProCGroups.FiniteGeneration
27section
31/--
32Free pro-\(C\) groups via a strengthened universal property. The lifting property quantifies
33over all continuous maps into pro-\(C\) groups, rather than only maps whose image generates the
34target.
35-/
36structure IsFreeProCGroup
37 {X : Type u} [TopologicalSpace X]
38 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
39 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
40 (ι : X → F) : Prop where
41 /--
42 Open normal subgroups with quotients in `C` form a neighborhood basis at one in `F`.
43 -/
44 hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C F
45 /-- The canonical map from the generating space into `F` is continuous. -/
46 continuous_ι : Continuous ι
47 /-- The image of the canonical map topologically generates `F`. -/
48 generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
49 /--
50 Every continuous map from `X` to a pro-`C` target extends to a unique continuous group
51 homomorphism from `F`.
52 -/
53 existsUnique_lift :
54 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
55 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G],
57 ∀ (φ : X → G), Continuous φ →
58 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x
61namespace IsFreeProCGroup
63variable {X : Type u} [TopologicalSpace X]
64variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
65variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
66variable {ι : X → F}
68/--
69A map from the chosen generators into a pro-\(C\) target extends to the corresponding continuous
70homomorphism from the free pro-\(C\) group.
71-/
72noncomputable def lift (hι : IsFreeProCGroup (C := C) ι)
73 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
74 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
75 (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : X → G)
76 (hφ : Continuous φ) : F →* G :=
77 Classical.choose (ExistsUnique.exists (hι.existsUnique_lift hG φ hφ))
79/-- The universal-property lift has the prescribed values on the chosen generators. -/
80theorem lift_spec (hι : IsFreeProCGroup (C := C) ι)
81 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
82 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
83 (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : X → G)
84 (hφ : Continuous φ) :
85 Continuous (hι.lift hG φ hφ) ∧ ∀ x, hι.lift hG φ hφ (ι x) = φ x :=
86 Classical.choose_spec (ExistsUnique.exists (hι.existsUnique_lift hG φ hφ))
88/-- The universal-property lift is unique among continuous maps with the prescribed values. -/
89theorem lift_unique (hι : IsFreeProCGroup (C := C) ι)
90 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
91 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
92 (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : X → G)
93 (hφ : Continuous φ)
94 {f : F →* G} (hf : Continuous f) (hfac : ∀ x, f (ι x) = φ x) :
95 f = hι.lift hG φ hφ := by
96 exact (hι.existsUnique_lift hG φ hφ).unique ⟨hf, hfac⟩ (hι.lift_spec hG φ hφ)
98/-- The universal-property lift bundled as a continuous monoid homomorphism. -/
99noncomputable def liftHom (hι : IsFreeProCGroup (C := C) ι)
100 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
101 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
103 (hφ : Continuous φ) : F →ₜ* G where
104 toMonoidHom := hι.lift hG φ hφ
105 continuous_toFun := (hι.lift_spec hG φ hφ).1
107/-- Forgetting continuity from liftHom gives the underlying universal-property lift. -/
108@[simp] theorem liftHom_toMonoidHom (hι : IsFreeProCGroup (C := C) ι)
109 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
110 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
112 (hφ : Continuous φ) :
113 (hι.liftHom hG φ hφ).toMonoidHom = hι.lift hG φ hφ :=
114 rfl
116/--
117The lift homomorphism from a free pro-\(C\) group evaluates according to the chosen generator
118map.
119-/
120@[simp] theorem liftHom_apply (hι : IsFreeProCGroup (C := C) ι)
121 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
122 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
124 (hφ : Continuous φ) (x : X) :
125 hι.liftHom hG φ hφ (ι x) = φ x :=
126 (hι.lift_spec hG φ hφ).2 x
128/-- The lift homomorphism is uniquely determined by its values on the generators. -/
129theorem liftHom_unique (hι : IsFreeProCGroup (C := C) ι)
130 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
131 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
133 (hφ : Continuous φ)
134 {f : F →ₜ* G} (hfac : ∀ x, f (ι x) = φ x) :
135 f = hι.liftHom hG φ hφ := by
136 ext y
137 exact congrArg (fun g : F →* G => g y)
138 (hι.lift_unique hG φ hφ f.continuous_toFun hfac)
140/--
141Continuous homomorphisms out of a free pro-\(C\) group are determined by their values on the
142chosen generators.
143-/
144theorem hom_ext (hι : IsFreeProCGroup (C := C) ι)
145 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
146 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
148 {f g : F →* G} (hf : Continuous f) (hg : Continuous g)
149 (hfg : ∀ x, f (ι x) = g (ι x)) :
150 f = g := by
151 let φ : X → G := fun x => f (ι x)
152 have hφ : Continuous φ := hf.comp hι.continuous_ι
153 exact
154 (hι.existsUnique_lift hG φ hφ).unique
155 ⟨hf, fun _ => rfl⟩ ⟨hg, fun x => (hfg x).symm⟩
157/-- Two universal-property lifts are equal when they agree on all generators. -/
158theorem lift_eq_of_forall (hι : IsFreeProCGroup (C := C) ι)
159 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
160 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
162 {φ ψ : X → G} (hφ : Continuous φ) (hψ : Continuous ψ)
163 (h : ∀ x, φ x = ψ x) :
164 hι.lift hG φ hφ = hι.lift hG ψ hψ := by
165 apply hι.hom_ext hG
166 (hι.lift_spec hG φ hφ).1
167 (hι.lift_spec hG ψ hψ).1
168 intro x
169 calc
170 hι.lift hG φ hφ (ι x) = φ x := (hι.lift_spec hG φ hφ).2 x
171 _ = ψ x := h x
172 _ = hι.lift hG ψ hψ (ι x) := ((hι.lift_spec hG ψ hψ).2 x).symm
174/-- The lift of the canonical generator map to the same free pro-\(C\) group is the identity. -/
175@[simp] theorem lift_id (hι : IsFreeProCGroup (C := C) ι) :
176 hι.lift hι.hasOpenNormalBasisInClass ι hι.continuous_ι = MonoidHom.id F := by
177 symm
178 exact hι.lift_unique hι.hasOpenNormalBasisInClass ι hι.continuous_ι continuous_id (by
179 intro x
180 rfl)
182/-- An endomorphism of a free pro-\(C\) group fixing the generators is the identity. -/
183theorem endomorphism_eq_id (hι : IsFreeProCGroup (C := C) ι)
184 {f : F →* F} (hf : Continuous f) (hfac : ∀ x, f (ι x) = ι x) :
185 f = MonoidHom.id F := by
186 exact hι.hom_ext hι.hasOpenNormalBasisInClass hf continuous_id hfac
188/-- Composition of free pro-\(C\) lifts is again the lift of the composed generator map. -/
189theorem lift_comp (hι : IsFreeProCGroup (C := C) ι)
190 {G H : Type u}
191 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
192 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
193 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
194 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
197 (φ : X → G) (hφ : Continuous φ)
198 (ψ : G →* H) (hψ : Continuous ψ) :
199 ψ.comp (hι.lift hG φ hφ) =
200 hι.lift hH (fun x => ψ (φ x)) (hψ.comp hφ) := by
201 apply hι.lift_unique hH (fun x => ψ (φ x)) (hψ.comp hφ)
202 (hψ.comp (hι.lift_spec hG φ hφ).1)
203 intro x
204 simp only [MonoidHom.coe_comp, Function.comp_apply, (hι.lift_spec hG φ hφ).2 x]
207end IsFreeProCGroup
210end
212section
216/-- A family converges to `1` when it tends to `1` along the cofinite filter. -/
217def FamilyConvergesToOne
218 {X : Type v}
219 {G : Type u} [Group G] [TopologicalSpace G]
220 (μ : X → G) : Prop :=
221 Filter.Tendsto μ Filter.cofinite (𝓝 1)
223/-- The weaker condition obtained by testing family convergence only against open subgroups. -/
224def FamilyConvergesToOneAlongOpenSubgroups
225 {X : Type v}
226 {G : Type u} [Group G] [TopologicalSpace G]
227 (μ : X → G) : Prop :=
228 ∀ U : OpenSubgroup G, {x : X | μ x ∉ (U : Set G)}.Finite
230namespace FamilyConvergesToOne
232variable {X : Type v}
233variable {G : Type u} [Group G] [TopologicalSpace G]
235/-- Genuine family convergence implies convergence along open subgroups. -/
236theorem to_alongOpenSubgroups {μ : X → G}
237 (hμ : FamilyConvergesToOne (G := G) μ) :
238 FamilyConvergesToOneAlongOpenSubgroups (G := G) μ := by
239 intro U
240 have hU : (U : Set G) ∈ 𝓝 (1 : G) :=
241 U.isOpen.mem_nhds U.one_mem
242 have heventually : ∀ᶠ x : X in Filter.cofinite, μ x ∈ U :=
243 hμ.eventually hU
244 change {x : X | μ x ∈ U} ∈ Filter.cofinite at heventually
245 rw [Filter.mem_cofinite] at heventually
246 simpa only [Set.compl_setOf, SetLike.mem_coe] using heventually
248/-- Convergence is preserved by a continuous homomorphism. -/
249theorem comp
250 {H : Type*} [TopologicalSpace H] [Group H]
251 {μ : X → G}
252 (hμ : FamilyConvergesToOne (G := G) μ) (f : G →ₜ* H) :
253 FamilyConvergesToOne (G := H) (fun x => f (μ x)) := by
254 change Filter.Tendsto (f.toContinuousMap ∘ μ) Filter.cofinite (𝓝 1)
255 have hf1 : f.toContinuousMap (1 : G) = 1 := f.map_one
256 simpa only [hf1] using (f.continuous.tendsto (1 : G)).comp hμ
258/-- Families indexed by a finite type converge to `1`. -/
259theorem of_finite_domain [Finite X] (μ : X → G) :
260 FamilyConvergesToOne (G := G) μ := by
261 rw [FamilyConvergesToOne, Filter.tendsto_def]
262 intro W _
263 rw [Filter.mem_cofinite]
264 exact Set.toFinite _
266/-- On an infinite index type in a `T₁` space, a constant family converges to `1` exactly when
267its value is `1`. In particular, the old open-subgroup-only counterexample is rejected. -/
268theorem const_iff [Infinite X] [T1Space G] (g : G) :
269 FamilyConvergesToOne (G := G) (fun _ : X => g) ↔ g = 1 := by
270 simp only [FamilyConvergesToOne, tendsto_const_nhds_iff]
272end FamilyConvergesToOne
274namespace FamilyConvergesToOneAlongOpenSubgroups
276variable {X : Type v}
277variable {G : Type u} [Group G] [TopologicalSpace G]
279/-- A family converging to `1` has range converging to `1` as a set. -/
280theorem range {μ : X → G} (hμ : FamilyConvergesToOneAlongOpenSubgroups (G := G) μ) :
281 Generation.ConvergesToOneAlongOpenSubgroups (G := G) (Set.range μ) := by
282 intro U
283 have hsubset :
284 Set.range μ \ (U : Set G) ⊆ μ '' {x : X | μ x ∉ (U : Set G)} := by
285 rintro y ⟨⟨x, rfl⟩, hxU⟩
286 exact ⟨x, hxU, rfl⟩
287 exact (hμ U).image μ |>.subset hsubset
289/-- Convergence to `1` is preserved by a continuous homomorphism. -/
290theorem comp
291 {H : Type*} [TopologicalSpace H] [Group H]
292 {μ : X → G}
293 (hμ : FamilyConvergesToOneAlongOpenSubgroups (G := G) μ) (f : G →ₜ* H) :
294 FamilyConvergesToOneAlongOpenSubgroups (G := H) (fun x => f (μ x)) := by
295 intro U
296 simpa using hμ (OpenSubgroup.comap (f := (f : G →* H)) f.continuous U)
298/-- Range convergence implies family convergence for injectively indexed families. -/
299theorem of_set_of_injective {μ : X → G}
300 (hμ : Generation.ConvergesToOneAlongOpenSubgroups (G := G) (Set.range μ))
301 (hinj : Function.Injective μ) :
302 FamilyConvergesToOneAlongOpenSubgroups (G := G) μ := by
303 intro U
304 have himage :
305 μ '' {x : X | μ x ∉ (U : Set G)} = Set.range μ \ (U : Set G) := by
306 ext y
307 constructor
308 · rintro ⟨x, hxU, rfl⟩
309 exact ⟨⟨x, rfl⟩, hxU⟩
310 · rintro ⟨⟨x, rfl⟩, hxU⟩
311 exact ⟨x, hxU, rfl⟩
312 letI : Finite (μ '' {x : X | μ x ∉ (U : Set G)}) := by
313 rw [himage]
314 exact (hμ U).to_subtype
315 exact Finite.Set.finite_of_finite_image {x : X | μ x ∉ (U : Set G)} (by
316 intro a _ b _ hab
317 exact hinj hab)
319/-- Families indexed by a finite type converge to `1`. -/
320theorem of_finite_domain [Finite X] (μ : X → G) :
321 FamilyConvergesToOneAlongOpenSubgroups (G := G) μ := by
322 intro U
323 exact Set.finite_univ.subset (by intro x _; trivial)
325/-- In a nonarchimedean group, open subgroups detect genuine family convergence. -/
326theorem to_familyConvergesToOne [NonarchimedeanGroup G] {μ : X → G}
327 (hμ : FamilyConvergesToOneAlongOpenSubgroups (G := G) μ) :
328 FamilyConvergesToOne (G := G) μ := by
329 rw [FamilyConvergesToOne, Filter.tendsto_def]
330 intro W hW
331 obtain ⟨U, hUW⟩ := NonarchimedeanGroup.is_nonarchimedean W hW
332 rw [Filter.mem_cofinite]
333 change {x : X | μ x ∉ W}.Finite
334 exact (hμ U).subset (by
335 intro x hxW hxU
336 exact hxW (hUW hxU))
338end FamilyConvergesToOneAlongOpenSubgroups
340/-- For nonarchimedean groups, genuine family convergence is equivalent to the
341open-subgroup test. -/
342theorem familyConvergesToOne_iff_alongOpenSubgroups
343 {X : Type v} {G : Type u} [Group G] [TopologicalSpace G]
344 [NonarchimedeanGroup G] {μ : X → G} :
345 FamilyConvergesToOne (G := G) μ ↔
346 FamilyConvergesToOneAlongOpenSubgroups (G := G) μ :=
347 ⟨FamilyConvergesToOne.to_alongOpenSubgroups,
348 FamilyConvergesToOneAlongOpenSubgroups.to_familyConvergesToOne⟩
350/-- An open-subgroup-convergent family whose image topologically generates the target; here
351convergence means finiteness outside every open subgroup. -/
352structure ConvergingGeneratingMap
353 (X : Type v)
354 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
355 /-- The family of elements of `G`, indexed by `X`. -/
356 toFun : X → G
357 /--
358 Outside every open subgroup of `G`, the family has only finitely many terms; thus it converges
359 to one in the open-subgroup sense.
360 -/
361 convergesToOneAlongOpenSubgroups : FamilyConvergesToOneAlongOpenSubgroups (G := G) toFun
362 /-- The range of the family topologically generates `G`. -/
363 generates : Generation.TopologicallyGenerates (G := G) (Set.range toFun)
365namespace ConvergingGeneratingMap
367variable {X Y : Type v}
368variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
370/-- A convergent generating map coerces to its underlying map into the group. -/
371instance instCoeFunConvergingGeneratingMap :
372 CoeFun (ConvergingGeneratingMap X G) (fun _ => X → G) where
373 coe φ := φ.toFun
375/-- The stored function of a convergent generating map agrees with its function coercion. -/
376@[simp] theorem toFun_eq_coe (φ : ConvergingGeneratingMap X G) :
377 φ.toFun = (φ : X → G) := rfl
379/-- Reindexing along an equivalence preserves family convergence and generation. -/
380def reindex (φ : ConvergingGeneratingMap X G) (e : Y ≃ X) :
381 ConvergingGeneratingMap Y G where
382 toFun := fun y => φ (e y)
383 convergesToOneAlongOpenSubgroups := by
384 intro U
385 have hsubset :
386 {y : Y | φ (e y) ∉ (U : Set G)} ⊆
387 e.symm '' {x : X | φ x ∉ (U : Set G)} := by
388 intro y hy
389 exact ⟨e y, hy, by simp only [Equiv.symm_apply_apply]⟩
390 exact (φ.convergesToOneAlongOpenSubgroups U).image e.symm |>.subset hsubset
391 generates := by
392 have hrange : Set.range (fun y : Y => φ (e y)) = Set.range (φ : X → G) := by
393 ext z
394 constructor
395 · rintro ⟨y, rfl⟩
396 exact ⟨e y, rfl⟩
397 · rintro ⟨x, rfl⟩
398 exact ⟨e.symm x, by simp only [Equiv.apply_symm_apply]⟩
399 simpa [hrange] using φ.generates
401/-- The range of a convergent generating map generates the group and converges to one along open
402subgroups. -/
403theorem generatesAndConvergesToOneAlongOpenSubgroups (φ : ConvergingGeneratingMap X G) :
404 Generation.GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) (Set.range (φ : X → G)) :=
405 ⟨φ.generates, φ.convergesToOneAlongOpenSubgroups.range⟩
407end ConvergingGeneratingMap
409/-- A pointed pro-`C` group with unique lifts only for pointed maps whose images topologically
410generate their targets.
412This is intentionally not the unrestricted pointed-free universal property. -/
413structure IsEpimorphicallyPointedFreeProCGroupOn
414 (X : Type u) [TopologicalSpace X] (x0 : X)
415 (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
416 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
417 (ι : X → F) : Prop where
418 /--
419 Open normal subgroups with quotients in `C` form a neighborhood basis at one in `F`.
420 -/
421 hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C F
422 /-- The canonical pointed map into `F` is continuous. -/
423 continuous_ι : Continuous ι
424 /-- The distinguished source point `x0` is sent to the identity of `F`. -/
425 map_base : ι x0 = 1
426 /-- The image of the canonical pointed map topologically generates `F`. -/
427 generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
428 /--
429 Every continuous, basepoint-preserving map whose image generates a pro-`C` target extends to
430 a unique continuous group homomorphism from `F`.
431 -/
432 existsUnique_lift :
433 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
434 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G],
436 ∀ (φ : X → G), Continuous φ → φ x0 = 1 →
437 Generation.TopologicallyGenerates (G := G) (Set.range φ) →
438 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x
440/-- A pro-`C` group with unique lifts only for open-subgroup-convergent families whose images
441topologically generate their targets. The convergence hypothesis is
442`FamilyConvergesToOneAlongOpenSubgroups`, not the unqualified filter predicate.
444The `Epimorphically` qualifier records the missing unrestricted mapping property. -/
445structure IsEpimorphicallyFreeProCGroupOnConvergingSet
446 (X : Type v)
447 (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
448 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
449 (ι : X → F) : Prop where
450 /--
451 Open normal subgroups with quotients in `C` form a neighborhood basis at one in `F`.
452 -/
453 hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C F
454 /--
455 The canonical generator family has only finitely many terms outside each open subgroup of
456 `F`.
457 -/
458 convergesToOneAlongOpenSubgroups : FamilyConvergesToOneAlongOpenSubgroups (G := F) ι
459 /-- The canonical converging family topologically generates `F`. -/
460 generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
461 /--
462 Every converging family that topologically generates a pro-`C` target extends to a unique
463 continuous group homomorphism from `F`.
464 -/
465 existsUnique_lift :
466 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
467 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G],
469 ∀ (φ : X → G), FamilyConvergesToOneAlongOpenSubgroups (G := G) φ →
470 Generation.TopologicallyGenerates (G := G) (Set.range φ) →
471 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x
473/-- The canonical map of a free pro-`C` group on a topological space is injective whenever the
474predicate supplies enough separating pro-`C` targets. -/
475theorem freeProCGroupOn_injective
476 {X : Type u} [TopologicalSpace X]
477 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
478 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
479 {ι : X → F}
480 (hι : IsFreeProCGroup (C := C) ι)
481 (hsep :
482 ∀ ⦃x y : X⦄, x ≠ y →
483 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
484 (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
486 ∃ φ : X → A, Continuous φ ∧
487 Generation.TopologicallyGenerates (G := A) (Set.range φ) ∧ φ x ≠ φ y) :
488 Function.Injective ι := by
489 intro x y hEq
490 by_contra hxy
491 rcases hsep hxy with
492 ⟨A, _instGroupA, _instTopA, _instTopGroupA, _instCompactA, _instT2A, _instTDA,
493 hA, φ, hφ, hgenφ, hφxy⟩
494 rcases hι.existsUnique_lift hA φ hφ with ⟨f, hf, _huniq⟩
495 have hcontr : φ x = φ y := by
496 simpa [hf.2 x, hf.2 y] using congrArg f hEq
497 exact hφxy hcontr
499/-- Under an explicit nontrivial cyclic pro-`C` target hypothesis, the identity does not lie in
500the image of the topological basis of a free pro-`C` group. -/
501theorem one_not_mem_range_of_freeProCGroupOn
502 {X : Type u} [TopologicalSpace X] [Nonempty X]
503 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
504 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
505 {ι : X → F}
506 (hι : IsFreeProCGroup (C := C) ι)
507 (hnontrivial :
508 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
509 (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
510 ProCGroups.ProC.HasOpenNormalBasisInClass C A ∧ ∃ a : A, a ≠ 1 ∧
511 Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
512 (1 : F) ∉ Set.range ι := by
513 intro h1
514 rcases h1 with ⟨x, hx⟩
515 rcases hnontrivial with
516 ⟨A, _instGroupA, _instTopA, _instTopGroupA, _instCompactA, _instT2A, _instTDA,
517 hA, a, ha1, hgena⟩
518 let φ : X → A := fun _ => a
519 have hφ : Continuous φ := continuous_const
520 have hrange : Set.range φ = ({a} : Set A) := by
521 ext b
522 constructor
523 · rintro ⟨y, rfl⟩
524 simp only [mem_singleton_iff, φ]
525 · intro hb
526 rw [Set.mem_singleton_iff] at hb
527 subst b
528 exact ⟨Classical.choice ‹Nonempty X›, rfl⟩
529 have hgenφ : Generation.TopologicallyGenerates (G := A) (Set.range φ) := by
530 simpa [hrange] using hgena
531 rcases hι.existsUnique_lift hA φ hφ with ⟨f, hf, _huniq⟩
532 have haeq : a = 1 := by
533 simpa [φ, hx] using (hf.2 x).symm
534 exact ha1 haeq
536/-- Under an explicit nontrivial cyclic pro-`C` target hypothesis, the identity does not lie in a
537basis converging to `1`. -/
538theorem one_not_mem_range_of_epimorphicallyFreeProCGroupOnConvergingSet
539 {X : Type u}
540 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
541 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
542 {ι : X → F}
543 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
544 (hnontrivial :
545 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
546 (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
547 ProCGroups.ProC.HasOpenNormalBasisInClass C A ∧ ∃ a : A, a ≠ 1 ∧
548 Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
549 (1 : F) ∉ Set.range ι := by
550 classical
551 intro h1
552 rcases h1 with ⟨x, hx⟩
553 rcases hnontrivial with
554 ⟨A, _instGroupA, _instTopA, _instTopGroupA, _instCompactA, _instT2A, _instTDA,
555 hA, a, ha1, hgena⟩
556 let φ : X → A := fun z => if z = x then a else 1
557 have hφconv : FamilyConvergesToOneAlongOpenSubgroups (G := A) φ := by
558 intro U
559 have hsubset : {z : X | φ z ∉ (U : Set A)} ⊆ ({x} : Set X) := by
560 intro z hz
561 by_cases hzx : z = x
562 · simp only [hzx, mem_singleton_iff]
563 · exfalso
564 exact hz (by simp only [hzx, ↓reduceIte, SetLike.mem_coe, one_mem, φ])
565 exact (Set.finite_singleton x).subset hsubset
566 have hφgen : Generation.TopologicallyGenerates (G := A) (Set.range φ) := by
567 have hsub : ({a} : Set A) ⊆ Set.range φ := by
568 intro z hz
569 rw [Set.mem_singleton_iff] at hz
570 subst z
571 exact ⟨x, by simp only [↓reduceIte, φ]⟩
572 exact Generation.topologicallyGenerates_mono (G := A) hgena hsub
573 rcases hι.existsUnique_lift hA φ hφconv hφgen with ⟨f, hf, _⟩
574 have haeq : a = 1 := by
575 simpa [φ, hx] using (hf.2 x).symm
576 exact ha1 haeq
578/-- Under the same nontrivial cyclic-target hypothesis, the basis map for a free pro-`C` group on
579a set converging to `1` is injective. -/
580theorem epimorphicallyFreeProCGroupOnConvergingSet_injective
581 {X : Type u}
582 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
583 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
584 {ι : X → F}
585 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
586 (hnontrivial :
587 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
588 (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
589 ProCGroups.ProC.HasOpenNormalBasisInClass C A ∧ ∃ a : A, a ≠ 1 ∧
590 Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
591 Function.Injective ι := by
592 classical
593 intro x y hEq
594 by_contra hxy
595 rcases hnontrivial with
596 ⟨A, _instGroupA, _instTopA, _instTopGroupA, _instCompactA, _instT2A, _instTDA,
597 hA, a, ha1, hgena⟩
598 have hyx : y ≠ x := by
599 intro hyx'
600 exact hxy hyx'.symm
601 let φ : X → A := fun z => if z = x then a else 1
602 have hφconv : FamilyConvergesToOneAlongOpenSubgroups (G := A) φ := by
603 intro U
604 have hsubset : {z : X | φ z ∉ (U : Set A)} ⊆ ({x} : Set X) := by
605 intro z hz
606 by_cases hzx : z = x
607 · simp only [hzx, mem_singleton_iff]
608 · exfalso
609 exact hz (by simp only [hzx, ↓reduceIte, SetLike.mem_coe, one_mem, φ])
610 exact (Set.finite_singleton x).subset hsubset
611 have hφgen : Generation.TopologicallyGenerates (G := A) (Set.range φ) := by
612 have hsub : ({a} : Set A) ⊆ Set.range φ := by
613 intro z hz
614 rw [Set.mem_singleton_iff] at hz
615 subst z
616 exact ⟨x, by simp only [↓reduceIte, φ]⟩
617 exact Generation.topologicallyGenerates_mono (G := A) hgena hsub
618 rcases hι.existsUnique_lift hA φ hφconv hφgen with ⟨f, hf, _⟩
619 have hfa : f (ι x) = a := by
620 simpa [φ] using hf.2 x
621 have hf1 : f (ι y) = 1 := by
622 simpa [φ, hyx] using hf.2 y
623 have haeq : a = 1 := by
624 rw [← hfa, ← hf1]
625 exact congrArg f hEq
626 exact ha1 haeq
628/-- A nontrivial cyclic topological group has a nontrivial singleton topological generator. -/
629theorem exists_nontrivial_singleton_topologicalGenerator
630 {A : Type u} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]
631 [IsCyclic A] [Nontrivial A] :
632 ∃ a : A, a ≠ 1 ∧ Generation.TopologicallyGenerates (G := A) ({a} : Set A) := by
633 obtain ⟨a, ha⟩ := IsCyclic.exists_generator (α := A)
634 have ha1 : a ≠ 1 := by
635 intro hEq
636 have hallOne : ∀ x : A, x = 1 := by
637 intro x
638 obtain ⟨n, hn⟩ := Subgroup.mem_zpowers_iff.mp (ha x)
639 simpa [hEq] using hn.symm
640 exact not_subsingleton A ⟨fun x y => by rw [hallOne x, hallOne y]⟩
641 refine ⟨a, ha1, ?_⟩
642 rw [Generation.TopologicallyGenerates]
643 apply top_unique
644 intro x _
645 exact Subgroup.le_topologicalClosure _ <| by
646 simpa [Subgroup.zpowers_eq_closure] using ha x
648/-- A concrete finite-group class containing a nontrivial finite cyclic group admits a
649nontrivial topologically cyclic pro-`C` model. -/
650theorem exists_nontrivial_topologicallyCyclic_proC_of_finiteGroupClass
651 (C : ProCGroups.FiniteGroupClass.{u})
653 (hcyc :
654 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
655 C A ∧ IsCyclic A ∧ Nontrivial A) :
656 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
657 (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
659 ∃ a : A, a ≠ 1 ∧ Generation.TopologicallyGenerates (G := A) ({a} : Set A) := by
660 rcases hcyc with ⟨A, _instGroupA, _instFiniteA, hCA, hAcyc, hAnontriv⟩
661 let _ : TopologicalSpace A := ⊥
662 let _ : DiscreteTopology A := ⟨rfl⟩
663 let _ : IsTopologicalGroup A := by infer_instance
664 letI : IsCyclic A := hAcyc
665 letI : Nontrivial A := hAnontriv
668 (C := C) (G := A) hquot hCA
669 rcases exists_nontrivial_singleton_topologicalGenerator (A := A) with ⟨a, ha1, hgena⟩
670 exact
671 ⟨A, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
672 hAProC, a, ha1, hgena⟩
674/-- For a finite-rank free pro-`C` group, any generating family with the same finite cardinality
675is again a converging-set basis. -/
676theorem finite_generatingFamily_is_basis
677 {X : Type u} {Y : Type u}
678 [Finite X] [Finite Y]
679 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
680 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
681 {ι : X → F} {μ : Y → F}
682 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
683 (hcard : Cardinal.mk X = Cardinal.mk Y)
684 (hgen : Generation.TopologicallyGenerates (G := F) (Set.range μ)) :
685 IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) Y F μ := by
686 classical
687 have hXY : Nonempty (X ≃ Y) := by
688 simpa [← Cardinal.eq] using hcard
689 let eXY : X ≃ Y := Classical.choice hXY
690 let ψ : X → F := fun x => μ (eXY x)
691 have hψconv : FamilyConvergesToOneAlongOpenSubgroups (G := F) ψ := by
692 exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := F) ψ
693 have hψgen : Generation.TopologicallyGenerates (G := F) (Set.range ψ) := by
694 have hrange : Set.range ψ = Set.range μ := by
695 ext z
696 constructor
697 · rintro ⟨x, rfl⟩
698 exact ⟨eXY x, rfl⟩
699 · rintro ⟨y, rfl⟩
700 exact ⟨eXY.symm y, by simp only [Equiv.apply_symm_apply, ψ]⟩
701 simpa [hrange] using hgen
702 rcases hι.existsUnique_lift hι.hasOpenNormalBasisInClass ψ hψconv hψgen with ⟨σ, hσ, hσuniq⟩
703 have hrangeμ : Set.range μ ⊆ (σ.range : Set F) := by
704 rintro z ⟨y, rfl⟩
705 exact ⟨ι (eXY.symm y), by simpa [ψ] using hσ.2 (eXY.symm y)⟩
706 have hσgen : Generation.TopologicallyGenerates (G := F) ((σ.range : Set F)) :=
707 Generation.topologicallyGenerates_mono (G := F) hgen hrangeμ
708 have hσclosed : IsClosed ((σ.range : Set F)) := by
709 simpa using (isCompact_range hσ.1).isClosed
710 have hσclosure_le : (σ.range : Subgroup F).topologicalClosure ≤ σ.range :=
711 Subgroup.topologicalClosure_minimal _ le_rfl hσclosed
712 have hσclosure_top : (σ.range : Subgroup F).topologicalClosure = ⊤ := by
713 have htop :
714 (Subgroup.closure (σ.range : Set F)).topologicalClosure = (⊤ : Subgroup F) := by
715 simpa [Generation.TopologicallyGenerates] using hσgen
716 have hclosure_eq : (σ.range : Subgroup F) = Subgroup.closure (σ.range : Set F) := by
717 simpa using (Subgroup.closure_eq (σ.range)).symm
718 rw [hclosure_eq]
719 exact htop
720 have hσrange_top : σ.range = ⊤ := by
721 apply top_unique
722 intro z hz
723 have hz' : z ∈ ((σ.range : Subgroup F).topologicalClosure : Set F) := by
724 rw [hσclosure_top]
725 simp only [Subgroup.coe_top, mem_univ]
726 exact hσclosure_le hz'
727 have hσsurj : Function.Surjective σ := by
728 intro z
729 have hz : z ∈ (σ.range : Set F) := by
730 simp only [hσrange_top, Subgroup.coe_top, mem_univ]
731 simpa using hz
732 let σc : ContinuousMonoidHom F F :=
733 { toMonoidHom := σ
734 continuous_toFun := hσ.1 }
735 have hFG : _root_.ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated F := by
736 letI : Fintype Y := Fintype.ofFinite Y
737 refine ⟨Finset.univ.image μ, ?_⟩
738 simpa [Finset.coe_image] using hgen
739 rcases
740 (surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated
741 (G := F)) hFG σc hσsurj with
742 ⟨e, he⟩
743 refine ⟨hι.hasOpenNormalBasisInClass, ?_, hgen, ?_⟩
744 · exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := F) μ
745 · intro G _ _ _ _ _ _ hG φ hφ hgenφ
746 let φX : X → G := fun x => φ (eXY x)
747 have hφXconv : FamilyConvergesToOneAlongOpenSubgroups (G := G) φX := by
748 exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := G) φX
749 have hφXgen : Generation.TopologicallyGenerates (G := G) (Set.range φX) := by
750 have hrange : Set.range φX = Set.range φ := by
751 ext z
752 constructor
753 · rintro ⟨x, rfl⟩
754 exact ⟨eXY x, rfl⟩
755 · rintro ⟨y, rfl⟩
756 exact ⟨eXY.symm y, by simp only [Equiv.apply_symm_apply, φX]⟩
757 simpa [hrange] using hgenφ
758 rcases hι.existsUnique_lift hG φX hφXconv hφXgen with ⟨fX, hfX, hfXuniq⟩
759 let fY : F →* G := fX.comp e.symm.toMonoidHom
760 refine ⟨fY, ⟨hfX.1.comp e.symm.continuous, ?_⟩, ?_⟩
761 · intro y
762 have hpre : e.symm (μ y) = ι (eXY.symm y) := by
763 apply e.injective
764 calc
765 e (e.symm (μ y)) = μ y := by simp only [ContinuousMulEquiv.apply_symm_apply]
766 _ = σ (ι (eXY.symm y)) := by
767 symm
768 simpa [ψ] using hσ.2 (eXY.symm y)
769 _ = e (ι (eXY.symm y)) := by
770 have h := (he (ι (eXY.symm y))).symm
771 change σ (ι (eXY.symm y)) = e (ι (eXY.symm y)) at h
772 exact h
773 calc
774 fY (μ y) = fX (e.symm (μ y)) := rfl
775 _ = fX (ι (eXY.symm y)) := by rw [hpre]
776 _ = φX (eXY.symm y) := hfX.2 (eXY.symm y)
777 _ = φ y := by simp only [Equiv.apply_symm_apply, φX]
778 · intro g hg
779 have hcomp : g.comp e.toMonoidHom = fX := by
780 apply hfXuniq
781 refine ⟨hg.1.comp e.continuous, ?_⟩
782 intro x
783 calc
784 (g.comp e.toMonoidHom) (ι x) = g (e (ι x)) := rfl
785 _ = g (σ (ι x)) := by
786 have h := he (ι x)
787 change e (ι x) = σ (ι x) at h
788 exact congrArg g h
789 _ = g (μ (eXY x)) := by
790 exact congrArg g (by simpa [ψ] using hσ.2 x)
791 _ = φ (eXY x) := hg.2 (eXY x)
792 _ = φX x := rfl
793 ext z
794 have hz := congrArg (fun k : F →* G => k (e.symm z)) hcomp
795 have hz' : g (e (e.symm z)) = fX (e.symm z) := by
796 change (g.comp e.toMonoidHom) (e.symm z) = fX (e.symm z)
797 exact hz
798 calc
799 g z = g (e (e.symm z)) := by
800 exact congrArg g (e.apply_symm_apply z).symm
801 _ = fX (e.symm z) := hz'
802 _ = fY z := rfl
804/-- Concrete finite-group-class specialization of `finite_generatingFamily_is_basis`. -/
805theorem finite_generatingFamily_is_basis_of_finiteGroupClass
806 (C : ProCGroups.FiniteGroupClass.{u})
807 {X : Type u} {Y : Type u}
808 [Finite X] [Finite Y]
809 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
810 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
811 {ι : X → F} {μ : Y → F}
812 (hι :
813 IsEpimorphicallyFreeProCGroupOnConvergingSet
814 (C := C) X F ι)
815 (hcard : Cardinal.mk X = Cardinal.mk Y)
816 (hgen : Generation.TopologicallyGenerates (G := F) (Set.range μ)) :
817 IsEpimorphicallyFreeProCGroupOnConvergingSet
818 (C := C) Y F μ := by
819 exact finite_generatingFamily_is_basis
820 (C := C)
821 hι hcard hgen
823/-- Concrete finite-group-class specialization when a nontrivial cyclic target is available. -/
824theorem finite_generatingFamily_is_basis_of_finiteGroupClass_cyclic
825 (C : ProCGroups.FiniteGroupClass.{u})
827 (hcyc :
828 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
829 C A ∧ IsCyclic A ∧ Nontrivial A)
830 {X : Type u} {Y : Type u}
831 [Finite X] [Finite Y]
832 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
833 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
834 {ι : X → F} {μ : Y → F}
835 (hι :
836 IsEpimorphicallyFreeProCGroupOnConvergingSet
837 (C := C) X F ι)
838 (hcard : Cardinal.mk X = Cardinal.mk Y)
839 (hgen : Generation.TopologicallyGenerates (G := F) (Set.range μ)) :
840 IsEpimorphicallyFreeProCGroupOnConvergingSet
841 (C := C) Y F μ := by
842 rcases exists_nontrivial_topologicallyCyclic_proC_of_finiteGroupClass C hquot hcyc with
843 ⟨A, _instGroupA, _instTopA, _instTopGroupA, _instCompactA, _instT2A, _instTDA,
844 hA, a, ha1, hgena⟩
845 exact finite_generatingFamily_is_basis
846 (C := C)
847 hι hcard hgen
849/--
850If a continuous homomorphism has range containing a topological generating set, then it is
851surjective between profinite groups.
852-/
853theorem surjective_hom_of_rangeContainsGeneratingSet
854 {X : Type u}
855 {F : Type u} [Group F] [TopologicalSpace F] [CompactSpace F]
856 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
857 {ι : X → G}
858 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range ι))
859 {σ : F →* G} (hσ : Continuous σ)
860 (hsub : Set.range ι ⊆ (σ.range : Set G)) :
861 Function.Surjective σ := by
862 have hσgen : Generation.TopologicallyGenerates (G := G) ((σ.range : Set G)) :=
863 Generation.topologicallyGenerates_mono (G := G) hgen hsub
864 have hσclosed : IsClosed ((σ.range : Set G)) := by
865 simpa using (isCompact_range hσ).isClosed
866 have hσclosure_le : (σ.range : Subgroup G).topologicalClosure ≤ σ.range :=
867 Subgroup.topologicalClosure_minimal _ le_rfl hσclosed
868 have hσclosure_top : (σ.range : Subgroup G).topologicalClosure = ⊤ := by
869 have htop :
870 (Subgroup.closure (σ.range : Set G)).topologicalClosure = (⊤ : Subgroup G) := by
871 simpa [Generation.TopologicallyGenerates] using hσgen
872 have hclosure_eq : (σ.range : Subgroup G) = Subgroup.closure (σ.range : Set G) := by
873 simpa using (Subgroup.closure_eq (σ.range)).symm
874 rw [hclosure_eq]
875 exact htop
876 have hσrange_top : σ.range = ⊤ := by
877 apply top_unique
878 intro z hz
879 have hz' : z ∈ ((σ.range : Subgroup G).topologicalClosure : Set G) := by
880 rw [hσclosure_top]
881 simp only [Subgroup.coe_top, mem_univ]
882 exact hσclosure_le hz'
883 intro z
884 have hz : z ∈ (σ.range : Set G) := by
885 simp only [hσrange_top, Subgroup.coe_top, mem_univ]
886 simpa using hz
888/-- A topologically finitely generated free pro-`C` group on a converging set has finite basis,
889provided `C` admits a nontrivial cyclic pro-`C` target. -/
890theorem finite_of_topologicallyFinitelyGenerated_epimorphicallyFreeProCGroupOnConvergingSet
891 {X : Type u}
892 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
893 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
894 {ι : X → F}
895 (hfg : FiniteGeneration.TopologicallyFinitelyGenerated F)
896 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
897 (hnontrivial :
898 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
899 (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
900 ProCGroups.ProC.HasOpenNormalBasisInClass C A ∧ ∃ a : A, a ≠ 1 ∧
901 Generation.TopologicallyGenerates (G := A) ({a} : Set A)) :
902 Finite X := by
903 classical
904 by_cases hXfin : Finite X
905 · exact hXfin
906 · have hXinf : Infinite X := by
907 by_contra hXnotinf
908 exact hXfin (not_infinite_iff_finite.mp hXnotinf)
909 letI : Infinite X := hXinf
910 letI : Nonempty X := Infinite.nonempty (α := X)
911 rcases
912 (FiniteGeneration.topologicallyFinitelyGenerated_iff_exists_topologicallyGeneratedByAtMost
913 (G := F)).mp hfg with
914 ⟨_n, s, _hsle, hgen⟩
915 have hsle : Cardinal.mk ↥s ≤ Cardinal.mk X := by
916 exact (show Cardinal.mk ↥s < Cardinal.mk X from calc
917 Cardinal.mk ↥s < Cardinal.aleph0 := by
918 exact (Cardinal.mk_lt_aleph0_iff).2 (Finite.of_fintype ↥s)
919 _ ≤ Cardinal.mk X := Cardinal.aleph0_le_mk X).le
920 have hsle' : Cardinal.mk ↥s ≤ Cardinal.mk (Set.univ : Set X) := by
921 simpa using hsle
922 obtain ⟨p, _hpSub, hpCard⟩ := (Cardinal.le_mk_iff_exists_subset
923 (c := Cardinal.mk ↥s) (s := (Set.univ : Set X))).1 hsle'
924 have hpEquiv : Nonempty (p ≃ ↥s) := by
925 simpa [← Cardinal.eq] using hpCard
926 let e : p ≃ ↥s := Classical.choice hpEquiv
927 have hpfinite : p.Finite :=
928 Set.finite_coe_iff.mp (Finite.of_equiv (↥s) e.symm)
929 let φ : X → F := fun x => if hx : x ∈ p then (e ⟨x, hx⟩ : F) else 1
930 have hφconv : FamilyConvergesToOneAlongOpenSubgroups (G := F) φ := by
931 intro U
932 have hsubset : {x : X | φ x ∉ (U : Set F)} ⊆ p := by
933 intro x hx
934 by_cases hxp : x ∈ p
935 · exact hxp
936 · exfalso
937 exact hx (by simp only [hxp, ↓reduceDIte, SetLike.mem_coe, one_mem, φ])
938 exact hpfinite.subset hsubset
939 have hφgen : Generation.TopologicallyGenerates (G := F) (Set.range φ) := by
940 have hsub : (s : Set F) ⊆ Set.range φ := by
941 intro z hz
942 let a : ↥s := ⟨z, hz⟩
943 refine ⟨(e.symm a).1, ?_⟩
944 have hp : (e.symm a).1 ∈ p := (e.symm a).2
945 simp only [hp, ↓reduceDIte, Subtype.coe_eta, Equiv.apply_symm_apply, φ, a]
946 exact Generation.topologicallyGenerates_mono (G := F) hgen hsub
947 rcases hι.existsUnique_lift hι.hasOpenNormalBasisInClass φ hφconv hφgen with ⟨σ, hσ, _⟩
948 have hφsubσ : Set.range φ ⊆ (σ.range : Set F) := by
949 rintro z ⟨x, rfl⟩
950 exact ⟨ι x, hσ.2 x⟩
951 have hσsurj : Function.Surjective σ :=
952 surjective_hom_of_rangeContainsGeneratingSet
953 hφgen hσ.1 hφsubσ
954 let σc : ContinuousMonoidHom F F := {
955 toMonoidHom := σ
956 continuous_toFun := hσ.1
957 }
958 rcases
959 (surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated
960 (G := F))
961 hfg σc hσsurj with
962 ⟨eσ, heσ⟩
963 have hσinj : Function.Injective σ := by
964 intro a b hab
965 have h' : eσ a = eσ b := by
966 calc
967 eσ a = σ a := by
968 have h := heσ a
969 change eσ a = σ a at h
970 exact h
971 _ = σ b := hab
972 _ = eσ b := by
973 have h := (heσ b).symm
974 change σ b = eσ b at h
975 exact h
976 exact eσ.injective h'
977 have hιinj : Function.Injective ι :=
978 epimorphicallyFreeProCGroupOnConvergingSet_injective (hι := hι) hnontrivial
979 have hφinj : Function.Injective φ := by
980 intro x y hxy
981 apply hιinj
982 apply hσinj
983 calc
984 σ (ι x) = φ x := hσ.2 x
985 _ = φ y := hxy
986 _ = σ (ι y) := (hσ.2 y).symm
987 have hφsub : Set.range φ ⊆ (s : Set F) ∪ ({1} : Set F) := by
988 rintro z ⟨x, rfl⟩
989 by_cases hxp : x ∈ p
990 · left
991 simp only [hxp, ↓reduceDIte, Subtype.coe_prop, φ]
992 · right
993 simp only [hxp, ↓reduceDIte, mem_singleton_iff, φ]
994 have hφfin : (Set.range φ).Finite :=
995 (s.finite_toSet.union (Set.finite_singleton (1 : F))).subset hφsub
996 have hXlt : Cardinal.mk X < Cardinal.aleph0 := by
997 calc
998 Cardinal.mk X = Cardinal.mk (Set.range φ) := by
999 simpa using (Cardinal.mk_range_eq φ hφinj).symm
1000 _ < Cardinal.aleph0 := by
1001 exact (Cardinal.mk_lt_aleph0_iff).2 hφfin.to_subtype
1002 exact False.elim (hXfin ((Cardinal.mk_lt_aleph0_iff).1 hXlt))
1004/-- A fixed free pro-`C` group on a set converging to `1` admits a continuous epimorphism onto any
1005profinite pro-`C` target generated by the image of its basis. -/
1006theorem exists_epimorphicallyFreeProCGroupOnConvergingSet_surjecting
1007 {X : Type u}
1008 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1009 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
1010 {ι : X → F}
1011 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1012 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1013 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
1015 (φ : X → G)
1016 (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
1017 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
1018 ∃ ψ : F →* G, Continuous ψ ∧ Function.Surjective ψ ∧ ∀ x, ψ (ι x) = φ x := by
1019 rcases hF.existsUnique_lift hG φ hφ hgen with ⟨ψ, hψ, _⟩
1020 have hsub : Set.range φ ⊆ (ψ.range : Set G) := by
1021 rintro z ⟨x, rfl⟩
1022 exact ⟨ι x, hψ.2 x⟩
1023 have hψsurj : Function.Surjective ψ :=
1024 surjective_hom_of_rangeContainsGeneratingSet
1025 hgen hψ.1 hsub
1026 exact ⟨ψ, hψ.1, hψsurj, hψ.2⟩
1028/-- The pro-`C` completion of the abstract free group on a finite basis is free pro-`C` on that
1029basis. -/
1030theorem proCCompletionOfAbstractFreeGroup_is_free
1031 {X : Type u} [Finite X]
1032 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
1033 [DiscreteTopology (FreeGroup X)]
1034 {Fhat : Type u} [Group Fhat] [TopologicalSpace Fhat] [IsTopologicalGroup Fhat]
1035 [CompactSpace Fhat] [T2Space Fhat] [TotallyDisconnectedSpace Fhat]
1036 {ι : FreeGroup X →ₜ* Fhat}
1037 (hι : ProCGroups.Completion.IsProCCompletion C (FreeGroup X) Fhat ι) :
1038 IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X Fhat
1039 (fun x => ι (FreeGroup.of x)) := by
1040 refine ⟨hι.hasOpenNormalBasisInClass, ?_, ?_, ?_⟩
1041 · exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := Fhat)
1042 (fun x : X => ι (FreeGroup.of x))
1043 · have himage :
1044 ι '' Set.range (FreeGroup.of : X → FreeGroup X) =
1045 Set.range (fun x : X => ι (FreeGroup.of x)) := by
1046 calc
1047 ι '' Set.range (FreeGroup.of : X → FreeGroup X) =
1048 Set.range ((⇑ι) ∘ (FreeGroup.of : X → FreeGroup X)) :=
1049 (Set.range_comp ι (FreeGroup.of : X → FreeGroup X)).symm
1050 _ = Set.range (fun x : X => ι (FreeGroup.of x)) := by rfl
1051 have hclosure :
1052 Subgroup.closure (Set.range fun x : X => ι (FreeGroup.of x)) =
1053 ι.toMonoidHom.range := by
1054 calc
1055 Subgroup.closure (Set.range fun x : X => ι (FreeGroup.of x))
1056 = Subgroup.map ι.toMonoidHom
1057 (Subgroup.closure (Set.range (FreeGroup.of : X → FreeGroup X))) := by
1058 simpa [himage] using
1059 (ι.toMonoidHom.map_closure (Set.range (FreeGroup.of : X → FreeGroup X))).symm
1060 _ = ι.toMonoidHom.range := by
1061 rw [FreeGroup.closure_range_of X, MonoidHom.range_eq_map]
1062 rw [Generation.TopologicallyGenerates, hclosure]
1063 rw [SetLike.ext'_iff, Subgroup.topologicalClosure_coe, Subgroup.coe_top]
1064 simpa [DenseRange, MonoidHom.coe_range, dense_iff_closure_eq] using hι.denseRange
1065 · intro G _ _ _ _ _ _ hG φ _hφ hgen
1066 let φfree : FreeGroup X →ₜ* G :=
1067 { toMonoidHom := FreeGroup.lift φ
1068 continuous_toFun := by
1069 simpa using (continuous_of_discreteTopology : Continuous (FreeGroup.lift φ)) }
1070 let φhat : Fhat →ₜ* G := hι.lift hG φfree
1071 refine ⟨φhat.toMonoidHom, ?_, ?_⟩
1072 · refine ⟨φhat.continuous_toFun, ?_⟩
1073 intro x
1074 have hfac := congrArg (fun ψ : FreeGroup X →ₜ* G => ψ (FreeGroup.of x))
1075 (hι.lift_spec hG φfree)
1076 have hfree : φfree (FreeGroup.of x) = φ x := by
1077 change FreeGroup.lift φ (FreeGroup.of x) = φ x
1078 simp only [FreeGroup.lift_apply_of]
1079 exact hfac.trans hfree
1080 · intro g hg
1081 let gCont : Fhat →ₜ* G := { toMonoidHom := g, continuous_toFun := hg.1 }
1082 have hfac' : gCont.comp ι = φfree := by
1083 apply ContinuousMonoidHom.toMonoidHom_injective
1084 ext x
1085 change g (ι (FreeGroup.of x)) = FreeGroup.lift φ (FreeGroup.of x)
1086 exact (hg.2 x).trans (by simp only [FreeGroup.lift_apply_of])
1087 exact congrArg ContinuousMonoidHom.toMonoidHom (hι.lift_unique hG φfree hfac')
1089namespace IsEpimorphicallyFreeProCGroupOnConvergingSet
1091variable {X : Type v}
1092variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1093variable {F' : Type u} [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
1094variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
1095variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
1096variable {ι : X → F}
1098/-- The lift supplied by the corresponding free pro-`C` universal property. -/
1099noncomputable def lift
1100 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1101 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1102 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
1104 (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
1105 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
1106 F →* G :=
1107 Classical.choose (ExistsUnique.exists (hι.existsUnique_lift hG φ hφ hgen))
1109/-- The universal-property lift has the prescribed values on the chosen generators. -/
1110theorem lift_spec
1111 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1112 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1113 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
1115 (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
1116 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
1117 Continuous (hι.lift hG φ hφ hgen) ∧
1118 ∀ x, hι.lift hG φ hφ hgen (ι x) = φ x :=
1119 Classical.choose_spec (ExistsUnique.exists (hι.existsUnique_lift hG φ hφ hgen))
1121/-- The universal-property lift is unique among continuous maps with the prescribed values. -/
1122theorem lift_unique
1123 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1124 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1125 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
1127 (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
1128 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ))
1129 {f : F →* G} (hf : Continuous f) (hfac : ∀ x, f (ι x) = φ x) :
1130 f = hι.lift hG φ hφ hgen := by
1131 exact
1132 (hι.existsUnique_lift hG φ hφ hgen).unique ⟨hf, hfac⟩
1133 (hι.lift_spec hG φ hφ hgen)
1135/-- For a concrete finite-group class, the generated-target universal property of a free
1136pro-`C` group on a converging set extends any target map that converges to `1`. This formulation
1137supports retractions that collapse all but finitely many basis elements. -/
1138theorem existsUnique_lift_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass
1139 (C : ProCGroups.FiniteGroupClass.{u})
1142 (hι :
1143 IsEpimorphicallyFreeProCGroupOnConvergingSet
1144 (C := C) X F ι)
1145 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1146 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
1148 (φ : X → G) (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ) :
1149 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x := by
1150 classical
1151 let K : ClosedSubgroup G := Generation.closedSubgroupGenerated (G := G) (Set.range φ)
1152 letI : CompactSpace ↥(K : Subgroup G) := by
1153 exact
1154 (show IsClosed (((K : Subgroup G) : Set G)) from
1155 K.2).isClosedEmbedding_subtypeVal.compactSpace
1156 let φK : X → ↥(K : Subgroup G) := Generation.closedSubgroupGeneratedMap (G := G) φ
1157 have hφKconv : FamilyConvergesToOneAlongOpenSubgroups (G := ↥(K : Subgroup G)) φK := by
1158 intro U
1159 have hU_nhds : ((U : Subgroup ↥(K : Subgroup G)) : Set ↥(K : Subgroup G)) ∈
1160 𝓝 (1 : ↥(K : Subgroup G)) :=
1161 U.isOpen'.mem_nhds U.one_mem'
1162 rcases
1163 (mem_nhds_subtype ((K : Subgroup G) : Set G) (1 : ↥(K : Subgroup G))
1164 ((U : Subgroup ↥(K : Subgroup G)) : Set ↥(K : Subgroup G))).1 hU_nhds with
1165 ⟨W₀, hW₀_nhds, hW₀U⟩
1166 rcases mem_nhds_iff.mp hW₀_nhds with ⟨W, hWU₀, hWopen, h1W⟩
1167 rcases hG W hWopen h1W with ⟨V, hVW, _hCV⟩
1168 have hsub :
1169 {x : X | φK x ∉ (U : Set ↥(K : Subgroup G))} ⊆
1170 {x : X | φ x ∉ ((V.toOpenSubgroup : OpenSubgroup G) : Set G)} := by
1171 intro x hx hxV
1172 exact hx (hW₀U (by
1173 change φ x ∈ W₀
1174 exact hWU₀ (hVW hxV)))
1175 exact (hφ V.toOpenSubgroup).subset hsub
1176 have hφKgen :
1177 Generation.TopologicallyGenerates (G := ↥(K : Subgroup G)) (Set.range φK) := by
1178 simpa [φK] using
1179 (Generation.closedSubgroupGeneratedMap_topologicallyGenerates (G := G) φ)
1180 have hK : ProCGroups.ProC.HasOpenNormalBasisInClass C ↥(K : Subgroup G) :=
1182 rcases hι.existsUnique_lift hK φK hφKconv hφKgen with ⟨fK, hfK, huniqK⟩
1183 let incl : ↥(K : Subgroup G) →* G := (K : Subgroup G).subtype
1184 let f : F →* G := incl.comp fK
1185 refine ⟨f, ⟨?_, ?_⟩, ?_⟩
1186 · exact continuous_subtype_val.comp hfK.1
1187 · intro x
1188 exact congrArg Subtype.val (hfK.2 x)
1189 · intro g hg
1190 have hgK_mem : ∀ y : F, g y ∈ (K : Subgroup G) := by
1191 intro y
1192 have hy :
1193 y ∈ (Generation.closedSubgroupGenerated (G := F) (Set.range ι) : Subgroup F) := by
1194 change y ∈ ((Subgroup.closure (Set.range ι)).topologicalClosure : Subgroup F)
1195 rw [hι.generates_range]
1196 simp only [Subgroup.mem_top]
1197 have hgy :=
1198 Generation.map_mem_closedSubgroupGenerated_image
1199 (G := F) (H := G)
1200 ({ toMonoidHom := g, continuous_toFun := hg.1 } : F →ₜ* G)
1201 (X := Set.range ι) hy
1202 have himage :
1203 (({ toMonoidHom := g, continuous_toFun := hg.1 } : F →ₜ* G) ''
1204 Set.range ι) = Set.range φ := by
1205 ext z
1206 constructor
1207 · rintro ⟨y, ⟨x, rfl⟩, rfl⟩
1208 exact ⟨x, (hg.2 x).symm⟩
1209 · rintro ⟨x, rfl⟩
1210 exact ⟨ι x, ⟨x, rfl⟩, hg.2 x⟩
1211 change
1212 g y ∈ Generation.closedSubgroupGenerated
1213 (({ toMonoidHom := g, continuous_toFun := hg.1 } : F →ₜ* G) ''
1214 Set.range ι) at hgy
1215 rw [himage] at hgy
1216 exact hgy
1217 let gK : F →* ↥(K : Subgroup G) :=
1218 { toFun := fun y => ⟨g y, hgK_mem y⟩
1219 map_one' := by
1220 apply Subtype.ext
1221 simp only [map_one, OneMemClass.coe_one]
1222 map_mul' := by
1223 intro a b
1224 apply Subtype.ext
1225 simp only [map_mul, MulMemClass.mk_mul_mk]}
1226 have hgKcont : Continuous gK := by
1227 exact Continuous.subtype_mk hg.1 (fun y => (gK y).2)
1228 have hgKfac : ∀ x, gK (ι x) = φK x := by
1229 intro x
1230 apply Subtype.ext
1231 exact hg.2 x
1232 have hgK_eq : gK = fK := huniqK gK ⟨hgKcont, hgKfac⟩
1233 ext y
1234 exact congrArg Subtype.val (congrArg (fun f : F →* ↥(K : Subgroup G) => f y) hgK_eq)
1236/-- Continuous-homomorphism form of
1237`existsUnique_lift_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass`. -/
1238theorem existsUnique_liftHom_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass
1239 (C : ProCGroups.FiniteGroupClass.{u})
1242 (hι :
1243 IsEpimorphicallyFreeProCGroupOnConvergingSet
1244 (C := C) X F ι)
1245 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1246 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
1248 (φ : X → G) (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ) :
1249 ∃! f : F →ₜ* G, ∀ x, f (ι x) = φ x := by
1250 rcases existsUnique_lift_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass
1251 C hIso hSub hι hG φ hφ with
1252 ⟨f, hf, huniq⟩
1253 let fc : F →ₜ* G :=
1254 { toMonoidHom := f
1255 continuous_toFun := hf.1 }
1256 refine ⟨fc, hf.2, ?_⟩
1257 intro g hg
1258 apply ContinuousMonoidHom.toMonoidHom_injective
1259 exact huniq g.toMonoidHom ⟨g.continuous, hg⟩
1261/-- In a free pro-`Σ` group with nonempty `Σ`, a free generator has no positive torsion. -/
1262theorem generator_pow_ne_one_of_sigma
1263 {σ : Set ℕ} (hσ : ∃ p, p ∈ σ ∧ Nat.Prime p)
1264 (hι :
1265 IsEpimorphicallyFreeProCGroupOnConvergingSet
1267 (i : X) (N : ℕ) (hN : 0 < N) :
1268 (ι i) ^ N ≠ 1 := by
1269 classical
1270 rcases hσ with ⟨p, hpσ, hp⟩
1271 let M := p ^ (N + 1)
1272 have hMpos : 0 < M := pow_pos hp.pos (N + 1)
1275 (sigma := σ) (p := p) (k := N + 1) hpσ hp
1276 let T := ULift.{u} (Multiplicative (ZMod M))
1277 letI : NeZero M := ⟨Nat.ne_of_gt hMpos⟩
1278 letI : Finite T := by
1279 let e : T ≃ Multiplicative (ZMod M) := Equiv.ulift
1280 exact Finite.of_equiv (Multiplicative (ZMod M)) e.symm
1281 letI : TopologicalSpace T := ⊥
1282 letI : DiscreteTopology T := ⟨rfl⟩
1283 letI : IsTopologicalGroup T := by infer_instance
1284 let φ : X → T :=
1285 fun j => if j = i then ULift.up (Multiplicative.ofAdd (1 : ZMod M)) else 1
1286 have hφconv : FamilyConvergesToOneAlongOpenSubgroups (G := T) φ := by
1287 intro U
1288 refine (Set.finite_singleton i).subset ?_
1289 intro j hj
1290 by_cases hji : j = i
1291 · simp only [hji, Set.mem_singleton_iff]
1292 · have hφj : φ j = 1 := by simp only [hji, ↓reduceIte, φ]
1293 have hmem : φ j ∈ (U : Set T) := by simp only [hφj, SetLike.mem_coe, one_mem]
1294 exact False.elim (hj hmem)
1297 have hT :
1302 (G := T)
1304 hTclass
1305 rcases hι.existsUnique_liftHom_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass
1309 hT φ hφconv with
1310 ⟨f, hf, _⟩
1311 intro hpow
1312 have hf_pow : f ((ι i) ^ N) = 1 := by simp only [hpow, map_one]
1313 have hcalc : f ((ι i) ^ N) = ULift.up (Multiplicative.ofAdd (N : ZMod M)) := by
1314 calc
1315 f ((ι i) ^ N) = (f (ι i)) ^ N := by simp only [map_pow]
1316 _ = (φ i) ^ N := by rw [hf i]
1317 _ = (ULift.up (Multiplicative.ofAdd (1 : ZMod M))) ^ N := by simp only [↓reduceIte, φ]
1318 _ = ULift.up (Multiplicative.ofAdd (N : ZMod M)) := by
1319 apply ULift.ext
1320 change (Multiplicative.ofAdd (1 : ZMod M)) ^ N =
1321 Multiplicative.ofAdd (N : ZMod M)
1322 change Multiplicative.ofAdd ((N : ℕ) • (1 : ZMod M)) =
1323 Multiplicative.ofAdd (N : ZMod M)
1324 simp only [nsmul_eq_mul, mul_one]
1325 have hlt_pow : N < p ^ (N + 1) :=
1326 lt_of_lt_of_le
1327 (Nat.lt_pow_self (n := N) (a := p) hp.one_lt)
1328 (Nat.pow_le_pow_right hp.pos (Nat.le_succ N))
1329 have hNmod : (N : ZMod M) ≠ 0 := by
1330 intro hzero
1331 have hdiv : M ∣ N := (ZMod.natCast_eq_zero_iff N M).mp hzero
1332 exact (Nat.not_dvd_of_pos_of_lt hN hlt_pow) hdiv
1333 have hofAdd_ne : ULift.up (Multiplicative.ofAdd (N : ZMod M)) ≠ (1 : T) := by
1334 intro h
1335 have hdown : Multiplicative.ofAdd (N : ZMod M) = 1 := congrArg ULift.down h
1336 have hz : (N : ZMod M) = 0 := by
1337 change Multiplicative.ofAdd (N : ZMod M) =
1338 Multiplicative.ofAdd (0 : ZMod M) at hdown
1339 exact Multiplicative.ofAdd.injective hdown
1340 exact hNmod hz
1341 exact hofAdd_ne (hcalc.symm.trans hf_pow)
1343/-- Integer-power form of `generator_pow_ne_one_of_sigma`. -/
1344theorem generator_zpow_ne_one_of_sigma
1345 {σ : Set ℕ} (hσ : ∃ p, p ∈ σ ∧ Nat.Prime p)
1346 (hι :
1347 IsEpimorphicallyFreeProCGroupOnConvergingSet
1349 (i : X) (n : ℤ) (hn : n ≠ 0) :
1350 (ι i) ^ n ≠ 1 := by
1351 intro hzn
1352 have hnat_pos : 0 < n.natAbs := Int.natAbs_pos.mpr hn
1353 have hnat_ne :
1354 (ι i) ^ n.natAbs ≠ 1 :=
1355 hι.generator_pow_ne_one_of_sigma hσ i n.natAbs hnat_pos
1356 apply hnat_ne
1357 by_cases hnonneg : 0 ≤ n
1358 · have hnat : (n.natAbs : ℤ) = n := Int.natAbs_of_nonneg hnonneg
1359 simpa [zpow_natCast, hnat] using hzn
1360 · have hneg : n < 0 := lt_of_not_ge hnonneg
1361 have hnat : (n.natAbs : ℤ) = -n := Int.ofNat_natAbs_of_nonpos hneg.le
1362 have hzn' : (ι i) ^ (-n) = 1 := by
1363 calc
1364 (ι i) ^ (-n) = ((ι i) ^ n)⁻¹ := by rw [zpow_neg]
1365 _ = 1 := by simp only [hzn, inv_one]
1366 simpa [zpow_natCast, hnat] using hzn'
1368/-- The continuous homomorphism supplied by the free pro-`C` universal property. -/
1369noncomputable def liftHom
1370 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1371 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1372 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
1374 (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
1375 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) :
1376 F →ₜ* G where
1377 toMonoidHom := hι.lift hG φ hφ hgen
1378 continuous_toFun := (hι.lift_spec hG φ hφ hgen).1
1380/-- Bundled version of `liftHom`, taking a converging generating map as a single argument. -/
1381noncomputable def liftConvergingGeneratingMap
1382 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1383 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1384 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
1385 (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : ConvergingGeneratingMap X G) :
1386 F →ₜ* G :=
1387 hι.liftHom hG φ φ.convergesToOneAlongOpenSubgroups φ.generates
1389/-- The bundled lift has the prescribed value on each generator. -/
1390@[simp] theorem liftConvergingGeneratingMap_apply
1391 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1392 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1393 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
1394 (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C (G)) (φ : ConvergingGeneratingMap X G) (x
1395 : X) :
1396 hι.liftConvergingGeneratingMap hG φ (ι x) = φ x := by
1397 change hι.lift hG φ φ.convergesToOneAlongOpenSubgroups φ.generates (ι x) = φ x
1398 exact (hι.lift_spec hG φ φ.convergesToOneAlongOpenSubgroups φ.generates).2 x
1400/-- `liftHom` has the prescribed value on each generator. -/
1401@[simp] theorem liftHom_apply
1402 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1403 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
1404 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
1406 (hφ : FamilyConvergesToOneAlongOpenSubgroups (G := G) φ)
1407 (hgen : Generation.TopologicallyGenerates (G := G) (Set.range φ)) (x : X) :
1408 hι.liftHom hG φ hφ hgen (ι x) = φ x :=
1409 (hι.lift_spec hG φ hφ hgen).2 x
1411section FiniteSupportRetracts
1413variable {C : ProCGroups.FiniteGroupClass.{u}}
1414variable [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
1415variable {X : Type v} [DecidableEq X]
1416variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1417variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
1418variable {ι : X → F}
1420/-- The unique continuous endomorphism of a free pro-`C` group that keeps the finite set `S`
1421of basis elements and sends the remaining basis elements to `1`. -/
1422theorem existsUnique_collapseToFinset_of_finiteGroupClass
1423 (hι :
1424 IsEpimorphicallyFreeProCGroupOnConvergingSet
1425 (C := C) X F ι)
1426 (S : Finset X) :
1427 ∃! φ : F →ₜ* F, ∀ x, φ (ι x) = if x ∈ S then ι x else 1 := by
1428 have hconv :
1429 FamilyConvergesToOneAlongOpenSubgroups (G := F) (fun x => if x ∈ S then ι x else 1) := by
1430 intro U
1431 classical
1432 refine S.finite_toSet.subset ?_
1433 intro x hx
1434 by_cases hxS : x ∈ S
1435 · exact hxS
1436 · exfalso
1437 exact hx (by simp only [hxS, ↓reduceIte, SetLike.mem_coe, one_mem])
1438 exact
1439 hι.existsUnique_liftHom_of_convergesToOneAlongOpenSubgroups_of_finiteGroupClass
1440 C C.isomClosed hVar.out.subgroupClosed
1441 hι.hasOpenNormalBasisInClass (fun x => if x ∈ S then ι x else 1) hconv
1443/-- The finite-support retraction of a free pro-`C` group onto the closed subgroup generated by a
1444finite set of basis elements. -/
1445noncomputable def collapseToFinset
1446 (hι :
1447 IsEpimorphicallyFreeProCGroupOnConvergingSet
1448 (C := C) X F ι)
1449 (S : Finset X) :
1450 F →ₜ* F :=
1451 Classical.choose (ExistsUnique.exists (hι.existsUnique_collapseToFinset_of_finiteGroupClass S))
1453/-- Collapsing to a finite set fixes the selected generators. -/
1454@[simp] theorem collapseToFinset_apply_mem
1455 (hι :
1456 IsEpimorphicallyFreeProCGroupOnConvergingSet
1457 (C := C) X F ι)
1458 {S : Finset X} {x : X} (hx : x ∈ S) :
1459 hι.collapseToFinset S (ι x) = ι x := by
1460 simpa [hx, collapseToFinset] using
1461 (Classical.choose_spec
1462 (ExistsUnique.exists (hι.existsUnique_collapseToFinset_of_finiteGroupClass S)) x)
1464/-- Collapsing to a finite set sends every unselected generator to the identity. -/
1465@[simp] theorem collapseToFinset_apply_not_mem
1466 (hι :
1467 IsEpimorphicallyFreeProCGroupOnConvergingSet
1468 (C := C) X F ι)
1469 {S : Finset X} {x : X} (hx : x ∉ S) :
1470 hι.collapseToFinset S (ι x) = 1 := by
1471 simpa [hx, collapseToFinset] using
1472 (Classical.choose_spec
1473 (ExistsUnique.exists (hι.existsUnique_collapseToFinset_of_finiteGroupClass S)) x)
1475/-- Collapsing twice to the same finite set is the same as collapsing once. -/
1476@[simp] theorem collapseToFinset_idempotent
1477 (hι :
1478 IsEpimorphicallyFreeProCGroupOnConvergingSet
1479 (C := C) X F ι)
1480 (S : Finset X) :
1481 (hι.collapseToFinset S).comp (hι.collapseToFinset S) =
1482 hι.collapseToFinset S := by
1483 apply Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
1484 rintro _ ⟨x, rfl⟩
1485 by_cases hx : x ∈ S
1486 · simp only [ContinuousMonoidHom.comp_toFun, hx, collapseToFinset_apply_mem]
1487 · simp only [ContinuousMonoidHom.comp_toFun, hx, not_false_eq_true,
1488 collapseToFinset_apply_not_mem, map_one]
1490/-- A homomorphism that kills every basis element outside `S` is unchanged after precomposition
1491with the finite-support retraction. -/
1492theorem comp_collapseToFinset_eq_of_eq_one_outside
1493 (hι :
1494 IsEpimorphicallyFreeProCGroupOnConvergingSet
1495 (C := C) X F ι)
1496 {G : Type w} [Group G] [TopologicalSpace G] [T2Space G]
1497 (φ : F →ₜ* G) (S : Finset X)
1498 (hφ : ∀ x, x ∉ S → φ (ι x) = 1) :
1499 φ.comp (hι.collapseToFinset S) = φ := by
1500 apply Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
1501 rintro _ ⟨x, rfl⟩
1502 by_cases hx : x ∈ S
1503 · simp only [ContinuousMonoidHom.comp_toFun, hx, collapseToFinset_apply_mem]
1504 · simp only [ContinuousMonoidHom.comp_toFun, hx, not_false_eq_true,
1505 collapseToFinset_apply_not_mem, map_one,
1506 hφ x hx]
1508/-- The map from the free pro-`C` group onto the range of its finite-support retraction. -/
1509noncomputable def collapseToFinsetRange
1510 (hι :
1511 IsEpimorphicallyFreeProCGroupOnConvergingSet
1512 (C := C) X F ι)
1513 (S : Finset X) :
1514 F →ₜ* ↥((hι.collapseToFinset S : F →* F).range) :=
1515 { toMonoidHom := (hι.collapseToFinset S : F →* F).rangeRestrict
1516 continuous_toFun :=
1517 (hι.collapseToFinset S).continuous.subtype_mk (fun x => ⟨x, rfl⟩) }
1519/-- The inclusion of the range of a finite-support retraction back into the ambient free group. -/
1520noncomputable def collapseToFinsetInclusion
1521 (hι :
1522 IsEpimorphicallyFreeProCGroupOnConvergingSet
1523 (C := C) X F ι)
1524 (S : Finset X) :
1525 ↥((hι.collapseToFinset S : F →* F).range) →ₜ* F :=
1526 { toMonoidHom := ((hι.collapseToFinset S : F →* F).range).subtype
1527 continuous_toFun := continuous_subtype_val }
1529/-- The range of the finite-support retraction, viewed as the finite-basis retract. -/
1530abbrev FinsetSupportRetract
1531 (hι :
1532 IsEpimorphicallyFreeProCGroupOnConvergingSet
1533 (C := C) X F ι)
1534 (S : Finset X) : Type u :=
1535 ↥((hι.collapseToFinset S : F →* F).range)
1537/-- The finite basis of the finite-support retract. -/
1538noncomputable def finsetSupportBasis
1539 (hι :
1540 IsEpimorphicallyFreeProCGroupOnConvergingSet
1541 (C := C) X F ι)
1542 (S : Finset X) :
1543 S → hι.FinsetSupportRetract S := by
1544 intro x
1545 refine ⟨ι x.1, ?_⟩
1546 exact ⟨ι x.1, hι.collapseToFinset_apply_mem x.2⟩
1548/-- The range of the finite-support retraction is closed. -/
1549theorem isClosed_range_collapseToFinset
1550 (hι :
1551 IsEpimorphicallyFreeProCGroupOnConvergingSet
1552 (C := C) X F ι)
1553 (S : Finset X) :
1554 IsClosed (((hι.collapseToFinset S : F →* F).range : Set F)) := by
1555 let r : F →ₜ* F := hι.collapseToFinset S
1556 let Fix : Subgroup F := (r : F →* F).eqLocus (MonoidHom.id F)
1557 have hFixClosed : IsClosed (Fix : Set F) := by
1558 change IsClosed {x : F | r x = x}
1559 exact isClosed_eq r.continuous continuous_id
1560 have hFixEq : Fix = (r : F →* F).range := by
1561 ext x
1562 constructor
1563 · intro hx
1564 refine ⟨x, ?_⟩
1565 change (r : F →* F) x = x at hx
1566 exact hx
1567 · rintro ⟨y, rfl⟩
1568 change r (r y) = r y
1569 exact congrArg (fun ψ : F →ₜ* F => ψ y) (hι.collapseToFinset_idempotent S)
1570 simpa [r, Fix, hFixEq] using hFixClosed
1572/-- The closed finite-support retract carries its canonical compact topology. -/
1573noncomputable instance instCompactSpaceFinsetSupportRetract
1574 (hι :
1575 IsEpimorphicallyFreeProCGroupOnConvergingSet
1576 (C := C) X F ι)
1577 (S : Finset X) :
1578 CompactSpace (hι.FinsetSupportRetract S) :=
1579 (hι.isClosed_range_collapseToFinset S).isClosedEmbedding_subtypeVal.compactSpace
1581/-- The finite-support retract again has an open-normal \(C\)-basis. -/
1582theorem hasOpenNormalBasisInClass_finsetSupportRetract
1583 (hι :
1584 IsEpimorphicallyFreeProCGroupOnConvergingSet
1585 (C := C) X F ι)
1586 (S : Finset X) :
1587 ProCGroups.ProC.HasOpenNormalBasisInClass C (hι.FinsetSupportRetract S) := by
1588 exact
1590 C.isomClosed hVar.out.subgroupClosed
1591 hι.hasOpenNormalBasisInClass ((hι.collapseToFinset S : F →* F).range)
1592 (hι.isClosed_range_collapseToFinset S)
1594/-- The finite-support retract is free pro-`C` on its retained finite basis. -/
1595theorem isFreeProCGroupOnConvergingSet_finsetSupportBasis
1596 (hι :
1597 IsEpimorphicallyFreeProCGroupOnConvergingSet
1598 (C := C) X F ι)
1599 (S : Finset X) :
1600 IsEpimorphicallyFreeProCGroupOnConvergingSet
1601 (C := C)
1602 S (hι.FinsetSupportRetract S) (hι.finsetSupportBasis S) := by
1603 let R : Type u := hι.FinsetSupportRetract S
1604 let B : S → R := hι.finsetSupportBasis S
1605 let rRange : F →ₜ* R := hι.collapseToFinsetRange S
1606 let rIncl : R →ₜ* F := hι.collapseToFinsetInclusion S
1607 refine ⟨hι.hasOpenNormalBasisInClass_finsetSupportRetract S, ?_, ?_, ?_⟩
1608 · simpa [B] using FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := R) B
1609 · have hgen :
1610 Generation.TopologicallyGenerates (G := R) (Set.range B) := by
1611 let Img : Set R := rRange '' Set.range ι
1612 have hsurj : Function.Surjective rRange := by
1613 exact MonoidHom.rangeRestrict_surjective (hι.collapseToFinset S : F →* F)
1614 have hImgGen : Generation.TopologicallyGenerates (G := R) Img := by
1615 exact
1616 Generation.topologicallyGenerates_image_of_continuousSurjective
1617 (f := rRange.toMonoidHom) rRange.continuous hsurj hι.generates_range
1618 have hBsub : Set.range B ⊆ Img := by
1619 intro y hy
1620 rcases hy with ⟨x, rfl⟩
1621 refine ⟨ι x.1, ⟨x.1, rfl⟩, ?_⟩
1622 apply Subtype.ext
1623 change (hι.collapseToFinset S (ι x.1) : F) = ι x.1
1624 exact hι.collapseToFinset_apply_mem x.2
1625 have hImgSub : Img ⊆ ((Subgroup.closure (Set.range B) : Subgroup R) : Set R) := by
1626 intro y hy
1627 rcases hy with ⟨x, ⟨j, rfl⟩, rfl⟩
1628 by_cases hj : j ∈ S
1629 · exact
1630 Subgroup.subset_closure ⟨⟨j, hj⟩, by
1631 apply Subtype.ext
1632 change ι j = (hι.collapseToFinset S (ι j) : F)
1633 exact (hι.collapseToFinset_apply_mem hj).symm⟩
1634 · have hy1 : rRange (ι j) = 1 := by
1635 apply Subtype.ext
1636 change (hι.collapseToFinset S (ι j) : F) = 1
1637 exact hι.collapseToFinset_apply_not_mem hj
1638 rw [hy1]
1639 exact (Subgroup.closure (Set.range B)).one_mem
1640 have hclosureEq :
1641 Subgroup.closure Img = Subgroup.closure (Set.range B) := by
1642 apply le_antisymm
1643 · exact (Subgroup.closure_le (K := Subgroup.closure (Set.range B))).2 hImgSub
1644 · exact Subgroup.closure_mono hBsub
1645 change (Subgroup.closure (Set.range B)).topologicalClosure = ⊤
1646 change (Subgroup.closure Img).topologicalClosure = ⊤ at hImgGen
1647 rw [← hclosureEq]
1648 exact hImgGen
1649 simpa [B] using hgen
1650 · intro G _ _ _ _ _ _ hG φ hφ hgen
1651 let φext : X → G := fun x => if hx : x ∈ S then φ ⟨x, hx⟩ else 1
1652 have hφext : FamilyConvergesToOneAlongOpenSubgroups (G := G) φext := by
1653 intro U
1654 refine S.finite_toSet.subset ?_
1655 intro x hx
1656 by_cases hxS : x ∈ S
1657 · exact hxS
1658 · exfalso
1659 exact hx (by simp only [hxS, ↓reduceDIte, SetLike.mem_coe, one_mem, φext])
1660 have hφextgen : Generation.TopologicallyGenerates (G := G) (Set.range φext) := by
1661 have hsub : Set.range φ ⊆ Set.range φext := by
1662 intro y hy
1663 rcases hy with ⟨x, rfl⟩
1664 exact ⟨x.1, by simp only [x.2, ↓reduceDIte, Subtype.coe_eta, φext]⟩
1665 exact Generation.topologicallyGenerates_mono (G := G) hgen hsub
1666 let Φ : F →ₜ* G := hι.liftHom hG φext hφext hφextgen
1667 have hΦspec : ∀ x, Φ (ι x) = φext x := by
1668 intro x
1669 exact hι.liftHom_apply hG φext hφext hφextgen x
1670 let Φbar : R →ₜ* G :=
1671 { toMonoidHom := Φ.toMonoidHom.comp rIncl.toMonoidHom
1672 continuous_toFun := Φ.continuous.comp rIncl.continuous }
1673 have hΦbar : ∀ x : S, Φbar (B x) = φ x := by
1674 intro x
1675 change Φ (ι x.1) = φ x
1676 simpa [φext, B, Φbar, rIncl, collapseToFinsetInclusion, finsetSupportBasis] using
1677 hΦspec x.1
1678 refine ⟨Φbar.toMonoidHom, ⟨Φbar.continuous, hΦbar⟩, ?_⟩
1679 intro ψ hψ
1680 let ψc : R →ₜ* G :=
1681 { toMonoidHom := ψ
1682 continuous_toFun := hψ.1 }
1683 have hψcomp : ψc.comp rRange = Φ := by
1684 apply Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
1685 rintro _ ⟨x, rfl⟩
1686 by_cases hx : x ∈ S
1687 · have hψx : ψc (rRange (ι x)) = φ ⟨x, hx⟩ := by
1688 have hBasis : rRange (ι x) = B ⟨x, hx⟩ := by
1689 apply Subtype.ext
1690 change (hι.collapseToFinset S (ι x) : F) = ι x
1691 exact hι.collapseToFinset_apply_mem hx
1692 exact hBasis ▸ hψ.2 ⟨x, hx⟩
1693 have hΦx : Φ (ι x) = φ ⟨x, hx⟩ := by
1694 simpa [φext, hx] using hΦspec x
1695 exact hψx.trans hΦx.symm
1696 · have hrx : rRange (ι x) = 1 := by
1697 apply Subtype.ext
1698 change (hι.collapseToFinset S (ι x) : F) = 1
1699 exact hι.collapseToFinset_apply_not_mem hx
1700 have hΦx : Φ (ι x) = 1 := by
1701 simpa [φext, hx] using hΦspec x
1702 calc
1703 ψc (rRange (ι x)) = ψc 1 := by rw [hrx]
1704 _ = 1 := by simp only [map_one]
1705 _ = Φ (ι x) := hΦx.symm
1706 have hΦbarcomp : Φbar.comp rRange = Φ := by
1707 ext y
1708 change Φ (hι.collapseToFinset S y) = Φ y
1709 have hfix :
1710 Φ.comp (hι.collapseToFinset S) = Φ := by
1711 exact hι.comp_collapseToFinset_eq_of_eq_one_outside Φ S (by
1712 intro x hx
1713 simpa [φext, hx] using hΦspec x)
1714 exact congrArg (fun f : F →ₜ* G => f y) hfix
1715 have hsurj : Function.Surjective rRange := by
1716 exact MonoidHom.rangeRestrict_surjective (hι.collapseToFinset S : F →* F)
1717 ext z
1718 rcases hsurj z with ⟨y, rfl⟩
1719 have hEq : ψc.comp rRange = Φbar.comp rRange := hψcomp.trans hΦbarcomp.symm
1720 exact congrArg (fun f : F →ₜ* G => f y) hEq
1722/-- If `S ⊆ T`, then collapsing first to `T` and then to `S` is the same as
1723collapsing directly to `S`. This is the basic compatibility relation for the finite-basis
1724projections. -/
1725theorem collapseToFinset_small_comp_large_of_subset
1726 (hι :
1727 IsEpimorphicallyFreeProCGroupOnConvergingSet
1728 (C := C) X F ι)
1729 {S T : Finset X} (hST : S ⊆ T) :
1730 (hι.collapseToFinset S).comp (hι.collapseToFinset T) =
1731 hι.collapseToFinset S := by
1732 apply Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
1733 rintro _ ⟨x, rfl⟩
1734 by_cases hxS : x ∈ S
1735 · have hxT : x ∈ T := hST hxS
1736 simp only [ContinuousMonoidHom.comp_toFun, hxT, collapseToFinset_apply_mem, hxS]
1737 · by_cases hxT : x ∈ T
1738 · simp only [ContinuousMonoidHom.comp_toFun, hxT, collapseToFinset_apply_mem, hxS,
1739 not_false_eq_true,
1740collapseToFinset_apply_not_mem]
1741 · simp only [ContinuousMonoidHom.comp_toFun, hxT, not_false_eq_true,
1742 collapseToFinset_apply_not_mem, map_one,
1743hxS]
1745/-- If `S ⊆ T`, then collapsing to `S` and then to `T` is again the collapse to `S`.
1746Equivalently, the finite-support image for `S` is fixed by every larger finite-support
1747projection. -/
1748theorem collapseToFinset_large_comp_small_of_subset
1749 (hι :
1750 IsEpimorphicallyFreeProCGroupOnConvergingSet
1751 (C := C) X F ι)
1752 {S T : Finset X} (hST : S ⊆ T) :
1753 (hι.collapseToFinset T).comp (hι.collapseToFinset S) =
1754 hι.collapseToFinset S := by
1755 apply Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
1756 rintro _ ⟨x, rfl⟩
1757 by_cases hxS : x ∈ S
1758 · have hxT : x ∈ T := hST hxS
1759 simp only [ContinuousMonoidHom.comp_toFun, hxS, collapseToFinset_apply_mem, hxT]
1760 · simp only [ContinuousMonoidHom.comp_toFun, hxS, not_false_eq_true,
1761 collapseToFinset_apply_not_mem, map_one]
1763/-- The transition map from the finite-support retract for `T` to the one for `S`, for
1764`S ⊆ T`. It is the projection obtained by including the `T`-retract into the ambient free
1765pro-`C` group and then collapsing to `S`. -/
1766noncomputable def finsetSupportTransition
1767 (hι :
1768 IsEpimorphicallyFreeProCGroupOnConvergingSet
1769 (C := C) X F ι)
1770 {S T : Finset X} :
1771 hι.FinsetSupportRetract T →ₜ* hι.FinsetSupportRetract S :=
1772 { toMonoidHom := (hι.collapseToFinsetRange S).toMonoidHom.comp
1773 (hι.collapseToFinsetInclusion T).toMonoidHom
1774 continuous_toFun :=
1775 (hι.collapseToFinsetRange S).continuous.comp
1776 (hι.collapseToFinsetInclusion T).continuous }
1778/-- The transition from a larger finite support to a smaller one preserves the basis elements
1779indexed by the smaller support. -/
1780@[simp] theorem finsetSupportTransition_apply_basis
1781 (hι :
1782 IsEpimorphicallyFreeProCGroupOnConvergingSet
1783 (C := C) X F ι)
1784 {S T : Finset X} (hST : S ⊆ T) (x : S) :
1785 hι.finsetSupportTransition (S := S) (T := T)
1786 (hι.finsetSupportBasis T ⟨x.1, hST x.2⟩) =
1787 hι.finsetSupportBasis S x := by
1788 apply Subtype.ext
1789 change hι.collapseToFinset S (ι x.1) = ι x.1
1790 exact hι.collapseToFinset_apply_mem x.2
1792/-- Compatibility of the ambient projection `F → R_T` with the transition
1793`R_T → R_S`. -/
1794theorem finsetSupportTransition_comp_collapseToFinsetRange
1795 (hι :
1796 IsEpimorphicallyFreeProCGroupOnConvergingSet
1797 (C := C) X F ι)
1798 {S T : Finset X} (hST : S ⊆ T) :
1799 (hι.finsetSupportTransition (S := S) (T := T)).comp (hι.collapseToFinsetRange T) =
1800 hι.collapseToFinsetRange S := by
1801 ext x
1802 change hι.collapseToFinset S (hι.collapseToFinset T x) =
1803 hι.collapseToFinset S x
1804 exact congrArg (fun f : F →ₜ* F => f x)
1805 (hι.collapseToFinset_small_comp_large_of_subset hST)
1807end FiniteSupportRetracts
1809/-- Continuous homomorphisms out of a free pro-`C` group on a converging generating set are
1810determined by their values on the chosen generators. -/
1811theorem hom_ext
1812 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1813 {G : Type u} [Group G] [TopologicalSpace G] [T2Space G]
1814 {f g : F →ₜ* G} (hfg : ∀ x, f (ι x) = g (ι x)) :
1815 f = g := by
1816 exact Generation.continuousMonoidHom_ext_of_topologicallyGenerates hι.generates_range
1817 (by
1818 intro y hy
1819 rcases hy with ⟨x, rfl⟩
1820 exact hfg x)
1822/-- The lift of the canonical generator map to the same free pro-`C` group is the identity. -/
1823@[simp 900] theorem lift_id
1824 (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι) :
1825 hι.lift hι.hasOpenNormalBasisInClass ι hι.convergesToOneAlongOpenSubgroups
1826 hι.generates_range = MonoidHom.id F := by
1827 symm
1828 exact hι.lift_unique hι.hasOpenNormalBasisInClass ι hι.convergesToOneAlongOpenSubgroups
1829 hι.generates_range continuous_id
1830 (by intro x; rfl)
1832end IsEpimorphicallyFreeProCGroupOnConvergingSet
1834/-- Packaged carrier with the epimorphic convergent-family lifting property. -/
1835structure EpimorphicallyFreeProCGroupOnConvergingSetData
1837 /-- The index type of the distinguished converging generating family. -/
1838 basis : Type u
1839 /-- The bundled pro-`C` group generated by the distinguished family. -/
1840 carrier : ProCGrp C
1841 /-- The distinguished family of elements of the bundled carrier. -/
1842 inclusion : basis → carrier
1843 /--
1844 The inclusion is convergent and generating, and satisfies the epimorphic free pro-`C`
1845 universal property.
1846 -/
1847 isEpimorphicallyFree :
1848 IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) basis carrier inclusion
1850/--
1851The cardinality of a finite converging-set basis is the topological rank of the free pro-\(C\)
1852group, provided the finite class has a nontrivial cyclic quotient witness.
1854theorem basisCard_eq_topologicalRank_of_finiteBasis
1855 (C : ProCGroups.FiniteGroupClass.{u})
1857 (hcyc :
1858 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
1859 C A ∧ IsCyclic A ∧ Nontrivial A)
1860 (Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData
1861 (C := C))
1862 [Finite Fdata.basis] :
1863 Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier := by
1864 classical
1865 letI : Fintype Fdata.basis := Fintype.ofFinite Fdata.basis
1866 rcases exists_nontrivial_topologicallyCyclic_proC_of_finiteGroupClass C hquot hcyc with
1867 ⟨A, _instGroupA, _instTopA, _instTopGroupA, _instCompactA, _instT2A, _instTDA,
1868 hA, a, ha1, hgena⟩
1869 have hnontrivial :
1870 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A)
1871 (_ : CompactSpace A) (_ : T2Space A) (_ : TotallyDisconnectedSpace A),
1873 ∃ a : A, a ≠ 1 ∧ Generation.TopologicallyGenerates (G := A) ({a} : Set A) :=
1874 ⟨A, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
1875 hA, a, ha1, hgena⟩
1876 have hιinj : Function.Injective Fdata.inclusion :=
1877 epimorphicallyFreeProCGroupOnConvergingSet_injective
1878 Fdata.isEpimorphicallyFree hnontrivial
1879 have hfg : _root_.ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated Fdata.carrier := by
1880 refine ⟨Finset.univ.image Fdata.inclusion, ?_⟩
1881 simpa [Finset.coe_image] using Fdata.isEpimorphicallyFree.generates_range
1882 have hdle :
1883 Generation.topologicalRank Fdata.carrier ≤ (Fintype.card Fdata.basis : Cardinal) := by
1884 calc
1885 Generation.topologicalRank Fdata.carrier ≤ Cardinal.mk (Set.range Fdata.inclusion) := by
1886 exact Generation.topologicalRank_le_mk_of_topologicallyGenerates
1887 Fdata.isEpimorphicallyFree.generates_range
1888 _ = Cardinal.mk Fdata.basis := by
1889 simpa using (Cardinal.mk_range_eq Fdata.inclusion hιinj)
1890 _ = (Fintype.card Fdata.basis : Cardinal) := by simp only [Cardinal.mk_fintype]
1891 have hdlt : Generation.topologicalRank Fdata.carrier < Cardinal.aleph0 := by
1892 exact lt_of_le_of_lt hdle (Cardinal.natCast_lt_aleph0 (n := Fintype.card Fdata.basis))
1893 let d : ℕ := Cardinal.toNat (Generation.topologicalRank Fdata.carrier)
1894 have hdEq : Generation.topologicalRank Fdata.carrier = d := by
1895 symm
1896 exact Cardinal.cast_toNat_of_lt_aleph0 hdlt
1897 have hdleNat : d ≤ Fintype.card Fdata.basis := by
1898 simpa [d, Nat.card_eq_fintype_card] using
1899 Cardinal.toNat_le_toNat hdle
1900 (Cardinal.natCast_lt_aleph0 (n := Fintype.card Fdata.basis))
1901 by_cases hd0 : d = 0
1902 · have hdEq0 : Generation.topologicalRank Fdata.carrier = 0 := by simpa [d, hd0] using hdEq
1903 have hgen0 :
1904 _root_.ProCGroups.FiniteGeneration.TopologicallyGeneratedByAtMost
1905 (G := Fdata.carrier) 0 :=
1906 _root_.ProCGroups.FiniteGeneration.topologicallyGeneratedByAtMost_of_topologicalRank_eq_nat
1907 (G := Fdata.carrier) hdEq0
1908 rcases hgen0 with ⟨s, hs, hsgen⟩
1909 have hs0 : s.card = 0 := Nat.eq_zero_of_le_zero hs
1910 have hsempty : s = ∅ := Finset.card_eq_zero.mp hs0
1911 have htriv : ∀ x : Fdata.carrier, x = 1 := by
1912 intro x
1913 have hxmem :
1914 x ∈
1915 ((Subgroup.closure
1916 (((s : Finset Fdata.carrier) : Set Fdata.carrier))).topologicalClosure :
1917 Set Fdata.carrier) := by
1918 rw [Generation.TopologicallyGenerates] at hsgen
1919 rw [hsgen]
1920 simp only [Subgroup.coe_top, mem_univ]
1921 simpa [hsempty, Subgroup.coe_topologicalClosure_bot, closure_singleton] using hxmem
1922 have hEmpty : IsEmpty Fdata.basis := by
1923 refine ⟨fun b => ?_⟩
1924 have hb1 : Fdata.inclusion b = 1 := htriv (Fdata.inclusion b)
1925 exact
1926 (one_not_mem_range_of_epimorphicallyFreeProCGroupOnConvergingSet
1927 (hι := Fdata.isEpimorphicallyFree) hnontrivial) ⟨b, hb1⟩
1928 letI : IsEmpty Fdata.basis := hEmpty
1929 have hcard0 : Cardinal.mk Fdata.basis = 0 := by simp only [Cardinal.mk_eq_zero]
1930 rw [hdEq0]
1931 exact hcard0
1932 · have hdPos : 0 < d := Nat.pos_of_ne_zero hd0
1933 rcases _root_.ProCGroups.FiniteGeneration.exists_generatingTuple_of_topologicalRank_le_of_finite
1934 (G := Fdata.carrier) hfg
1935 (show Generation.topologicalRank Fdata.carrier ≤ d by simp only [hdEq, le_refl]) with
1936 ⟨φ, hφgen⟩
1937 let i0 : Fin d := ⟨0, hdPos⟩
1938 have hdleNat' : Fintype.card (Fin d) ≤ Fintype.card Fdata.basis := by
1939 simpa using hdleNat
1940 have hEmb : Nonempty (Fin d ↪ Fdata.basis) := by
1941 exact Function.Embedding.nonempty_of_card_le (α := Fin d) (β := Fdata.basis) hdleNat'
1942 have hConst : Nonempty (Fdata.basis → Fin d) := ⟨fun _ => i0⟩
1943 rcases (Function.exists_surjective_iff).2 ⟨hConst, hEmb⟩ with ⟨q, hqsurj⟩
1944 let ψ : Fdata.basis → Fdata.carrier := fun b => φ (q b)
1945 have hψconv : FamilyConvergesToOneAlongOpenSubgroups (G := Fdata.carrier) ψ := by
1946 exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := Fdata.carrier) ψ
1947 have hψrange : Set.range ψ = Set.range φ := by
1948 ext x
1949 constructor
1950 · rintro ⟨b, rfl⟩
1951 exact ⟨q b, rfl⟩
1952 · rintro ⟨i, rfl⟩
1953 rcases hqsurj i with ⟨b, rfl⟩
1954 exact ⟨b, rfl⟩
1955 have hψgen : Generation.TopologicallyGenerates (G := Fdata.carrier) (Set.range ψ) := by
1956 simpa [hψrange] using hφgen
1957 rcases Fdata.isEpimorphicallyFree.existsUnique_lift
1958 Fdata.isEpimorphicallyFree.hasOpenNormalBasisInClass ψ hψconv hψgen with
1959 ⟨σ, hσ, _⟩
1960 have hσsub : Set.range φ ⊆ (σ.range : Set Fdata.carrier) := by
1961 rintro z ⟨i, rfl⟩
1962 rcases hqsurj i with ⟨b, hb⟩
1963 refine ⟨Fdata.inclusion b, ?_⟩
1964 simpa [ψ, hb] using hσ.2 b
1965 have hσsurj : Function.Surjective σ := by
1966 have hσgen :
1967 Generation.TopologicallyGenerates (G := Fdata.carrier)
1968 ((σ.range : Set Fdata.carrier)) :=
1969 Generation.topologicallyGenerates_mono (G := Fdata.carrier) hφgen hσsub
1970 have hσclosed : IsClosed ((σ.range : Set Fdata.carrier)) := by
1971 simpa using (isCompact_range hσ.1).isClosed
1972 have hσclosure_le : (σ.range : Subgroup Fdata.carrier).topologicalClosure ≤ σ.range :=
1973 Subgroup.topologicalClosure_minimal _ le_rfl hσclosed
1974 have hσclosure_top : (σ.range : Subgroup Fdata.carrier).topologicalClosure = ⊤ := by
1975 have htop :
1976 (Subgroup.closure (σ.range : Set Fdata.carrier)).topologicalClosure =
1977 (⊤ : Subgroup Fdata.carrier) := by
1978 simpa [Generation.TopologicallyGenerates] using hσgen
1979 have hclosure_eq :
1980 (σ.range : Subgroup Fdata.carrier) =
1981 Subgroup.closure (σ.range : Set Fdata.carrier) := by
1982 simpa using (Subgroup.closure_eq (σ.range)).symm
1983 rw [hclosure_eq]
1984 exact htop
1985 have hσrange_top : σ.range = ⊤ := by
1986 apply top_unique
1987 intro z hz
1988 have hz' :
1989 z ∈
1990 ((σ.range : Subgroup Fdata.carrier).topologicalClosure :
1991 Set Fdata.carrier) := by
1992 rw [hσclosure_top]
1993 simp only [Subgroup.coe_top, mem_univ]
1994 exact hσclosure_le hz'
1995 intro z
1996 have hz : z ∈ (σ.range : Set Fdata.carrier) := by
1997 simp only [hσrange_top, Subgroup.coe_top, mem_univ]
1998 simpa using hz
1999 let σc : ContinuousMonoidHom Fdata.carrier Fdata.carrier :=
2000 { toMonoidHom := σ
2001 continuous_toFun := hσ.1 }
2002 rcases
2003 (surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated
2004 (G := Fdata.carrier) hfg σc hσsurj) with
2005 ⟨eσ, heσ⟩
2006 have hσinj : Function.Injective σ := by
2007 intro a b hab
2008 have h' : eσ a = eσ b := by
2009 calc
2010 eσ a = σ a := by
2011 have h := heσ a
2012 change eσ a = σ a at h
2013 exact h
2014 _ = σ b := hab
2015 _ = eσ b := by
2016 have h := (heσ b).symm
2017 change σ b = eσ b at h
2018 exact h
2019 exact eσ.injective h'
2020 have hqinj : Function.Injective q := by
2021 intro b₁ b₂ hb
2022 apply hιinj
2023 apply hσinj
2024 calc
2025 σ (Fdata.inclusion b₁) = ψ b₁ := hσ.2 b₁
2026 _ = φ (q b₁) := rfl
2027 _ = φ (q b₂) := by simp only [hb]
2028 _ = ψ b₂ := rfl
2029 _ = σ (Fdata.inclusion b₂) := (hσ.2 b₂).symm
2030 have hcardEq : Fintype.card Fdata.basis = d := by
2031 have hcardLe : Fintype.card Fdata.basis ≤ d := by
2032 simpa using Fintype.card_le_of_injective q hqinj
2033 exact le_antisymm hcardLe hdleNat
2034 calc
2035 Cardinal.mk Fdata.basis = (Fintype.card Fdata.basis : Cardinal) := by simp only
2036 [Cardinal.mk_fintype]
2037 _ = d := by exact_mod_cast hcardEq
2038 _ = Generation.topologicalRank Fdata.carrier := hdEq.symm
2041/--
2042For a finite discrete pointed space, removing the basepoint from the pointed generating family
2043gives a converging-set basis.
2045theorem freeOnFinitePointedDiscreteSpace_has_convergingSetBasis
2046 {X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X] {x0 : X}
2047 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
2048 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
2049 {ι : X → F}
2050 (hι : IsEpimorphicallyPointedFreeProCGroupOn (C := C) X x0 F ι) :
2051 IsEpimorphicallyFreeProCGroupOnConvergingSet
2052 (C := C) {x : X // x ≠ x0} F (fun x => ι x) := by
2053 classical
2054 let μ : {x : X // x ≠ x0} → F := fun x => ι x
2055 refine ⟨hι.hasOpenNormalBasisInClass, ?_, ?_, ?_⟩
2056 · exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := F) μ
2057 · have hrange : Set.range ι = Set.range μ ∪ ({1} : Set F) := by
2058 ext z
2059 constructor
2060 · rintro ⟨x, rfl⟩
2061 by_cases hx : x = x0
2062 · right
2063 simpa [hx] using hι.map_base
2064 · left
2065 exact ⟨⟨x, hx⟩, rfl⟩
2066 · intro hz
2067 rcases hz with hz | hz
2068 · rcases hz with ⟨x, rfl⟩
2069 exact ⟨x, rfl⟩
2070 · exact ⟨x0, hι.map_base.trans (by simpa using hz.symm)⟩
2071 have hgen' :
2072 Generation.TopologicallyGenerates (G := F) (Set.range μ ∪ ({1} : Set F)) := by
2073 simpa [μ, hrange] using hι.generates_range
2074 exact (Generation.topologicallyGenerates_union_one_iff (G := F) (X := Set.range μ)).1 hgen'
2075 · intro G _ _ _ _ _ _ hG φ _hφconv hgenφ
2076 let φhat : X → G := fun x => if h : x = x0 then 1 else φ ⟨x, h⟩
2077 have hφhat : Continuous φhat := continuous_of_discreteTopology
2078 have hφhat0 : φhat x0 = 1 := by
2079 simp only [ne_eq, ↓reduceDIte, φhat]
2080 have hrange : Set.range φhat = Set.range φ ∪ ({1} : Set G) := by
2081 ext z
2082 constructor
2083 · rintro ⟨x, rfl⟩
2084 by_cases hx : x = x0
2085 · right
2086 simp only [ne_eq, hx, ↓reduceDIte, mem_singleton_iff, φhat]
2087 · left
2088 exact ⟨⟨x, hx⟩, by simp only [ne_eq, hx, ↓reduceDIte, φhat]⟩
2089 · intro hz
2090 rcases hz with hz | hz
2091 · rcases hz with ⟨x, rfl⟩
2092 exact ⟨x, by simp only [ne_eq, x.2, ↓reduceDIte, Subtype.coe_eta, φhat]⟩
2093 · exact ⟨x0, by simpa [φhat] using hz.symm⟩
2094 have hφhatgen :
2095 Generation.TopologicallyGenerates (G := G) (Set.range φhat) := by
2096 have hgen' :
2097 Generation.TopologicallyGenerates (G := G) (Set.range φ ∪ ({1} : Set G)) := by
2098 exact (Generation.topologicallyGenerates_union_one_iff (G := G) (X := Set.range φ)).2 hgenφ
2099 simpa [φhat, hrange] using hgen'
2100 rcases hι.existsUnique_lift hG φhat hφhat hφhat0 hφhatgen with ⟨f, hf, huniq⟩
2101 refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
2102 · intro x
2103 simpa [μ, φhat, x.2] using hf.2 (x : X)
2104 · intro g hg
2105 apply huniq g
2106 refine ⟨hg.1, ?_⟩
2107 intro x
2108 by_cases hx : x = x0
2109 · calc
2110 g (ι x) = g (ι x0) := by rw [hx]
2111 _ = g 1 := by rw [hι.map_base]
2112 _ = 1 := map_one g
2113 _ = φhat x := by simp only [ne_eq, hx, ↓reduceDIte, φhat]
2114 · simpa [μ, φhat, hx] using hg.2 ⟨x, hx⟩
2116/-- For a finite discrete pointed space, the resulting converging-set basis is finite. -/
2117theorem freeOnFinitePointedDiscreteSpace_has_finiteConvergingSetBasis
2118 {X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X] {x0 : X}
2119 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
2120 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
2121 {ι : X → F}
2122 (hι : IsEpimorphicallyPointedFreeProCGroupOn (C := C) X x0 F ι) :
2123 ∃ Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} (C := C),
2124 Nonempty (Fdata.carrier ≃ₜ* F) ∧ Finite Fdata.basis := by
2125 let B : Type u := {x : X // x ≠ x0}
2126 let Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} (C := C) :=
2127 { basis := B
2128 carrier := ProCGrp.of C (ProfiniteGrp.of F) hι.hasOpenNormalBasisInClass
2129 inclusion := fun x => ι x
2130 isEpimorphicallyFree :=
2131 freeOnFinitePointedDiscreteSpace_has_convergingSetBasis
2132 (C := C) (X := X) (x0 := x0) (F := F) (ι := ι) hι }
2133 refine ⟨Fdata, ⟨ContinuousMulEquiv.refl F⟩, ?_⟩
2134 dsimp [Fdata, B]
2135 infer_instance
2137end
2139end ProCGroups.FreeProC