FenchelNielsenZomorrodian/Discrete/Singerman/FreeGroupWords.lean
1import ReidemeisterSchreier.Discrete.Presentations.Relators
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Singerman/FreeGroupWords.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Singerman/Reidemeister-Schreier bridge
14Cyclic quotient actions, cyclic product identities, Schreier kernel computations, free-group word identities, and kernel transport for the compact Fuchsian proof.
15-/
17namespace FenchelNielsen
19theorem list_ofFn_one_add {α : Type*} {n : ℕ} (f : Fin (1 + n) → α) :
20 List.ofFn f =
21 f ⟨0, by omega⟩ ::
22 List.ofFn (fun j : Fin n => f ⟨1 + j.val, by omega⟩) := by
23 rw [List.ofFn_congr (show 1 + n = n + 1 by omega)]
24 rw [List.ofFn_succ]
25 simp only [Fin.cast_zero, Fin.mk_zero', List.cons.injEq, List.ofFn_inj, true_and]
26 funext j
27 apply congrArg f
28 ext
29 simp only [Fin.val_cast, Fin.val_succ]
30 omega
32theorem list_ofFn_two_add {α : Type*} {n : ℕ} (f : Fin (2 + n) → α) :
33 List.ofFn f =
34 f ⟨0, by omega⟩ :: f ⟨1, by omega⟩ ::
35 List.ofFn (fun j : Fin n => f ⟨2 + j.val, by omega⟩) := by
36 rw [List.ofFn_congr (show 2 + n = (1 + n) + 1 by omega)]
37 rw [List.ofFn_succ]
38 rw [List.ofFn_congr (show 1 + n = n + 1 by omega)]
39 rw [List.ofFn_succ]
40 simp only [Fin.cast_zero, Fin.succ_zero_eq_one', Fin.mk_zero', List.cons.injEq,
41 List.ofFn_inj, true_and]
42 constructor
43 · apply congrArg f
44 ext
45 simp only [Fin.val_cast, Fin.coe_ofNat_eq_mod, Nat.mod_succ_eq_iff_lt, Nat.succ_eq_add_one,
46 lt_add_iff_pos_left, add_pos_iff, zero_lt_one, true_or]
47 · funext j
48 apply congrArg f
49 ext
50 simp only [Fin.val_cast, Fin.val_succ]
51 omega
53theorem freeGroup_of_pow_ne_one {X : Type*}
54 (x : X) {n : ℕ} (hn : n ≠ 0) :
55 (FreeGroup.of x : FreeGroup X) ^ n ≠ 1 := by
56 classical
57 intro h
58 let χ : X → Multiplicative ℤ :=
59 fun y => if y = x then Multiplicative.ofAdd (1 : ℤ) else 1
60 have hmap := congrArg (FreeGroup.lift χ) h
61 have hn0 : n = 0 := by
62 simpa [χ, map_pow] using hmap
63 exact hn hn0
65private theorem freeGroup_isReduced_pow_mul_of_mul_pow_inv_word {X : Type*}
66 {x y : X} (hxy : x ≠ y) (a b : ℕ) :
67 FreeGroup.IsReduced
68 (List.replicate a (x, true) ++ [(y, true)] ++ List.replicate b (x, false)) := by
69 apply List.IsChain.append
70 · apply List.IsChain.append
71 · exact List.isChain_replicate_of_rel a (by intro _; rfl)
72 · simp only [List.IsChain.singleton]
73 · intro u hu v hv huv
74 simp only [List.head?_cons, Option.mem_def, Option.some.injEq] at hv
75 subst v
76 by_cases ha : a = 0
77 · simp only [ha, List.replicate_zero, List.getLast?_nil, Option.mem_def, reduceCtorEq] at hu
78 · have hlast : u = (x, true) := by
79 simpa [List.getLast?_replicate, ha] using hu.symm
80 subst u
81 exact False.elim (hxy huv)
82 · exact List.isChain_replicate_of_rel b (by intro _; rfl)
83 · intro u hu v hv huv
84 by_cases hb : b = 0
85 · simp only [hb, List.replicate_zero, List.head?_nil, Option.mem_def, reduceCtorEq] at hv
86 · have hvx : v = (x, false) := by
87 simpa [List.head?_replicate, hb] using hv.symm
88 subst v
89 have huy : u = (y, true) := by
90 simpa using hu.symm
91 subst u
92 exact False.elim (hxy huv.symm)
94theorem freeGroup_toWord_pow_mul_of_mul_pow_inv {X : Type*} [DecidableEq X]
95 {x y : X} (hxy : x ≠ y) (a b : ℕ) :
96 FreeGroup.toWord
97 ((FreeGroup.of x : FreeGroup X) ^ a * FreeGroup.of y *
98 ((FreeGroup.of x : FreeGroup X) ^ b)⁻¹) =
99 List.replicate a (x, true) ++ [(y, true)] ++ List.replicate b (x, false) := by
100 let L := List.replicate a (x, true) ++ [(y, true)] ++ List.replicate b (x, false)
101 have hmk :
102 (FreeGroup.of x : FreeGroup X) ^ a * FreeGroup.of y *
103 ((FreeGroup.of x : FreeGroup X) ^ b)⁻¹ =
104 FreeGroup.mk L := by
105 simp only [FreeGroup.of, FreeGroup.pow_mk, List.flatten_replicate_singleton, FreeGroup.mul_mk,
106 FreeGroup.inv_mk, FreeGroup.invRev, List.map_replicate, Bool.not_true, List.reverse_replicate, List.append_assoc,
107 List.cons_append, List.nil_append, L]
108 rw [hmk, FreeGroup.toWord_mk]
109 exact (freeGroup_isReduced_pow_mul_of_mul_pow_inv_word hxy a b).reduce_eq
111private theorem freeGroup_pow_mul_of_mul_pow_inv_word_initialLength {X : Type*} [DecidableEq X]
112 {x y : X} (hxy : x ≠ y) (a b : ℕ) :
113 (List.takeWhile (fun q : X × Bool => q = (x, true))
114 (List.replicate a (x, true) ++ [(y, true)] ++ List.replicate b (x, false))).length =
115 a := by
116 have hyx : (y, true) ≠ (x, true) := by
117 intro h
118 exact hxy (by cases h; rfl)
119 induction a with
121 | succ a _ih => simp [List.replicate_succ, hyx]
123theorem freeGroup_pow_mul_of_mul_pow_inv_left_exponent_eq_of_eq {X : Type*}
124 {x y : X} (hxy : x ≠ y) {a b c d : ℕ}
125 (h :
126 (FreeGroup.of x : FreeGroup X) ^ a * FreeGroup.of y *
127 ((FreeGroup.of x : FreeGroup X) ^ b)⁻¹ =
128 (FreeGroup.of x : FreeGroup X) ^ c * FreeGroup.of y *
129 ((FreeGroup.of x : FreeGroup X) ^ d)⁻¹) :
130 a = c := by
131 classical
132 have hwords := congrArg (fun w : FreeGroup X => FreeGroup.toWord w) h
133 change
134 FreeGroup.toWord
135 ((FreeGroup.of x : FreeGroup X) ^ a * FreeGroup.of y *
136 ((FreeGroup.of x : FreeGroup X) ^ b)⁻¹) =
137 FreeGroup.toWord
138 ((FreeGroup.of x : FreeGroup X) ^ c * FreeGroup.of y *
139 ((FreeGroup.of x : FreeGroup X) ^ d)⁻¹) at hwords
140 rw [freeGroup_toWord_pow_mul_of_mul_pow_inv hxy a b,
141 freeGroup_toWord_pow_mul_of_mul_pow_inv hxy c d] at hwords
142 have htake := congrArg
143 (fun L : List (X × Bool) =>
144 (List.takeWhile (fun q : X × Bool => q = (x, true)) L).length) hwords
145 change
146 (List.takeWhile (fun q : X × Bool => q = (x, true))
147 (List.replicate a (x, true) ++ [(y, true)] ++ List.replicate b (x, false))).length =
148 (List.takeWhile (fun q : X × Bool => q = (x, true))
149 (List.replicate c (x, true) ++ [(y, true)] ++ List.replicate d (x, false))).length at htake
150 rw [freeGroup_pow_mul_of_mul_pow_inv_word_initialLength hxy a b,
151 freeGroup_pow_mul_of_mul_pow_inv_word_initialLength hxy c d] at htake
152 exact htake
154end FenchelNielsen