Yamaguchi Lean 4 Library
ReidemeisterSchreier/Profinite/OpenSubgroups/MinimalPower.lean
ReidemeisterSchreier/Profinite/OpenSubgroups/MinimalPower/Source

ReidemeisterSchreier/Profinite/OpenSubgroups/MinimalPower.lean

1import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisFiniteRank
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/MinimalPower.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Profinite open-subgroup Schreier theory
14Profinite open subgroup quotients, finite permutation targets, dense free models, exact right Schreier generation, and topological rank bounds.
15-/
17open scoped Topology Pointwise
19namespace ReidemeisterSchreier
20namespace Profinite
22open ProCGroups
23open ProCGroups.FreeProC
24open ProCGroups.ProC
26universe u
29/-- Pointed profinite Reidemeister-Schreier over a converging-set basis, with a prescribed
30minimal generator power landing in the open subgroup. -/
32 (C : ProCGroups.FiniteGroupClass.{u})
38 {X : Type u}
39 [TopologicalSpace X] [DiscreteTopology X]
40 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
41 {ι : X → F}
44 (H : OpenSubgroup F) (x : X) {N : ℕ}
45 (hN : 0 < N)
46 (hpow : (ι x) ^ N ∈ (H : Subgroup F))
47 (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
48 ∃ κ : OpenSubgroupRightQuotient H × OnePoint X → ↥(H : Subgroup F),
49 Continuous κ ∧
50 (∀ q : OpenSubgroupRightQuotient H, κ (q, OnePoint.infty) = 1) ∧
51 κ (openSubgroupRightCoset H (1 : F), OnePoint.infty) = 1 ∧
52 (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈ Set.range κ ∧
53 IsCompact (Set.range κ) ∧
54 IsClosed (Set.range κ) ∧
57 (Set.range κ)
58 ⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
59 ⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
60 ↥(H : Subgroup F) Subtype.val := by
61 classical
62 let iInf : OnePoint X → F := fun z => z.elim 1 ι
63 have hιTendsto : Filter.Tendsto ι Filter.cofinite (𝓝 (1 : F)) := by
64 letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
65 letI : T2Space F := IsProCGroup.t2Space hF.isProC
66 letI : TotallyDisconnectedSpace F := IsProCGroup.totallyDisconnectedSpace hF.isProC
67 rw [Filter.tendsto_def]
68 intro s hs
69 rcases mem_nhds_iff.mp hs with ⟨W, hWs, hWopen, h1W⟩
71 (G := F) hWopen h1W with
72 ⟨U, hUW⟩
73 have hfinite : {x : X | ι x ∉ (U : Set F)}.Finite :=
74 hF.convergesToOne U.toOpenSubgroup
75 have hcof : ∀ᶠ x : X in Filter.cofinite, ι x ∈ (U : Set F) :=
76 Filter.eventually_cofinite.2 hfinite
77 exact hcof.mono fun x hx => hWs (hUW hx)
78 have hPointed :
81 (OnePoint X) OnePoint.infty F iInf := by
82 refine ⟨hF.isProC, ?_, by simp only [OnePoint.elim_infty, iInf], ?_, ?_⟩
83 · rw [OnePoint.continuous_iff_from_discrete]
84 simpa [iInf] using hιTendsto
85 · have hsub : Set.range ι ⊆ Set.range iInf := by
86 rintro y ⟨x, rfl⟩
87 exact ⟨(x : OnePoint X), rfl⟩
88 exact Generation.topologicallyGenerates_mono (G := F) hF.generates_range hsub
89 · intro G _ _ _ hG φ hφ hφ0 hgenφ
90 let ψ : X → G := fun x => φ x
91 have hψTendsto : Filter.Tendsto ψ Filter.cofinite (𝓝 (1 : G)) := by
92 have hraw := (OnePoint.continuous_iff_from_discrete (f := φ)).1 hφ
93 simpa [ψ, hφ0] using hraw
94 have hψconv : FamilyConvergesToOne (G := G) ψ := by
95 intro U
96 exact Filter.eventually_cofinite.mp <|
97 hψTendsto (U.isOpen'.mem_nhds U.one_mem')
98 have hφrange : Set.range φ = Set.range ψ ∪ ({1} : Set G) := by
99 ext z
100 constructor
101 · rintro ⟨x, rfl⟩
102 refine OnePoint.rec ?_ ?_ x
103 · right
104 simpa [iInf] using hφ0
105 · intro y
106 left
107 exact ⟨y, rfl⟩
108 · intro hz
109 rcases hz with hz | hz
110 · rcases hz with ⟨y, rfl⟩
111 exact ⟨(y : OnePoint X), rfl⟩
112 · exact ⟨OnePoint.infty, hφ0.trans hz.symm⟩
113 have hψgen : Generation.TopologicallyGenerates (G := G) (Set.range ψ) := by
114 have hgenφ' :
115 Generation.TopologicallyGenerates (G := G) (Set.range ψ ∪ ({1} : Set G)) := by
116 simpa [hφrange] using hgenφ
117 exact (Generation.topologicallyGenerates_union_one_iff (G := G) (X := Set.range ψ)).1
118 hgenφ'
119 rcases hF.existsUnique_lift hG ψ hψconv hψgen with ⟨f, hf, huniq⟩
120 refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
121 · intro z
122 refine OnePoint.rec ?_ ?_ z
123 · calc
124 f (iInf OnePoint.infty) = f 1 := rfl
125 _ = 1 := map_one f
126 _ = φ OnePoint.infty := hφ0.symm
127 · intro y
128 exact hf.2 y
129 · intro g hg
130 apply huniq g
131 refine ⟨hg.1, ?_⟩
132 intro y
133 simpa [iInf, ψ] using hg.2 (y : OnePoint X)
134 let x' : OnePoint X := x
135 have hpow' : (iInf x') ^ N ∈ (H : Subgroup F) := by
136 simpa [iInf, x'] using hpow
137 have hmin' : ∀ m : ℕ, 0 < m → m < N → (iInf x') ^ m ∉ (H : Subgroup F) := by
138 intro m hm hlt
139 simpa [iInf, x'] using hmin m hm hlt
140 exact
142 (C := C) hForm hSub hIso hQuot hExt hPointed H x' hN hpow' hmin'
145/-- Finite-rank pointed control over a converging-set free pro-`C` group: if `x ^ N` is the
146first positive power of a basis element landing in `H`, and this power is nontrivial, the finite
147converging-set basis model for `H` can be chosen so that `x ^ N` is in the basis image. -/
149 {C : ProCGroups.FiniteGroupClass.{u}}
155 {X : Type u} [Finite X]
156 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
157 {ι : X → F}
158 [DiscreteTopology (Set.range ι)]
161 (H : OpenSubgroup F) (x : X) {N : ℕ}
162 (hN : 0 < N)
163 (hpow : (ι x) ^ N ∈ (H : Subgroup F))
164 (hpow_ne : (ι x) ^ N ≠ 1)
165 (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
168 ∃ e : Fdata.carrier ≃ₜ* ↥(H : Subgroup F),
169 (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈
170 Set.range (e ∘ Fdata.inclusion) ∧
171 Finite Fdata.basis := by
172 classical
173 letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
174 letI : T2Space F := IsProCGroup.t2Space hF.isProC
175 letI : TopologicalSpace X := ⊥
176 letI : DiscreteTopology X := ⟨rfl⟩
177 letI : Fintype X := Fintype.ofFinite X
178 rcases
180 C hForm hSub hIso hQuot hExt hF H x hN hpow hmin with
181 ⟨κ, _hκcont, _hκbase, hκone, hxpowRange, _hκcompact, _hκclosed, hκfree⟩
182 letI : Finite (OpenSubgroupRightQuotient H) :=
184 letI : Finite (OnePoint X) := Finite.of_fintype (OnePoint X)
185 letI : Finite (Set.range κ) := (Set.finite_range κ).to_subtype
186 let x0 : Set.range κ :=
187 ⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
188 ⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
189 letI : DiscreteTopology (Set.range κ) :=
190 DiscreteTopology.of_finite_of_isClosed_singleton fun _ => isClosed_singleton
191 let B : Type u := {y : Set.range κ // y ≠ x0}
192 let μ : B → ↥(H : Subgroup F) := fun y => y.1.1
193 have hμfree :
195 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) B ↥(H : Subgroup F) μ := by
196 simpa [B, μ, x0] using
201 { basis := B
202 carrier := ↥(H : Subgroup F)
203 instGroup := inferInstance
204 instTopologicalSpace := inferInstance
205 instIsTopologicalGroup := inferInstance
206 inclusion := μ
207 isFree := hμfree }
208 let ypow : Set.range κ := ⟨⟨(ι x) ^ N, hpow⟩, hxpowRange⟩
209 have hypow_ne_x0 : ypow ≠ x0 := by
210 intro hEq
211 apply hpow_ne
212 have hval : (ypow : ↥(H : Subgroup F)) = (x0 : ↥(H : Subgroup F)) :=
213 congrArg Subtype.val hEq
214 have hx0val : (x0 : ↥(H : Subgroup F)) = 1 := by
215 simpa [x0] using hκone
216 simpa [ypow] using hval.trans hx0val
217 let bpow : B := ⟨ypow, hypow_ne_x0⟩
218 have hbpow : μ bpow = (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) := rfl
219 refine ⟨Fdata, ContinuousMulEquiv.refl _, ?_, ?_⟩
220 · refine ⟨bpow, ?_⟩
221 simpa [Fdata, μ] using hbpow
222 · dsimp [Fdata, B]
223 infer_instance
225/-- Finite-rank pointed profinite Reidemeister-Schreier: if `x ^ N` is the first positive power of
226the chosen ambient basis element landing in `H`, and this power is nontrivial, then one can choose
227the exact finite-rank basis model of `H` so that `x ^ N` belongs to the basis image. -/
229 (C : ProCGroups.FiniteGroupClass.{u})
233 (hcyc :
234 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
235 C A ∧ IsCyclic A ∧ Nontrivial A)
236 {X : Type u} [Finite X]
237 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
238 {ι : X → F}
239 [DiscreteTopology (Set.range ι)]
242 (H : OpenSubgroup F) (x : X) {N : ℕ}
243 (hN : 0 < N)
244 (hpow : (ι x) ^ N ∈ (H : Subgroup F))
245 (hpow_ne : (ι x) ^ N ≠ 1)
246 (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
249 ∃ e : Fdata.carrier ≃ₜ* ↥(H : Subgroup F),
250 (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈
251 Set.range (e ∘ Fdata.inclusion) ∧
252 Cardinal.mk Fdata.basis =
253 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
254 Cardinal) := by
255 classical
256 rcases hVar.closureBundle_of_isomClosed_extensionClosed hIso hExt with
257 ⟨hForm, hSub, hIso', hQuot, hExt'⟩
258 rcases
260 (C := C) hForm hSub hIso' hQuot hExt' hF H x hN hpow hpow_ne hmin with
261 ⟨Fdata, eData, hxrange, hFin⟩
262 letI : Finite Fdata.basis := hFin
264 (C := C) hVar hIso hExt hcyc hF H with
265 ⟨Fexact, hFexactEquiv, hExactCard⟩
266 have hFexactLt : Cardinal.mk Fexact.basis < Cardinal.aleph0 := by
267 calc
268 Cardinal.mk Fexact.basis =
269 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
270 Cardinal) := hExactCard
271 _ < Cardinal.aleph0 := Cardinal.natCast_lt_aleph0
272 letI : Finite Fexact.basis := Cardinal.lt_aleph0_iff_finite.mp hFexactLt
273 have hExactBasis :
274 Cardinal.mk Fexact.basis = Generation.topologicalRank Fexact.carrier :=
276 have hDataBasis :
277 Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier :=
279 rcases hFexactEquiv with ⟨eExact⟩
280 have hExactProf : ProCGroups.IsProfiniteGroup Fexact.carrier :=
282 have hDataProf : ProCGroups.IsProfiniteGroup Fdata.carrier :=
284 have hRankEq :
285 Generation.topologicalRank Fexact.carrier =
286 Generation.topologicalRank Fdata.carrier := by
287 exact Generation.topologicalRank_eq_of_continuousMulEquiv
288 hExactProf hDataProf (eExact.trans eData.symm)
289 have hCard :
290 Cardinal.mk Fdata.basis =
291 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
292 Cardinal) := by
293 calc
294 Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier := hDataBasis
295 _ = Generation.topologicalRank Fexact.carrier := hRankEq.symm
296 _ = Cardinal.mk Fexact.basis := hExactBasis.symm
297 _ = (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
298 Cardinal) := hExactCard
299 exact ⟨Fdata, eData, hxrange, hCard⟩
301/-- Preimage form of the finite pointed-control theorem. -/
303 {C : ProCGroups.FiniteGroupClass.{u}}
309 {X : Type u} [Finite X]
310 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
311 {ι : X → F}
312 [DiscreteTopology (Set.range ι)]
315 {Q : Type u} [Group Q] [TopologicalSpace Q]
316 (π : F →* Q) (hπcont : Continuous π)
317 (H : OpenSubgroup Q) (x : X) {N : ℕ}
318 (hN : 0 < N)
319 (hpow : (ι x) ^ N ∈ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F))
320 (hpow_ne : (ι x) ^ N ≠ 1)
321 (hmin :
322 ∀ m : ℕ, 0 < m → m < N →
323 (ι x) ^ m ∉ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) :
326 ∃ e : Fdata.carrier ≃ₜ*
327 ↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F),
328 (⟨(ι x) ^ N, hpow⟩ :
329 ↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) ∈
330 Set.range (e ∘ Fdata.inclusion) ∧
331 Finite Fdata.basis := by
332 exact
334 (C := C) hForm hSub hIso hQuot hExt hF
335 (OpenSubgroup.comap π hπcont H) x hN hpow hpow_ne hmin
337/-- Preimage form of the finite-rank pointed Reidemeister-Schreier theorem.
339This is the version for `π⁻¹(H)`, with the Schreier rank transform expressed using the
340quotient-side index `Nat.card (Q ⧸ H)`. -/
342 (C : ProCGroups.FiniteGroupClass.{u})
346 (hcyc :
347 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
348 C A ∧ IsCyclic A ∧ Nontrivial A)
349 {X : Type u} [Finite X]
350 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
351 {ι : X → F}
352 [DiscreteTopology (Set.range ι)]
355 {Q : Type u} [Group Q] [TopologicalSpace Q]
356 (π : F →* Q) (hπcont : Continuous π) (hπsurj : Function.Surjective π)
357 (H : OpenSubgroup Q) (x : X) {N : ℕ}
358 (hN : 0 < N)
359 (hpow : (ι x) ^ N ∈ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F))
360 (hpow_ne : (ι x) ^ N ≠ 1)
361 (hmin :
362 ∀ m : ℕ, 0 < m → m < N →
363 (ι x) ^ m ∉ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) :
366 ∃ e : Fdata.carrier ≃ₜ*
367 ↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F),
368 (⟨(ι x) ^ N, hpow⟩ :
369 ↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) ∈
370 Set.range (e ∘ Fdata.inclusion) ∧
371 Cardinal.mk Fdata.basis =
372 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (Q ⧸ (H : Subgroup Q))) :
373 Cardinal) := by
374 classical
376 (C := C) hVar hIso hExt hcyc hF
377 (OpenSubgroup.comap π hπcont H) x hN hpow hpow_ne hmin with
378 ⟨Fdata, e, hxNrange, hCard⟩
379 have hIndex :
380 Nat.card
381 (F ⧸ (((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F))) =
382 Nat.card (Q ⧸ (H : Subgroup Q)) := by
383 simpa [OpenSubgroup.comap] using
384 (Subgroup.index_comap_of_surjective (H := (H : Subgroup Q)) (f := π) hπsurj)
385 refine ⟨Fdata, e, hxNrange, ?_⟩
386 calc
387 Cardinal.mk Fdata.basis =
388 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X)
389 (Nat.card
390 (F ⧸
391 (((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)))) :
392 Cardinal) := hCard
393 _ = (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (Q ⧸ (H : Subgroup Q))) :
394 Cardinal) := by
395 exact_mod_cast congrArg (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X)) hIndex
397/-- Right-coset formulation of the finite pointed-control theorem for preimages of open
398subgroups. -/
400 {C : ProCGroups.FiniteGroupClass.{u}}
406 {X : Type u} [Finite X]
407 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
408 {ι : X → F}
409 [DiscreteTopology (Set.range ι)]
412 {Q : Type u} [Group Q] [TopologicalSpace Q]
413 (π : F →* Q) (hπcont : Continuous π)
414 (H : OpenSubgroup Q) (x : X) {N : ℕ}
415 (hN : 0 < N)
416 (hcosetPow :
417 openSubgroupRightCoset H ((π (ι x)) ^ N) = openSubgroupRightCoset H (1 : Q))
418 (hcosetMin :
419 ∀ m : ℕ, 0 < m → m < N →
420 openSubgroupRightCoset H ((π (ι x)) ^ m) ≠ openSubgroupRightCoset H (1 : Q))
421 (hpow_ne : (ι x) ^ N ≠ 1) :
424 ∃ e : Fdata.carrier ≃ₜ*
425 ↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F),
426 (⟨(ι x) ^ N,
427 by
428 change π ((ι x) ^ N) ∈ (H : Subgroup Q)
429 have hmemQ : (π (ι x)) ^ N ∈ (H : Subgroup Q) :=
431 simpa [map_pow] using hmemQ
432 ⟩ :
433 ↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) ∈
434 Set.range (e ∘ Fdata.inclusion) ∧
435 Finite Fdata.basis := by
436 have hpow :
437 (ι x) ^ N ∈ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F) := by
438 change π ((ι x) ^ N) ∈ (H : Subgroup Q)
439 have hmemQ : (π (ι x)) ^ N ∈ (H : Subgroup Q) :=
441 simpa [map_pow] using hmemQ
442 have hmin :
443 ∀ m : ℕ, 0 < m → m < N →
444 (ι x) ^ m ∉ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F) := by
445 intro m hm hlt hmcomap
446 have hmemQ : (π (ι x)) ^ m ∈ (H : Subgroup Q) := by
447 change π ((ι x) ^ m) ∈ (H : Subgroup Q) at hmcomap
448 simpa [map_pow] using hmcomap
449 exact hcosetMin m hm hlt <|
451 simpa [hpow] using
453 (C := C) hForm hSub hIso hQuot hExt hF π hπcont H x hN hpow hpow_ne hmin
455/-- Right-coset formulation of the finite-rank exact theorem for preimages of open subgroups. -/
457 (C : ProCGroups.FiniteGroupClass.{u})
461 (hcyc :
462 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
463 C A ∧ IsCyclic A ∧ Nontrivial A)
464 {X : Type u} [Finite X]
465 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
466 {ι : X → F}
467 [DiscreteTopology (Set.range ι)]
470 {Q : Type u} [Group Q] [TopologicalSpace Q]
471 (π : F →* Q) (hπcont : Continuous π) (hπsurj : Function.Surjective π)
472 (H : OpenSubgroup Q) (x : X) {N : ℕ}
473 (hN : 0 < N)
474 (hcosetPow :
475 openSubgroupRightCoset H ((π (ι x)) ^ N) = openSubgroupRightCoset H (1 : Q))
476 (hcosetMin :
477 ∀ m : ℕ, 0 < m → m < N →
478 openSubgroupRightCoset H ((π (ι x)) ^ m) ≠ openSubgroupRightCoset H (1 : Q))
479 (hpow_ne : (ι x) ^ N ≠ 1) :
482 ∃ e : Fdata.carrier ≃ₜ*
483 ↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F),
484 (⟨(ι x) ^ N,
485 by
486 change π ((ι x) ^ N) ∈ (H : Subgroup Q)
487 have hmemQ : (π (ι x)) ^ N ∈ (H : Subgroup Q) :=
489 simpa [map_pow] using hmemQ
490 ⟩ :
491 ↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) ∈
492 Set.range (e ∘ Fdata.inclusion) ∧
493 Cardinal.mk Fdata.basis =
494 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (Q ⧸ (H : Subgroup Q))) :
495 Cardinal) := by
496 have hpow :
497 (ι x) ^ N ∈ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F) := by
498 change π ((ι x) ^ N) ∈ (H : Subgroup Q)
499 have hmemQ : (π (ι x)) ^ N ∈ (H : Subgroup Q) :=
501 simpa [map_pow] using hmemQ
502 have hmin :
503 ∀ m : ℕ, 0 < m → m < N →
504 (ι x) ^ m ∉ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F) := by
505 intro m hm hlt hmcomap
506 have hmemQ : (π (ι x)) ^ m ∈ (H : Subgroup Q) := by
507 change π ((ι x) ^ m) ∈ (H : Subgroup Q) at hmcomap
508 simpa [map_pow] using hmcomap
509 exact hcosetMin m hm hlt <|
511 simpa [hpow] using
513 (C := C) hVar hIso hExt hcyc hF π hπcont hπsurj H x hN hpow hpow_ne hmin
516end Profinite
517end ReidemeisterSchreier