Source: ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Generators

1import ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Transversals

3/-!

4# Reidemeister Schreier / Discrete / Open Subgroups / Generators

6From a right Schreier transversal, this module constructs canonical

7representatives and Schreier generators, identifies the nontrivial

8representative-generator pairs, and proves their basic action identities.

9-/

11namespace ReidemeisterSchreier.Discrete.OpenSubgroups

13section SchreierGenerators

15open scoped Pointwise

16open FreeGroup

18/--

19The Schreier transversal itself carries the same right-coset action, transported along the

20equivalence with right cosets.

21-/

22@[reducible] noncomputable def schreierTransversalRightCosetAction

23 {X : Type u} [DecidableEq X]

24 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

25 (hT : IsRightSchreierTransversal (X := X) L T) :

26 MulAction (FreeGroup X) T := by

27 letI : MulAction (FreeGroup X) (Quotient (QuotientGroup.rightRel L)) :=

28 rightCosetLeftMulActionByInverse L

29 let e : T ≃ Quotient (QuotientGroup.rightRel L) := hT.1.rightQuotientEquiv.symm

30 refine

31 { smul := fun g t => e.symm (g • e t)

32 one_smul := by

33 intro t

34 change e.symm (1 • e t) = t

35 rw [one_smul]

36 exact e.left_inv t

37 mul_smul := by

38 intro g h t

39 change e.symm ((g * h) • e t) = e.symm (g • e (e.symm (h • e t)))

40 rw [mul_smul, e.apply_symm_apply] }

42/-- The chosen representative of a right coset attached to a right Schreier transversal. -/

43noncomputable def schreierRepresentative {X : Type u} [DecidableEq X]

44 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

45 (hT : IsRightSchreierTransversal (X := X) L T) :

46 FreeGroup X → T :=

47 hT.1.toRightFun

49/-- An element of the Schreier transversal is its own chosen representative. -/

50@[simp] theorem schreierRepresentative_eq_of_mem {X : Type u} [DecidableEq X]

51 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

52 (hT : IsRightSchreierTransversal (X := X) L T)

53 {t : FreeGroup X} (ht : t ∈ T) :

54 schreierRepresentative (X := X) hT t = ⟨t, ht⟩ := by

55 apply (Subgroup.isComplement_iff_existsUnique_mul_inv_mem.mp hT.1 t).unique

56 · exact hT.1.mul_inv_toRightFun_mem t

57 · simp only [mul_inv_cancel, SetLike.mem_coe, one_mem]

59/-- Every element of the subgroup has the identity as its chosen Schreier representative. -/

60@[simp] theorem schreierRepresentative_eq_one_of_mem {X : Type u} [DecidableEq X]

61 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

62 (hT : IsRightSchreierTransversal (X := X) L T)

63 {g : FreeGroup X} (hg : g ∈ L) :

64 schreierRepresentative (X := X) hT g = ⟨1, hT.2.1⟩ := by

65 apply (Subgroup.isComplement_iff_existsUnique_mul_inv_mem.mp hT.1 g).unique

66 · exact hT.1.mul_inv_toRightFun_mem g

67 · simpa using hg

69/--

70If \(t\) lies in the transversal and \(g t^{-1}\) lies in the subgroup, then \(t\) is the

71chosen representative of \(g\).

72-/

73theorem schreierRepresentative_eq_of_mem_mul_inv_mem {X : Type u} [DecidableEq X]

74 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

75 (hT : IsRightSchreierTransversal (X := X) L T)

76 {g t : FreeGroup X} (ht : t ∈ T) (hgt : g * t⁻¹ ∈ L) :

77 schreierRepresentative (X := X) hT g = ⟨t, ht⟩ := by

78 apply (Subgroup.isComplement_iff_existsUnique_mul_inv_mem.mp hT.1 g).unique

79 · exact hT.1.mul_inv_toRightFun_mem g

80 · exact hgt

