ReidemeisterSchreier/Discrete/OpenSubgroups/PrefixTree.lean
1import Mathlib.GroupTheory.Schreier
2import ReidemeisterSchreier.Discrete.OpenSubgroups.Generators
3import ReidemeisterSchreier.Discrete.OpenSubgroups.Words.NielsenSchreierCompat
4import ReidemeisterSchreier.FreeGroup.Automorphisms
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ReidemeisterSchreier/Discrete/OpenSubgroups/PrefixTree.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Schreier prefix trees
17Builds the prefix tree attached to a Schreier transversal and proves the edge, cancellation, and generator-vanishing lemmas used in the basis theorem.
18-/
20namespace ReidemeisterSchreier.Discrete.OpenSubgroups
22section SchreierPrefixTrees
24open scoped Pointwise
25open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj Quiver FreeGroup
27theorem prefixParentEdge_mem_transversal {X : Type u} [DecidableEq X]
28 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
29 (hT : IsRightSchreierTransversal (X := X) L T)
30 (t : T) (ht1 : (t : FreeGroup X) ≠ 1) :
31 (FreeGroup.prefixParentEdgeOfNeOne (X := X) (t := (t : FreeGroup X)) ht1).parent ∈ T := by
32 rw [FreeGroup.prefixParentEdgeOfNeOne_parent]
33 exact prefixParent_mem_of_mem (X := X) hT t.property
35theorem exists_inverseBasis_edge_of_ne_one {X : Type u} [DecidableEq X]
36 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
37 (hT : IsRightSchreierTransversal (X := X) L T)
38 (t : T) (ht1 : (t : FreeGroup X) ≠ 1) :
39 ∃ x : X,
40 letI := schreierTransversalRightCosetAction (X := X) hT
41 (FreeGroup.inverseBasis X x •
42 (⟨FreeGroup.prefixParent (t : FreeGroup X),
43 prefixParent_mem_of_mem (X := X) hT t.property⟩ : T) = t) ∨
44 (FreeGroup.inverseBasis X x • t =
45 (⟨FreeGroup.prefixParent (t : FreeGroup X),
46 prefixParent_mem_of_mem (X := X) hT t.property⟩ : T)) := by
47 let edge := FreeGroup.prefixParentEdgeOfNeOne (X := X) (t := (t : FreeGroup X)) ht1
48 have hlastEdge :
49 FreeGroup.lastLetter? (t : FreeGroup X) = some edge.letter :=
50 FreeGroup.prefixParentEdgeOfNeOne_lastLetter? (X := X) (t := (t : FreeGroup X)) ht1
51 rcases hletter : edge.letter with ⟨x, b⟩
52 cases b with
53 | false =>
54 have hlast? :
55 FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, false) : SignedLetter X) := by
56 simpa [edge, hletter] using hlastEdge
57 rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff
58 (g := (t : FreeGroup X)) (y := ((x, false) : SignedLetter X))).1 hlast? with
59 ⟨hw, hlast⟩
60 refine ⟨x, Or.inr ?_⟩
61 letI := schreierTransversalRightCosetAction (X := X) hT
62 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
63 prefixParent_mem_of_mem (X := X) hT t.property⟩
64 rw [FreeGroup.inverseBasis_apply,
65 schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ t]
66 simpa [p] using
67 schreierRepresentative_eq_prefixParent_of_cancels (X := X) hT t.property hw hlast
68 | true =>
69 have hlast? :
70 FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, true) : SignedLetter X) := by
71 simpa [edge, hletter] using hlastEdge
72 rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff
73 (g := (t : FreeGroup X)) (y := ((x, true) : SignedLetter X))).1 hlast? with
74 ⟨hw, hlast⟩
75 refine ⟨x, Or.inl ?_⟩
76 letI := schreierTransversalRightCosetAction (X := X) hT
77 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
78 prefixParent_mem_of_mem (X := X) hT t.property⟩
79 rw [FreeGroup.inverseBasis_apply,
80 schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ p]
81 simpa [p] using
82 schreierRepresentative_eq_of_prefixParent_last_pos (X := X) hT t.property hw hlast
84/-- The canonical prefix tree on the Schreier transversal. Its unique incoming edge for a non-root
85vertex is determined by the last letter of the reduced word of that vertex. -/
86noncomputable def schreierPrefixTree {X : Type u} [DecidableEq X]
87 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
88 (hT : IsRightSchreierTransversal (X := X) L T) :
89 letI := schreierTransversalRightCosetAction (X := X) hT
90 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
91 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
92 WideSubquiver
93 (Quiver.Symmetrify <| IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)) := by
94 letI := schreierTransversalRightCosetAction (X := X) hT
95 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
96 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
97 exact fun a b =>
98 { e |
99 ∃ hw : FreeGroup.toWord (((show ActionCategory (FreeGroup X) T from b).back : T) :
100 FreeGroup X) ≠ [],
101 let tb : T := (show ActionCategory (FreeGroup X) T from b).back
102 let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),
103 prefixParent_mem_of_mem (X := X) hT tb.property⟩
104 (show ActionCategory (FreeGroup X) T from a).back = pb ∧
105 match e with
106 | Sum.inl g => (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, true)
107 | Sum.inr g => (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, false) }
109theorem mem_schreierPrefixTree_inl_iff {X : Type u} [DecidableEq X]
110 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
111 (hT : IsRightSchreierTransversal (X := X) L T) :
112 letI := schreierTransversalRightCosetAction (X := X) hT
113 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
114 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
115 ∀ {a b : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)}
116 (g : a ⟶ b),
117 (Sum.inl g :
118 @Quiver.Hom
119 (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))
120 inferInstance a b) ∈
121 schreierPrefixTree (X := X) hT a b ↔
122 ∃ hw : FreeGroup.toWord ((((show ActionCategory (FreeGroup X) T from b).back : T)) :
123 FreeGroup X) ≠ [],
124 let tb : T := (show ActionCategory (FreeGroup X) T from b).back
125 let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),
126 prefixParent_mem_of_mem (X := X) hT tb.property⟩
127 (show ActionCategory (FreeGroup X) T from a).back = pb ∧
128 (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, true) := by
129 letI := schreierTransversalRightCosetAction (X := X) hT
130 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
131 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
132 intro a b g
133 rfl
135theorem mem_schreierPrefixTree_inr_iff {X : Type u} [DecidableEq X]
136 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
137 (hT : IsRightSchreierTransversal (X := X) L T) :
138 letI := schreierTransversalRightCosetAction (X := X) hT
139 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
140 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
141 ∀ {a b : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)}
142 (g : b ⟶ a),
143 (Sum.inr g :
144 @Quiver.Hom
145 (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))
146 inferInstance a b) ∈
147 schreierPrefixTree (X := X) hT a b ↔
148 ∃ hw : FreeGroup.toWord ((((show ActionCategory (FreeGroup X) T from b).back : T)) :
149 FreeGroup X) ≠ [],
150 let tb : T := (show ActionCategory (FreeGroup X) T from b).back
151 let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),
152 prefixParent_mem_of_mem (X := X) hT tb.property⟩
153 (show ActionCategory (FreeGroup X) T from a).back = pb ∧
154 (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, false) := by
155 letI := schreierTransversalRightCosetAction (X := X) hT
156 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
157 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
158 intro a b g
159 rfl
161theorem schreierPrefixTree_edge_of_last_pos {X : Type u} [DecidableEq X]
162 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
163 (hT : IsRightSchreierTransversal (X := X) L T)
164 (t : T) {x : X} (hw : FreeGroup.toWord (t : FreeGroup X) ≠ [])
165 (hlast : (FreeGroup.toWord (t : FreeGroup X)).getLast hw = (x, true)) :
166 letI := schreierTransversalRightCosetAction (X := X) hT
167 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
168 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
169 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
170 prefixParent_mem_of_mem (X := X) hT t.property⟩
171 let pA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
172 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
173 ((p : T) : ActionCategory (FreeGroup X) T)
174 let tA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
175 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
176 ((t : T) : ActionCategory (FreeGroup X) T)
177 ∃ e : @Quiver.Hom
178 (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))
179 inferInstance pA tA,
180 e ∈ schreierPrefixTree (X := X) hT pA tA := by
181 letI := schreierTransversalRightCosetAction (X := X) hT
182 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
183 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
184 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
185 prefixParent_mem_of_mem (X := X) hT t.property⟩
186 refine ⟨Sum.inl ⟨x, ?_⟩, ?_⟩
187 · change (FreeGroup.of x)⁻¹ • p = t
188 rw [schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ p]
189 simpa [p] using
190 schreierRepresentative_eq_of_prefixParent_last_pos (X := X) hT t.property hw hlast
191 · rw [mem_schreierPrefixTree_inl_iff (X := X) hT]
192 exact ⟨hw, rfl, by simpa using hlast⟩
194theorem schreierPrefixTree_edge_of_last_neg {X : Type u} [DecidableEq X]
195 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
196 (hT : IsRightSchreierTransversal (X := X) L T)
197 (t : T) {x : X} (hw : FreeGroup.toWord (t : FreeGroup X) ≠ [])
198 (hlast : (FreeGroup.toWord (t : FreeGroup X)).getLast hw = (x, false)) :
199 letI := schreierTransversalRightCosetAction (X := X) hT
200 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
201 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
202 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
203 prefixParent_mem_of_mem (X := X) hT t.property⟩
204 let pA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
205 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
206 ((p : T) : ActionCategory (FreeGroup X) T)
207 let tA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
208 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
209 ((t : T) : ActionCategory (FreeGroup X) T)
210 ∃ e : @Quiver.Hom
211 (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))
212 inferInstance pA tA,
213 e ∈ schreierPrefixTree (X := X) hT pA tA := by
214 letI := schreierTransversalRightCosetAction (X := X) hT
215 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
216 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
217 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
218 prefixParent_mem_of_mem (X := X) hT t.property⟩
219 refine ⟨Sum.inr ⟨x, ?_⟩, ?_⟩
220 · change (FreeGroup.of x)⁻¹ • t = p
221 rw [schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ t]
222 simpa [p] using
223 schreierRepresentative_eq_prefixParent_of_cancels (X := X) hT t.property hw hlast
224 · rw [mem_schreierPrefixTree_inr_iff (X := X) hT]
225 exact ⟨hw, rfl, by simpa using hlast⟩
227theorem schreierPrefixTree_parent_edge_of_ne_one {X : Type u} [DecidableEq X]
228 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
229 (hT : IsRightSchreierTransversal (X := X) L T)
230 (t : T) (ht1 : (t : FreeGroup X) ≠ 1) :
231 letI := schreierTransversalRightCosetAction (X := X) hT
232 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
233 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
234 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
235 prefixParent_mem_of_mem (X := X) hT t.property⟩
236 let pA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
237 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
238 ((p : T) : ActionCategory (FreeGroup X) T)
239 let tA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
240 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
241 ((t : T) : ActionCategory (FreeGroup X) T)
242 ∃ e : @Quiver.Hom
243 (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))
244 inferInstance pA tA,
245 e ∈ schreierPrefixTree (X := X) hT pA tA := by
246 let edge := FreeGroup.prefixParentEdgeOfNeOne (X := X) (t := (t : FreeGroup X)) ht1
247 have hlastEdge :
248 FreeGroup.lastLetter? (t : FreeGroup X) = some edge.letter :=
249 FreeGroup.prefixParentEdgeOfNeOne_lastLetter? (X := X) (t := (t : FreeGroup X)) ht1
250 rcases hletter : edge.letter with ⟨x, b⟩
251 cases b with
252 | false =>
253 have hlast? :
254 FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, false) : SignedLetter X) := by
255 simpa [edge, hletter] using hlastEdge
256 rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff
257 (g := (t : FreeGroup X)) (y := ((x, false) : SignedLetter X))).1 hlast? with
258 ⟨hw, hlast⟩
259 exact schreierPrefixTree_edge_of_last_neg (X := X) hT t hw hlast
260 | true =>
261 have hlast? :
262 FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, true) : SignedLetter X) := by
263 simpa [edge, hletter] using hlastEdge
264 rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff
265 (g := (t : FreeGroup X)) (y := ((x, true) : SignedLetter X))).1 hlast? with
266 ⟨hw, hlast⟩
267 exact schreierPrefixTree_edge_of_last_pos (X := X) hT t hw hlast
269lemma schreierPrefixTree_root_or_arrow {X : Type u} [DecidableEq X]
270 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
271 (hT : IsRightSchreierTransversal (X := X) L T) :
272 letI := schreierTransversalRightCosetAction (X := X) hT
273 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
274 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
275 ∀ b : schreierPrefixTree (X := X) hT,
276 b = ((((⟨(1 : FreeGroup X), hT.2.1⟩ : T) : ActionCategory (FreeGroup X) T) :
277 schreierPrefixTree (X := X) hT)) ∨
278 ∃ a, Nonempty (a ⟶ b) := by
279 letI := schreierTransversalRightCosetAction (X := X) hT
280 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
281 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
282 intro b
283 let tb : T := (show ActionCategory (FreeGroup X) T from b).back
284 by_cases hb1 : (tb : FreeGroup X) = 1
285 · left
286 cases b with
288 cases fst
289 cases snd with
291 have hb1' : val = 1 := by
292 simpa [tb] using hb1
293 cases hb1'
294 rfl
295 · right
296 let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),
297 prefixParent_mem_of_mem (X := X) hT tb.property⟩
298 refine ⟨((pb : T) : ActionCategory (FreeGroup X) T), ?_⟩
299 rcases schreierPrefixTree_parent_edge_of_ne_one (X := X) hT tb hb1 with ⟨e, he⟩
300 exact ⟨⟨e, he⟩⟩
302lemma schreierPrefixTree_unique_arrow {X : Type u} [DecidableEq X]
303 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
304 (hT : IsRightSchreierTransversal (X := X) L T) :
305 letI := schreierTransversalRightCosetAction (X := X) hT
306 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
307 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
308 ∀ ⦃a b c : schreierPrefixTree (X := X) hT⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f := by
309 letI := schreierTransversalRightCosetAction (X := X) hT
310 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
311 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
312 intro a b c e f
313 rcases e with ⟨e0, hme⟩
314 rcases f with ⟨f0, hmf⟩
315 have hme0 := hme
316 have hmf0 := hmf
317 rcases hme with ⟨hwe, hsrca, hlast_e⟩
318 rcases hmf with ⟨hwf, hsrcb, hlast_f⟩
319 let tc : T := (show ActionCategory (FreeGroup X) T from c).back
320 let pc : T := ⟨FreeGroup.prefixParent (tc : FreeGroup X),
321 prefixParent_mem_of_mem (X := X) hT tc.property⟩
322 have ha_back : (show ActionCategory (FreeGroup X) T from a).back = pc := by
323 simpa [tc, pc] using hsrca
324 have hb_back : (show ActionCategory (FreeGroup X) T from b).back = pc := by
325 simpa [tc, pc] using hsrcb
326 have hab : a = b := actionCategory_eq_of_back_eq (h := ha_back.trans hb_back.symm)
327 refine ⟨hab, ?_⟩
328 subst hab
329 have hUnder : e0 = f0 := by
330 cases e0 with
331 | inl ge =>
332 cases f0 with
333 | inl gf =>
334 have hxeq : ge.1 = gf.1 := by
335 have hlast : (ge.1, true) = (gf.1, true) := by
336 calc
337 (ge.1, true) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by
338 simpa [tc] using hlast_e.symm
339 _ = (gf.1, true) := by simpa [tc] using hlast_f
340 exact congrArg Prod.fst hlast
341 have hgegf : ge = gf := Subtype.ext hxeq
342 subst hgegf
343 rfl
344 | inr gf =>
345 exfalso
346 have hlast : (ge.1, true) = (gf.1, false) := by
347 calc
348 (ge.1, true) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by
349 simpa [tc] using hlast_e.symm
350 _ = (gf.1, false) := by simpa [tc] using hlast_f
351 have : (true : Bool) = false := congrArg Prod.snd hlast
352 cases this
353 | inr ge =>
354 cases f0 with
355 | inl gf =>
356 exfalso
357 have hlast : (ge.1, false) = (gf.1, true) := by
358 calc
359 (ge.1, false) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by
360 simpa [tc] using hlast_e.symm
361 _ = (gf.1, true) := by simpa [tc] using hlast_f
362 have : (false : Bool) = true := congrArg Prod.snd hlast
363 cases this
364 | inr gf =>
365 have hxeq : ge.1 = gf.1 := by
366 have hlast : (ge.1, false) = (gf.1, false) := by
367 calc
368 (ge.1, false) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by
369 simpa [tc] using hlast_e.symm
370 _ = (gf.1, false) := by simpa [tc] using hlast_f
371 exact congrArg Prod.fst hlast
372 have hgegf : ge = gf := Subtype.ext hxeq
373 subst hgegf
374 rfl
375 have hEq : (⟨e0, hme0⟩ : a ⟶ c) = ⟨f0, hmf0⟩ := by
376 apply Subtype.ext
377 exact hUnder
378 cases hEq
379 rfl
381lemma schreierPrefixTree_height_lt {X : Type u} [DecidableEq X]
382 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
383 (hT : IsRightSchreierTransversal (X := X) L T) :
384 letI := schreierTransversalRightCosetAction (X := X) hT
385 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
386 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
387 ∀ ⦃a b : schreierPrefixTree (X := X) hT⦄ (_ : a ⟶ b),
388 (FreeGroup.toWord (((show ActionCategory (FreeGroup X) T from a).back : T) :
389 FreeGroup X)).length <
390 (FreeGroup.toWord (((show ActionCategory (FreeGroup X) T from b).back : T) :
391 FreeGroup X)).length := by
392 letI := schreierTransversalRightCosetAction (X := X) hT
393 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
394 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
395 intro a b e
396 rcases e with ⟨_, hmem⟩
397 rcases hmem with ⟨hw, hsrc, _⟩
398 let tb : T := (show ActionCategory (FreeGroup X) T from b).back
399 have htb1 : (tb : FreeGroup X) ≠ 1 := by
400 exact mt (FreeGroup.toWord_eq_nil_iff.mpr) hw
401 have hlt :=
402 Internal.FreeGroupWord.FreeGroup.toWord_length_prefixParent_lt (t := (tb : FreeGroup X)) htb1
403 have hsrc' : (show ActionCategory (FreeGroup X) T from a).back =
404 ⟨FreeGroup.prefixParent (tb : FreeGroup X),
405 prefixParent_mem_of_mem (X := X) hT tb.property⟩ := by
406 simpa [tb] using hsrc
407 simpa [tb, hsrc', Internal.FreeGroupWord.FreeGroup.toWord_prefixParent] using hlt
409noncomputable instance schreierPrefixTree_arborescence {X : Type u} [DecidableEq X]
410 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
411 (hT : IsRightSchreierTransversal (X := X) L T) :
412 letI := schreierTransversalRightCosetAction (X := X) hT
413 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
414 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
415 Quiver.Arborescence (schreierPrefixTree (X := X) hT) := by
416 letI := schreierTransversalRightCosetAction (X := X) hT
417 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
418 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
419 refine Quiver.arborescenceMk
420 ((((⟨(1 : FreeGroup X), hT.2.1⟩ : T) : ActionCategory (FreeGroup X) T) :
421 schreierPrefixTree (X := X) hT))
422 (fun a =>
423 (FreeGroup.toWord (((show ActionCategory (FreeGroup X) T from a).back : T) :
424 FreeGroup X)).length)
425 ?_ ?_ ?_
426 · intro a b e
427 exact schreierPrefixTree_height_lt (X := X) hT e
428 · intro a b c e f
429 exact schreierPrefixTree_unique_arrow (X := X) hT e f
430 · intro b
431 exact schreierPrefixTree_root_or_arrow (X := X) hT b
433/-- The classical Schreier generators attached to a right Schreier transversal algebraically
434generate the subgroup. This is the exact generation statement behind Schreier's lemma; the later
435exact free-basis theorem still requires the additional Nielsen-Schreier argument. -/
436theorem closure_schreierGeneratorSet_eq_top {X : Type u} [DecidableEq X]
437 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
438 (hT : IsRightSchreierTransversal (X := X) L T) :
439 Subgroup.closure (schreierGeneratorSet (X := X) hT : Set L) = ⊤ := by
440 let U : Set L :=
441 (T * Set.range (FreeGroup.of : X → FreeGroup X)).image fun g =>
442 ⟨g * (hT.1.toRightFun g : FreeGroup X)⁻¹, hT.1.mul_inv_toRightFun_mem g⟩
443 have hUtop : Subgroup.closure U = ⊤ := by
444 simpa [U] using
445 (Subgroup.closure_mul_image_eq_top
446 (H := L) (R := T) (S := Set.range (FreeGroup.of : X → FreeGroup X))
447 hT.1 hT.2.1 (FreeGroup.closure_range_of X))
448 have hSchreier_le :
449 (schreierGeneratorSet (X := X) hT : Set L) ⊆ U := by
450 intro z hz
451 rcases hz with ⟨t, ht, x, rfl, _hz1⟩
452 refine ⟨t * FreeGroup.of x, ⟨t, ht, FreeGroup.of x, ⟨x, rfl⟩, rfl⟩, ?_⟩
453 apply Subtype.ext
454 rfl
455 have hU_le :
456 U ⊆ insert 1 (schreierGeneratorSet (X := X) hT : Set L) := by
457 intro z hz
458 rcases hz with ⟨g, hg, rfl⟩
459 rcases hg with ⟨t, ht, y, hy, rfl⟩
460 rcases hy with ⟨x, rfl⟩
461 by_cases hgen : schreierGenerator (X := X) hT t x = 1
462 · left
463 simpa [schreierGenerator, schreierRepresentative] using congrArg Subtype.val hgen
464 · right
465 exact ⟨t, ht, x, rfl, hgen⟩
466 have hclosureU_le :
467 Subgroup.closure U ≤
468 Subgroup.closure (schreierGeneratorSet (X := X) hT : Set L) := by
469 refine (Subgroup.closure_mono hU_le).trans ?_
470 exact le_of_eq (Subgroup.closure_insert_one
471 (schreierGeneratorSet (X := X) hT : Set L))
472 apply top_unique
473 calc
474 ⊤ = Subgroup.closure U := hUtop.symm
475 _ ≤ Subgroup.closure (schreierGeneratorSet (X := X) hT : Set L) := hclosureU_le
477/-- The root vertex group in the Schreier action groupoid is canonically the subgroup `L`,
478via the action label of an endomorphism. -/
479noncomputable def schreierRootEndMulEquiv {X : Type u} [DecidableEq X]
480 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
481 (hT : IsRightSchreierTransversal (X := X) L T) :
482 letI := schreierTransversalRightCosetAction (X := X) hT
483 CategoryTheory.End
484 (show ActionCategory (FreeGroup X) T from ((⟨(1 : FreeGroup X), hT.2.1⟩ : T) :
485 ActionCategory (FreeGroup X) T)) ≃* L := by
486 letI := schreierTransversalRightCosetAction (X := X) hT
487 let rootT : T := ⟨(1 : FreeGroup X), hT.2.1⟩
488 let eStab : MulAction.stabilizer (FreeGroup X) rootT ≃* L := by
489 refine MulEquiv.subgroupCongr ?_
490 ext g
491 constructor
492 · intro hg
493 have hfix : g • rootT = rootT := hg
494 have hrep : schreierRepresentative (X := X) hT (g⁻¹) = rootT := by
495 simpa [rootT] using (schreierTransversalRightCosetAction_smul (X := X) hT g rootT).symm.trans hfix
496 have hmemInv : g⁻¹ ∈ L := by
497 have hm : g⁻¹ *
498 (((schreierRepresentative (X := X) hT (g⁻¹) : T) : FreeGroup X))⁻¹ ∈ L :=
499 hT.1.mul_inv_toRightFun_mem (g⁻¹)
500 simpa [hrep, rootT] using hm
501 simpa using L.inv_mem hmemInv
502 · intro hg
503 change g • rootT = rootT
504 rw [schreierTransversalRightCosetAction_smul (X := X) hT g rootT]
505 simpa [rootT] using schreierRepresentative_eq_one_of_mem (X := X) hT (L.inv_mem hg)
506 let eSubmonoid : MulAction.stabilizerSubmonoid (FreeGroup X) rootT ≃* L :=
507 { toFun := fun g => eStab ⟨g.1, g.2⟩
508 invFun := fun l => ⟨(eStab.symm l).1, (eStab.symm l).2⟩
509 left_inv := by intro g; rfl
510 right_inv := by intro l; rfl
511 map_mul' := by intro g h; rfl }
512 exact (CategoryTheory.ActionCategory.stabilizerIsoEnd (FreeGroup X) rootT).symm.trans eSubmonoid
514/-- The cocycle functor on the Schreier action groupoid. It sends a morphism `a ⟶ b` labelled by
515`g` to the subgroup element `b g a⁻¹`, which is the inverse of the corresponding classical
516Schreier generator. -/
517noncomputable def schreierLabelFunctor {X : Type u} [DecidableEq X]
518 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
519 (hT : IsRightSchreierTransversal (X := X) L T) :
520 letI := schreierTransversalRightCosetAction (X := X) hT
521 ActionCategory (FreeGroup X) T ⥤ CategoryTheory.SingleObj L := by
522 letI := schreierTransversalRightCosetAction (X := X) hT
523 refine
524 { obj := fun _ => ()
525 map := fun {a b} p => ?_
526 map_id := ?_
527 map_comp := ?_ }
528 · let g : FreeGroup X := p.1
529 refine ⟨((b.back : T) : FreeGroup X) * g * (((a.back : T) : FreeGroup X))⁻¹, ?_⟩
530 have hp : schreierRepresentative (X := X) hT
531 ((((a.back : T) : FreeGroup X)) * g⁻¹) = b.back := by
532 rw [← schreierTransversalRightCosetAction_smul (X := X) hT g a.back]
533 exact p.2
534 have hmem : (((a.back : T) : FreeGroup X)) * g⁻¹ *
535 (((b.back : T) : FreeGroup X))⁻¹ ∈ L := by
536 have hmem0 : (((a.back : T) : FreeGroup X)) * g⁻¹ *
537 (((schreierRepresentative (X := X) hT
538 ((((a.back : T) : FreeGroup X)) * g⁻¹) : T) : FreeGroup X))⁻¹ ∈ L := by
539 simpa [schreierRepresentative] using
540 hT.1.mul_inv_toRightFun_mem ((((a.back : T) : FreeGroup X)) * g⁻¹)
541 rw [hp] at hmem0
542 exact hmem0
543 simpa [mul_assoc] using L.inv_mem hmem
544 · intro a
545 apply Subtype.ext
546 change (((a.back : T) : FreeGroup X) * (1 : FreeGroup X) *
547 (((a.back : T) : FreeGroup X))⁻¹) = 1
548 simp only [mul_one, mul_inv_cancel]
549 · intro a b c p q
550 let gp : FreeGroup X := p.1
551 let gq : FreeGroup X := q.1
552 apply Subtype.ext
553 change (((c.back : T) : FreeGroup X) * (gq * gp) *
554 (((a.back : T) : FreeGroup X))⁻¹) =
555 ((((c.back : T) : FreeGroup X) * gq * (((b.back : T) : FreeGroup X))⁻¹) *
556 (((b.back : T) : FreeGroup X) * gp * (((a.back : T) : FreeGroup X))⁻¹))
557 simp only [mul_assoc, inv_mul_cancel_left]
559@[simp 900] theorem schreierLabelFunctor_map_of {X : Type u} [DecidableEq X]
560 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
561 (hT : IsRightSchreierTransversal (X := X) L T) :
562 letI := schreierTransversalRightCosetAction (X := X) hT
563 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
564 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
565 ∀ {a b : ActionCategory (FreeGroup X) T}
566 (e : ((show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from a) ⟶ b)),
567 ((schreierLabelFunctor (X := X) hT).map (IsFreeGroupoid.of e) : L) =
568 (schreierGenerator (X := X) hT (((a.back : T) : FreeGroup X)) e.1)⁻¹ := by
569 letI := schreierTransversalRightCosetAction (X := X) hT
570 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
571 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
572 intro a b e
573 have hb : schreierRepresentative (X := X) hT
574 ((((a.back : T) : FreeGroup X)) * FreeGroup.of e.1) = b.back := by
575 have hp : FreeGroup.inverseBasis X e.1 • a.back = b.back := e.property
576 rw [FreeGroup.inverseBasis_apply,
577 schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of e.1)⁻¹ a.back] at hp
578 simpa using hp
579 apply Subtype.ext
580 change (((b.back : T) : FreeGroup X) * (FreeGroup.of e.1)⁻¹ *
581 (((a.back : T) : FreeGroup X))⁻¹) =
582 ((((schreierGenerator (X := X) hT (((a.back : T) : FreeGroup X)) e.1 : L) :
583 FreeGroup X))⁻¹)
586lemma schreierLabelFunctor_map_of_eq_one_of_mem_tree {X : Type u} [DecidableEq X]
587 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
588 (hT : IsRightSchreierTransversal (X := X) L T) :
589 letI := schreierTransversalRightCosetAction (X := X) hT
590 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
591 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
592 ∀ {a b : ActionCategory (FreeGroup X) T}
593 (e : ((show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from a) ⟶ b)),
594 e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b →
595 (schreierLabelFunctor (X := X) hT).map (IsFreeGroupoid.of e) = (1 : L) := by
596 letI := schreierTransversalRightCosetAction (X := X) hT
597 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
598 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
599 intro a b e he
600 rw [schreierLabelFunctor_map_of (X := X) hT e]
601 rcases he with htree | htree
602 · rcases htree with ⟨hw, hsrc, hlast⟩
603 let tb : T := b.back
604 have hsrc' : a.back = ⟨FreeGroup.prefixParent (tb : FreeGroup X),
605 prefixParent_mem_of_mem (X := X) hT tb.property⟩ := by
606 simpa [tb] using hsrc
607 have hgen :
608 schreierGenerator (X := X) hT
609 (FreeGroup.prefixParent (tb : FreeGroup X)) e.1 = (1 : L) := by
610 exact schreierGenerator_eq_one_of_prefixParent_last_pos (X := X) hT
611 (t := (tb : FreeGroup X)) tb.property hw hlast
612 have hgen' : schreierGenerator (X := X) hT (((a.back : T) : FreeGroup X)) e.1 = (1 : L) := by
613 simpa [hsrc'] using hgen
614 exact inv_eq_one.mpr hgen'
615 · rcases htree with ⟨hw, hsrc, hlast⟩
616 let ta : T := a.back
617 have hgen : schreierGenerator (X := X) hT (ta : FreeGroup X) e.1 = (1 : L) := by
618 exact schreierGenerator_eq_one_of_cancels (X := X) hT
619 (t := (ta : FreeGroup X)) ta.property hw hlast
620 exact inv_eq_one.mpr (by simpa [ta] using hgen)
622lemma schreierGenerator_eq_one_implies_mem_prefixTree {X : Type u} [DecidableEq X]
623 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
624 (hT : IsRightSchreierTransversal (X := X) L T) :
625 letI := schreierTransversalRightCosetAction (X := X) hT
626 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
627 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
628 ∀ {a b : CategoryTheory.ActionCategory (FreeGroup X) T}
629 (e :
630 (show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from
631 a) ⟶ b),
632 schreierGenerator (X := X) hT (a.back : FreeGroup X) e.1 = 1 →
633 e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b := by
634 letI := schreierTransversalRightCosetAction (X := X) hT
635 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
636 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
637 intro a b e hgen
638 let ta : T := a.back
639 have hrep : schreierRepresentative (X := X) hT
640 ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) = b.back := by
641 have hp : FreeGroup.inverseBasis X e.1 • a.back = b.back := e.property
642 rw [FreeGroup.inverseBasis_apply,
643 schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of e.1)⁻¹ a.back] at hp
644 simpa [ta] using hp
645 have hraw :
646 (((schreierRepresentative (X := X) hT
647 ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) : T) : FreeGroup X)) =
648 ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := by
649 exact (schreierGenerator_eq_one_iff (X := X) (hT := hT)
650 (t := ((ta : T) : FreeGroup X)) (x := e.1)).mp hgen
651 by_cases hcancel : ∃ hw : FreeGroup.toWord ((ta : T) : FreeGroup X) ≠ [],
652 (FreeGroup.toWord ((ta : T) : FreeGroup X)).getLast hw = (e.1, false)
653 · rcases hcancel with ⟨hw, hlast⟩
654 have hb : (b.back : FreeGroup X) = FreeGroup.prefixParent ((ta : T) : FreeGroup X) := by
655 calc
656 (b.back : FreeGroup X)
657 = (((schreierRepresentative (X := X) hT
658 ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) : T) : FreeGroup X)) := by
659 exact congrArg Subtype.val hrep.symm
660 _ = ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := hraw
661 _ = FreeGroup.prefixParent ((ta : T) : FreeGroup X) :=
662 Internal.FreeGroupWord.FreeGroup.mul_of_eq_prefixParent_of_cancels
663 ((ta : T) : FreeGroup X) e.1 hw hlast
664 refine Or.inr ?_
665 refine ⟨hw, ?_⟩
666 constructor
667 · apply Subtype.ext
668 simpa [ta] using hb
669 · simpa [ta] using hlast
670 · have hword : FreeGroup.toWord (((ta : T) : FreeGroup X) * FreeGroup.of e.1) =
671 FreeGroup.toWord ((ta : T) : FreeGroup X) ++ [(e.1, true)] :=
672 Internal.FreeGroupWord.FreeGroup.toWord_mul_of_of_not_cancels
673 ((ta : T) : FreeGroup X) e.1 hcancel
674 have hb : (b.back : FreeGroup X) = ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := by
675 calc
676 (b.back : FreeGroup X)
677 = (((schreierRepresentative (X := X) hT
678 ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) : T) : FreeGroup X)) := by
679 exact congrArg Subtype.val hrep.symm
680 _ = ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := hraw
681 have hbw : FreeGroup.toWord (b.back : FreeGroup X) =
682 FreeGroup.toWord ((ta : T) : FreeGroup X) ++ [(e.1, true)] := by
683 simpa [hb] using hword
684 have hbw_ne : FreeGroup.toWord (b.back : FreeGroup X) ≠ [] := by
685 rw [hbw]
686 simp only [Lean.Elab.WF.paramLet, ne_eq, List.append_eq_nil_iff, FreeGroup.toWord_eq_nil_iff,
687 List.cons_ne_self, and_false, not_false_eq_true]
688 have hprefix : FreeGroup.prefixParent (b.back : FreeGroup X) = ((ta : T) : FreeGroup X) := by
689 apply FreeGroup.toWord_injective
690 rw [Internal.FreeGroupWord.FreeGroup.toWord_prefixParent, hbw]
691 simp only [Lean.Elab.WF.paramLet, ne_eq, List.cons_ne_self, not_false_eq_true, List.dropLast_append_of_ne_nil,
692 List.dropLast_singleton, List.append_nil]
693 refine Or.inl ?_
694 refine ⟨hbw_ne, ?_⟩
695 constructor
696 · apply Subtype.ext
697 exact hprefix.symm
698 · simp only [hbw, Lean.Elab.WF.paramLet, ne_eq, List.cons_ne_self, not_false_eq_true,
699 List.getLast_append_of_ne_nil, List.getLast_singleton]
701/-- A generator edge lies in the symmetrized prefix tree exactly when the associated Schreier
703theorem schreierGenerator_eq_one_iff_mem_prefixTree {X : Type u} [DecidableEq X]
704 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
705 (hT : IsRightSchreierTransversal (X := X) L T) :
706 letI := schreierTransversalRightCosetAction (X := X) hT
707 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
708 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
709 ∀ {a b : CategoryTheory.ActionCategory (FreeGroup X) T}
710 (e :
711 (show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from
712 a) ⟶ b),
713 schreierGenerator (X := X) hT (a.back : FreeGroup X) e.1 = 1 ↔
714 e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b := by
715 letI := schreierTransversalRightCosetAction (X := X) hT
716 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
717 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
718 intro a b e
719 constructor
720 · exact schreierGenerator_eq_one_implies_mem_prefixTree (X := X) hT e
721 · intro he
722 have hmap :=
723 schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he
724 rw [schreierLabelFunctor_map_of (X := X) hT e] at hmap
725 exact inv_eq_one.mp hmap
728end SchreierPrefixTrees
730end ReidemeisterSchreier.Discrete.OpenSubgroups