FenchelNielsenZomorrodian/Discrete/Singerman/CyclicSchreierKernel.lean

1import FenchelNielsenZomorrodian.Discrete.Core.EllipticQuotientHom

2import FenchelNielsenZomorrodian.Discrete.Singerman.CyclicQuotientActions

4/-

5PUBLIC_PAGE_SNAPSHOT

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

7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Singerman/CyclicSchreierKernel.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

11-/

12/-!

13# Singerman/Reidemeister-Schreier bridge

15Cyclic quotient actions, cyclic product identities, Schreier kernel computations, free-group word identities, and kernel transport for the compact Fuchsian proof.

16-/

18namespace FenchelNielsen

19def CyclicSchreierRelatorData

20 {X Y : Type} [DecidableEq X] {N : ℕ} [NeZero N] {rels : Set (FreeGroup X)}

21 (f : X → Multiplicative (ZMod N))

22 (x : X)

23 (hx : FreeGroup.lift f (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))

24 (targetRelators : Set (FreeGroup Y)) : Type :=

25 (let φ : FreeGroup X →* Multiplicative (ZMod N) := FreeGroup.lift f

26 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

27 let hT : IsRightSchreierTransversal φ.ker T :=

28 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

29 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=

30 freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator φ x hx

31 ReidemeisterSchreier.Discrete.Presentations.RelatorQuotientMutualMapData

32 (ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e

33 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := rels) T))

34 targetRelators)

35noncomputable def cyclicSchreierKernelEquivPresentedGroupOfRelatorData

36 {X Y : Type} [DecidableEq X] {N : ℕ} [NeZero N] {rels : Set (FreeGroup X)}

37 (f : X → Multiplicative (ZMod N))

38 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1)

39 (x : X)

40 (hx : FreeGroup.lift f (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))

41 (targetRelators : Set (FreeGroup Y))

42 (hData : CyclicSchreierRelatorData (rels := rels) f x hx targetRelators) :

43 (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker ≃*

44 PresentedGroup targetRelators := by

45 classical

46 let φ : FreeGroup X →* Multiplicative (ZMod N) := FreeGroup.lift f

47 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

48 let hT : IsRightSchreierTransversal φ.ker T :=

49 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

50 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=

51 freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator φ x hx

52 let R : Set (FreeGroup ↥(schreierGeneratorSet hT)) :=

53 ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e

54 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := rels) T)

55 let hTarget :

56 FreeGroup ↥(schreierGeneratorSet hT) ⧸ Subgroup.normalClosure R ≃*

57 PresentedGroup targetRelators :=

58 ReidemeisterSchreier.Discrete.Presentations.quotientEquivOfRelatorQuotientMutualMapData R targetRelators

59 (by simpa [CyclicSchreierRelatorData, φ, T, hT, e, R] using hData)

60 let hKernel :

61 FreeGroup ↥(schreierGeneratorSet hT) ⧸ Subgroup.normalClosure R ≃*

62 (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker := by

63 simpa [φ, T, hT, e, R] using

64 (presentedFreeKernelCyclicSchreierRelatorQuotientEquivPresentedKernel

65 (N := N) (rels := rels) (f := f) hrels x hx)

66 exact hKernel.symm.trans hTarget

68def FuchsianEllipticCyclicRelatorData

69 {p : ℕ} [NeZero p] {Y : Type} (σ : FuchsianSignature)

70 (ξ : Fin σ.numPeriods → Multiplicative (ZMod p))

71 (i₀ : Fin σ.numPeriods)

72 (hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod p))

73 (targetRelators : Set (FreeGroup Y)) : Type :=

74 (letI := Classical.decEq (FuchsianGenerator σ)

75 let f := ellipticQuotientGeneratorImage σ ξ

76 let x := FuchsianGenerator.elliptic i₀

77 let hx :

78 FreeGroup.lift f (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by

79 simp only [FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage, hi₀, f, x]

80 CyclicSchreierRelatorData (N := p) (rels := relators σ) f x hx targetRelators)

82def FuchsianEllipticCyclicSchreierRelatorData

83 {p : ℕ} [NeZero p] (σ τ : FuchsianSignature)

84 (ξ : Fin σ.numPeriods → Multiplicative (ZMod p))

85 (i₀ : Fin σ.numPeriods)

86 (hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod p)) : Type :=

87 FuchsianEllipticCyclicRelatorData σ ξ i₀ hi₀ (relators τ)

89noncomputable def fuchsianEllipticCyclicKernelEquivPresentedGroupOfRelatorData

90 {p : ℕ} [NeZero p] {Y : Type} (σ : FuchsianSignature)

91 (ξ : Fin σ.numPeriods → Multiplicative (ZMod p))

92 (hpow : ∀ i, ξ i ^ σ.periods i = 1)

93 (hprod : ∏ i : Fin σ.numPeriods, ξ i = 1)

94 (i₀ : Fin σ.numPeriods)

95 (hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod p))

96 (targetRelators : Set (FreeGroup Y))