82/-- Membership of a word in the prefix tree implies membership of its prefix parent. -/

83theorem prefixParent_mem_of_mem {X : Type u} [DecidableEq X]

84 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

85 (hT : IsRightSchreierTransversal (X := X) L T)

86 {t : FreeGroup X} (ht : t ∈ T) :

87 FreeGroup.prefixParent t ∈ T := by

88 refine hT.2.2 ht ?_

89 refine ⟨(FreeGroup.toWord t).length - 1, Nat.sub_le (FreeGroup.toWord t).length 1, ?_⟩

90 simp only [prefixParent, List.dropLast_eq_take]

92/--

93The right-coset action updates a Schreier representative by multiplying on the right and then

94choosing the representative of the resulting coset.

95-/

96theorem schreierTransversalRightCosetAction_smul {X : Type u} [DecidableEq X]

97 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

98 (hT : IsRightSchreierTransversal (X := X) L T)

99 (g : FreeGroup X) (t : T) :

100 letI := schreierTransversalRightCosetAction (X := X) hT

101 g • t = schreierRepresentative (X := X) hT ((t : FreeGroup X) * g⁻¹) := by

102 let e : T ≃ Quotient (QuotientGroup.rightRel L) := hT.1.rightQuotientEquiv.symm

103 have ht : e t = Quotient.mk'' (t : FreeGroup X) := by

104 simpa [e] using (hT.1.mk''_rightQuotientEquiv (e t)).symm

105 change

106 hT.1.rightQuotientEquiv (g • hT.1.rightQuotientEquiv.symm t) =

107 hT.1.rightQuotientEquiv (Quotient.mk'' ((t : FreeGroup X) * g⁻¹))

108 rw [ht, rightCosetLeftMulActionByInverse_mk_smul]

109

110/-- The Schreier expression attached to any word \(t\) and basis element \(x\). -/

111noncomputable def schreierGenerator {X : Type u} [DecidableEq X]

112 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

113 (hT : IsRightSchreierTransversal (X := X) L T) (t : FreeGroup X) (x : X) : L := by

114 refine

115 ⟨t * FreeGroup.of x *

