FenchelNielsenZomorrodian/Discrete/Singerman/CyclicProductIdentities.lean

1import FenchelNielsenZomorrodian.Discrete.Singerman.FreeGroupWords

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Singerman/CyclicProductIdentities.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

18def conjugateRangeProduct {G : Type*} [Group G] (x t : G) (n : ℕ) : G :=

19 ((List.finRange n).map fun k : Fin n => x ^ (k : ℕ) * t * (x ^ (k : ℕ))⁻¹).prod

20theorem MonoidHom.map_list_prod_ofFn₂

21 {M N : Type*} [Monoid M] [Monoid N] (f : M →* N) {p n : ℕ}

22 (g : Fin p → Fin n → M) :

23 f ((List.ofFn (fun k : Fin p => (List.ofFn (fun j : Fin n => g k j)).prod)).prod) =

24 (List.ofFn (fun k : Fin p =>

25 (List.ofFn (fun j : Fin n => f (g k j))).prod)).prod := by

26 rw [map_list_prod]

27 rw [List.map_ofFn]

28 congr

29 funext k

30 change f ((List.ofFn (fun j : Fin n => g k j)).prod) =

31 (List.ofFn (fun j : Fin n => f (g k j))).prod

32 rw [map_list_prod]

33 rw [List.map_ofFn]

34 rfl

35theorem list_ofFn_reverse_last_desc {α : Type*} {p : ℕ} (hp : 0 < p)

36 (B : Fin p → α) :

37 (List.ofFn B).reverse =

38 B ⟨p - 1, by omega⟩ ::

39 List.ofFn (fun i : Fin (p - 1) => B ⟨p - 2 - i.val, by omega⟩) := by

40 apply List.ext_get

41 · simp only [List.length_reverse, List.length_ofFn, List.length_cons]

42 omega

43 · intro i h₁ h₂

