ReidemeisterSchreier/Discrete/OpenSubgroups/FreeBasis.lean
1import ReidemeisterSchreier.Discrete.OpenSubgroups.PrefixTree
2import ReidemeisterSchreier.Quiver
3import ReidemeisterSchreier.Schreier
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ReidemeisterSchreier/Discrete/OpenSubgroups/FreeBasis.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Schreier bases for open subgroups of free groups
16Constructs Schreier bases from right Schreier transversals using prefix trees, complement edges,
17and nontrivial Schreier pairs as the preferred basis index.
18-/
20namespace ReidemeisterSchreier.Discrete.OpenSubgroups
23/-- The total generator arrows in the action groupoid attached to a chosen free basis are indexed
24by a pair consisting of a vertex and a basis element. -/
25noncomputable def FreeGroupBasis.actionGroupoidGeneratorTotalEquiv
26 {ι G A : Type u} [Group G] [MulAction G A] (b : FreeGroupBasis ι G) :
27 letI : IsFreeGroupoid (CategoryTheory.ActionCategory G A) :=
28 FreeGroupBasis.actionGroupoidIsFree b
29 Quiver.Total (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory G A)) ≃ A × ι := by
30 letI : IsFreeGroupoid (CategoryTheory.ActionCategory G A) :=
31 FreeGroupBasis.actionGroupoidIsFree b
32 refine
33 { toFun := fun e => (e.left.back, e.hom.1)
34 invFun := fun ai =>
35 { left := show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory G A) from
36 ((ai.1 : A) : CategoryTheory.ActionCategory G A)
37 right := show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory G A) from
38 ((b ai.2 • ai.1 : A) : CategoryTheory.ActionCategory G A)
39 hom := ⟨ai.2, rfl⟩ }
40 left_inv := ?_
41 right_inv := ?_ }
42 · intro e
43 cases e with
45 cases left with
47 cases right with
49 cases hom with
51 dsimp
52 cases hi
53 rfl
54 · intro ai
55 rfl
57/-- Complement edges of the symmetrized Schreier prefix tree. These are the canonical indexing
58objects for the Schreier free basis. -/
59noncomputable abbrev schreierComplementEdges
60 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
61 (hT : IsRightSchreierTransversal (X := X) L T) : Type u := by
62 letI := schreierTransversalRightCosetAction (X := X) hT
63 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
64 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
65 exact
66 ↥(((Quiver.wideSubquiverEquivSetTotal <|
67 Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT))ᶜ :
68 Set (Quiver.Total
69 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)))))
71/-- The Schreier basis indexed by complement edges of the prefix tree. -/
72noncomputable def schreierComplementEdgesBasis
73 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
74 (hT : IsRightSchreierTransversal (X := X) L T) :
75 FreeGroupBasis (schreierComplementEdges (X := X) hT) L := by
76 letI := schreierTransversalRightCosetAction (X := X) hT
77 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
78 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
79 exact
80 (IsFreeGroupoid.SpanningTree.endBasis (schreierPrefixTree (X := X) hT)).map
81 (schreierRootEndMulEquiv (X := X) hT)
83/-- Auxiliary bridge from nontrivial Schreier pairs to the classical Schreier generator value set. -/
84private noncomputable def nontrivialSchreierPairsEquivSchreierGeneratorSet
85 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
86 (hT : IsRightSchreierTransversal (X := X) L T) :
87 NontrivialSchreierPair (X := X) hT ≃ ↥(schreierGeneratorSet (X := X) hT) := by
88 classical
89 letI := schreierTransversalRightCosetAction (X := X) hT
90 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
91 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
92 let C :
93 Set (Quiver.Total
94 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))) :=
95 ((Quiver.wideSubquiverEquivSetTotal <|
96 Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT))ᶜ : Set _)
97 let toSch : ↑C → ↥(schreierGeneratorSet (X := X) hT) := fun i =>
98 ⟨schreierGenerator (X := X) hT (((i.1.left.back : T) : FreeGroup X)) i.1.hom.1,
99 by
100 refine ⟨
102 i.1.hom.1, rfl, ?_⟩
103 intro hgen
104 exact i.2 (show i.1 ∈ Quiver.wideSubquiverEquivSetTotal
105 (Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)) from
106 schreierGenerator_eq_one_implies_mem_prefixTree (X := X) hT i.1.hom hgen)⟩
107 let b : FreeGroupBasis ↑C L :=
108 (IsFreeGroupoid.SpanningTree.endBasis (schreierPrefixTree (X := X) hT)).map
109 (schreierRootEndMulEquiv (X := X) hT)
110 have hval : ∀ i : ↑C, (b i : L) = (((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) := by
111 intro i
112 rw [FreeGroupBasis.map_apply, IsFreeGroupoid.SpanningTree.endBasis_apply]
113 have htree : ∀ {a b : IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)}
114 (e : a ⟶ b),
115 e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b →
116 (schreierLabelFunctor (X := X) hT).map (IsFreeGroupoid.of e) = (1 : L) := by
117 intro a b e he
118 exact schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he
119 have hloop := IsFreeGroupoid.SpanningTree.map_loopOfHom_eq_map
120 (T := schreierPrefixTree (X := X) hT)
121 (F := schreierLabelFunctor (X := X) hT)
122 (hTree := by
123 intro a b e he
124 exact htree e he)
125 (q := IsFreeGroupoid.of i.1.hom)
126 let loop := IsFreeGroupoid.SpanningTree.loopOfHom (schreierPrefixTree (X := X) hT)
127 (IsFreeGroupoid.of i.1.hom)
128 have hrootEq : (schreierRootEndMulEquiv (X := X) hT loop : L) =
129 (schreierLabelFunctor (X := X) hT).map loop := by
130 apply Subtype.ext
131 change loop.1 = (1 : FreeGroup X) * loop.1 * (1 : FreeGroup X)⁻¹
132 simp only [CategoryTheory.actionAsFunctor_obj, CategoryTheory.actionAsFunctor_map, one_mul, inv_one, mul_one]
133 exact hrootEq.trans <| hloop.trans <| schreierLabelFunctor_map_of (X := X) hT i.1.hom
134 have hto_inj : Function.Injective toSch := by
135 intro i j hij
136 apply b.injective
137 have hz : ((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L) =
138 ((toSch j : ↥(schreierGeneratorSet (X := X) hT)) : L) := congrArg Subtype.val hij
139 have hz_inv : (((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) =
140 (((toSch j : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) := congrArg Inv.inv hz
141 exact (hval i).trans (hz_inv.trans (hval j).symm)
142 have hto_surj : Function.Surjective toSch := by
143 intro z
144 rcases z.2 with ⟨t, ht, x, hz, hne⟩
145 let a : CategoryTheory.ActionCategory (FreeGroup X) T :=
146 ((⟨t, ht⟩ : T) : CategoryTheory.ActionCategory (FreeGroup X) T)
147 let b0 : CategoryTheory.ActionCategory (FreeGroup X) T :=
148 (schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T)
149 let e :
150 ((show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from a) ⟶
151 b0) :=
152 ⟨x, by
153 rw [FreeGroup.inverseBasis_apply]
154 change (FreeGroup.of x)⁻¹ • (show T from CategoryTheory.ActionCategory.back a) =
155 (show T from CategoryTheory.ActionCategory.back b0)
156 simpa [a, b0] using
157 (schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ (⟨t, ht⟩ : T))⟩
158 have he_not : ⟨a, b0, e⟩ ∈ C := by
159 change ¬ e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b0
160 intro he
161 have hgen1_inv :
162 (schreierGenerator (X := X) hT
163 ((show T from CategoryTheory.ActionCategory.back a) : FreeGroup X) e.1)⁻¹ = 1 := by
164 have htreeLabel :=
165 schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he
166 rw [schreierLabelFunctor_map_of (X := X) hT e] at htreeLabel
167 exact htreeLabel
168 have hgen1 :
169 schreierGenerator (X := X) hT
170 ((show T from CategoryTheory.ActionCategory.back a) : FreeGroup X) e.1 = 1 :=
171 inv_eq_one.mp hgen1_inv
172 exact hne (by simpa [a, e, hz] using hgen1)
173 refine ⟨⟨⟨a, b0, e⟩, he_not⟩, ?_⟩
174 apply Subtype.ext
175 simpa [toSch, a, e] using hz.symm
176 let eC : ↑C ≃ ↥(schreierGeneratorSet (X := X) hT) := Equiv.ofBijective toSch ⟨hto_inj, hto_surj⟩
177 let ePair :
178 ↑C ≃ NontrivialSchreierPair (X := X) hT := by
179 let eTotal :
180 Quiver.Total (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)) ≃
181 T × X :=
182 FreeGroupBasis.actionGroupoidGeneratorTotalEquiv (FreeGroup.inverseBasis X)
183 refine
184 { toFun := fun i =>
185 ⟨eTotal i.1, by
186 intro hgen
187 have hgen' :
188 schreierGenerator (X := X) hT
189 (((show T from CategoryTheory.ActionCategory.back i.1.left) : T) : FreeGroup X)
190 i.1.hom.1 = 1 := by
191 simpa [eTotal] using hgen
192 exact i.2 (show i.1 ∈ Quiver.wideSubquiverEquivSetTotal
193 (Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)) from
194 schreierGenerator_eq_one_implies_mem_prefixTree (X := X) hT i.1.hom hgen')⟩
195 invFun := fun p =>
196 let e := eTotal.symm p.1
197 ⟨e, by
198 intro he
199 have htreeLabel :=
200 schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e.hom
201 (show e.hom ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)
202 e.left e.right from he)
203 rw [schreierLabelFunctor_map_of (X := X) hT e.hom] at htreeLabel
204 have hgen' :
205 schreierGenerator (X := X) hT
206 (((show T from CategoryTheory.ActionCategory.back e.left) : T) : FreeGroup X)
207 e.hom.1 = 1 := inv_eq_one.mp htreeLabel
208 exact p.2 (by simpa [eTotal] using hgen')⟩
209 left_inv := by
210 intro i
211 apply Subtype.ext
212 simp only [Equiv.symm_apply_apply, eTotal]
213 right_inv := by
214 intro p
215 apply Subtype.ext
216 simp only [ne_eq, Equiv.apply_symm_apply, eTotal]}
217 exact ePair.symm.trans eC
219/-- Complement edges are equivalent to nontrivial Schreier pairs. -/
220noncomputable def schreierComplementEdgesEquivNontrivialPairs
221 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
222 (hT : IsRightSchreierTransversal (X := X) L T) :
223 schreierComplementEdges (X := X) hT ≃ NontrivialSchreierPair (X := X) hT := by
224 classical
225 letI := schreierTransversalRightCosetAction (X := X) hT
226 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
227 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
228 let C :
229 Set (Quiver.Total
230 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))) :=
231 ((Quiver.wideSubquiverEquivSetTotal <|
232 Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT))ᶜ : Set _)
233 change ↑C ≃ NontrivialSchreierPair (X := X) hT
234 let eTotal :
235 Quiver.Total (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)) ≃
236 T × X :=
237 FreeGroupBasis.actionGroupoidGeneratorTotalEquiv (FreeGroup.inverseBasis X)
238 refine
239 { toFun := fun i =>
240 ⟨eTotal i.1, by
241 intro hgen
242 have hgen' :
243 schreierGenerator (X := X) hT
244 (((show T from CategoryTheory.ActionCategory.back i.1.left) : T) : FreeGroup X)
245 i.1.hom.1 = 1 := by
246 simpa [eTotal] using hgen
247 exact i.2 (show i.1 ∈ Quiver.wideSubquiverEquivSetTotal
248 (Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)) from
249 (schreierGenerator_eq_one_iff_mem_prefixTree (X := X) hT i.1.hom).1 hgen')⟩
250 invFun := fun p =>
251 let e := eTotal.symm p.1
252 ⟨e, by
253 intro he
254 have hgen' :
255 schreierGenerator (X := X) hT
256 (((show T from CategoryTheory.ActionCategory.back e.left) : T) : FreeGroup X)
257 e.hom.1 = 1 :=
258 (schreierGenerator_eq_one_iff_mem_prefixTree (X := X) hT e.hom).2
259 (show e.hom ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)
260 e.left e.right from he)
261 exact p.2 (by simpa [eTotal] using hgen')⟩
262 left_inv := by
263 intro i
264 apply Subtype.ext
265 simp only [Equiv.symm_apply_apply, eTotal]
266 right_inv := by
267 intro p
268 apply Subtype.ext
269 simp only [ne_eq, Equiv.apply_symm_apply, eTotal]}
271/-- The Schreier free basis indexed by nontrivial Schreier pairs. This is the preferred
272Schreier-basis API; the classical value-set basis is a reindexing of this one. -/
273noncomputable def nontrivialSchreierPairBasis
274 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
275 (hT : IsRightSchreierTransversal (X := X) L T) :
276 FreeGroupBasis (NontrivialSchreierPair (X := X) hT) L :=
277 (schreierComplementEdgesBasis (X := X) hT).reindex
278 (schreierComplementEdgesEquivNontrivialPairs (X := X) hT)
280/-- The free group equivalence obtained directly from the preferred pair-indexed Schreier basis. -/
281noncomputable def nontrivialSchreierPairBasisEquiv
282 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
283 (hT : IsRightSchreierTransversal (X := X) L T) :
284 FreeGroup (NontrivialSchreierPair (X := X) hT) ≃* L :=
285 (nontrivialSchreierPairBasis (X := X) hT).repr.symm
287/-- The preferred pair-indexed basis equivalence sends each free generator to its Schreier
288basis element. -/
289@[simp] theorem nontrivialSchreierPairBasisEquiv_of
290 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
291 (hT : IsRightSchreierTransversal (X := X) L T)
292 (p : NontrivialSchreierPair (X := X) hT) :
293 nontrivialSchreierPairBasisEquiv (X := X) hT (FreeGroup.of p) =
294 nontrivialSchreierPairBasis (X := X) hT p := by
295 apply (nontrivialSchreierPairBasis (X := X) hT).repr.injective
296 calc
297 (nontrivialSchreierPairBasis (X := X) hT).repr
298 (nontrivialSchreierPairBasisEquiv (X := X) hT (FreeGroup.of p))
299 = FreeGroup.of p := by simp only [nontrivialSchreierPairBasisEquiv, MulEquiv.apply_symm_apply]
300 _ = (nontrivialSchreierPairBasis (X := X) hT).repr
301 (nontrivialSchreierPairBasis (X := X) hT p) :=
302 (FreeGroupBasis.repr_apply_coe (nontrivialSchreierPairBasis (X := X) hT) p).symm
304private theorem nontrivialSchreierPairsEquivSchreierGeneratorSet_apply
305 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
306 (hT : IsRightSchreierTransversal (X := X) L T)
307 (p : NontrivialSchreierPair (X := X) hT) :
308 ((nontrivialSchreierPairsEquivSchreierGeneratorSet (X := X) hT p :
309 ↥(schreierGeneratorSet (X := X) hT)) : L) =
310 schreierGenerator (X := X) hT ((p.1.1 : T) : FreeGroup X) p.1.2 := by
311 rfl
313/-- The Schreier-generator map is injective on nontrivial Schreier pairs. -/
315 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
316 (hT : IsRightSchreierTransversal (X := X) L T) :
317 Function.Injective
318 (nontrivialSchreierPairGenerator (X := X) hT) := by
319 intro p q hpq
320 apply (nontrivialSchreierPairsEquivSchreierGeneratorSet (X := X) hT).injective
321 apply Subtype.ext
323 nontrivialSchreierPairGenerator] using hpq
325/-- A right Schreier transversal has cardinality equal to the corresponding right-coset index. -/
327 {X : Type u} [DecidableEq X]
328 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
329 [Finite (Quotient (QuotientGroup.rightRel L))]
330 (hT : IsRightSchreierTransversal (X := X) L T) :
331 Nat.card T = Nat.card (Quotient (QuotientGroup.rightRel L)) := by
332 exact Nat.card_congr hT.1.rightQuotientEquiv.symm
334/-- Direct combinatorial count of complement edges in the Schreier prefix tree:
335all labelled edges minus tree edges. -/
337 {X : Type u} [DecidableEq X] [Finite X]
338 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
339 [Finite T]
340 (hT : IsRightSchreierTransversal (X := X) L T) :
341 Nat.card (schreierComplementEdges (X := X) hT) =
342 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T) := by
343 classical
344 letI := schreierTransversalRightCosetAction (X := X) hT
345 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
346 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
347 let Ttree :
348 WideSubquiver
349 (Quiver.Symmetrify
350 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))) :=
351 schreierPrefixTree (X := X) hT
352 letI : Quiver.Arborescence Ttree := by
353 dsimp [Ttree]
354 infer_instance
355 let totalGen :=
356 Quiver.Total (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))
357 let covered : Set totalGen :=
358 Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify Ttree)
359 let rootT : T := ⟨(1 : FreeGroup X), hT.2.1⟩
360 let root : CategoryTheory.ActionCategory (FreeGroup X) T :=
361 CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T rootT
362 letI : Fintype X := Fintype.ofFinite X
363 letI : Fintype T := Fintype.ofFinite T
364 haveI : Finite (CategoryTheory.ActionCategory (FreeGroup X) T) :=
365 Finite.of_equiv T (CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T)
366 haveI : Finite Ttree :=
367 Finite.of_equiv (CategoryTheory.ActionCategory (FreeGroup X) T)
368 (show _ ≃ Ttree from Equiv.refl _)
369 haveI : Finite totalGen :=
370 Finite.of_equiv (T × X)
371 (FreeGroupBasis.actionGroupoidGeneratorTotalEquiv (FreeGroup.inverseBasis X)).symm
372 letI : Fintype totalGen := Fintype.ofFinite totalGen
373 letI : Fintype (schreierComplementEdges (X := X) hT) :=
374 Fintype.ofFinite (schreierComplementEdges (X := X) hT)
375 letI : Fintype {e : totalGen // e ∈ covered} :=
376 Fintype.ofFinite {e : totalGen // e ∈ covered}
377 letI : Fintype {a : CategoryTheory.ActionCategory (FreeGroup X) T // a ≠ root} :=
378 Fintype.ofFinite {a : CategoryTheory.ActionCategory (FreeGroup X) T // a ≠ root}
379 letI : Fintype {v : Ttree // v ≠ Quiver.root Ttree} :=
380 Fintype.ofFinite {v : Ttree // v ≠ Quiver.root Ttree}
381 haveI : Finite (Quiver.Total Ttree) :=
382 Finite.of_equiv {v : Ttree // v ≠ Quiver.root Ttree}
383 (Quiver.Arborescence.totalEquivNonRoot Ttree).symm
384 letI : Fintype (Quiver.Total Ttree) := Fintype.ofFinite (Quiver.Total Ttree)
385 have hYcard :
386 Fintype.card (schreierComplementEdges (X := X) hT) =
387 Fintype.card totalGen - Fintype.card {e : totalGen // e ∈ covered} := by
388 change
389 Fintype.card {e : totalGen // e ∈ ((covered : Set totalGen)ᶜ)} =
390 Fintype.card totalGen - Fintype.card {e : totalGen // e ∈ covered}
391 simpa only [Set.mem_compl_iff] using
392 (Fintype.card_subtype_compl (fun e : totalGen => e ∈ covered) :
393 Fintype.card {e : totalGen // ¬ e ∈ covered} =
394 Fintype.card totalGen - Fintype.card {e : totalGen // e ∈ covered})
395 have hTotal :
396 Fintype.card totalGen = Fintype.card T * Fintype.card X := by
397 simpa [totalGen, Fintype.card_prod] using
398 Fintype.card_congr
399 (FreeGroupBasis.actionGroupoidGeneratorTotalEquiv
400 (ι := X) (G := FreeGroup X) (A := T) (FreeGroup.inverseBasis X))
401 let eObjNonRoot :
402 {a : CategoryTheory.ActionCategory (FreeGroup X) T // a ≠ root} ≃
403 {t : T // t ≠ rootT} := {
404 toFun := fun a => ⟨(CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T).symm a.1, by
405 intro h
406 apply a.2
407 simpa [root] using congrArg (CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T) h⟩
408 invFun := fun t => ⟨CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T t.1, by
409 intro h
410 apply t.2
411 simpa [root] using
412 congrArg (CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T).symm h⟩
413 left_inv := by
414 intro a
415 apply Subtype.ext
416 simp only [ne_eq, Equiv.apply_symm_apply]
417 right_inv := by
418 intro t
419 apply Subtype.ext
420 simp only [ne_eq, Equiv.symm_apply_apply]}
421 haveI : Subsingleton {t : T // t = rootT} :=
422 ⟨fun t t' => Subtype.ext (by simp only [t.property, t'.property])⟩
423 have hOne :
424 Fintype.card {t : T // t = rootT} = 1 := by
425 exact Fintype.card_ofSubsingleton (⟨rootT, rfl⟩ : {t : T // t = rootT})
426 have hTcompl :
427 Fintype.card {t : T // t ≠ rootT} = Fintype.card T - 1 := by
428 calc
429 Fintype.card {t : T // t ≠ rootT}
430 = Fintype.card T - Fintype.card {t : T // t = rootT} := by
431 exact Fintype.card_subtype_compl (fun t : T => t = rootT)
432 _ = Fintype.card T - 1 := by rw [hOne]
433 have hNonRoot :
434 Fintype.card {v : Ttree // v ≠ Quiver.root Ttree} = Fintype.card T - 1 := by
435 simpa [Ttree, root, rootT] using (Fintype.card_congr eObjNonRoot).trans hTcompl
436 have hCovered :
437 Fintype.card {e : totalGen // e ∈ covered} = Fintype.card T - 1 := by
438 calc
439 Fintype.card {e : totalGen // e ∈ covered}
440 = Fintype.card (Quiver.Total Ttree) := by
441 simpa [totalGen, covered] using
442 Fintype.card_congr (Quiver.coveredArrowEquivTotal Ttree)
443 _ = Fintype.card {v : Ttree // v ≠ Quiver.root Ttree} := by
444 simpa using Fintype.card_congr (Quiver.Arborescence.totalEquivNonRoot Ttree)
445 _ = Fintype.card T - 1 := hNonRoot
446 have hYcalcF :
447 Fintype.card (schreierComplementEdges (X := X) hT) =
448 Fintype.card T * Fintype.card X - (Fintype.card T - 1) := by
449 rw [hYcard, hTotal, hCovered]
450 have hYcalc :
451 Nat.card (schreierComplementEdges (X := X) hT) =
452 Nat.card T * Nat.card X - (Nat.card T - 1) := by
453 simpa [Nat.card_eq_fintype_card] using hYcalcF
454 by_cases hX0 : Nat.card X = 0
455 · have hX0F : Fintype.card X = 0 := by
456 simpa [Nat.card_eq_fintype_card] using hX0
457 calc
458 Nat.card (schreierComplementEdges (X := X) hT)
459 = Nat.card T * Nat.card X - (Nat.card T - 1) := hYcalc
460 _ = 0 := by simp only [Nat.card_eq_fintype_card, hX0F, mul_zero, zero_tsub]
461 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T) := by
462 simp only [Schreier.rankTransform, Nat.card_eq_fintype_card, hX0F, ↓reduceIte]
463 · obtain ⟨r, hr⟩ := Nat.exists_eq_succ_of_ne_zero hX0
464 rw [hr] at hYcalc ⊢
465 calc
466 Nat.card (schreierComplementEdges (X := X) hT)
467 = Nat.card T * (r + 1) - (Nat.card T - 1) := hYcalc
468 _ = Nat.card T * r + Nat.card T - (Nat.card T - 1) := by
469 rw [Nat.mul_succ]
470 _ = Nat.card T * r + (Nat.card T - (Nat.card T - 1)) := by
471 rw [Nat.add_sub_assoc (Nat.sub_le _ _)]
472 _ = Nat.card T * r + 1 := by
473 have hTpos : 0 < Nat.card T := by
474 simpa [Nat.card_eq_fintype_card] using
475 (Fintype.card_pos_iff.mpr ⟨rootT⟩)
476 obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hTpos)
477 rw [hn]
478 simp only [Nat.succ_eq_add_one, add_tsub_cancel_right, add_tsub_cancel_left]
479 _ = 1 + Nat.card T * r := by
480 rw [Nat.add_comm]
481 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (r + 1) (Nat.card T) := by
482 rw [_root_.ReidemeisterSchreier.Schreier.rankTransform_succ]
484/-- Direct Schreier-rank count for the preferred pair-indexed generator type. -/
486 {X : Type u} [DecidableEq X] [Finite X]
487 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
488 [Finite T]
489 (hT : IsRightSchreierTransversal (X := X) L T) :
490 Nat.card (NontrivialSchreierPair (X := X) hT) =
491 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T) := by
492 calc
493 Nat.card (NontrivialSchreierPair (X := X) hT)
494 = Nat.card (schreierComplementEdges (X := X) hT) := by
495 exact Nat.card_congr
496 (schreierComplementEdgesEquivNontrivialPairs (X := X) hT).symm
497 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T) :=
498 natCard_schreierComplementEdges_eq_rankTransform_direct (X := X) (L := L) hT
500/-- Direct Schreier-rank count with the index expressed as the usual left-coset quotient. -/
502 {X : Type u} [DecidableEq X] [Finite X]
503 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
504 [Finite (FreeGroup X ⧸ L)]
505 (hT : IsRightSchreierTransversal (X := X) L T) :
506 Nat.card (NontrivialSchreierPair (X := X) hT) =
507 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (FreeGroup X ⧸ L)) := by
508 classical
509 haveI : Finite (Quotient (QuotientGroup.rightRel L)) :=
510 Finite.of_equiv (FreeGroup X ⧸ L)
511 (QuotientGroup.quotientRightRelEquivQuotientLeftRel L).symm
512 haveI : Finite T :=
513 Finite.of_equiv (Quotient (QuotientGroup.rightRel L)) hT.1.rightQuotientEquiv
514 have hTcard :
515 Nat.card T = Nat.card (FreeGroup X ⧸ L) := by
516 calc
517 Nat.card T = Nat.card (Quotient (QuotientGroup.rightRel L)) := by
518 exact (Nat.card_congr hT.1.rightQuotientEquiv).symm
519 _ = Nat.card (FreeGroup X ⧸ L) := by
520 exact Nat.card_congr (QuotientGroup.quotientRightRelEquivQuotientLeftRel L)
521 calc
522 Nat.card (NontrivialSchreierPair (X := X) hT)
523 = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T) :=
524 natCard_nontrivialSchreierPairs_eq_rankTransform_direct (X := X) (L := L) hT
525 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (FreeGroup X ⧸ L)) := by
526 rw [hTcard]
528/-- A finite-index subgroup of a free group admits a free basis of Schreier-transformed
529cardinality. -/
531 {X : Type u} {L : Subgroup (FreeGroup X)} [Finite X] [Finite (FreeGroup X ⧸ L)] :
532 ∃ Y : Type u, Nonempty (FreeGroupBasis Y L) ∧
533 Nat.card Y = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (FreeGroup X ⧸ L)) := by
534 classical
535 let A : Type u := FreeGroup X ⧸ L
536 letI : MulAction (FreeGroup X) A :=
537 inferInstanceAs (MulAction (FreeGroup X) (FreeGroup X ⧸ L))
538 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) A) :=
539 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
540 let root : CategoryTheory.ActionCategory (FreeGroup X) A :=
541 CategoryTheory.ActionCategory.objEquiv (FreeGroup X) A (((1 : FreeGroup X) : A))
542 let rootGen :
543 Quiver.Symmetrify
544 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) A)) :=
545 show Quiver.Symmetrify
546 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) A)) from
547 (show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) A) from root)
548 letI : Quiver.RootedConnected rootGen := by
549 simpa [rootGen] using
550 (IsFreeGroupoid.generators_connected
551 (CategoryTheory.ActionCategory (FreeGroup X) A) root)
552 let Ttree :
553 WideSubquiver
554 (Quiver.Symmetrify
555 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) A))) :=
556 Quiver.geodesicSubtree rootGen
557 letI : Quiver.Arborescence Ttree := Quiver.geodesicArborescence rootGen
558 let Y :=
559 (((Quiver.wideSubquiverEquivSetTotal <|
560 Quiver.wideSubquiverSymmetrify Ttree)ᶜ : Set _))
561 let b : FreeGroupBasis ↑Y L :=
562 (IsFreeGroupoid.SpanningTree.endBasis Ttree).map <|
563 by
564 simpa [A, root, rootGen, Ttree] using
565 (CategoryTheory.ActionCategory.endMulEquivSubgroup L)
566 refine ⟨↑Y, ⟨b⟩, ?_⟩
567 let totalGen :=
568 Quiver.Total (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) A))
569 let covered : Set totalGen :=
570 Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify Ttree)
571 letI : Fintype X := Fintype.ofFinite X
572 letI : Fintype A := Fintype.ofFinite A
573 haveI : Finite (CategoryTheory.ActionCategory (FreeGroup X) A) :=
574 Finite.of_equiv A (CategoryTheory.ActionCategory.objEquiv (FreeGroup X) A)
575 haveI : Finite Ttree :=
576 Finite.of_equiv (CategoryTheory.ActionCategory (FreeGroup X) A)
577 (show _ ≃ Ttree from Equiv.refl _)
578 haveI : Finite totalGen :=
579 Finite.of_equiv (A × X)
580 (FreeGroupBasis.actionGroupoidGeneratorTotalEquiv (FreeGroup.inverseBasis X)).symm
581 letI : Fintype totalGen := Fintype.ofFinite totalGen
582 letI : Fintype ↑Y := Fintype.ofFinite ↑Y
583 letI : Fintype {e : totalGen // e ∈ covered} := Fintype.ofFinite {e : totalGen // e ∈ covered}
584 letI : Fintype {a : CategoryTheory.ActionCategory (FreeGroup X) A // a ≠ root} :=
585 Fintype.ofFinite {a : CategoryTheory.ActionCategory (FreeGroup X) A // a ≠ root}
586 letI : Fintype {v : Ttree // v ≠ Quiver.root Ttree} :=
587 Fintype.ofFinite {v : Ttree // v ≠ Quiver.root Ttree}
588 haveI : Finite (Quiver.Total Ttree) :=
589 Finite.of_equiv {v : Ttree // v ≠ Quiver.root Ttree}
590 (Quiver.Arborescence.totalEquivNonRoot Ttree).symm
591 letI : Fintype (Quiver.Total Ttree) := Fintype.ofFinite (Quiver.Total Ttree)
592 have hYcard :
593 Fintype.card ↑Y = Fintype.card totalGen - Fintype.card {e : totalGen // e ∈ covered} := by
594 change
595 Fintype.card {e : totalGen // e ∈ ((covered : Set totalGen)ᶜ)} =
596 Fintype.card totalGen - Fintype.card {e : totalGen // e ∈ covered}
597 simpa only [Set.mem_compl_iff] using
598 (Fintype.card_subtype_compl (fun e : totalGen => e ∈ covered) :
599 Fintype.card {e : totalGen // ¬ e ∈ covered} =
600 Fintype.card totalGen - Fintype.card {e : totalGen // e ∈ covered})
601 have hTotal :
602 Fintype.card totalGen = Fintype.card A * Fintype.card X := by
603 simpa [totalGen, Fintype.card_prod] using
604 Fintype.card_congr
605 (FreeGroupBasis.actionGroupoidGeneratorTotalEquiv
606 (ι := X) (G := FreeGroup X) (A := A) (FreeGroup.inverseBasis X))
607 let eObjNonRoot :
608 {a : CategoryTheory.ActionCategory (FreeGroup X) A // a ≠ root} ≃
609 {q : A // q ≠ (((1 : FreeGroup X) : A))} := {
610 toFun := fun a => ⟨(CategoryTheory.ActionCategory.objEquiv (FreeGroup X) A).symm a.1, by
611 intro h
612 apply a.2
613 simpa [root] using congrArg (CategoryTheory.ActionCategory.objEquiv (FreeGroup X) A) h⟩
614 invFun := fun q => ⟨CategoryTheory.ActionCategory.objEquiv (FreeGroup X) A q.1, by
615 intro h
616 apply q.2
617 simpa [root] using
618 congrArg (CategoryTheory.ActionCategory.objEquiv (FreeGroup X) A).symm h⟩
619 left_inv := by
620 intro a
621 apply Subtype.ext
622 simp only [ne_eq, Equiv.apply_symm_apply]
623 right_inv := by
624 intro q
625 apply Subtype.ext
626 simp only [ne_eq, Equiv.symm_apply_apply]}
627 haveI : Subsingleton {q : A // q = (((1 : FreeGroup X) : A))} :=
628 ⟨fun q q' => Subtype.ext (by simp only [q.property, q'.property])⟩
629 have hOne :
630 Fintype.card {q : A // q = (((1 : FreeGroup X) : A))} = 1 := by
631 exact
632 Fintype.card_ofSubsingleton
633 (⟨((1 : FreeGroup X) : A), rfl⟩ : {q : A // q = (((1 : FreeGroup X) : A))})
634 have hAcompl :
635 Fintype.card {q : A // q ≠ (((1 : FreeGroup X) : A))} = Fintype.card A - 1 := by
636 calc
637 Fintype.card {q : A // q ≠ (((1 : FreeGroup X) : A))}
638 = Fintype.card A - Fintype.card {q : A // q = (((1 : FreeGroup X) : A))} := by
639 exact Fintype.card_subtype_compl (fun q : A => q = (((1 : FreeGroup X) : A)))
640 _ = Fintype.card A - 1 := by rw [hOne]
641 have hNonRoot :
642 Fintype.card {v : Ttree // v ≠ Quiver.root Ttree} = Fintype.card A - 1 := by
643 simpa [Ttree, root, rootGen] using (Fintype.card_congr eObjNonRoot).trans hAcompl
644 have hCovered :
645 Fintype.card {e : totalGen // e ∈ covered} = Fintype.card A - 1 := by
646 calc
647 Fintype.card {e : totalGen // e ∈ covered}
648 = Fintype.card (Quiver.Total Ttree) := by
649 simpa [totalGen, covered] using
650 Fintype.card_congr (Quiver.coveredArrowEquivTotal Ttree)
651 _ = Fintype.card {v : Ttree // v ≠ Quiver.root Ttree} := by
652 simpa using Fintype.card_congr (Quiver.Arborescence.totalEquivNonRoot Ttree)
653 _ = Fintype.card A - 1 := hNonRoot
654 have hYcalcF :
655 Fintype.card ↑Y = Fintype.card A * Fintype.card X - (Fintype.card A - 1) := by
656 rw [hYcard, hTotal, hCovered]
657 have hYcalc :
658 Nat.card ↑Y = Nat.card A * Nat.card X - (Nat.card A - 1) := by
659 simpa [Nat.card_eq_fintype_card] using hYcalcF
660 by_cases hX0 : Nat.card X = 0
661 · haveI : IsEmpty X := Finite.card_eq_zero_iff.mp hX0
662 have hId :
663 (MonoidHom.id (FreeGroup X)) = (1 : FreeGroup X →* FreeGroup X) := by
664 apply FreeGroup.ext_hom
665 intro x
666 exact isEmptyElim x
667 have htriv : ∀ g : FreeGroup X, g = 1 := by
668 intro g
669 exact congrArg (fun f : FreeGroup X →* FreeGroup X => f g) hId
670 haveI : Subsingleton (FreeGroup X) :=
671 ⟨fun g h => by rw [htriv g, htriv h]⟩
672 have hLtop : L = ⊤ := by
673 ext g
674 constructor
675 · intro _
676 trivial
677 · intro _
678 rw [htriv g]
679 exact L.one_mem
680 have hA1 : Nat.card A = 1 := by
681 have hA1' : Nat.card (FreeGroup X ⧸ L) = 1 := by
682 rw [hLtop]
683 exact Nat.card_eq_one_iff_unique.mpr
684 ⟨QuotientGroup.subsingleton_quotient_top, ⟨((1 : FreeGroup X) :
685 FreeGroup X ⧸ (⊤ : Subgroup (FreeGroup X)))⟩⟩
686 simpa [A] using hA1'
687 rw [hX0, hA1] at hYcalc
688 simpa [_root_.ReidemeisterSchreier.Schreier.rankTransform, hX0] using hYcalc
689 · obtain ⟨r, hr⟩ := Nat.exists_eq_succ_of_ne_zero hX0
690 rw [hr] at hYcalc ⊢
691 calc
692 Nat.card ↑Y = Nat.card A * (r + 1) - (Nat.card A - 1) := hYcalc
693 _ = Nat.card A * r + Nat.card A - (Nat.card A - 1) := by
694 rw [Nat.mul_succ]
695 _ = Nat.card A * r + (Nat.card A - (Nat.card A - 1)) := by
696 rw [Nat.add_sub_assoc (Nat.sub_le _ _)]
697 _ = Nat.card A * r + 1 := by
698 have hApos : 0 < Nat.card A := by
699 simpa [Nat.card_eq_fintype_card] using
700 (Fintype.card_pos_iff.mpr ⟨((1 : FreeGroup X) : A)⟩)
701 obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hApos)
702 rw [hn]
703 simp only [Nat.succ_eq_add_one, add_tsub_cancel_right, add_tsub_cancel_left]
704 _ = 1 + Nat.card A * r := by
705 rw [Nat.add_comm]
706 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (r + 1) (Nat.card A) := by
707 rw [_root_.ReidemeisterSchreier.Schreier.rankTransform_succ]
710end ReidemeisterSchreier.Discrete.OpenSubgroups