116 ((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X)⁻¹, ?_⟩

117 exact hT.1.mul_inv_toRightFun_mem (t * FreeGroup.of x)

118

119/--

120The canonical index type for the nontrivial Schreier generators attached to a right Schreier

121transversal. This pair-indexed type is the preferred basis index; the value-set Schreier

122generator set records the same nontrivial generators by their subgroup values.

123-/

124abbrev NontrivialSchreierPair {X : Type u} [DecidableEq X]

125 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

126 (hT : IsRightSchreierTransversal (X := X) L T) : Type u :=

127 {p : T × X // schreierGenerator (X := X) hT ((p.1 : T) : FreeGroup X) p.2 ≠ 1}

128

129/-- The Schreier generator value represented by a nontrivial Schreier pair. -/

130noncomputable def nontrivialSchreierPairGenerator {X : Type u} [DecidableEq X]

131 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

132 (hT : IsRightSchreierTransversal (X := X) L T) :

133 NontrivialSchreierPair (X := X) hT → L :=

134 fun p => schreierGenerator (X := X) hT ((p.1.1 : T) : FreeGroup X) p.1.2

135

136/--

137The Schreier generator or pair map is evaluated by the chosen section and coset representative.

138-/

139@[simp] theorem nontrivialSchreierPairGenerator_apply {X : Type u} [DecidableEq X]

140 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

141 (hT : IsRightSchreierTransversal (X := X) L T)

142 (p : NontrivialSchreierPair (X := X) hT) :

143 nontrivialSchreierPairGenerator (X := X) hT p =

144 schreierGenerator (X := X) hT ((p.1.1 : T) : FreeGroup X) p.1.2 :=

145 rfl

146

147/--

148The classical Schreier generator value set attached to a right Schreier transversal. This value

149set records the resulting Schreier generators, while the nontrivial Schreier pairs provide the

150preferred basis index.

151-/

152def schreierGeneratorSet {X : Type u} [DecidableEq X]

153 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

154 (hT : IsRightSchreierTransversal (X := X) L T) : Set L :=

155 {z | ∃ t ∈ T, ∃ x : X, z = schreierGenerator (X := X) hT t x ∧ z ≠ 1}

156

157/-- Membership in the Schreier generator set is equivalent to the displayed generator condition. -/

158@[simp] theorem mem_schreierGeneratorSet_iff {X : Type u} [DecidableEq X]

159 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

160 {hT : IsRightSchreierTransversal (X := X) L T} {z : L} :

161 z ∈ schreierGeneratorSet (X := X) hT ↔

162 ∃ t ∈ T, ∃ x : X, z = schreierGenerator (X := X) hT t x ∧ z ≠ 1 :=

163 Iff.rfl

164

165/--

166A nontrivial Schreier generator associated to an element of the transversal lies in the Schreier

167generator set.

168-/

169theorem schreierGenerator_mem_schreierGeneratorSet_of_mem_of_ne_one

170 {X : Type u} [DecidableEq X]

171 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

172 (hT : IsRightSchreierTransversal (X := X) L T)

173 {t : FreeGroup X} (ht : t ∈ T) (x : X)

174 (hne : schreierGenerator (X := X) hT t x ≠ 1) :

175 schreierGenerator (X := X) hT t x ∈ schreierGeneratorSet (X := X) hT :=

176 ⟨t, ht, x, rfl, hne⟩

177

178/-- A nontrivial Schreier generator belongs to the Schreier generator set. -/

179theorem schreierGenerator_mem_schreierGeneratorSet_of_ne_one

180 {X : Type u} [DecidableEq X]

181 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

182 (hT : IsRightSchreierTransversal (X := X) L T)

183 (t : T) (x : X)

184 (hne : schreierGenerator (X := X) hT (t : FreeGroup X) x ≠ 1) :

185 schreierGenerator (X := X) hT (t : FreeGroup X) x ∈

186 schreierGeneratorSet (X := X) hT :=

187 schreierGenerator_mem_schreierGeneratorSet_of_mem_of_ne_one

188 (X := X) hT t.property x hne

189

190/-- The value-set formulation is precisely the range of the pair-indexed generator map. -/

191theorem schreierGeneratorSet_eq_range_nontrivialSchreierPairGenerator

192 {X : Type u} [DecidableEq X]

193 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

194 (hT : IsRightSchreierTransversal (X := X) L T) :

195 schreierGeneratorSet (X := X) hT =

196 Set.range (nontrivialSchreierPairGenerator (X := X) hT) := by

197 ext z

198 constructor

199 · intro hz

200 rcases hz with ⟨t, ht, x, hz, hne⟩

201 refine ⟨⟨(⟨t, ht⟩, x), ?_⟩, ?_⟩

202 · simpa [hz] using hne

203 · simp only [nontrivialSchreierPairGenerator, hz]

204 · rintro ⟨p, rfl⟩

205 exact schreierGenerator_mem_schreierGeneratorSet_of_ne_one

206 (X := X) hT p.1.1 p.1.2 p.2

207

208/-- The Schreier generator is trivial exactly in the corresponding subgroup-membership case. -/

209@[simp] theorem schreierGenerator_eq_one_of_mem {X : Type u} [DecidableEq X]

210 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

211 (hT : IsRightSchreierTransversal (X := X) L T)

212 {t : FreeGroup X} {x : X}

213 (htx : t * FreeGroup.of x ∈ T) :

214 schreierGenerator (X := X) hT t x = 1 := by

215 apply Subtype.ext

216 simp only [schreierGenerator, schreierRepresentative_eq_of_mem (X := X) hT htx, mul_inv_rev,

217 mul_assoc,

218 mul_inv_cancel_left, mul_inv_cancel, OneMemClass.coe_one]

219

220/--

221If the representative-generator product lies in the subgroup, the corresponding Schreier

222generator is the represented subgroup element.

223-/

224@[simp] theorem schreierGenerator_eq_of_mul_mem {X : Type u} [DecidableEq X]

225 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

226 (hT : IsRightSchreierTransversal (X := X) L T)

227 {t : FreeGroup X} {x : X}

228 (htx : t * FreeGroup.of x ∈ L) :

229 schreierGenerator (X := X) hT t x = ⟨t * FreeGroup.of x, htx⟩ := by

230 apply Subtype.ext

231 simp only [schreierGenerator, schreierRepresentative_eq_one_of_mem (X := X) hT htx, inv_one,

232 mul_one]

233

234/-- The Schreier generator is trivial exactly under the corresponding coset condition. -/

235theorem schreierGenerator_eq_one_iff {X : Type u} [DecidableEq X]

236 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

237 {hT : IsRightSchreierTransversal (X := X) L T}

238 {t : FreeGroup X} {x : X} :

239 schreierGenerator (X := X) hT t x = 1 ↔

240 ((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X) =

241 t * FreeGroup.of x := by

242 constructor

243 · intro h

244 have hval : t * FreeGroup.of x *

245 (((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X))⁻¹ = 1 := by

246 exact congrArg Subtype.val h

247 have hmul := congrArg

248 (fun g : FreeGroup X =>

249 g * ((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X)) hval

250 simpa [mul_assoc] using hmul.symm

251 · intro hrep

252 apply Subtype.ext

253 simp only [schreierGenerator, hrep, mul_inv_rev, mul_assoc, mul_inv_cancel_left, mul_inv_cancel,

254 OneMemClass.coe_one]

255

256

257/--

258Pointed discrete Reidemeister--Schreier statement: if \(x^N\) is the first positive power of a

259free generator landing in \(L\), one may choose a right Schreier transversal whose distinguished

260Schreier generator is exactly \(x^N\).

261-/

262theorem exists_rightSchreierTransversal_of_minimalGeneratorPower

263 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} (x : X) {N : ℕ}

264 (hN : 0 < N)

265 (hpow : (FreeGroup.of x) ^ N ∈ L)

266 (hmin : ∀ m : ℕ, 0 < m → m < N → (FreeGroup.of x) ^ m ∉ L) :

267 ∃ T : Set (FreeGroup X), ∃ hT : IsRightSchreierTransversal (X := X) L T,

268 (FreeGroup.of x) ^ (N - 1) ∈ T ∧

269 schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x =

270 ⟨(FreeGroup.of x) ^ N, hpow⟩ := by

271 let T₀ : Set (FreeGroup X) := Set.range fun i : Fin N => (FreeGroup.of x) ^ (i : ℕ)

272 have hT₀ : IsRightPartialSchreierTransversal (X := X) L T₀ :=

273 isRightPartialSchreierTransversal_generatorPowers_of_minimalPower

274 (X := X) (L := L) x hN hmin

275 rcases exists_rightSchreierTransversal_of_partial (X := X) (L := L) hT₀ with

276 ⟨T, hsub, hT⟩

277 have hpred : (FreeGroup.of x) ^ (N - 1) ∈ T := by

278 apply hsub

279 exact ⟨⟨N - 1, Nat.pred_lt (Nat.ne_of_gt hN)⟩, rfl⟩

280 have hmul :

281 (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x = (FreeGroup.of x) ^ N := by

282 calc

283 (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x = (FreeGroup.of x) ^ ((N - 1).succ) := by

284 rw [pow_succ]

285 _ = (FreeGroup.of x) ^ N := by

286 simpa using congrArg (fun n : ℕ => (FreeGroup.of x) ^ n) (Nat.succ_pred_eq_of_pos hN)

287 have hmul_mem : (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x ∈ L := by

288 rw [hmul]

289 exact hpow

290 refine ⟨T, hT, hpred, ?_⟩

291 calc

292 schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x =

293 ⟨(FreeGroup.of x) ^ (N - 1) * FreeGroup.of x, hmul_mem⟩ := by

294 exact schreierGenerator_eq_of_mul_mem (X := X) hT hmul_mem

295 _ = ⟨(FreeGroup.of x) ^ N, hpow⟩ := by

296 apply Subtype.ext

297 exact hmul

298

299/--

300If the last letter of a transversal word cancels with x, the Schreier representative of t x is

301the prefix parent of t.

302-/

303theorem schreierRepresentative_eq_prefixParent_of_cancels {X : Type u} [DecidableEq X]

304 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

305 (hT : IsRightSchreierTransversal (X := X) L T)

306 {t : FreeGroup X} {x : X}

307 (ht : t ∈ T) (hw : FreeGroup.toWord t ≠ [])

308 (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :

309 schreierRepresentative (X := X) hT (t * FreeGroup.of x) =

310 ⟨FreeGroup.prefixParent t, prefixParent_mem_of_mem (X := X) hT ht⟩ := by

311 rw [Internal.FreeGroupWord.FreeGroup.mul_of_eq_prefixParent_of_cancels t x hw hlast]

312 exact schreierRepresentative_eq_of_mem (X := X) hT (prefixParent_mem_of_mem (X := X) hT ht)

313

314/--

315If a transversal word ends in x, the Schreier representative of its prefix parent multiplied by

316x is the original word.

317-/

318theorem schreierRepresentative_eq_of_prefixParent_last_pos {X : Type u} [DecidableEq X]

319 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

320 (hT : IsRightSchreierTransversal (X := X) L T)

321 {t : FreeGroup X} (ht : t ∈ T) {x : X}

322 (hw : FreeGroup.toWord t ≠ [])

323 (hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :

324 schreierRepresentative (X := X) hT (FreeGroup.prefixParent t * FreeGroup.of x) = ⟨t, ht⟩ := by

325 rw [Internal.FreeGroupWord.FreeGroup.prefixParent_mul_of_of_last_pos t x hw hlast]

326 exact schreierRepresentative_eq_of_mem (X := X) hT ht

327

328/--

329If the last letter of a transversal word cancels with x, the corresponding Schreier generator is

330trivial.

331-/

332@[simp] theorem schreierGenerator_eq_one_of_cancels {X : Type u} [DecidableEq X]

333 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

334 (hT : IsRightSchreierTransversal (X := X) L T)

335 {t : FreeGroup X} {x : X}

336 (ht : t ∈ T) (hw : FreeGroup.toWord t ≠ [])

337 (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :

338 schreierGenerator (X := X) hT t x = 1 := by

339 apply schreierGenerator_eq_one_of_mem (X := X) hT

340 rw [Internal.FreeGroupWord.FreeGroup.mul_of_eq_prefixParent_of_cancels t x hw hlast]

341 exact prefixParent_mem_of_mem (X := X) hT ht

342

343/--

344If a transversal word ends in x, the Schreier generator attached to its prefix parent and x is

345trivial.

346-/

347@[simp] theorem schreierGenerator_eq_one_of_prefixParent_last_pos {X : Type u} [DecidableEq X]

348 {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

349 (hT : IsRightSchreierTransversal (X := X) L T)

350 {t : FreeGroup X} (ht : t ∈ T) {x : X}

351 (hw : FreeGroup.toWord t ≠ [])

352 (hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :

353 schreierGenerator (X := X) hT (FreeGroup.prefixParent t) x = 1 := by

354 apply schreierGenerator_eq_one_of_mem (X := X) hT

355 rw [Internal.FreeGroupWord.FreeGroup.prefixParent_mul_of_of_last_pos t x hw hlast]

356 exact ht

357

358

359end SchreierGenerators

360

361end ReidemeisterSchreier.Discrete.OpenSubgroups