Yamaguchi Lean 4 Library
Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.BasisFiniteRank
ProCGroups/ReidemeisterSchreier/Profinite/OpenSubgroups/BasisFiniteRank/Source

Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.BasisFiniteRank

1import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems
2import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.RankBound
4/-!
5# Finite-rank bases of open subgroups
7Starting from a finite converging-set basis, this module constructs a basis of
8the open subgroup and proves the classical finite Schreier rank formula. The
9padding lemma works on so that its index lives in the ambient
10universe; its public generating-family wrapper is indexed by , while the
11bundled free basis used in the final rank argument retains the lifted carrier.
12-/
14open scoped Topology Pointwise
16namespace ReidemeisterSchreier
17namespace Profinite
19open ProCGroups
20open ProCGroups.FreeProC
21open ProCGroups.ProC
23universe u
25/--
26Finite converging-set basis data for an open subgroup of a free pro-\(C\) group on a finite
27converging set. The carrier is the open subgroup itself.
28-/
29theorem exists_finiteIndexBasisCarrierAndMap_openSubgroup
30 (C : ProCGroups.FiniteGroupClass.{u})
35 {X : Type u} [Finite X]
36 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
37 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
38 {ι : X → F}
39 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
40 (C := C) X F ι)
41 (H : OpenSubgroup F) :
42 ∃ (B : Type u), Finite B ∧
43 ∃ μ : B → ↥(H : Subgroup F),
44 IsEpimorphicallyFreeProCGroupOnConvergingSet
45 (C := C)
46 B ↥(H : Subgroup F) μ := by
47 classical
48 letI : TopologicalSpace X := ⊥
49 letI : DiscreteTopology X := ⟨rfl⟩
50 letI : Fintype X := Fintype.ofFinite X
51 rcases
52 exists_compactPointedBasis_openSubgroup_of_freeProCOnConvergingSet
53 C hForm hSub hIso hExt hF H with
54 ⟨κ, _hκcont, _hκallBase, _hκbase, _hκcompact, _hκclosed, hκfree⟩
55 letI : Finite (OpenSubgroupRightQuotient H) :=
56 finite_openSubgroupRightQuotient (F := F) H
57 have hRangeFin : (Set.range ι).Finite := Set.finite_range ι
58 letI : Finite (Set.range ι) := hRangeFin.to_subtype
59 letI : Fintype (Set.range ι) := Fintype.ofFinite (Set.range ι)
60 letI : Finite (OnePoint X) := Finite.of_fintype (OnePoint X)
61 letI : Finite (Set.range κ) := (Set.finite_range κ).to_subtype
62 let x0 : Set.range κ :=
63 ⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
64 ⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
65 letI : DiscreteTopology (Set.range κ) :=
66 DiscreteTopology.of_finite_of_isClosed_singleton fun _ => isClosed_singleton
67 let B : Type u := {y : Set.range κ // y ≠ x0}
68 let μ : B → ↥(H : Subgroup F) := fun y => y.1.1
69 have hμfree :
70 IsEpimorphicallyFreeProCGroupOnConvergingSet
71 (C := C) B ↥(H : Subgroup F) μ := by
72 simpa [B, μ, x0] using
73 freeOnFinitePointedDiscreteSpace_has_convergingSetBasis
74 (C := C) hκfree
75 exact ⟨B, inferInstance, μ, hμfree⟩
77/--
78An exact-size finite generating family for the open subgroup, indexed by the Schreier
79rank-transform cardinal. This is a generating family, not a basis: the padding step may repeat
80the distinguished padding element 1.
81-/
82private theorem exists_exactGeneratingFamily_openSubgroup_of_finiteBasis_ulift
83 (C : ProCGroups.FiniteGroupClass.{u})
89 (hcyc :
90 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
91 C A ∧ IsCyclic A ∧ Nontrivial A)
92 {X : Type u} [Finite X]
93 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
94 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
95 {ι : X → F}
96 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
97 (C := C) X F ι)
98 (H : OpenSubgroup F) :
99 ∃ κ :
100 ULift.{u} (Fin (_root_.ReidemeisterSchreier.Schreier.rankTransform
101 (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))))) →
102 ↥(H : Subgroup F),
103 Generation.GeneratesAndConvergesToOneAlongOpenSubgroups
104 (G := ↥(H : Subgroup F)) (Set.range κ) := by
105 classical
106 let n : ℕ := _root_.ReidemeisterSchreier.Schreier.rankTransform
107 (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))
108 rcases exists_finiteIndexBasisCarrierAndMap_openSubgroup
109 C hForm hSub hIso hExt hF H with
110 ⟨B, hBfin, μ, hμfree⟩
111 letI : Finite B := hBfin
112 letI : Fintype B := Fintype.ofFinite B
113 let Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData
114 (C := C) :=
115 { basis := B
116 carrier :=
117 ProCGrp.of C (ProfiniteGrp.of ↥(H : Subgroup F)) hμfree.hasOpenNormalBasisInClass
118 inclusion := μ
119 isEpimorphicallyFree := hμfree }
120 letI : Fintype X := Fintype.ofFinite X
121 let Fambient : EpimorphicallyFreeProCGroupOnConvergingSetData
122 (C := C) :=
123 { basis := X
124 carrier := ProCGrp.of C (ProfiniteGrp.of F) hF.hasOpenNormalBasisInClass
125 inclusion := ι
126 isEpimorphicallyFree := hF }
127 have hAmbientRank :
128 Cardinal.mk X = Generation.topologicalRank F :=
129 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fambient
130 have hdF : Generation.topologicalRank F = Nat.card X := by
131 calc
132 Generation.topologicalRank F = Cardinal.mk X := hAmbientRank.symm
133 _ = (Nat.card X : Cardinal) := by simp only [Cardinal.mk_fintype, Nat.card_eq_fintype_card]
134 have hdHle :
135 Generation.topologicalRank ↥(H : Subgroup F) ≤ (n : Cardinal) := by
136 simpa [n] using
137 topologicalRank_openSubgroup_le_rankTransform_of_topologicalRank_eq_nat
138 (G := F) hdF H
139 have hBasisRank :
140 Cardinal.mk B = Generation.topologicalRank ↥(H : Subgroup F) := by
141 convert basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fdata using 1
142 rfl
143 have hBcardLe : Cardinal.mk B ≤ (n : Cardinal) := hBasisRank.trans_le hdHle
144 have hBcardNat : Fintype.card B ≤ Fintype.card (ULift.{u} (Fin n)) := by
145 have hleNat : Fintype.card B ≤ n := by
146 simpa [Nat.card_eq_fintype_card] using
147 Cardinal.toNat_le_toNat hBcardLe (Cardinal.natCast_lt_aleph0 (n := n))
148 simpa using hleNat
149 have hEmb : Nonempty (B ↪ ULift.{u} (Fin n)) :=
150 Function.Embedding.nonempty_of_card_le hBcardNat
151 let e : B ↪ ULift.{u} (Fin n) := Classical.choice hEmb
152 let κ : ULift.{u} (Fin n) → ↥(H : Subgroup F) :=
153 Function.extend e μ (fun _ => 1)
154 have hext : κ ∘ e = μ := by
155 simpa [κ] using
156 (Function.extend_comp e.injective μ (fun _ => (1 : ↥(H : Subgroup F))))
157 have hrange :
158 Set.range μ ⊆ Set.range κ := by
159 rintro z ⟨b, rfl⟩
160 refine ⟨e b, ?_⟩
161 exact congrArg (fun f => f b) hext
162 have hκgen :
163 Generation.TopologicallyGenerates (G := ↥(H : Subgroup F)) (Set.range κ) :=
164 Generation.topologicallyGenerates_mono (G := ↥(H : Subgroup F)) hμfree.generates_range hrange
165 have hκconv : Generation.ConvergesToOneAlongOpenSubgroups (G := ↥(H : Subgroup F)) (Set.range
166 κ) :=
167 Generation.ConvergesToOneAlongOpenSubgroups.of_finite (G := ↥(H : Subgroup F))
168 (Set.finite_range κ)
169 exact ⟨κ, ⟨hκgen, hκconv⟩⟩
172/-- An exact-size finite generating family for the open subgroup on the canonical Fin index.
173The universe lift used to construct the padding embedding remains an implementation detail. -/
174theorem exists_exactGeneratingFamily_openSubgroup_of_finiteBasis
175 (C : ProCGroups.FiniteGroupClass.{u})
181 (hcyc :
182 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
183 C A ∧ IsCyclic A ∧ Nontrivial A)
184 {X : Type u} [Finite X]
185 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
186 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
187 {ι : X → F}
188 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
189 (C := C) X F ι)
190 (H : OpenSubgroup F) :
191 ∃ κ :
192 Fin (_root_.ReidemeisterSchreier.Schreier.rankTransform
193 (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))) →
194 ↥(H : Subgroup F),
195 Generation.GeneratesAndConvergesToOneAlongOpenSubgroups
196 (G := ↥(H : Subgroup F)) (Set.range κ) := by
197 rcases exists_exactGeneratingFamily_openSubgroup_of_finiteBasis_ulift
198 C hForm hSub hIso hQuot hExt hcyc hF H with
199 ⟨κ, hκ⟩
200 let κFin :
201 Fin (_root_.ReidemeisterSchreier.Schreier.rankTransform
202 (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))) →
203 ↥(H : Subgroup F) :=
204 fun i => κ (ULift.up i)
205 refine ⟨κFin, ?_⟩
206 have hrange : Set.range κFin = Set.range κ := by
207 apply Set.Subset.antisymm
208 · rintro y ⟨i, rfl⟩
209 exact ⟨ULift.up i, rfl⟩
210 · rintro y ⟨i, rfl⟩
211 exact ⟨i.down, by cases i; rfl⟩
212 rw [hrange]
213 exact hκ
215/--
216Finite-rank extension-closed variety case using the Schreier rank-transform cardinality bound.
217-/
218theorem exists_basis_openSubgroup_of_extensionClosed_finiteRank
219 (C : ProCGroups.FiniteGroupClass.{u})
223 (hcyc :
224 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
225 C A ∧ IsCyclic A ∧ Nontrivial A)
226 {X : Type u} [Finite X]
227 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
228 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
229 {ι : X → F}
230 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
231 (C := C) X F ι)
232 (H : OpenSubgroup F) :
233 ∃ Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
234 (C := C),
235 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
236 Cardinal.mk Fdata.basis =
237 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H :
238 Subgroup F))) :
239 Cardinal) := by
240 classical
241 rcases hVar.closureBundle_of_isomClosed_extensionClosed hIso hExt with
242 ⟨hForm, hSub, hIso', hQuot, hExt'⟩
243 let n : ℕ := _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H
244 : Subgroup F)))
245 rcases exists_finiteIndexBasisCarrierAndMap_openSubgroup
246 C hForm hSub hIso' hExt' hF H with
247 ⟨B, hBfin, μ, hμfree⟩
248 letI : Finite B := hBfin
249 letI : Fintype B := Fintype.ofFinite B
250 let Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData
251 (C := C) :=
252 { basis := B
253 carrier :=
254 ProCGrp.of C (ProfiniteGrp.of ↥(H : Subgroup F)) hμfree.hasOpenNormalBasisInClass
255 inclusion := μ
256 isEpimorphicallyFree := hμfree }
257 letI : Fintype X := Fintype.ofFinite X
258 let Fambient : EpimorphicallyFreeProCGroupOnConvergingSetData
259 (C := C) :=
260 { basis := X
261 carrier := ProCGrp.of C (ProfiniteGrp.of F) hF.hasOpenNormalBasisInClass
262 inclusion := ι
263 isEpimorphicallyFree := hF }
264 have hAmbientRank :
265 Cardinal.mk X = Generation.topologicalRank F :=
266 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fambient
267 have hdF : Generation.topologicalRank F = Nat.card X := by
268 calc
269 Generation.topologicalRank F = Cardinal.mk X := hAmbientRank.symm
270 _ = (Nat.card X : Cardinal) := by simp only [Cardinal.mk_fintype, Nat.card_eq_fintype_card]
271 have hdHle :
272 Generation.topologicalRank ↥(H : Subgroup F) ≤ (n : Cardinal) := by
273 simpa [n] using
274 topologicalRank_openSubgroup_le_rankTransform_of_topologicalRank_eq_nat
275 (G := F) hdF H
276 have hDataBasis :
277 Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier :=
278 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fdata
279 have hle : Cardinal.mk Fdata.basis ≤ (n : Cardinal) := by
280 simpa [Fdata] using hDataBasis.trans_le hdHle
281 rcases exists_exactGeneratingFamily_openSubgroup_of_finiteBasis_ulift
282 C hForm hSub hIso' hQuot hExt' hcyc hF H with
283 ⟨κ, hκ⟩
284 letI : TopologicalSpace (FreeGroup (ULift.{u} (Fin n))) := ⊥
285 letI : DiscreteTopology (FreeGroup (ULift.{u} (Fin n))) := ⟨rfl⟩
286 letI : IsTopologicalGroup (FreeGroup (ULift.{u} (Fin n))) := by infer_instance
287 let φ : FreeGroup (ULift.{u} (Fin n)) →ₜ* ↥(H : Subgroup F) :=
288 { toMonoidHom := FreeGroup.lift κ
289 continuous_toFun := continuous_of_discreteTopology }
290 have hComp :
292 (C)
293 (FreeGroup (ULift.{u} (Fin n))) ↥(H : Subgroup F) φ := by
294 obtain ⟨Y, hYfree, hYcard⟩ :=
295 exists_freeBasis_comap_freeGroupLift_of_openSubgroup_of_rankTransform
296 (F := F) (X := X) hF.generates_range H
297 let βF : FreeGroup X →* F := FreeGroup.lift ι
298 let L : Subgroup (FreeGroup X) := Subgroup.comap βF (H : Subgroup F)
299 let ψ : L →* ↥(H : Subgroup F) :=
300 { toFun := fun g => ⟨βF g.1, g.2⟩
301 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
302 map_mul' := by
303 intro a b
304 ext
305 simp only [Subgroup.coe_mul, map_mul]}
306 letI : TopologicalSpace (FreeGroup X) := ⊥
307 letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
308 letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
309 have hβFdense : DenseRange βF :=
310 denseRange_freeGroupLift_of_topologicallyGenerates
311 (F := F) (X := X) hF.generates_range
312 have hψdense : DenseRange ψ := by
313 exact denseRange_comapMap_of_openSubgroup (φ := βF) hβFdense H.isOpen'
314 letI : TopologicalSpace (FreeGroup Y) := ⊥
315 letI : DiscreteTopology (FreeGroup Y) := ⟨rfl⟩
316 letI : IsTopologicalGroup (FreeGroup Y) := by infer_instance
317 let bY : FreeGroupBasis Y L := Classical.choice hYfree
318 let eY : FreeGroup Y ≃* L := bY.repr.symm
319 let φY : FreeGroup Y →ₜ* ↥(H : Subgroup F) :=
320 { toMonoidHom := ψ.comp eY.toMonoidHom
321 continuous_toFun := continuous_of_discreteTopology }
322 have hψcont : Continuous ψ := by
323 simpa using (continuous_of_discreteTopology : Continuous ψ)
324 have hφYdense : DenseRange φY := by
325 change DenseRange (fun y : FreeGroup Y => ψ (eY y))
326 exact hψdense.comp (Function.Surjective.denseRange eY.surjective) hψcont
327 have hψfinite :
328 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
329 [Finite Q] [DiscreteTopology Q],
330 C Q →
331 ∀ χL : L →* Q,
332 ∃! φbar : ↥(H : Subgroup F) →* Q,
333 Continuous φbar ∧ φbar.comp ψ = χL := by
334 intro Q _ _ _ _ _ hQ χL
335 rcases
336 exists_continuousFiniteQuotientLift_of_comap_freeGroupLift
337 (C := C)
338 (hForm := hForm) (hSub := hSub) (hIso := hIso')
339 (hQuot := hQuot) (hExt := hExt')
340 (X := X) (F := F) (ι := ι) hF H hQ χL with
341 ⟨φbar, hφbarCont, hφbarFac⟩
342 refine ⟨φbar, ⟨hφbarCont, hφbarFac⟩, ?_⟩
343 intro φbar' hφbar'
344 have hEq : (fun h : ↥(H : Subgroup F) => φbar h) = fun h => φbar' h := by
345 apply DenseRange.equalizer (f := ψ) hψdense
346 · exact hφbarCont
347 · exact hφbar'.1
348 · funext l
349 exact congrArg (fun f : L →* Q => f l) (hφbarFac.trans hφbar'.2.symm)
350 apply MonoidHom.ext
351 intro h
352 simpa using (congrArg (fun f : ↥(H : Subgroup F) → Q => f h) hEq).symm
353 have hfinite :
354 DenseAbstractSchreierFiniteQuotientLiftProperty
355 (C := C) H φY.toMonoidHom := by
356 exact denseAbstractSchreierFiniteQuotientLiftProperty_of_equiv
357 (C := C) (H := H) (eY := eY) (ψ := ψ) hψfinite
358 have hCompY :
360 (C)
361 (FreeGroup Y) ↥(H : Subgroup F) φY := by
362 exact isProCCompletion_denseAbstractSchreier_of_finiteQuotientLifts
363 (C := C)
364 (hForm := hForm) (hSub := hSub) (hIso := hIso')
365 (X := X) (F := F) (ι := ι) hF H hφYdense hfinite
366 exact
367 isProCCompletion_freeGroupLift_of_exactGeneratingFamily_of_completion
368 (C := C) hSub hIso' hQuot hcyc
369 (Y := Y) (Z := ULift.{u} (Fin n)) (by simpa [n] using hYcard) hCompY hκ
370 have hκfree :
371 IsEpimorphicallyFreeProCGroupOnConvergingSet
372 (C := C) (ULift.{u} (Fin n)) ↥(H : Subgroup F) κ := by
373 have hfree :=
374 proCCompletionOfAbstractFreeGroup_is_free
375 (C := C)
376 (X := ULift.{u} (Fin n)) (Fhat := ↥(H : Subgroup F)) (ι := φ) hComp
377 convert hfree using 1
378 ext x
379 change ((κ x : ↥(H : Subgroup F)) : F) =
380 ((FreeGroup.lift κ (FreeGroup.of x) : ↥(H : Subgroup F)) : F)
381 simp only [FreeGroup.lift_apply_of]
382 let Fexact : EpimorphicallyFreeProCGroupOnConvergingSetData
383 (C := C) :=
384 { basis := ULift.{u} (Fin n)
385 carrier :=
386 ProCGrp.of C (ProfiniteGrp.of ↥(H : Subgroup F)) hκfree.hasOpenNormalBasisInClass
387 inclusion := κ
388 isEpimorphicallyFree := hκfree }
389 have hExactBasis :
390 Cardinal.mk Fexact.basis = Generation.topologicalRank Fexact.carrier :=
391 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fexact
392 have hExactCard : Cardinal.mk Fexact.basis = (n : Cardinal) := by
393 simp only [Cardinal.mk_fintype, Fintype.card_ulift, Fintype.card_fin, Fexact]
394 have hge : (n : Cardinal) ≤ Cardinal.mk Fdata.basis := by
395 exact le_of_eq <| by
396 calc
397 (n : Cardinal) = Cardinal.mk Fexact.basis := hExactCard.symm
398 _ = Generation.topologicalRank Fexact.carrier := hExactBasis
399 _ = Generation.topologicalRank Fdata.carrier := by rfl
400 _ = Cardinal.mk Fdata.basis := hDataBasis.symm
401 refine ⟨Fdata, ⟨ContinuousMulEquiv.refl _⟩, ?_⟩
402 have hCard : Cardinal.mk Fdata.basis = (n : Cardinal) := le_antisymm hle hge
403 simpa [n] using hCard
405/--
406Finite-rank Melnikov-formation variant with explicit subgroup closure, using the Schreier
407rank-transform cardinality bound.
408-/
409theorem exists_basis_openSubgroup_of_melnikovFormation_finiteRank_of_subgroupClosed
410 (C : ProCGroups.FiniteGroupClass.{u})
413 (hcyc :
414 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
415 C A ∧ IsCyclic A ∧ Nontrivial A)
416 {X : Type u} [Finite X]
417 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
418 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
419 {ι : X → F}
420 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
421 (C := C) X F ι)
422 (H : OpenSubgroup F) :
423 ∃ Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
424 (C := C),
425 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
426 Cardinal.mk Fdata.basis =
427 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H :
428 Subgroup F))) :
429 Cardinal) := by
431 { subgroupClosed := hSub
432 quotientClosed := hC.quotientClosed
433 finiteProductClosed := hC.formation.finiteProductClosed }
434 exact
435 exists_basis_openSubgroup_of_extensionClosed_finiteRank
436 (C := C) hVar hC.isomClosed hC.extensionClosed hcyc hF H
438end Profinite
439end ReidemeisterSchreier