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

Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.MinimalPower

1import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.BasisFiniteRank
3/-!
4# Pointed bases controlled by a minimal generator power
6If the first positive power of a distinguished generator entering an open
7subgroup is nontrivial, this module constructs a finite converging-set basis
8containing that power and refines the finite-rank Schreier basis theorem while
9retaining the distinguished basis element.
10-/
12open scoped Topology Pointwise
14namespace ReidemeisterSchreier
15namespace Profinite
17open ProCGroups
18open ProCGroups.FreeProC
19open ProCGroups.ProC
21universe u
24/--
25This is the pointed profinite Reidemeister--Schreier theorem over a converging-set basis, with a
26prescribed minimal generator power landing in the open subgroup.
27-/
28theorem exists_compactPointedBasis_openSubgroup_of_minGeneratorPower
29 (C : ProCGroups.FiniteGroupClass.{u})
34 {X : Type u}
35 [TopologicalSpace X] [DiscreteTopology 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) (x : X) {N : ℕ}
42 (hN : 0 < N)
43 (hpow : (ι x) ^ N ∈ (H : Subgroup F))
44 (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
45 ∃ κ : OpenSubgroupRightQuotient H × OnePoint X → ↥(H : Subgroup F),
46 Continuous κ ∧
47 (∀ q : OpenSubgroupRightQuotient H, κ (q, OnePoint.infty) = 1) ∧
48 κ (openSubgroupRightCoset H (1 : F), OnePoint.infty) = 1 ∧
49 (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈ Set.range κ ∧
50 IsCompact (Set.range κ) ∧
51 IsClosed (Set.range κ) ∧
52 IsEpimorphicallyPointedFreeProCGroupOn
53 (C := C)
54 (Set.range κ)
55 ⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
56 ⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
57 ↥(H : Subgroup F) Subtype.val := by
58 classical
59 let iInf : OnePoint X → F := fun z => z.elim 1 ι
60 have hιTendsto : Filter.Tendsto ι Filter.cofinite (𝓝 (1 : F)) := by
61 rw [Filter.tendsto_def]
62 intro s hs
63 rcases mem_nhds_iff.mp hs with ⟨W, hWs, hWopen, h1W⟩
65 (G := F) hWopen h1W with
66 ⟨U, hUW⟩
67 have hfinite : {x : X | ι x ∉ (U : Set F)}.Finite :=
68 hF.convergesToOneAlongOpenSubgroups U.toOpenSubgroup
69 have hcof : ∀ᶠ x : X in Filter.cofinite, ι x ∈ (U : Set F) :=
70 Filter.eventually_cofinite.2 hfinite
71 exact hcof.mono fun x hx => hWs (hUW hx)
72 have hPointed :
73 IsEpimorphicallyPointedFreeProCGroupOn
74 (C := C)
75 (OnePoint X) OnePoint.infty F iInf := by
76 refine ⟨hF.hasOpenNormalBasisInClass, ?_, by simp only [OnePoint.elim_infty, iInf], ?_, ?_⟩
77 · rw [OnePoint.continuous_iff_from_discrete]
78 simpa [iInf] using hιTendsto
79 · have hsub : Set.range ι ⊆ Set.range iInf := by
80 rintro y ⟨x, rfl⟩
81 exact ⟨(x : OnePoint X), rfl⟩
82 exact Generation.topologicallyGenerates_mono (G := F) hF.generates_range hsub
83 · intro G _ _ _ _ _ _ hG φ hφ hφ0 hgenφ
84 let ψ : X → G := fun x => φ x
85 have hψTendsto : Filter.Tendsto ψ Filter.cofinite (𝓝 (1 : G)) := by
86 have hraw := (OnePoint.continuous_iff_from_discrete (f := φ)).1 hφ
87 simpa [ψ, hφ0] using hraw
88 have hψconv : FamilyConvergesToOneAlongOpenSubgroups (G := G) ψ := by
89 intro U
90 exact Filter.eventually_cofinite.mp <|
91 hψTendsto (U.isOpen'.mem_nhds U.one_mem')
92 have hφrange : Set.range φ = Set.range ψ ∪ ({1} : Set G) := by
93 ext z
94 constructor
95 · rintro ⟨x, rfl⟩
96 refine OnePoint.rec ?_ ?_ x
97 · right
98 simpa [iInf] using hφ0
99 · intro y
100 left
101 exact ⟨y, rfl⟩
102 · intro hz
103 rcases hz with hz | hz
104 · rcases hz with ⟨y, rfl⟩
105 exact ⟨(y : OnePoint X), rfl⟩
106 · exact ⟨OnePoint.infty, hφ0.trans hz.symm⟩
107 have hψgen : Generation.TopologicallyGenerates (G := G) (Set.range ψ) := by
108 have hgenφ' :
109 Generation.TopologicallyGenerates (G := G) (Set.range ψ ∪ ({1} : Set G)) := by
110 simpa [hφrange] using hgenφ
111 exact (Generation.topologicallyGenerates_union_one_iff (G := G) (X := Set.range ψ)).1
112 hgenφ'
113 rcases hF.existsUnique_lift hG ψ hψconv hψgen with ⟨f, hf, huniq⟩
114 refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
115 · intro z
116 refine OnePoint.rec ?_ ?_ z
117 · calc
118 f (iInf OnePoint.infty) = f 1 := rfl
119 _ = 1 := map_one f
120 _ = φ OnePoint.infty := hφ0.symm
121 · intro y
122 exact hf.2 y
123 · intro g hg
124 apply huniq g
125 refine ⟨hg.1, ?_⟩
126 intro y
127 simpa [iInf, ψ] using hg.2 (y : OnePoint X)
128 let x' : OnePoint X := x
129 have hpow' : (iInf x') ^ N ∈ (H : Subgroup F) := by
130 simpa [iInf, x'] using hpow
131 have hmin' : ∀ m : ℕ, 0 < m → m < N → (iInf x') ^ m ∉ (H : Subgroup F) := by
132 intro m hm hlt
133 simpa [iInf, x'] using hmin m hm hlt
134 exact
135 exists_pointedFreeRightSchreierGeneratorFamily_of_openSubgroup_of_minimalGeneratorPower
136 (C := C) hForm hSub hIso hExt hPointed H x' hN hpow' hmin'
139/--
140Finite-rank pointed control over a converging-set free pro-\(C\) group: if \(x^N\) is the first
141positive power of a basis element landing in \(H\), and this power is nontrivial, the finite
142converging-set basis model for \(H\) can be chosen so that \(x^N\) lies in the basis image.
143-/
144theorem exists_finiteConvergingSetBasis_openSubgroup_of_minimalGeneratorPower
145 {C : ProCGroups.FiniteGroupClass.{u}}
150 {X : Type u} [Finite X]
151 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
152 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
153 {ι : X → F}
154 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
155 (C := C) X F ι)
156 (H : OpenSubgroup F) (x : X) {N : ℕ}
157 (hN : 0 < N)
158 (hpow : (ι x) ^ N ∈ (H : Subgroup F))
159 (hpow_ne : (ι x) ^ N ≠ 1)
160 (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
161 ∃ Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
162 (C := C),
163 ∃ e : Fdata.carrier ≃ₜ* ↥(H : Subgroup F),
164 (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈
165 Set.range (e ∘ Fdata.inclusion) ∧
166 Finite Fdata.basis := by
167 classical
168 letI : TopologicalSpace X := ⊥
169 letI : DiscreteTopology X := ⟨rfl⟩
170 letI : Fintype X := Fintype.ofFinite X
171 rcases
172 exists_compactPointedBasis_openSubgroup_of_minGeneratorPower
173 C hForm hSub hIso hExt hF H x hN hpow hmin with
174 ⟨κ, _hκcont, _hκbase, hκone, hxpowRange, _hκcompact, _hκclosed, hκfree⟩
175 letI : Finite (OpenSubgroupRightQuotient H) :=
176 finite_openSubgroupRightQuotient (F := F) H
177 letI : Finite (OnePoint X) := Finite.of_fintype (OnePoint X)
178 letI : Finite (Set.range κ) := (Set.finite_range κ).to_subtype
179 let x0 : Set.range κ :=
180 ⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
181 ⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
182 letI : DiscreteTopology (Set.range κ) :=
183 DiscreteTopology.of_finite_of_isClosed_singleton fun _ => isClosed_singleton
184 let B : Type u := {y : Set.range κ // y ≠ x0}
185 let μ : B → ↥(H : Subgroup F) := fun y => y.1.1
186 have hμfree :
187 IsEpimorphicallyFreeProCGroupOnConvergingSet
188 (C := C) B ↥(H : Subgroup F) μ := by
189 simpa [B, μ, x0] using
190 freeOnFinitePointedDiscreteSpace_has_convergingSetBasis
191 (C := C) hκfree
192 let Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData
193 (C := C) :=
194 { basis := B
195 carrier :=
196 ProCGrp.of C (ProfiniteGrp.of ↥(H : Subgroup F)) hμfree.hasOpenNormalBasisInClass
197 inclusion := μ
198 isEpimorphicallyFree := hμfree }
199 let ypow : Set.range κ := ⟨⟨(ι x) ^ N, hpow⟩, hxpowRange⟩
200 have hypow_ne_x0 : ypow ≠ x0 := by
201 intro hEq
202 apply hpow_ne
203 have hval : (ypow : ↥(H : Subgroup F)) = (x0 : ↥(H : Subgroup F)) :=
204 congrArg Subtype.val hEq
205 have hx0val : (x0 : ↥(H : Subgroup F)) = 1 := by
206 simpa [x0] using hκone
207 simpa [ypow] using hval.trans hx0val
208 let bpow : B := ⟨ypow, hypow_ne_x0⟩
209 have hbpow : μ bpow = (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) := rfl
210 refine ⟨Fdata, ContinuousMulEquiv.refl _, ?_, ?_⟩
211 · refine ⟨bpow, ?_⟩
212 change μ bpow = (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F))
213 exact hbpow
214 · dsimp [Fdata, B]
215 infer_instance
217/--
218Finite-rank pointed profinite Reidemeister--Schreier theorem: if \(x^N\) is the first positive
219power of the chosen ambient basis element landing in \(H\), and this power is nontrivial, then
220one can choose a finite-rank basis model of \(H\) whose basis image contains \(x^N\).
221-/
222theorem exists_basis_openSubgroup_of_extensionClosed_finiteRank_of_minimalGeneratorPower
223 (C : ProCGroups.FiniteGroupClass.{u})
227 (hcyc :
228 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
229 C A ∧ IsCyclic A ∧ Nontrivial A)
230 {X : Type u} [Finite X]
231 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
232 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
233 {ι : X → F}
234 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
235 (C := C) X F ι)
236 (H : OpenSubgroup F) (x : X) {N : ℕ}
237 (hN : 0 < N)
238 (hpow : (ι x) ^ N ∈ (H : Subgroup F))
239 (hpow_ne : (ι x) ^ N ≠ 1)
240 (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
241 ∃ Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
242 (C := C),
243 ∃ e : Fdata.carrier ≃ₜ* ↥(H : Subgroup F),
244 (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈
245 Set.range (e ∘ Fdata.inclusion) ∧
246 Cardinal.mk Fdata.basis =
247 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H :
248 Subgroup F))) :
249 Cardinal) := by
250 classical
251 rcases hVar.closureBundle_of_isomClosed_extensionClosed hIso hExt with
252 ⟨hForm, hSub, hIso', hQuot, hExt'⟩
253 rcases
254 exists_finiteConvergingSetBasis_openSubgroup_of_minimalGeneratorPower
255 (C := C) hForm hSub hIso' hExt' hF H x hN hpow hpow_ne hmin with
256 ⟨Fdata, eData, hxrange, hFin⟩
257 letI : Finite Fdata.basis := hFin
258 rcases exists_basis_openSubgroup_of_extensionClosed_finiteRank
259 (C := C) hVar hIso hExt hcyc hF H with
260 ⟨Fexact, hFexactEquiv, hExactCard⟩
261 have hFexactLt : Cardinal.mk Fexact.basis < Cardinal.aleph0 := by
262 calc
263 Cardinal.mk Fexact.basis =
264 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H :
265 Subgroup F))) :
266 Cardinal) := hExactCard
267 _ < Cardinal.aleph0 := Cardinal.natCast_lt_aleph0
268 letI : Finite Fexact.basis := Cardinal.lt_aleph0_iff_finite.mp hFexactLt
269 have hExactBasis :
270 Cardinal.mk Fexact.basis = Generation.topologicalRank Fexact.carrier :=
271 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fexact
272 have hDataBasis :
273 Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier :=
274 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fdata
275 rcases hFexactEquiv with ⟨eExact⟩
276 have hRankEq :
277 Generation.topologicalRank Fexact.carrier =
278 Generation.topologicalRank Fdata.carrier := by
279 exact Generation.topologicalRank_eq_of_continuousMulEquiv
280 (eExact.trans eData.symm)
281 have hCard :
282 Cardinal.mk Fdata.basis =
283 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H :
284 Subgroup F))) :
285 Cardinal) := by
286 calc
287 Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier := hDataBasis
288 _ = Generation.topologicalRank Fexact.carrier := hRankEq.symm
289 _ = Cardinal.mk Fexact.basis := hExactBasis.symm
290 _ = (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H :
291 Subgroup F))) :
292 Cardinal) := hExactCard
293 exact ⟨Fdata, eData, hxrange, hCard⟩
295end Profinite
296end ReidemeisterSchreier