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

Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.DenseFreeModel

1import ProCGroups.WreathProducts
2import ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis
3import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets
5/-!
6# Dense abstract free models of open subgroups
8This module transports right-coset sections across a dense free-group lift,
9proves that the preimage of an open subgroup remains dense, and applies the
10discrete Nielsen--Schreier basis theorem to compute the abstract preimage
11rank. The result feeds the later pro-\(C\) completion argument.
12-/
14open Set
15open scoped Topology Pointwise
17namespace ReidemeisterSchreier
18namespace Profinite
20open ProCGroups
21open ProCGroups.WreathProducts
22open ReidemeisterSchreier.Discrete.OpenSubgroups
24universe u v w
27section RightQuotientTransport
29open FreeGroup
31variable {F : Type u} [Group F]
32variable {P : Type v} [Group P]
33variable {Y : Type w}
35/-- The right relator map is compatible with comap of the open subgroup. -/
36theorem rightRel_map_of_comap
37 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
38 (K : Subgroup P) (hβ : π.comp βF = β)
39 {a b : FreeGroup Y}
40 (hab : QuotientGroup.rightRel (Subgroup.comap β K) a b) :
41 QuotientGroup.rightRel (Subgroup.comap π K) (βF a) (βF b) := by
42 have ha : π (βF a) = β a := by
43 simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f a) hβ
44 have hb : π (βF b) = β b := by
45 simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f b) hβ
46 rw [QuotientGroup.rightRel_apply] at hab ⊢
47 simpa [MonoidHom.map_mul, MonoidHom.map_inv, ha, hb] using hab
49/-- Transport right-coset classes along a homomorphism compatible with two subgroup preimages. -/
50noncomputable def mapRightQuotientOfComap :
51 (π : F →* P) → (βF : FreeGroup Y →* F) → (β : FreeGroup Y →* P) →
52 (K : Subgroup P) → (hβ : π.comp βF = β) →
53 Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) →
54 Quotient (QuotientGroup.rightRel (Subgroup.comap π K))
55 | π, βF, β, K, hβ =>
56 Quotient.map' βF (fun _a _b hab => rightRel_map_of_comap π βF β K hβ hab)
58/-- Surjectivity of the free-group map makes the induced map on right-quotient classes surjective. -/
59theorem surjective_mapRightQuotientOfComap
60 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
61 (K : Subgroup P) (hβ : π.comp βF = β)
62 (hβsurj : Function.Surjective β) :
63 Function.Surjective
64 (mapRightQuotientOfComap π βF β K hβ) := by
65 intro q
66 refine Quotient.inductionOn' q ?_
67 intro p
68 rcases hβsurj (π p) with ⟨w, hw⟩
69 refine ⟨Quotient.mk'' w, ?_⟩
70 change Quotient.mk'' (βF w) = Quotient.mk'' p
71 apply Quotient.sound'
72 have hw' : π (βF w) = π p := by
73 calc
74 π (βF w) = β w := by
75 simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f w) hβ
76 _ = π p := hw
77 rw [QuotientGroup.rightRel_apply]
78 simp only [Subgroup.comap, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk, mem_preimage,
79 MonoidHom.map_mul, MonoidHom.map_inv, hw', mul_inv_cancel, SetLike.mem_coe, one_mem]
81/-- The induced map on right-quotient classes is injective under the comap compatibility equation. -/
82theorem injective_mapRightQuotientOfComap
83 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
84 (K : Subgroup P) (hβ : π.comp βF = β) :
85 Function.Injective (mapRightQuotientOfComap π βF β K hβ) := by
86 intro a b hab
87 revert hab
88 refine Quotient.inductionOn₂' a b ?_
89 intro x y hxy
90 apply Quotient.sound'
91 have hrel :
92 QuotientGroup.rightRel (Subgroup.comap π K) (βF x) (βF y) := Quotient.exact' hxy
93 have hx : π (βF x) = β x := by
94 simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f x) hβ
95 have hy : π (βF y) = β y := by
96 simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f y) hβ
97 rw [QuotientGroup.rightRel_apply] at hrel ⊢
98 change π (βF y * (βF x)⁻¹) ∈ K at hrel
99 change β (y * x⁻¹) ∈ K
100 simpa [MonoidHom.map_mul, MonoidHom.map_inv, hx, hy] using hrel
102/--
103If \(\beta : \mathrm{FreeGroup}(Y) \to P\) is surjective and \(\beta = \pi \circ \beta_F\), then
104the right cosets of \(\beta^{-1}(K)\) are canonically identified with the right cosets of
105\(\pi^{-1}(K)\).
106-/
107noncomputable def rightQuotientEquivOfComap
108 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
109 (K : Subgroup P) (hβ : π.comp βF = β)
110 (hβsurj : Function.Surjective β) :
111 Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) ≃
112 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) :=
113 Equiv.ofBijective
114 (mapRightQuotientOfComap π βF β K hβ)
115 ⟨injective_mapRightQuotientOfComap π βF β K hβ,
116 surjective_mapRightQuotientOfComap π βF β K hβ hβsurj⟩
118/-- The right-quotient comparison induced by comap is an equivalence. -/
119@[simp] theorem rightQuotientEquivOfComap_mk
120 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
121 (K : Subgroup P) (hβ : π.comp βF = β)
122 (hβsurj : Function.Surjective β) (w : FreeGroup Y) :
123 rightQuotientEquivOfComap π βF β K hβ hβsurj
124 (Quotient.mk'' w) =
125 Quotient.mk'' (βF w) := by
126 simp only [rightQuotientEquivOfComap, mapRightQuotientOfComap, Equiv.ofBijective_apply,
127 Quotient.map'_mk'']
129section SchreierSections
131variable [DecidableEq Y]
132variable {T : Set (FreeGroup Y)}
134/--
135Transport a discrete Schreier transversal for \(\beta^{-1}(K)\) to a right-coset section for
136\(\pi^{-1}(K)\) in the ambient group \(F\).
137-/
138noncomputable def rightSchreierSectionOfComap
139 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
140 (K : Subgroup P) (hβ : π.comp βF = β)
141 (hβsurj : Function.Surjective β)
142 (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T) :
143 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) → F :=
144 fun q =>
145 βF <|
146 rightTransversalSection (H := Subgroup.comap β K) hT.1
147 ((rightQuotientEquivOfComap π βF β K hβ hβsurj).symm q)
149/-- The transported right Schreier section satisfies its defining specification. -/
150@[simp 900] theorem rightSchreierSectionOfComap_spec
151 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
152 (K : Subgroup P) (hβ : π.comp βF = β)
153 (hβsurj : Function.Surjective β)
154 (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T)
155 (q : Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) :
156 Quotient.mk'' (rightSchreierSectionOfComap π βF β K hβ hβsurj hT q) = q := by
157 let e := rightQuotientEquivOfComap π βF β K hβ hβsurj
158 let τT := rightTransversalSection (H := Subgroup.comap β K) hT.1
159 calc
160 Quotient.mk'' (rightSchreierSectionOfComap π βF β K hβ hβsurj hT q)
161 = e (Quotient.mk'' (τT (e.symm q))) := by
162 simpa [rightSchreierSectionOfComap, e, τT] using
163 (rightQuotientEquivOfComap_mk π βF β K hβ hβsurj (τT (e.symm q))).symm
164 _ = e (e.symm q) := by
165 rw [rightTransversalSection_spec (H := Subgroup.comap β K) hT.1]
166 _ = q := e.apply_symm_apply q
168/--
169On a coset represented by an element of the chosen Schreier transversal, the transported section
170returns the image of that representative.
171-/
172@[simp 900] theorem rightSchreierSectionOfComap_eq_of_mem
173 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
174 (K : Subgroup P) (hβ : π.comp βF = β)
175 (hβsurj : Function.Surjective β)
176 (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T)
177 {t : FreeGroup Y} (ht : t ∈ T) :
178 rightSchreierSectionOfComap π βF β K hβ hβsurj hT
179 (Quotient.mk'' (βF t)) =
180 βF t := by
181 let e := rightQuotientEquivOfComap π βF β K hβ hβsurj
182 have heq :
183 e.symm (Quotient.mk'' (βF t)) = Quotient.mk'' t := by
184 apply e.injective
185 simp only [Equiv.apply_symm_apply, rightQuotientEquivOfComap_mk, e]
186 have hsec :
187 rightTransversalSection (H := Subgroup.comap β K) hT.1
188 (Quotient.mk'' t) = t := by
189 have hsub :
190 hT.1.rightQuotientEquiv (Quotient.mk'' t) = ⟨t, ht⟩ := by
191 have hq :
192 Quotient.mk'' t = hT.1.rightQuotientEquiv.symm ⟨t, ht⟩ := by
193 simpa using
194 hT.1.mk''_rightQuotientEquiv (hT.1.rightQuotientEquiv.symm ⟨t, ht⟩)
195 apply hT.1.rightQuotientEquiv.symm.injective
196 simpa using hq
197 simpa [rightTransversalSection] using congrArg Subtype.val hsub
198 rw [rightSchreierSectionOfComap, heq, hsec]
200/-- The transported Schreier section is normalized at the trivial right coset. -/
201@[simp 900] theorem rightSchreierSectionOfComap_one
202 (π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
203 (K : Subgroup P) (hβ : π.comp βF = β)
204 (hβsurj : Function.Surjective β)
205 (hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T) :
206 rightSchreierSectionOfComap π βF β K hβ hβsurj hT
207 (Quotient.mk'' (1 : F)) =
208 1 := by
209 have hβFone : βF (1 : FreeGroup Y) = 1 := by simp only [map_one]
210 rw [← hβFone]
211 exact rightSchreierSectionOfComap_eq_of_mem π βF β K hβ hβsurj hT hT.2.1
213end SchreierSections
215end RightQuotientTransport
217section DenseAbstractFreeModel
219open FreeGroup
221variable {X : Type u}
222variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
223variable {ι : X → F}
225/-- The abstract free-group lift of a topologically generating family has dense range. -/
226theorem denseRange_freeGroupLift_of_topologicallyGenerates
227 (hgen : ProCGroups.Generation.TopologicallyGenerates (G := F) (Set.range ι)) :
228 DenseRange (FreeGroup.lift ι : FreeGroup X →* F) := by
229 let φ : FreeGroup X →* F := FreeGroup.lift ι
230 have hsub : Set.range ι ⊆ (φ.range : Set F) := by
231 rintro _ ⟨x, rfl⟩
232 exact ⟨FreeGroup.of x, by simp only [FreeGroup.lift_apply_of, φ]⟩
233 have hφgen :
234 ProCGroups.Generation.TopologicallyGenerates (G := F) (φ.range : Set F) :=
236 have hdense : Dense ((φ.range : Subgroup F) : Set F) := by
237 rw [← Subgroup.closure_eq φ.range]
239 (G := F) (X := (φ.range : Set F))).1 hφgen
240 simpa [DenseRange, MonoidHom.coe_range] using hdense
242/--
243A dense abstract free-group lift topologically generates through the images of the free
244generators.
245-/
246theorem topologicallyGenerates_range_of_denseAbstractFreeLift
247 {Y : Type u}
248 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
249 {φ : FreeGroup Y →* H}
250 (hφ : DenseRange φ) :
252 (G := H) (Set.range fun y : Y => φ (FreeGroup.of y)) := by
253 let j : Y → H := fun y => φ (FreeGroup.of y)
254 have himage :
255 φ '' Set.range (FreeGroup.of : Y → FreeGroup Y) = Set.range j := by
256 ext h
257 constructor
258 · rintro ⟨_, ⟨y, rfl⟩, rfl⟩
259 exact ⟨y, rfl⟩
260 · rintro ⟨y, rfl⟩
261 exact ⟨FreeGroup.of y, ⟨y, rfl⟩, rfl⟩
262 have hclosure :
263 Subgroup.closure (Set.range j) = φ.range := by
264 calc
265 Subgroup.closure (Set.range j)
266 = Subgroup.map φ (Subgroup.closure (Set.range (FreeGroup.of : Y → FreeGroup Y))) := by
267 simpa [himage] using
268 (φ.map_closure (Set.range (FreeGroup.of : Y → FreeGroup Y))).symm
269 _ = φ.range := by
270 rw [FreeGroup.closure_range_of Y, MonoidHom.range_eq_map]
272 rw [SetLike.ext'_iff, Subgroup.topologicalClosure_coe, Subgroup.coe_top]
273 simpa [DenseRange, MonoidHom.coe_range, dense_iff_closure_eq] using hφ
275/--
276Restricting a dense homomorphism to the preimage of an open subgroup still has dense range in
277that subgroup.
278-/
279theorem denseRange_comapMap_of_openSubgroup
280 {G : Type u} [Group G]
281 {H : Type u} [Group H] [TopologicalSpace H]
282 {φ : G →* H} (hφ : DenseRange φ)
283 {U : Subgroup H} (hU : IsOpen (U : Set H)) :
284 DenseRange
285 ({ toFun := fun g : Subgroup.comap φ U => ⟨φ g.1, g.2⟩
286 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
287 map_mul' := by
288 intro a b
289 ext
290 simp only [Subgroup.coe_mul, map_mul]} : Subgroup.comap φ U →* U) := by
291 let ψ : Subgroup.comap φ U →* U :=
292 { toFun := fun g => ⟨φ g.1, g.2⟩
293 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
294 map_mul' := by
295 intro a b
296 ext
297 simp only [Subgroup.coe_mul, map_mul]}
298 have hdense : Dense (Set.range φ) := by
299 simpa [DenseRange] using hφ
300 have himage :
301 ((↑) : U → H) '' Set.range ψ = (U : Set H) ∩ Set.range φ := by
302 ext h
303 constructor
304 · rintro ⟨_, hu, rfl⟩
305 rcases hu with ⟨g, rfl⟩
306 exact ⟨g.2, ⟨g.1, rfl⟩⟩
307 · rintro ⟨hu, g, rfl⟩
308 exact ⟨⟨φ g, hu⟩, ⟨⟨g, hu⟩, rfl⟩, rfl⟩
309 have hsubset :
310 (U : Set H) ⊆ closure (((↑) : U → H) '' Set.range ψ) := by
311 rw [himage]
312 simpa [Set.inter_comm] using hdense.open_subset_closure_inter hU
313 have hDenseU : Dense (Set.range ψ : Set U) := by
314 exact (Subtype.dense_iff).2 hsubset
315 change Dense (Set.range ψ)
316 exact hDenseU
318section FiniteTargets
320variable {P : Type u} [Group P] [TopologicalSpace P] [DiscreteTopology P] [Finite P]
322omit [TopologicalSpace F] [IsTopologicalGroup F] [Finite P] in
323/-- A homomorphism into a finite discrete group is surjective as soon as it has dense range. -/
324theorem surjective_of_denseRange
325 {φ : F →* P} (hφ : DenseRange φ) :
326 Function.Surjective φ := by
327 have hclosed : IsClosed (Set.range φ) := isClosed_discrete _
328 have hclosure : closure (Set.range φ) = Set.univ := hφ.closure_range
329 have hrange : Set.range φ = Set.univ := by
330 rw [← hclosure]
331 exact (closure_eq_iff_isClosed.mpr hclosed).symm
332 intro p
333 have hp : p ∈ Set.range φ := by
334 simp only [hrange, mem_univ]
335 exact hp
337end FiniteTargets
339/--
340The abstract subgroup of \(\mathrm{FreeGroup}(X)\) lying over an open subgroup of a compact
341group via the dense free-group lift has the corresponding Schreier-transformed rank.
342-/
343theorem exists_freeBasis_comap_freeGroupLift_of_openSubgroup_of_rankTransform
344 {X : Type u} [Finite X]
345 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
346 {ι : X → F}
347 (hgen : ProCGroups.Generation.TopologicallyGenerates (G := F) (Set.range ι))
348 (H : OpenSubgroup F) :
349 ∃ Y : Type u,
350 Nonempty (FreeGroupBasis Y (Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F))) ∧
351 Nat.card Y = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F
352 ⧸ (H : Subgroup F))) := by
353 classical
354 let βF : FreeGroup X →* F := FreeGroup.lift ι
355 let L : Subgroup (FreeGroup X) := Subgroup.comap βF (H : Subgroup F)
356 let nQ : ℕ := Nat.card (F ⧸ (H : Subgroup F))
357 let P := openSubgroupIndexActionRange (G := F) H
358 (show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl)
359 let ρ : F →ₜ* P :=
360 openSubgroupIndexActionRangeContinuousHom (G := F) H
361 (show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl)
362 let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
363 let K : Subgroup P := MulAction.stabilizer P q0
364 let β : FreeGroup X →* P := ρ.toMonoidHom.comp βF
365 letI : TopologicalSpace (FreeGroup X) := ⊥
366 letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
367 letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
368 have hcomap : Subgroup.comap ρ.toMonoidHom K = (H : Subgroup F) := by
369 ext g
370 constructor
371 · intro hg
372 change ρ g • q0 = q0 at hg
373 rw [openSubgroupIndexActionRangeContinuousHom_smul_basepoint (G := F) H
374 (show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl) g] at hg
375 change (QuotientGroup.mk (s := (H : Subgroup F)) g : F ⧸ (H : Subgroup F)) =
376 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) at hg
377 simpa [QuotientGroup.eq] using hg
378 · intro hg
379 change ρ g • q0 = q0
380 exact openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem
381 (G := F) H (show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl) hg
382 have hβFdense : DenseRange βF :=
383 denseRange_freeGroupLift_of_topologicallyGenerates (F := F) (X := X) hgen
384 have hρsurj : Function.Surjective ρ := by
385 intro p
386 rcases p.down.2 with ⟨g, hg⟩
387 refine ⟨g, ?_⟩
388 apply ULift.ext
389 apply Subtype.ext
390 exact hg
391 have hβdense : DenseRange β := by
392 simpa [β, MonoidHom.comp_apply] using
393 (Function.Surjective.denseRange hρsurj).comp hβFdense ρ.continuous_toFun
394 have hβsurj : Function.Surjective β :=
395 surjective_of_denseRange (F := FreeGroup X) (P := P) hβdense
396 let H0 : Subgroup F := Subgroup.comap ρ.toMonoidHom K
397 have hH0 : H0 = (H : Subgroup F) := by
398 simpa [H0] using hcomap
399 let eQ :
400 Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) ≃
401 Quotient (QuotientGroup.rightRel H0) :=
402 rightQuotientEquivOfComap ρ.toMonoidHom βF β K rfl hβsurj
403 have hcomapL : Subgroup.comap β K = L := by
404 ext w
405 change β w ∈ K ↔ βF w ∈ (H : Subgroup F)
406 change βF w ∈ Subgroup.comap ρ.toMonoidHom K ↔ βF w ∈ (H : Subgroup F)
407 rw [hcomap]
408 let eQ0 :
409 Quotient (QuotientGroup.rightRel L) ≃
410 Quotient (QuotientGroup.rightRel H0) := by
411 simpa [hcomapL] using eQ
412 letI : Finite (F ⧸ (H : Subgroup F)) :=
414 letI : Finite (Quotient (QuotientGroup.rightRel (H : Subgroup F))) := by
415 exact
416 Finite.of_equiv (F ⧸ (H : Subgroup F))
417 (QuotientGroup.quotientRightRelEquivQuotientLeftRel (H : Subgroup F)).symm
418 have hRightEq :
419 Quotient (QuotientGroup.rightRel (H : Subgroup F)) =
420 Quotient (QuotientGroup.rightRel H0) := by
421 simpa using
422 congrArg (fun S : Subgroup F => Quotient (QuotientGroup.rightRel S)) hH0.symm
423 letI : Finite (Quotient (QuotientGroup.rightRel H0)) := by
424 exact Eq.ndrec
425 (motive := fun T => Finite T)
426 (inferInstance : Finite (Quotient (QuotientGroup.rightRel (H : Subgroup F))))
427 hRightEq
428 letI : Finite (Quotient (QuotientGroup.rightRel L)) :=
429 Finite.of_equiv
430 (Quotient (QuotientGroup.rightRel H0)) eQ0.symm
431 letI : Finite (FreeGroup X ⧸ L) :=
432 Finite.of_equiv
433 (Quotient (QuotientGroup.rightRel L))
434 (QuotientGroup.quotientRightRelEquivQuotientLeftRel L)
435 have hquotCard :
436 Nat.card (FreeGroup X ⧸ L) = Nat.card (F ⧸ (H : Subgroup F)) := by
437 calc
438 Nat.card (FreeGroup X ⧸ L)
439 = Nat.card (Quotient (QuotientGroup.rightRel L)) :=
440 Nat.card_congr (QuotientGroup.quotientRightRelEquivQuotientLeftRel L).symm
441 _ = Nat.card (Quotient (QuotientGroup.rightRel H0)) :=
442 Nat.card_congr eQ0
443 _ = Nat.card (Quotient (QuotientGroup.rightRel (H : Subgroup F))) := by
444 simpa using congrArg Nat.card hRightEq.symm
445 _ = Nat.card (F ⧸ (H : Subgroup F)) :=
446 Nat.card_congr (QuotientGroup.quotientRightRelEquivQuotientLeftRel (H : Subgroup F))
447 obtain ⟨Y, hYfree, hYcard⟩ :=
448 exists_freeBasis_subgroupOfFreeGroup_of_rankTransform (X := X) (L := L)
449 refine ⟨Y, hYfree, ?_⟩
450 simpa [hquotCard] using hYcard
452end DenseAbstractFreeModel
454end Profinite
455end ReidemeisterSchreier