44 rw [List.get_reverse' (List.ofFn B) ⟨i, h₁⟩ (by simp only [List.length_ofFn]; omega)]

45 cases i with

46 | zero =>

47 simp only [List.length_ofFn, tsub_zero, List.get_eq_getElem, List.getElem_ofFn, List.length_cons,

48 Fin.zero_eta, Fin.coe_ofNat_eq_mod, Nat.zero_mod, List.getElem_cons_zero]

49 | succ i =>

50 have hleft : p - 1 - (i + 1) = p - 2 - i := by omega

51 simp only [List.length_ofFn, hleft, List.get_eq_getElem, List.getElem_ofFn, List.length_cons,

52 List.getElem_cons_succ]

53theorem descending_block_inv_product_eq {G : Type*} [Group G] {p : ℕ} (hp : 0 < p)

54 (A : G) (B : Fin p → G) :

55 (B ⟨p - 1, by omega⟩ * A)⁻¹ *

56 (List.ofFn (fun i : Fin (p - 1) => (B ⟨p - 2 - i.val, by omega⟩)⁻¹)).prod =

57 A⁻¹ * (List.ofFn B).prod⁻¹ := by

58 have hrev := list_ofFn_reverse_last_desc hp B

59 have hprod :

60 (B ⟨p - 1, by omega⟩)⁻¹ *

61 (List.ofFn (fun i : Fin (p - 1) => (B ⟨p - 2 - i.val, by omega⟩)⁻¹)).prod =

62 (List.ofFn B).prod⁻¹ := by

63 rw [List.prod_inv_reverse]

64 rw [← List.map_reverse]

65 rw [hrev]

66 rw [List.map_cons, List.prod_cons, List.map_ofFn]

67 rfl

68 calc

69 (B ⟨p - 1, by omega⟩ * A)⁻¹ *

70 (List.ofFn (fun i : Fin (p - 1) => (B ⟨p - 2 - i.val, by omega⟩)⁻¹)).prod

71 = A⁻¹ *

72 ((B ⟨p - 1, by omega⟩)⁻¹ *

73 (List.ofFn (fun i : Fin (p - 1) => (B ⟨p - 2 - i.val, by omega⟩)⁻¹)).prod) := by

74 group

75 _ = A⁻¹ * (List.ofFn B).prod⁻¹ := by rw [hprod]

76/-- Expanding a conjugate range product over a finite list gives the corresponding block product. -/

77theorem conjugateRangeProduct_list_prod_eq_blocks

78 {G : Type*} [Group G] (x : G) {n : ℕ} (t : Fin n → G) (p : ℕ) :

79 conjugateRangeProduct x (List.ofFn t).prod p =

80 (List.ofFn (fun k : Fin p =>

81 (List.ofFn (fun j : Fin n =>

82 x ^ (k : ℕ) * t j * (x ^ (k : ℕ))⁻¹)).prod)).prod := by

83 unfold conjugateRangeProduct

84 rw [← List.ofFn_eq_map]

85 congr

86 funext k

87 calc

88 x ^ (k : ℕ) * (List.ofFn t).prod * (x ^ (k : ℕ))⁻¹ =

89 (List.map (fun u => x ^ (k : ℕ) * u * (x ^ (k : ℕ))⁻¹) (List.ofFn t)).prod := by

90 exact ReidemeisterSchreier.Discrete.Presentations.conjugate_list_prod (x ^ (k : ℕ)) (List.ofFn t)

91 _ = (List.ofFn (fun j : Fin n => x ^ (k : ℕ) * t j * (x ^ (k : ℕ))⁻¹)).prod := by

92 rw [List.map_ofFn]

93 rfl

94/-- Successor recursion for `conjugateRangeProduct`. -/

95theorem conjugateRangeProduct_succ {G : Type*} [Group G] (x t : G) (n : ℕ) :

96 conjugateRangeProduct x t (n + 1) =

97 conjugateRangeProduct x t n * (x ^ n * t * (x ^ n)⁻¹) := by

98 unfold conjugateRangeProduct

99 rw [List.finRange_succ_last, List.map_append, List.prod_append, List.map_map]

100 have hmap :

101 List.map ((fun k : Fin (n + 1) => x ^ (k : ℕ) * t * (x ^ (k : ℕ))⁻¹) ∘

102 Fin.castSucc) (List.finRange n) =

103 List.map (fun k : Fin n => x ^ (k : ℕ) * t * (x ^ (k : ℕ))⁻¹)

104 (List.finRange n) := by

105 apply List.map_congr_left

106 intro k _hk

107 simp only [Function.comp_apply, Fin.val_castSucc]

108 rw [hmap]

109 simp only [List.map_cons, Fin.val_last, List.map_nil, List.prod_cons, List.prod_nil, mul_one]

110theorem pow_mul_pow_mul_conjugateRangeProduct_eq_one_of_mul_eq_one

111 {G : Type*} [Group G] (x y t : G) (n : ℕ) (h : x * y * t = 1) :

112 x ^ n * y ^ n * conjugateRangeProduct x t n = 1 := by

113 induction n with

114 | zero =>

115 simp only [pow_zero, mul_one, conjugateRangeProduct, List.finRange_zero, List.map_nil, List.prod_nil]

116 | succ n ih =>

117 rw [conjugateRangeProduct_succ]

118 have hP : conjugateRangeProduct x t n = (x ^ n * y ^ n)⁻¹ := by

119 apply eq_inv_of_mul_eq_one_right

120 simpa [mul_assoc] using ih

121 rw [hP, pow_succ x n, pow_succ y n]

122 calc

123 (x ^ n * x) * (y ^ n * y) *

124 ((x ^ n * y ^ n)⁻¹ * (x ^ n * t * (x ^ n)⁻¹))

125 = x ^ n * (x * y * t) * (x ^ n)⁻¹ := by group

126 _ = 1 := by simp only [h, mul_one, mul_inv_cancel]

127/-- Block-product form of `pow_mul_pow_mul_conjugateRangeProduct_eq_one_of_mul_eq_one`. -/

128theorem pow_mul_pow_mul_conjugateBlockProduct_eq_one_of_mul_eq_one

129 {G : Type*} [Group G] (x y : G) {n : ℕ} (t : Fin n → G) (p : ℕ)

130 (h : x * y * (List.ofFn t).prod = 1) :

131 x ^ p * y ^ p *

132 (List.ofFn (fun k : Fin p =>

133 (List.ofFn (fun j : Fin n =>

134 x ^ (k : ℕ) * t j * (x ^ (k : ℕ))⁻¹)).prod)).prod = 1 := by

135 rw [← conjugateRangeProduct_list_prod_eq_blocks]

136 exact pow_mul_pow_mul_conjugateRangeProduct_eq_one_of_mul_eq_one x y (List.ofFn t).prod p h

137theorem pow_mul_pow_mul_conjugateBlockProduct_mem_normalClosure_of_mul_mem_normalClosure

138 {G : Type*} [Group G] {R : Set G} (x y : G) {n : ℕ} (t : Fin n → G) (p : ℕ)

139 (h : x * y * (List.ofFn t).prod ∈ Subgroup.normalClosure R) :

140 x ^ p * y ^ p *

141 (List.ofFn (fun k : Fin p =>

142 (List.ofFn (fun j : Fin n =>

143 x ^ (k : ℕ) * t j * (x ^ (k : ℕ))⁻¹)).prod)).prod ∈

144 Subgroup.normalClosure R := by

145 let N : Subgroup G := Subgroup.normalClosure R

146 let q : G →* G ⧸ N := QuotientGroup.mk' N

147 have hRel :

148 q x * q y * (List.ofFn (fun j : Fin n => q (t j))).prod = 1 := by

149 have hq : q (x * y * (List.ofFn t).prod) = 1 := by

150 exact (QuotientGroup.eq_one_iff (N := N) (x * y * (List.ofFn t).prod)).2 h

151 simpa [q, map_mul, map_list_prod] using hq

152 have hBlock :

153 q x ^ p * q y ^ p *

154 (List.ofFn (fun k : Fin p =>

155 (List.ofFn (fun j : Fin n =>

156 q x ^ (k : ℕ) * q (t j) * (q x ^ (k : ℕ))⁻¹)).prod)).prod = 1 :=

157 pow_mul_pow_mul_conjugateBlockProduct_eq_one_of_mul_eq_one

158 (q x) (q y) (fun j : Fin n => q (t j)) p hRel

159 have hqTarget :

160 q

161 (x ^ p * y ^ p *

162 (List.ofFn (fun k : Fin p =>

163 (List.ofFn (fun j : Fin n =>

164 x ^ (k : ℕ) * t j * (x ^ (k : ℕ))⁻¹)).prod)).prod) = 1 := by

165 calc

166 q

167 (x ^ p * y ^ p *

168 (List.ofFn (fun k : Fin p =>

169 (List.ofFn (fun j : Fin n =>

170 x ^ (k : ℕ) * t j * (x ^ (k : ℕ))⁻¹)).prod)).prod)

171 =

172 q x ^ p * q y ^ p *

173 (List.ofFn (fun k : Fin p =>

174 q ((List.ofFn (fun j : Fin n =>

175 x ^ (k : ℕ) * t j * (x ^ (k : ℕ))⁻¹)).prod))).prod := by

176 rw [map_mul, map_mul, map_pow, map_pow, map_list_prod]

177 rw [List.map_ofFn]

178 rfl

179 _ =

180 q x ^ p * q y ^ p *

181 (List.ofFn (fun k : Fin p =>

182 (List.ofFn (fun j : Fin n =>

183 q x ^ (k : ℕ) * q (t j) * (q x ^ (k : ℕ))⁻¹)).prod)).prod := by

184 congr

185 funext k

186 rw [map_list_prod]

187 rw [List.map_ofFn]

188 apply congrArg List.prod

189 rw [List.ofFn_inj]

190 funext j

191 simp only [QuotientGroup.coe_mk', Function.comp_apply, QuotientGroup.mk_mul, QuotientGroup.mk_pow,

192 QuotientGroup.mk_inv, QuotientGroup.mk'_apply, q]

193 _ = 1 := hBlock

194 exact

195 (QuotientGroup.eq_one_iff (N := N)

196 (x ^ p * y ^ p *

197 (List.ofFn (fun k : Fin p =>

198 (List.ofFn (fun j : Fin n =>

199 x ^ (k : ℕ) * t j * (x ^ (k : ℕ))⁻¹)).prod)).prod)).1 hqTarget

200def negOneCycleTailProduct {G : Type*} [Group G] (x y : G) (n : ℕ) : G :=

201 (List.ofFn (fun i : Fin n =>

202 x ^ (n - i.val) * y * (x ^ (n - 1 - i.val))⁻¹)).prod

203/-- Successor recursion for `negOneCycleTailProduct`. -/

204theorem negOneCycleTailProduct_succ {G : Type*} [Group G] (x y : G) (n : ℕ) :

205 negOneCycleTailProduct x y (n + 1) =

206 x ^ (n + 1) * y * (x ^ n)⁻¹ * negOneCycleTailProduct x y n := by

207 unfold negOneCycleTailProduct

208 rw [List.ofFn_succ, List.prod_cons]

209 simp only [Fin.val_zero, tsub_zero, Nat.add_sub_cancel_right]

210 congr 1

211 apply congrArg List.prod

212 rw [List.ofFn_inj]

213 funext i

214 have hi : i.val < n := i.isLt

215 have hsub : n - (i.val + 1) = n - 1 - i.val := by omega

216 simp only [Fin.val_succ, Nat.reduceSubDiff, hsub]

217/-- Closed form for `negOneCycleTailProduct`. -/

218theorem negOneCycleTailProduct_eq {G : Type*} [Group G] (x y : G) (n : ℕ) :

219 negOneCycleTailProduct x y n = x ^ n * y ^ n := by

220 induction n with

221 | zero =>

222 simp only [negOneCycleTailProduct, zero_tsub, pow_zero, one_mul, inv_one, mul_one, List.ofFn_zero,

223 List.prod_nil]

224 | succ n ih =>

225 rw [negOneCycleTailProduct_succ, ih]

226 rw [pow_succ]

227 group

228theorem negOneCycleProduct_eq_pow {G : Type*} [Group G] (x y : G) (n : ℕ) :

229 y * (x ^ n)⁻¹ * negOneCycleTailProduct x y n = y ^ (n + 1) := by

230 rw [negOneCycleTailProduct_eq]

231 rw [pow_succ']

232 group

233end FenchelNielsen