97 (D : FuchsianEllipticCyclicRelatorData σ ξ i₀ hi₀ targetRelators) :

98 (ellipticQuotientHom σ ξ hpow hprod).ker ≃*

99 PresentedGroup targetRelators := by

100 classical

101 letI := Classical.decEq (FuchsianGenerator σ)

102 let f := ellipticQuotientGeneratorImage σ ξ

103 let x := FuchsianGenerator.elliptic i₀

104 let hx :

105 FreeGroup.lift f (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by

106 simp only [FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage, hi₀, f, x]

107 let hrels : ∀ r ∈ relators σ, FreeGroup.lift f r = 1 :=

108 ellipticQuotientGeneratorImage_respects_relators σ ξ hpow hprod

109 have hD :

110 CyclicSchreierRelatorData (N := p) (rels := relators σ) f x hx targetRelators := by

111 simpa [FuchsianEllipticCyclicRelatorData, f, x, hx] using D

112 simpa [ellipticQuotientHom, f, x, hx, hrels] using

113 cyclicSchreierKernelEquivPresentedGroupOfRelatorData

114 (N := p) (rels := relators σ) f hrels x hx targetRelators hD

115

116noncomputable def fuchsianEllipticCyclicKernelEquivOfRelatorData

117 {p : ℕ} [NeZero p] (σ τ : FuchsianSignature)

118 (ξ : Fin σ.numPeriods → Multiplicative (ZMod p))

119 (hpow : ∀ i, ξ i ^ σ.periods i = 1)

120 (hprod : ∏ i : Fin σ.numPeriods, ξ i = 1)

121 (i₀ : Fin σ.numPeriods)

122 (hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod p))

123 (D : FuchsianEllipticCyclicSchreierRelatorData σ τ ξ i₀ hi₀) :

124 (ellipticQuotientHom σ ξ hpow hprod).ker ≃*

125 FuchsianPresentedGroup τ :=

126 fuchsianEllipticCyclicKernelEquivPresentedGroupOfRelatorData

127 σ ξ hpow hprod i₀ hi₀ (relators τ) D

128theorem freeGroupGeneratorPower_mem_range_cyclicQuotientRightRep

129 {X : Type*} {N : ℕ}

130 (φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)

131 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))

132 {m : ℕ} (hm : m < N) :

133 (FreeGroup.of x) ^ m ∈ Set.range (cyclicQuotientRightRep φ (FreeGroup.of x)) := by

134 classical

135 letI : NeZero N := ⟨Nat.ne_of_gt (lt_of_le_of_lt (Nat.zero_le m) hm)⟩

136 refine ⟨Quotient.mk'' ((FreeGroup.of x) ^ m), ?_⟩

137 have hφm : φ ((FreeGroup.of x) ^ m) = Multiplicative.ofAdd ((m : ℕ) : ZMod N) := by

138 rw [map_pow, hx]

139 apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective

140 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, mul_one]

141 have hval : (Multiplicative.toAdd (φ ((FreeGroup.of x) ^ m))).val = m := by

142 rw [hφm]

143 simpa using (ZMod.val_natCast_of_lt hm)

144 change (FreeGroup.of x) ^ (Multiplicative.toAdd (φ ((FreeGroup.of x) ^ m))).val =

145 (FreeGroup.of x) ^ m

146 rw [hval]

147private theorem freeGroupGeneratorPower_mul_generator_mem_range_cyclicQuotientRightRep

148 {X : Type*} {N : ℕ}

149 (φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)

150 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))

151 {k : ℕ} (hk : k + 1 < N) :

152 (FreeGroup.of x) ^ k * FreeGroup.of x ∈

153 Set.range (cyclicQuotientRightRep φ (FreeGroup.of x)) := by

154 simpa [pow_succ] using

155 freeGroupGeneratorPower_mem_range_cyclicQuotientRightRep φ x hx (m := k + 1) hk

156theorem cyclicQuotient_distinguished_schreierGenerator_eq_one_of_succ_lt

157 {X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]

158 (φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)

159 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))

160 {k : ℕ} (hk : k + 1 < N) :

161 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

162 let hT : IsRightSchreierTransversal φ.ker T :=

163 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

164 schreierGenerator hT ((FreeGroup.of x) ^ k) x = 1 := by

165 classical

166 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

167 let hT : IsRightSchreierTransversal φ.ker T :=

168 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

169 exact schreierGenerator_eq_one_of_mem hT

170 (freeGroupGeneratorPower_mul_generator_mem_range_cyclicQuotientRightRep φ x hx hk)

171theorem cyclicQuotient_distinguished_schreierGenerator_wrap_eq

172 {X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]

173 (φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)

174 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N)) :

175 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

176 let hT : IsRightSchreierTransversal φ.ker T :=

177 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

178 schreierGenerator hT ((FreeGroup.of x) ^ (N - 1)) x =

