ReidemeisterSchreier/Profinite/SchreierFormula.lean
1import ReidemeisterSchreier.Profinite.OpenSubgroups.RankBound
2import ReidemeisterSchreier.Profinite.OpenSubgroups.SchreierTransversals
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ReidemeisterSchreier/Profinite/SchreierFormula.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# ReidemeisterSchreier / Profinite / SchreierFormula
15Focused module in the public source tree. It contains declarations used by the library roots and by downstream proof modules.
16-/
18open scoped Topology Pointwise
20namespace ReidemeisterSchreier
21namespace Profinite
23open ProCGroups
24open ProCGroups.FreeProC
26universe u
28/-- `G` admits a free pro-`C` model on a converging set. -/
30 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
31 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
32 ∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
33 Nonempty (Fdata.carrier ≃ₜ* G)
35/-- `G` admits a free pro-`C` model on a converging set of cardinal `m`. -/
37 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
38 (G : Type u) [Group G] [TopologicalSpace G]
39 (m : Cardinal) : Prop :=
40 ∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
41 Nonempty (Fdata.carrier ≃ₜ* G) ∧ Cardinal.mk Fdata.basis = m
43section FormulaPredicates
45variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
47/-- A group with topological rank `r` satisfies Schreier's formula at rank `r` if every open
48normal subgroup has the expected rank transform. -/
50 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
51 (r : ℕ) : Prop :=
52 ∀ U : OpenNormalSubgroup G,
53 Generation.topologicalRank ↥(U : Subgroup G) =
54 (_root_.ReidemeisterSchreier.Schreier.rankTransform r (Nat.card (G ⧸ (U : Subgroup G))) : Cardinal)
56/-- A group satisfies Schreier's formula if the rank transform holds at its finite topological
57rank. -/
59 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
60 ∃ r : ℕ,
61 Generation.topologicalRank G = r ∧ SatisfiesOpenNormalSchreierFormulaAtRank (G := G) r
63end FormulaPredicates
65section ChosenLeftFamilies
67variable {X : Type u} [TopologicalSpace X] [CompactSpace X]
68variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
69variable {ι : X → F}
71/-- The chosen left Schreier generator family attached to an open subgroup. -/
72noncomputable def chosenLeftSchreierGeneratorFamily
73 (H : OpenSubgroup F) :
74 (F ⧸ (H : Subgroup F)) × X → ↥(H : Subgroup F) :=
75 fun p =>
77 (F := F) (H := H)
78 (σ := openSubgroupLeftSchreierSection (F := F) H)
79 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
80 (ι := ι) p.1 p.2
82omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
83@[simp] theorem chosenLeftSchreierGeneratorFamily_apply
84 (H : OpenSubgroup F) (q : F ⧸ (H : Subgroup F)) (x : X) :
85 chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) =
87 (F := F) (H := H)
88 (σ := openSubgroupLeftSchreierSection (F := F) H)
89 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
90 (ι := ι) q x :=
91 rfl
93/-- The nontrivial chosen left Schreier generators attached to an open subgroup. -/
95 (H : OpenSubgroup F) : Set ↥(H : Subgroup F) :=
97 (F := F) (H := H)
98 (σ := openSubgroupLeftSchreierSection (F := F) H)
99 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
100 (ι := ι)
102/-- The nontrivial chosen left Schreier pairs attached to an open subgroup. -/
104 (H : OpenSubgroup F) : Type u :=
106 (F := F) H
107 (openSubgroupLeftSchreierSection (F := F) H)
108 (openSubgroupLeftSchreierSection_rightInverse (F := F) H)
109 ι
111omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
112/-- The tautological map from chosen nontrivial left pairs to the chosen generator set. -/
113noncomputable def chosenLeftNontrivialSchreierPairsToGeneratorSet
114 (H : OpenSubgroup F) :
115 chosenLeftNontrivialSchreierPairs (F := F) (ι := ι) H →
116 ↥(chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) :=
118 (F := F) H
119 (openSubgroupLeftSchreierSection (F := F) H)
120 (openSubgroupLeftSchreierSection_rightInverse (F := F) H)
121 ι
123omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
124@[simp] theorem chosenLeftNontrivialSchreierPairsToGeneratorSet_apply
125 (H : OpenSubgroup F)
126 (p : chosenLeftNontrivialSchreierPairs (F := F) (ι := ι) H) :
127 ((chosenLeftNontrivialSchreierPairsToGeneratorSet (F := F) (ι := ι) H p :
128 ↥(chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H)) : ↥(H : Subgroup F)) =
129 chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H p.1 :=
130 rfl
132omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
134 (H : OpenSubgroup F) :
135 Function.Surjective
136 (chosenLeftNontrivialSchreierPairsToGeneratorSet (F := F) (ι := ι) H) := by
140 (F := F) (H := H)
141 (σ := openSubgroupLeftSchreierSection (F := F) H)
142 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
143 (ι := ι))
145omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
147 (H : OpenSubgroup F) :
148 chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H ⊆
149 Set.range (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H) := by
150 simpa [chosenLeftSchreierGeneratorSet, chosenLeftSchreierGeneratorFamily] using
152 (F := F) (H := H)
153 (σ := openSubgroupLeftSchreierSection (F := F) H)
154 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
155 (ι := ι))
157omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
159 (H : OpenSubgroup F) :
160 Subgroup.closure (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) =
161 Subgroup.closure (Set.range
162 (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H)) := by
163 simpa [chosenLeftSchreierGeneratorSet, chosenLeftSchreierGeneratorFamily] using
165 (F := F) (H := H)
166 (σ := openSubgroupLeftSchreierSection (F := F) H)
167 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
168 (ι := ι))
170omit [TopologicalSpace X] [CompactSpace X] in
172 {H : OpenSubgroup F} :
173 ProCGroups.Generation.TopologicallyGenerates (G := ↥(H : Subgroup F))
174 (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) ↔
175 ProCGroups.Generation.TopologicallyGenerates (G := ↥(H : Subgroup F))
176 (Set.range (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H)) := by
177 simpa [chosenLeftSchreierGeneratorSet, chosenLeftSchreierGeneratorFamily] using
179 (F := F) (H := H)
180 (σ := openSubgroupLeftSchreierSection (F := F) H)
181 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
182 (ι := ι))
184omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
186 (H : OpenSubgroup F) {q : F ⧸ (H : Subgroup F)} {x : X}
187 (hx : ι x ∈ (H : Subgroup F)) :
188 leftSchreierNextCoset (F := F) H (openSubgroupLeftSchreierSection (F := F) H) ι q x =
189 q :=
191 (F := F) (H := H)
192 (σ := openSubgroupLeftSchreierSection (F := F) H)
193 (ι := ι)
194 (openSubgroupLeftSchreierSection_rightInverse (F := F) H)
195 hx
197omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
199 (H : OpenSubgroup F) {q : F ⧸ (H : Subgroup F)} {x : X}
200 (hx : openSubgroupLeftSchreierSection (F := F) H q * ι x ∈ (H : Subgroup F)) :
201 leftSchreierNextCoset (F := F) H (openSubgroupLeftSchreierSection (F := F) H) ι q x =
202 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) :=
204 (F := F) (H := H)
205 (σ := openSubgroupLeftSchreierSection (F := F) H)
206 (ι := ι)
207 hx
209omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
211 (H : OpenSubgroup F) {q : F ⧸ (H : Subgroup F)} {x : X}
212 (hx : ι x ∈ (H : Subgroup F)) :
213 chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) = ⟨ι x, hx⟩ := by
214 simpa [chosenLeftSchreierGeneratorFamily] using
216 (F := F) (H := H)
217 (σ := openSubgroupLeftSchreierSection (F := F) H)
218 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
219 (ι := ι)
220 (q := q) (x := x) hx)
222omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
224 (H : OpenSubgroup F) {q : F ⧸ (H : Subgroup F)} {x : X}
225 (hx : ι x = 1) :
226 chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) = 1 := by
228 (F := F) (H := H)
229 (σ := openSubgroupLeftSchreierSection (F := F) H)
230 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
231 (ι := ι) (q := q) (x := x) hx
233omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
235 {H : OpenSubgroup F} {q : F ⧸ (H : Subgroup F)} {x : X} :
236 chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) = 1 ↔
237 openSubgroupLeftSchreierSection (F := F) H
238 (leftSchreierNextCoset (F := F) H
239 (openSubgroupLeftSchreierSection (F := F) H) ι q x) =
240 openSubgroupLeftSchreierSection (F := F) H q * ι x := by
241 simpa [chosenLeftSchreierGeneratorFamily] using
243 (F := F) (H := H)
244 (σ := openSubgroupLeftSchreierSection (F := F) H)
245 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
246 (ι := ι) (q := q) (x := x))
248omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
250 (H : OpenSubgroup F) {q : F ⧸ (H : Subgroup F)} {x : X}
251 (hx : openSubgroupLeftSchreierSection (F := F) H q * ι x ∈ (H : Subgroup F)) :
252 chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) =
253 ⟨openSubgroupLeftSchreierSection (F := F) H q * ι x, hx⟩ := by
254 simpa [chosenLeftSchreierGeneratorFamily] using
256 (F := F) (H := H)
257 (σ := openSubgroupLeftSchreierSection (F := F) H)
258 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
259 (ι := ι)
260 (openSubgroupLeftSchreierSection_one (F := F) H)
261 (q := q) (x := x) hx)
263omit [CompactSpace X] in
265 (H : OpenSubgroup F)
266 (hιcont : Continuous ι) :
267 Continuous (fun p : (F ⧸ (H : Subgroup F)) × X =>
268 leftSchreierNextCoset (F := F) H (openSubgroupLeftSchreierSection (F := F) H) ι
269 p.1 p.2) := by
271 (F := F) (H := H)
272 (σ := openSubgroupLeftSchreierSection (F := F) H)
273 (ι := ι)
274 (continuous_openSubgroupLeftSchreierSection (F := F) H)
275 hιcont
277omit [CompactSpace X] in
279 (H : OpenSubgroup F)
280 (hιcont : Continuous ι) :
281 Continuous (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H) := by
282 simpa [chosenLeftSchreierGeneratorFamily] using
284 (F := F) (H := H)
285 (σ := openSubgroupLeftSchreierSection (F := F) H)
286 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
287 (ι := ι)
288 (continuous_openSubgroupLeftSchreierSection (F := F) H)
289 hιcont)
291omit [TopologicalSpace X] [CompactSpace X] in
293 (H : OpenSubgroup F) [CompactSpace F] [Finite X] :
294 Nat.card (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) ≤
295 Nat.card (F ⧸ (H : Subgroup F)) * Nat.card X := by
296 letI : Finite (F ⧸ (H : Subgroup F)) :=
297 ProCGroups.openSubgroup_finiteQuotient (G := F) H
299 (F := F) (H := H)
300 (σ := openSubgroupLeftSchreierSection (F := F) H)
301 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
302 (ι := ι)
304omit [TopologicalSpace X] [CompactSpace X] in
306 (H : OpenSubgroup F) [CompactSpace F] [Finite X] :
307 Nat.card (chosenLeftNontrivialSchreierPairs (F := F) (ι := ι) H) ≤
308 Nat.card (F ⧸ (H : Subgroup F)) * Nat.card X := by
309 letI : Finite (F ⧸ (H : Subgroup F)) :=
310 ProCGroups.openSubgroup_finiteQuotient (G := F) H
311 simpa [chosenLeftNontrivialSchreierPairs] using
313 (F := F) (H := H)
314 (σ := openSubgroupLeftSchreierSection (F := F) H)
315 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
316 (ι := ι))
318omit [TopologicalSpace X] [CompactSpace X] in
320 (H : OpenSubgroup F) [CompactSpace F] [Finite X] :
321 Nat.card (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) ≤
322 Nat.card (chosenLeftNontrivialSchreierPairs (F := F) (ι := ι) H) := by
323 letI : Finite (F ⧸ (H : Subgroup F)) :=
324 ProCGroups.openSubgroup_finiteQuotient (G := F) H
325 simpa [chosenLeftSchreierGeneratorSet, chosenLeftNontrivialSchreierPairs] using
327 (F := F) (H := H)
328 (σ := openSubgroupLeftSchreierSection (F := F) H)
329 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
330 (ι := ι))
332omit [TopologicalSpace X] [CompactSpace X] in
334 [Finite X] {x0 : X} (hx0 : ι x0 = 1)
335 (H : OpenSubgroup F) [CompactSpace F] :
336 Nat.card (Set.range (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H)) ≤
337 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) := by
338 letI : Nonempty X := ⟨x0⟩
339 letI : Finite (F ⧸ (H : Subgroup F)) :=
340 ProCGroups.openSubgroup_finiteQuotient (G := F) H
341 let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
342 let κ' : Option ((F ⧸ (H : Subgroup F)) × {x : X // x ≠ x0}) → ↥(H : Subgroup F)
343 | none => 1
344 | some p => chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (p.1, p.2.1)
345 have hbase :
346 ∀ q : F ⧸ (H : Subgroup F),
347 chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x0) = 1 := by
348 intro q
349 simpa [chosenLeftSchreierGeneratorFamily] using
351 (F := F) (H := H)
352 (σ := openSubgroupLeftSchreierSection (F := F) H)
353 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
354 (ι := ι) (q := q) (x := x0) hx0)
355 have hrange :
356 Set.range (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H) =
357 Set.range κ' := by
358 ext y
359 constructor
360 · rintro ⟨⟨q, x⟩, rfl⟩
361 by_cases hx : x = x0
362 · refine ⟨none, ?_⟩
363 subst hx
364 simp only [ne_eq, chosenLeftSchreierGeneratorFamily_apply, hbase q, κ']
365 · refine ⟨some (q, ⟨x, hx⟩), ?_⟩
366 simp only [ne_eq, chosenLeftSchreierGeneratorFamily_apply, κ']
367 · rintro ⟨p, rfl⟩
368 cases p with
369 | none =>
370 exact ⟨(q0, x0), by simp only [hbase q0, ne_eq, chosenLeftSchreierGeneratorFamily_apply, κ']⟩
371 | some p =>
372 rcases p with ⟨q, x⟩
373 exact ⟨(q, x), by simp only [ne_eq, chosenLeftSchreierGeneratorFamily_apply, κ']⟩
374 have hcardCompl : Nat.card {x : X // x ≠ x0} = Nat.card X - 1 := by
375 letI : Fintype X := Fintype.ofFinite X
376 letI : Fintype {x : X // x = x0} := Fintype.ofFinite _
377 letI : Fintype {x : X // x ≠ x0} := Fintype.ofFinite _
378 simp only [ne_eq, Nat.card_eq_fintype_card, Fintype.card_subtype_compl, Fintype.card_unique]
379 have hsucc : Nat.card X = Nat.card {x : X // x ≠ x0} + 1 := by
380 exact (Nat.sub_eq_iff_eq_add Nat.card_pos).1 hcardCompl.symm
381 calc
382 Nat.card (Set.range (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H)) =
383 Nat.card (Set.range κ') := by
384 rw [hrange]
385 _ ≤ Nat.card (Option ((F ⧸ (H : Subgroup F)) × {x : X // x ≠ x0})) := by
386 exact Finite.card_range_le κ'
387 _ = Nat.card ((F ⧸ (H : Subgroup F)) × {x : X // x ≠ x0}) + 1 := by
388 rw [Finite.card_option]
389 _ = Nat.card (F ⧸ (H : Subgroup F)) * Nat.card {x : X // x ≠ x0} + 1 := by
390 rw [Nat.card_prod]
391 _ = 1 + Nat.card (F ⧸ (H : Subgroup F)) * Nat.card {x : X // x ≠ x0} := by
392 rw [Nat.add_comm]
393 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) := by
394 rw [hsucc, _root_.ReidemeisterSchreier.Schreier.rankTransform_succ]
396omit [TopologicalSpace X] [CompactSpace X] in
398 [Finite X] {x0 : X} (hx0 : ι x0 = 1)
399 (H : OpenSubgroup F) [CompactSpace F] :
400 Nat.card (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) ≤
401 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) := by
402 let f := chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H
403 have hsub : chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H ⊆ Set.range f := by
404 simpa [chosenLeftSchreierGeneratorSet, f, chosenLeftSchreierGeneratorFamily] using
406 (F := F) (H := H)
407 (σ := openSubgroupLeftSchreierSection (F := F) H)
408 (hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
409 (ι := ι))
410 letI : Finite (Set.range f) := Set.finite_range f
411 have hle :
412 Nat.card (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) ≤
413 Nat.card (Set.range f) := by
414 exact Nat.card_le_card_of_injective
415 (fun z : chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H =>
416 (⟨z.1, hsub z.2⟩ : Set.range f))
417 (by
418 intro a b h
419 apply Subtype.ext
420 exact congrArg (fun y : Set.range f => (y : ↥(H : Subgroup F))) h)
421 exact hle.trans
423 (F := F) (ι := ι) hx0 H)
425end ChosenLeftFamilies
427section ChosenRightFamilies
429variable {X : Type u} [TopologicalSpace X] [CompactSpace X]
430variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
431variable {ι : X → F}
433/-- The chosen right Schreier generator family attached to an open subgroup. -/
434noncomputable def chosenRightSchreierGeneratorFamily
435 (H : OpenSubgroup F) :
436 OpenSubgroupRightQuotient H × X → ↥(H : Subgroup F) :=
437 fun p =>
439 (F := F) (H := H)
440 (τ := openSubgroupRightCosetSection (F := F) H)
441 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
442 (ι := ι) p.1 p.2
444omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
445@[simp] theorem chosenRightSchreierGeneratorFamily_apply
446 (H : OpenSubgroup F) (q : OpenSubgroupRightQuotient H) (x : X) :
447 chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) =
449 (F := F) (H := H)
450 (τ := openSubgroupRightCosetSection (F := F) H)
451 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
452 (ι := ι) q x :=
453 rfl
455/-- The nontrivial chosen right Schreier generators attached to an open subgroup. -/
457 (H : OpenSubgroup F) : Set ↥(H : Subgroup F) :=
459 (F := F) (H := H)
460 (τ := openSubgroupRightCosetSection (F := F) H)
461 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
462 (ι := ι)
464/-- The nontrivial chosen right Schreier pairs attached to an open subgroup. -/
466 (H : OpenSubgroup F) : Type u :=
468 (F := F) H
469 (openSubgroupRightCosetSection (F := F) H)
470 (openSubgroupRightCosetSection_spec (F := F) H)
471 ι
473omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
474/-- The tautological map from chosen nontrivial right pairs to the chosen generator set. -/
475noncomputable def chosenRightNontrivialSchreierPairsToGeneratorSet
476 (H : OpenSubgroup F) :
477 chosenRightNontrivialSchreierPairs (F := F) (ι := ι) H →
478 ↥(chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) :=
480 (F := F) H
481 (openSubgroupRightCosetSection (F := F) H)
482 (openSubgroupRightCosetSection_spec (F := F) H)
483 ι
485omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
486@[simp] theorem chosenRightNontrivialSchreierPairsToGeneratorSet_apply
487 (H : OpenSubgroup F)
488 (p : chosenRightNontrivialSchreierPairs (F := F) (ι := ι) H) :
489 ((chosenRightNontrivialSchreierPairsToGeneratorSet (F := F) (ι := ι) H p :
490 ↥(chosenRightSchreierGeneratorSet (F := F) (ι := ι) H)) : ↥(H : Subgroup F)) =
491 chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H p.1 :=
492 rfl
494omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
496 (H : OpenSubgroup F) :
497 Function.Surjective
498 (chosenRightNontrivialSchreierPairsToGeneratorSet (F := F) (ι := ι) H) := by
502 (F := F) (H := H)
503 (τ := openSubgroupRightCosetSection (F := F) H)
504 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
505 (ι := ι))
507omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
509 (H : OpenSubgroup F) :
510 chosenRightSchreierGeneratorSet (F := F) (ι := ι) H ⊆
511 Set.range (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H) := by
512 simpa [chosenRightSchreierGeneratorSet, chosenRightSchreierGeneratorFamily] using
514 (F := F) (H := H)
515 (τ := openSubgroupRightCosetSection (F := F) H)
516 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
517 (ι := ι))
519omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
521 (H : OpenSubgroup F) :
522 Subgroup.closure (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) =
523 Subgroup.closure (Set.range
524 (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H)) := by
525 simpa [chosenRightSchreierGeneratorSet, chosenRightSchreierGeneratorFamily] using
527 (F := F) (H := H)
528 (τ := openSubgroupRightCosetSection (F := F) H)
529 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
530 (ι := ι))
532omit [TopologicalSpace X] [CompactSpace X] in
534 {H : OpenSubgroup F} :
535 ProCGroups.Generation.TopologicallyGenerates (G := ↥(H : Subgroup F))
536 (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) ↔
537 ProCGroups.Generation.TopologicallyGenerates (G := ↥(H : Subgroup F))
538 (Set.range (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H)) := by
539 simpa [chosenRightSchreierGeneratorSet, chosenRightSchreierGeneratorFamily] using
541 (F := F) (H := H)
542 (τ := openSubgroupRightCosetSection (F := F) H)
543 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
544 (ι := ι))
546omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
548 (H : OpenSubgroup F) {x : X}
549 (hx : ι x ∈ (H : Subgroup F)) :
550 rightSchreierNextCoset (F := F) H ι (openSubgroupRightCoset H (1 : F)) x =
551 openSubgroupRightCoset H (1 : F) :=
553 (F := F) (H := H) (ι := ι) hx
555omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
557 (H : OpenSubgroup F) {q : OpenSubgroupRightQuotient H} {x : X}
558 (hx : openSubgroupRightCosetSection (F := F) H q * ι x ∈ (H : Subgroup F)) :
559 rightSchreierNextCoset (F := F) H ι q x = openSubgroupRightCoset H (1 : F) :=
561 (F := F) (H := H)
562 (τ := openSubgroupRightCosetSection (F := F) H)
563 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
564 (ι := ι)
565 hx
567omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
569 (H : OpenSubgroup F) {q : OpenSubgroupRightQuotient H} {x : X}
570 (hx : ι x = 1) :
571 chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) = 1 := by
573 (F := F) (H := H)
574 (τ := openSubgroupRightCosetSection (F := F) H)
575 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
576 (ι := ι) (q := q) (x := x) hx
578omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
580 {H : OpenSubgroup F} {q : OpenSubgroupRightQuotient H} {x : X} :
581 chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) = 1 ↔
582 openSubgroupRightCosetSection (F := F) H
583 (rightSchreierNextCoset (F := F) H ι q x) =
584 openSubgroupRightCosetSection (F := F) H q * ι x := by
585 simpa [chosenRightSchreierGeneratorFamily] using
587 (F := F) (H := H)
588 (τ := openSubgroupRightCosetSection (F := F) H)
589 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
590 (ι := ι) (q := q) (x := x))
592omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
594 (H : OpenSubgroup F) {x : X}
595 (hx : ι x ∈ (H : Subgroup F)) :
596 chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H
597 (openSubgroupRightCoset H (1 : F), x) =
598 ⟨ι x, hx⟩ := by
599 simpa [chosenRightSchreierGeneratorFamily] using
601 (F := F) (H := H)
602 (τ := openSubgroupRightCosetSection (F := F) H)
603 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
604 (ι := ι)
605 (openSubgroupRightCosetSection_one (F := F) H)
606 (x := x) hx)
608omit [TopologicalSpace X] [CompactSpace X] [IsTopologicalGroup F] in
610 (H : OpenSubgroup F) {q : OpenSubgroupRightQuotient H} {x : X}
611 (hx : openSubgroupRightCosetSection (F := F) H q * ι x ∈ (H : Subgroup F)) :
612 chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) =
613 ⟨openSubgroupRightCosetSection (F := F) H q * ι x, hx⟩ := by
614 simpa [chosenRightSchreierGeneratorFamily] using
616 (F := F) (H := H)
617 (τ := openSubgroupRightCosetSection (F := F) H)
618 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
619 (ι := ι)
620 (openSubgroupRightCosetSection_one (F := F) H)
621 (q := q) (x := x) hx)
623omit [CompactSpace X] in
625 (H : OpenSubgroup F)
626 (hιcont : Continuous ι) :
627 Continuous (fun p : OpenSubgroupRightQuotient H × X =>
628 rightSchreierNextCoset (F := F) H ι p.1 p.2) := by
630 (F := F) (H := H)
631 (ι := ι)
632 hιcont
634omit [CompactSpace X] in
636 (H : OpenSubgroup F)
637 (hιcont : Continuous ι) :
638 Continuous (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H) := by
639 simpa [chosenRightSchreierGeneratorFamily] using
641 (F := F) (H := H)
642 (τ := openSubgroupRightCosetSection (F := F) H)
643 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
644 (ι := ι)
645 (continuous_openSubgroupRightCosetSection (F := F) H)
646 hιcont)
648omit [TopologicalSpace X] [CompactSpace X] in
650 (H : OpenSubgroup F) [CompactSpace F] [Finite X] :
651 Nat.card (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) ≤
652 Nat.card (OpenSubgroupRightQuotient H) * Nat.card X := by
654 (F := F) (H := H)
655 (τ := openSubgroupRightCosetSection (F := F) H)
656 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
657 (ι := ι)
659omit [TopologicalSpace X] [CompactSpace X] in
661 (H : OpenSubgroup F) [CompactSpace F] [Finite X] :
662 Nat.card (chosenRightNontrivialSchreierPairs (F := F) (ι := ι) H) ≤
663 Nat.card (OpenSubgroupRightQuotient H) * Nat.card X := by
664 letI : Finite (OpenSubgroupRightQuotient H) := finite_openSubgroupRightQuotient (F := F) H
665 simpa [chosenRightNontrivialSchreierPairs] using
667 (F := F) (H := H)
668 (τ := openSubgroupRightCosetSection (F := F) H)
669 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
670 (ι := ι))
672omit [TopologicalSpace X] [CompactSpace X] in
674 (H : OpenSubgroup F) [CompactSpace F] [Finite X] :
675 Nat.card (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) ≤
676 Nat.card (chosenRightNontrivialSchreierPairs (F := F) (ι := ι) H) := by
677 letI : Finite (OpenSubgroupRightQuotient H) := finite_openSubgroupRightQuotient (F := F) H
678 simpa [chosenRightSchreierGeneratorSet, chosenRightNontrivialSchreierPairs] using
680 (F := F) (H := H)
681 (τ := openSubgroupRightCosetSection (F := F) H)
682 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
683 (ι := ι))
685omit [TopologicalSpace X] [CompactSpace X] in
687 [Finite X] {x0 : X} (hx0 : ι x0 = 1)
688 (H : OpenSubgroup F) [CompactSpace F] :
689 Nat.card (Set.range (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H)) ≤
690 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (OpenSubgroupRightQuotient H)) := by
691 letI : Nonempty X := ⟨x0⟩
692 letI : Finite (OpenSubgroupRightQuotient H) := finite_openSubgroupRightQuotient (F := F) H
693 let q0 : OpenSubgroupRightQuotient H := openSubgroupRightCoset H (1 : F)
694 let κ' : Option (OpenSubgroupRightQuotient H × {x : X // x ≠ x0}) → ↥(H : Subgroup F)
695 | none => 1
696 | some p => chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (p.1, p.2.1)
697 have hbase :
698 ∀ q : OpenSubgroupRightQuotient H,
699 chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (q, x0) = 1 := by
700 intro q
701 simpa [chosenRightSchreierGeneratorFamily] using
703 (F := F) (H := H)
704 (τ := openSubgroupRightCosetSection (F := F) H)
705 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
706 (ι := ι) (q := q) (x := x0) hx0)
707 have hrange :
708 Set.range (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H) =
709 Set.range κ' := by
710 ext y
711 constructor
712 · rintro ⟨⟨q, x⟩, rfl⟩
713 by_cases hx : x = x0
714 · refine ⟨none, ?_⟩
715 subst hx
716 simp only [ne_eq, chosenRightSchreierGeneratorFamily_apply, hbase q, κ']
717 · refine ⟨some (q, ⟨x, hx⟩), ?_⟩
718 simp only [ne_eq, chosenRightSchreierGeneratorFamily_apply, κ']
719 · rintro ⟨p, rfl⟩
720 cases p with
721 | none =>
722 exact ⟨(q0, x0), by simp only [hbase q0, ne_eq, chosenRightSchreierGeneratorFamily_apply, κ']⟩
723 | some p =>
724 rcases p with ⟨q, x⟩
725 exact ⟨(q, x), by simp only [ne_eq, chosenRightSchreierGeneratorFamily_apply, κ']⟩
726 have hcardCompl : Nat.card {x : X // x ≠ x0} = Nat.card X - 1 := by
727 letI : Fintype X := Fintype.ofFinite X
728 letI : Fintype {x : X // x = x0} := Fintype.ofFinite _
729 letI : Fintype {x : X // x ≠ x0} := Fintype.ofFinite _
730 simp only [ne_eq, Nat.card_eq_fintype_card, Fintype.card_subtype_compl, Fintype.card_unique]
731 have hsucc : Nat.card X = Nat.card {x : X // x ≠ x0} + 1 := by
732 exact (Nat.sub_eq_iff_eq_add Nat.card_pos).1 hcardCompl.symm
733 calc
734 Nat.card (Set.range (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H)) =
735 Nat.card (Set.range κ') := by
736 rw [hrange]
737 _ ≤ Nat.card (Option (OpenSubgroupRightQuotient H × {x : X // x ≠ x0})) := by
738 exact Finite.card_range_le κ'
739 _ = Nat.card (OpenSubgroupRightQuotient H × {x : X // x ≠ x0}) + 1 := by
740 rw [Finite.card_option]
741 _ = Nat.card (OpenSubgroupRightQuotient H) * Nat.card {x : X // x ≠ x0} + 1 := by
742 rw [Nat.card_prod]
743 _ = 1 + Nat.card (OpenSubgroupRightQuotient H) * Nat.card {x : X // x ≠ x0} := by
744 rw [Nat.add_comm]
745 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (OpenSubgroupRightQuotient H)) := by
746 rw [hsucc, _root_.ReidemeisterSchreier.Schreier.rankTransform_succ]
748omit [TopologicalSpace X] [CompactSpace X] in
750 [Finite X] {x0 : X} (hx0 : ι x0 = 1)
751 (H : OpenSubgroup F) [CompactSpace F] :
752 Nat.card (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) ≤
753 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (OpenSubgroupRightQuotient H)) := by
754 let f := chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H
755 have hsub : chosenRightSchreierGeneratorSet (F := F) (ι := ι) H ⊆ Set.range f := by
756 simpa [chosenRightSchreierGeneratorSet, f, chosenRightSchreierGeneratorFamily] using
758 (F := F) (H := H)
759 (τ := openSubgroupRightCosetSection (F := F) H)
760 (hτ := openSubgroupRightCosetSection_spec (F := F) H)
761 (ι := ι))
762 letI : Finite (Set.range f) := Set.finite_range f
763 have hle :
764 Nat.card (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) ≤
765 Nat.card (Set.range f) := by
766 exact Nat.card_le_card_of_injective
767 (fun z : chosenRightSchreierGeneratorSet (F := F) (ι := ι) H =>
768 (⟨z.1, hsub z.2⟩ : Set.range f))
769 (by
770 intro a b h
771 apply Subtype.ext
772 exact congrArg (fun y : Set.range f => (y : ↥(H : Subgroup F))) h)
773 exact hle.trans
775 (F := F) (ι := ι) hx0 H)
777end ChosenRightFamilies
779end Profinite
780end ReidemeisterSchreier