ProCGroups/FreeProC/FinitelyGenerated.lean
1import ProCGroups.FreeProC.Criteria.InverseLimitsAndFiniteSubsets
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/FreeProC/FinitelyGenerated.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finitely generated free pro-C groups
15does not need the full converging-family bookkeeping at every use site: convergence to `1` is
16automatic, and for concrete finite-group classes the generated-target hypothesis can be discharged
17by corestricting to the closed subgroup generated by the image.
20as a reusable structure.
21-/
23open scoped Topology
25namespace ProCGroups.FreeProC
27universe u v w
29namespace IsFreeProCGroupOnConvergingSet
31/-- For a finite basis and a concrete finite-group class, every target map has a unique
33`FamilyConvergesToOne` proof by hand. -/
34theorem existsUnique_liftHom_of_finite
35 (C : ProCGroups.FiniteGroupClass.{u})
36 [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
37 [hIso : Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
38 {X : Type v} [Finite X]
39 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
40 {ι : X → F}
41 (hι :
43 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
44 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
45 (hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
46 (φ : X → G) :
47 ∃! f : F →ₜ* G, ∀ x, f (ι x) = φ x := by
48 exact
49 hι.existsUnique_liftHom_of_convergesToOne_of_finiteGroupClass
50 C hIso.out hVar.out.subgroupClosed hVar.out.quotientClosed
51 hG φ (FamilyConvergesToOne.of_finite_domain (G := G) φ)
53/-- The finite-rank lift of a map from the basis into a concrete finite-class pro-`C` target. -/
54noncomputable def liftHomOfFinite
55 (C : ProCGroups.FiniteGroupClass.{u})
56 [Fact (ProCGroups.FiniteGroupClass.Variety C)]
57 [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
58 {X : Type v} [Finite X]
59 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
60 {ι : X → F}
61 (hι :
63 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
64 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
65 (hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
66 (φ : X → G) :
67 F →ₜ* G :=
68 Classical.choose
69 (ExistsUnique.exists
70 (hι.existsUnique_liftHom_of_finite C hG φ))
72/-- The finite-rank lift has the prescribed value on each basis element. -/
73@[simp] theorem liftHomOfFinite_apply
74 (C : ProCGroups.FiniteGroupClass.{u})
75 [Fact (ProCGroups.FiniteGroupClass.Variety C)]
76 [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
77 {X : Type v} [Finite X]
78 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
79 {ι : X → F}
80 (hι :
82 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
83 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
84 (hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
85 (φ : X → G) (x : X) :
86 hι.liftHomOfFinite C hG φ (ι x) = φ x :=
87 Classical.choose_spec
88 (ExistsUnique.exists
89 (hι.existsUnique_liftHom_of_finite C hG φ)) x
91/-- The finite-rank lift is unique among continuous homomorphisms with the prescribed basis
92values. -/
93theorem liftHomOfFinite_unique
94 (C : ProCGroups.FiniteGroupClass.{u})
95 [Fact (ProCGroups.FiniteGroupClass.Variety C)]
96 [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
97 {X : Type v} [Finite X]
98 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
99 {ι : X → F}
100 (hι :
102 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
103 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
104 (hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
105 (φ : X → G)
106 {f : F →ₜ* G} (hf : ∀ x, f (ι x) = φ x) :
107 f = hι.liftHomOfFinite C hG φ := by
108 rcases hι.existsUnique_liftHom_of_finite C hG φ with
109 ⟨g, _hg, huniq⟩
110 have hchosen :
111 hι.liftHomOfFinite C hG φ = g := by
112 apply huniq
113 intro x
114 exact hι.liftHomOfFinite_apply C hG φ x
115 exact (huniq f hf).trans hchosen.symm
117/-- A finite discrete converging-set basis gives the usual free pro-`C` universal property for a
119theorem isFreeProCGroup_of_finite
120 (C : ProCGroups.FiniteGroupClass.{u})
121 [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
122 [hIso : Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
123 {X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X]
124 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
125 {ι : X → F}
126 (hι :
128 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι) :
129 IsFreeProCGroup (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι := by
130 refine
132 continuous_ι := continuous_of_discreteTopology
133 generates_range := hι.generates_range
134 existsUnique_lift := ?_ }
135 intro G _ _ _ hG φ _hφ
136 rcases hι.existsUnique_liftHom_of_finite C hG φ with
137 ⟨f, hf, huniq⟩
138 refine ⟨f.toMonoidHom, ⟨f.continuous, hf⟩, ?_⟩
139 intro g hg
140 let gc : F →ₜ* G := { toMonoidHom := g, continuous_toFun := hg.1 }
141 exact congrArg ContinuousMonoidHom.toMonoidHom (huniq gc hg.2)
145/-- A free pro-`C` group with an explicit finite basis `Fin n`. -/
146structure FiniteRankData
147 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u}) (n : ℕ) where
148 carrier : Type u
150 instTopologicalSpace : TopologicalSpace carrier
151 instIsTopologicalGroup : IsTopologicalGroup carrier
152 inclusion : Fin n → carrier
153 isFree : IsFreeProCGroupOnConvergingSet (ProC := ProC) (Fin n) carrier inclusion
155attribute [instance] FiniteRankData.instGroup
156attribute [instance] FiniteRankData.instTopologicalSpace
157attribute [instance] FiniteRankData.instIsTopologicalGroup
159namespace FiniteRankData
161variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}} {n : ℕ}
163/-- The carrier of finite-rank free pro-`C` data is a pro-`C` group. -/
164theorem isProC (Fdata : FiniteRankData ProC n) :
165 ProC (G := Fdata.carrier) :=
166 Fdata.isFree.isProC
168/-- Homomorphisms out of finite-rank free pro-`C` data are determined by the finite basis. -/
169theorem hom_ext
170 (Fdata : FiniteRankData ProC n)
171 {G : Type u} [Group G] [TopologicalSpace G] [T2Space G]
172 {f g : Fdata.carrier →ₜ* G}
173 (hfg : ∀ i, f (Fdata.inclusion i) = g (Fdata.inclusion i)) :
174 f = g :=
175 Fdata.isFree.hom_ext hfg
177/-- Lift a map from a finite basis into a concrete finite-class pro-`C` target. -/
178noncomputable def liftHom
179 (C : ProCGroups.FiniteGroupClass.{u})
180 [Fact (ProCGroups.FiniteGroupClass.Variety C)]
181 [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
182 {n : ℕ}
183 (Fdata :
185 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) n)
186 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
187 (hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
188 (φ : Fin n → G) :
189 Fdata.carrier →ₜ* G :=
190 Fdata.isFree.liftHomOfFinite C hG φ
192/-- The finite-rank lift has the prescribed value on the `i`th basis element. -/
193@[simp] theorem liftHom_apply
194 (C : ProCGroups.FiniteGroupClass.{u})
195 [Fact (ProCGroups.FiniteGroupClass.Variety C)]
196 [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
197 {n : ℕ}
198 (Fdata :
200 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) n)
201 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
202 (hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
203 (φ : Fin n → G) (i : Fin n) :
204 Fdata.liftHom C hG φ (Fdata.inclusion i) = φ i :=
205 Fdata.isFree.liftHomOfFinite_apply C hG φ i
207/-- The finite-rank lift is unique among continuous homomorphisms with the prescribed values on
209theorem liftHom_unique
210 (C : ProCGroups.FiniteGroupClass.{u})
211 [Fact (ProCGroups.FiniteGroupClass.Variety C)]
212 [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
213 {n : ℕ}
214 (Fdata :
216 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) n)
217 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
218 (hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
219 (φ : Fin n → G)
220 {f : Fdata.carrier →ₜ* G} (hf : ∀ i, f (Fdata.inclusion i) = φ i) :
221 f = Fdata.liftHom C hG φ :=
222 Fdata.isFree.liftHomOfFinite_unique C hG φ hf
224/-- The canonical continuous multiplicative equivalence between two finite-rank free pro-`C`
225groups with the same rank. -/
226noncomputable def equivOfSameRank
227 (Fdata Edata : FiniteRankData ProC n) :
228 Fdata.carrier ≃ₜ* Edata.carrier :=
229 Fdata.isFree.continuousMulEquivOfSameBasis Edata.isFree
231/-- The same-rank equivalence sends each basis element to the corresponding basis element. -/
232@[simp] theorem equivOfSameRank_apply
233 (Fdata Edata : FiniteRankData ProC n) (i : Fin n) :
234 Fdata.equivOfSameRank Edata (Fdata.inclusion i) = Edata.inclusion i :=
235 Fdata.isFree.continuousMulEquivOfSameBasis_apply Edata.isFree i
239/-- The finite-subset inverse system attached to a free pro-`C` group on a basis converging to
241structure FiniteSubsetSystem
242 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
243 (X : Type u)
244 (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
245 (ι : X → F) where
246 system : TopologicalGroupInverseSystemData (I := FiniteSubset X)
247 basis : ∀ s : FiniteSubset X, ↥s.1 → system.toInverseSystem.X s
248 stage_isFree :
249 ∀ s : FiniteSubset X,
250 IsFreeProCGroupOnConvergingSet (ProC := ProC)
251 ↥s.1 (system.toInverseSystem.X s) (basis s)
252 transition_basis :
253 ∀ {s t : FiniteSubset X} (hst : s ≤ t) (x : ↥t.1),
254 system.toInverseSystem.map hst (basis t x) =
255 by
256 classical
257 exact if hx : x.1 ∈ s.1 then basis s ⟨x.1, hx⟩ else 1
258 stage_embedding :
259 ∀ s : FiniteSubset X,
260 ∃ e : system.toInverseSystem.X s →* F,
261 Continuous e ∧
262 Function.Injective e ∧
263 IsClosed (Set.range e) ∧
264 ∀ x : ↥s.1, e (basis s x) = ι x.1
265 limitEquiv : Nonempty (F ≃ₜ* system.toInverseSystem.inverseLimit)
267/-- Construct the packaged finite-subset system from the explicit permanence hypotheses used by
269theorem exists_finiteSubsetSystem
270 {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
271 {X : Type u}
272 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
273 {ι : X → F}
274 (hProfinite :
275 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
276 @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
277 InverseSystems.IsProfiniteSpace G)
278 (hClosed :
279 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
280 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
281 (H : Subgroup G), IsClosed (H : Set G) →
282 @ProCGroups.ProC.ProCGroupPredicate.holds ProC H _ _ _)
283 (hFiniteQuot :
284 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
285 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
286 (U : OpenNormalSubgroup G),
287 @ProCGroups.ProC.ProCGroupPredicate.holds ProC (G ⧸ (U : Subgroup G)) _ _ _)
288 (hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι) :
289 Nonempty (FiniteSubsetSystem ProC X F ι) := by
290 rcases exists_finiteSubsetSystem_raw
291 (ProC := ProC) (X := X) (F := F) (ι := ι)
292 hProfinite hClosed hFiniteQuot hF with
293 ⟨S, basis, hbasis, htransition, hembed, hlimit⟩
294 exact
295 ⟨{ system := S
296 basis := basis
297 stage_isFree := hbasis
298 transition_basis := htransition
299 stage_embedding := hembed
300 limitEquiv := hlimit }⟩
302/-- A free pro-`C` group on a basis converging to `1` is a projective limit of the finite-rank
304theorem isLimit_finiteSubsets
305 {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
306 {X : Type u}
307 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
308 {ι : X → F}
309 (hProfinite :
310 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
311 @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
312 InverseSystems.IsProfiniteSpace G)
313 (hClosed :
314 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
315 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
316 (H : Subgroup G), IsClosed (H : Set G) →
317 @ProCGroups.ProC.ProCGroupPredicate.holds ProC H _ _ _)
318 (hFiniteQuot :
319 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
320 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
321 (U : OpenNormalSubgroup G),
322 @ProCGroups.ProC.ProCGroupPredicate.holds ProC (G ⧸ (U : Subgroup G)) _ _ _)
323 (hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι) :
324 ∃ S : FiniteSubsetSystem ProC X F ι,
325 Nonempty (F ≃ₜ* S.system.toInverseSystem.inverseLimit) := by
326 rcases exists_finiteSubsetSystem
327 (ProC := ProC) (X := X) (F := F) (ι := ι)
328 hProfinite hClosed hFiniteQuot hF with
329 ⟨S⟩
330 exact ⟨S, S.limitEquiv⟩
332/-- Infinite-basis spelling of the finite-subset projective-limit theorem. The construction is
333the same as in the arbitrary-basis theorem, but this name is convenient for the standard
334infinite-rank use case. -/
336 {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
337 {X : Type u} [Infinite X]
338 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
339 {ι : X → F}
340 (hProfinite :
341 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
342 @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
343 InverseSystems.IsProfiniteSpace G)
344 (hClosed :
345 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
346 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
347 (H : Subgroup G), IsClosed (H : Set G) →
348 @ProCGroups.ProC.ProCGroupPredicate.holds ProC H _ _ _)
349 (hFiniteQuot :
350 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
351 (_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
352 (U : OpenNormalSubgroup G),
353 @ProCGroups.ProC.ProCGroupPredicate.holds ProC (G ⧸ (U : Subgroup G)) _ _ _)
354 (hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι) :
355 ∃ S : FiniteSubsetSystem ProC X F ι,
356 Nonempty (F ≃ₜ* S.system.toInverseSystem.inverseLimit) :=
358 (ProC := ProC) (X := X) (F := F) (ι := ι)
359 hProfinite hClosed hFiniteQuot hF
361/-- Concrete finite-group-class version of the finite-subset projective-limit system. -/
363 (C : ProCGroups.FiniteGroupClass.{u})
364 [hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
365 [hIso : Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
366 {X : Type u}
367 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
368 {ι : X → F}
369 (hF :
371 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι) :
372 Nonempty
374 (ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι) := by
375 refine exists_finiteSubsetSystem
376 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
377 (X := X) (F := F) (ι := ι) ?_ ?_ ?_ hF
378 · intro G _ _ _ hG
379 let hGprof : ProCGroups.IsProfiniteGroup G :=
381 exact (InverseSystems.isProfiniteSpace_iff_compact_t2_totallyDisconnected (X := G)).2
385 · intro G _ _ _ hG H hH
386 exact
388 hIso.out hVar.out.subgroupClosed hVar.out.quotientClosed hG H hH
389 · intro G _ _ _ hG U
390 let hGprof : ProCGroups.IsProfiniteGroup G :=
392 letI : CompactSpace G := ProCGroups.IsProfiniteGroup.compactSpace hGprof
393 haveI : Finite (G ⧸ (U : Subgroup G)) :=
394 openNormalSubgroup_finiteQuotient (G := G) U
395 exact
397 (C := C) (G := G ⧸ (U : Subgroup G))
398 hVar.out.quotientClosed
399 (ProCGroups.ProC.IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
400 hIso.out hVar.out.quotientClosed hG U)
402/-- Concrete finite-group-class version: a free pro-`C` group on an infinite basis is the
405 (C : ProCGroups.FiniteGroupClass.{u})
406 [Fact (ProCGroups.FiniteGroupClass.Variety C)]
407 [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
408 {X : Type u} [Infinite X]
409 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
410 {ι : X → F}
411 (hF :
413 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι) :
414 ∃ S : FiniteSubsetSystem
415 (ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι,
416 Nonempty (F ≃ₜ* S.system.toInverseSystem.inverseLimit) := by
418 (C := C) (X := X) (F := F) (ι := ι) hF with
419 ⟨S⟩
420 exact ⟨S, S.limitEquiv⟩
422end ProCGroups.FreeProC