179 (⟨(FreeGroup.of x) ^ N, by

180 rw [MonoidHom.mem_ker]

181 rw [map_pow, hx]

182 apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective

183 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩ : φ.ker) := by

184 classical

185 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

186 let hT : IsRightSchreierTransversal φ.ker T :=

187 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

188 apply Subtype.ext

189 have hpowKer : (FreeGroup.of x) ^ N ∈ φ.ker := by

190 rw [MonoidHom.mem_ker]

191 rw [map_pow, hx]

192 apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective

193 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]

194 have hNpos : 0 < N := Nat.pos_of_ne_zero (NeZero.ne N)

195 have hsucc : N - 1 + 1 = N := Nat.sub_add_cancel (Nat.succ_le_iff.mpr hNpos)

196 have hprod : (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x = (FreeGroup.of x) ^ N := by

197 rw [← pow_succ, hsucc]

198 have hprodKer : (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x ∈ φ.ker := by

199 simpa [hprod] using hpowKer

200 simp only [schreierGenerator, hprod, schreierRepresentative_eq_one_of_mem hT hpowKer, inv_one, mul_one]

201theorem cyclicQuotient_trivialImage_schreierGenerator_eq_conj

202 {X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]

203 (φ : FreeGroup X →* Multiplicative (ZMod N)) (x y : X)

204 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))

205 (hy : φ (FreeGroup.of y) = 1) (k : Fin N) :

206 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

207 let hT : IsRightSchreierTransversal φ.ker T :=

208 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

209 schreierGenerator hT ((FreeGroup.of x) ^ k.val) y =

210 (⟨(FreeGroup.of x) ^ k.val * FreeGroup.of y *

211 ((FreeGroup.of x) ^ k.val)⁻¹, by

212 rw [MonoidHom.mem_ker]

213 simp only [map_mul, map_pow, hx, hy, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker) := by

214 classical

215 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

216 let hT : IsRightSchreierTransversal φ.ker T :=

217 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

218 let t : FreeGroup X := (FreeGroup.of x) ^ k.val

219 have ht : t ∈ T := by

220 simpa [T, t] using

221 freeGroupGeneratorPower_mem_range_cyclicQuotientRightRep φ x hx (m := k.val) k.isLt

222 have hker : (t * FreeGroup.of y) * t⁻¹ ∈ φ.ker := by

223 rw [MonoidHom.mem_ker]

224 simp only [map_mul, map_pow, hx, hy, mul_one, map_inv, mul_inv_cancel, t]

225 apply Subtype.ext

226 simp only [schreierGenerator, schreierRepresentative_eq_of_mem_mul_inv_mem hT ht hker, t]

227theorem cyclicQuotient_negOneImage_schreierGenerator_eq

228 {X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]

229 (φ : FreeGroup X →* Multiplicative (ZMod N)) (x y : X)

230 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))

231 (hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod N)) (k : Fin N) :

232 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

233 let hT : IsRightSchreierTransversal φ.ker T :=

234 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

235 let r : ℕ := ((k.val : ZMod N) - 1).val

236 schreierGenerator hT ((FreeGroup.of x) ^ k.val) y =

237 (⟨(FreeGroup.of x) ^ k.val * FreeGroup.of y *

238 ((FreeGroup.of x) ^ r)⁻¹, by

239 rw [MonoidHom.mem_ker]

240 rw [map_mul, map_inv, map_mul, map_pow, map_pow, hx, hy]

241 apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective

242 simp only [ofAdd_neg, toAdd_mul, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, mul_one, toAdd_inv, ZMod.natCast_val,

243 dvd_refl, ZMod.cast_sub, ZMod.cast_natCast, ZMod.cast_one, neg_sub, toAdd_one, r]

244 ring⟩ : φ.ker) := by

245 classical

246 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

247 let hT : IsRightSchreierTransversal φ.ker T :=

248 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

249 let r : ℕ := ((k.val : ZMod N) - 1).val

250 let t : FreeGroup X := (FreeGroup.of x) ^ k.val

251 let u : FreeGroup X := (FreeGroup.of x) ^ r

252 have hu : u ∈ T := by

253 simpa [T, u, r] using

254 freeGroupGeneratorPower_mem_range_cyclicQuotientRightRep

255 φ x hx (m := r) (ZMod.val_lt ((k.val : ZMod N) - 1))

256 have hker : (t * FreeGroup.of y) * u⁻¹ ∈ φ.ker := by

257 rw [MonoidHom.mem_ker]

258 rw [map_mul, map_inv, map_mul, map_pow, map_pow, hx, hy]

259 apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective

260 simp only [ofAdd_neg, toAdd_mul, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, mul_one, toAdd_inv, ZMod.natCast_val,

261 dvd_refl, ZMod.cast_sub, ZMod.cast_natCast, ZMod.cast_one, neg_sub, toAdd_one, r]

262 ring

263 apply Subtype.ext

264 simp only [schreierGenerator, schreierRepresentative_eq_of_mem_mul_inv_mem hT hu hker, u, r, t]

265end FenchelNielsen