Source: ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Transversals

1import Mathlib.GroupTheory.Schreier

2import ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Words.Basic

4/-!

5# Reidemeister Schreier / Discrete / Open Subgroups / Transversals

7This module defines full and partial right Schreier transversals in free

8groups, proves their complement and prefix-closure properties, and supplies

9the existence and extension results used later.

10-/

12namespace ReidemeisterSchreier.Discrete.OpenSubgroups

14section RightSchreierTransversals

16open scoped Pointwise

17open FreeGroup

19/--

20A right Schreier transversal is a right transversal containing every initial segment of each of

21its elements.

22-/

23def IsRightSchreierTransversal {X : Type u} [DecidableEq X]

24 (L : Subgroup (FreeGroup X)) (T : Set (FreeGroup X)) : Prop :=

25 Subgroup.IsComplement (L : Set (FreeGroup X)) T ∧

26 (1 : FreeGroup X) ∈ T ∧

27 ∀ ⦃t : FreeGroup X⦄, t ∈ T → freeGroupInitialSegments t ⊆ T

29/--

30A right partial Schreier transversal is prefix-closed, contains 1, and meets each right coset in

31at most one element.

32-/

33def IsRightPartialSchreierTransversal {X : Type u} [DecidableEq X]

34 (L : Subgroup (FreeGroup X)) (T : Set (FreeGroup X)) : Prop :=

35 (1 : FreeGroup X) ∈ T ∧

36 (∀ ⦃t : FreeGroup X⦄, t ∈ T → freeGroupInitialSegments t ⊆ T) ∧

37 ∀ ⦃a b : FreeGroup X⦄, a ∈ T → b ∈ T →

38 (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =

39 Quotient.mk'' b → a = b

41/-- A right Schreier transversal gives the required complement to the subgroup action. -/

42theorem IsRightSchreierTransversal.isComplement {X : Type u} [DecidableEq X]

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

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

45 Subgroup.IsComplement (L : Set (FreeGroup X)) T :=

46 hT.1

48/-- A right Schreier transversal contains the identity word. -/

49theorem IsRightSchreierTransversal.one_mem {X : Type u} [DecidableEq X]

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

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

52 (1 : FreeGroup X) ∈ T :=

53 hT.2.1

55/-- A right Schreier transversal is closed under initial segments. -/

56theorem IsRightSchreierTransversal.prefix_closed {X : Type u} [DecidableEq X]

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

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

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

60 freeGroupInitialSegments t ⊆ T :=

61 hT.2.2 ht

63/-- A right partial Schreier transversal contains the identity word. -/

64theorem IsRightPartialSchreierTransversal.one_mem {X : Type u} [DecidableEq X]

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

66 (hT : IsRightPartialSchreierTransversal (X := X) L T) :

67 (1 : FreeGroup X) ∈ T :=

68 hT.1

70/-- A right partial Schreier transversal is closed under initial segments. -/

71theorem IsRightPartialSchreierTransversal.prefix_closed {X : Type u} [DecidableEq X]

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

73 (hT : IsRightPartialSchreierTransversal (X := X) L T)

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

75 freeGroupInitialSegments t ⊆ T :=

76 hT.2.1 ht

78/-- Two right Schreier transversal representatives are equal when their right quotients agree. -/

79theorem IsRightPartialSchreierTransversal.eq_of_rightQuotient_eq

80 {X : Type u} [DecidableEq X]

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

82 (hT : IsRightPartialSchreierTransversal (X := X) L T)

83 {a b : FreeGroup X} (ha : a ∈ T) (hb : b ∈ T)

84 (hEq :

85 (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =

86 Quotient.mk'' b) :

87 a = b :=

88 hT.2.2 ha hb hEq

90/-- The prefix parent of a partial Schreier word satisfies the required membership condition. -/

91theorem prefixParent_mem_of_partial {X : Type u} [DecidableEq X]

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

93 (hT : IsRightPartialSchreierTransversal (X := X) L T)

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

95 FreeGroup.prefixParent t ∈ T := by

96 exact hT.2.1 ht ⟨(FreeGroup.toWord t).length - 1, Nat.sub_le (FreeGroup.toWord t).length 1, by

97 simp only [prefixParent, List.dropLast_eq_take]⟩

99/--

100A nonempty chain of right partial Schreier transversals has a union that is again a right

101partial Schreier transversal. This is the chain-upper-bound step used in the Zorn construction.

102-/

103theorem chain_sUnion_isRightPartialSchreierTransversal

104 {X : Type u} [DecidableEq X]

105 {L : Subgroup (FreeGroup X)} {c : Set (Set (FreeGroup X))}

106 (hcn : c.Nonempty)

107 (hc :

108 ∀ ⦃s⦄, s ∈ c → ∀ ⦃t⦄, t ∈ c → s ≠ t → s ⊆ t ∨ t ⊆ s)

109 (hcPartial :

110 ∀ ⦃s⦄, s ∈ c → IsRightPartialSchreierTransversal (X := X) L s) :

111 IsRightPartialSchreierTransversal (X := X) L (⋃₀ c) := by

112 refine ⟨?_, ?_, ?_⟩

113 · rcases hcn with ⟨s, hs⟩

114 exact Set.mem_sUnion_of_mem ((hcPartial hs).1) hs

115 · intro t ht u hu

116 rcases Set.mem_sUnion.mp ht with ⟨s, hs, hts⟩

117 exact Set.mem_sUnion.mpr ⟨s, hs, (hcPartial hs).2.1 hts hu⟩

118 · intro a b ha hb hab

119 rcases Set.mem_sUnion.mp ha with ⟨s, hs, has⟩

120 rcases Set.mem_sUnion.mp hb with ⟨t, ht, hbt⟩

121 by_cases hst : s = t

122 · subst hst

123 exact (hcPartial ht).2.2 has hbt hab

124 · rcases hc hs ht hst with hst' | hts'

125 · exact (hcPartial ht).2.2 (hst' has) hbt hab

126 · exact (hcPartial hs).2.2 has (hts' hbt) hab

127

128/-- Every right partial Schreier transversal extends to a full right Schreier transversal. -/

129theorem exists_rightSchreierTransversal_of_partial {X : Type u} [DecidableEq X]

130 {L : Subgroup (FreeGroup X)} {T₀ : Set (FreeGroup X)}

131 (hT₀ : IsRightPartialSchreierTransversal (X := X) L T₀) :

132 ∃ T : Set (FreeGroup X), T₀ ⊆ T ∧ IsRightSchreierTransversal (X := X) L T := by

133 classical

134 let S : Set (Set (FreeGroup X)) :=

135 {T | T₀ ⊆ T ∧ IsRightPartialSchreierTransversal (X := X) L T}

136 have hT₀S : T₀ ∈ S := by

137 exact ⟨Set.Subset.rfl, hT₀⟩

138 obtain ⟨T, hTS, hTmax⟩ :=

139 zorn_subset_nonempty S

140 (fun c hcS hc hcn => by

141 refine ⟨⋃₀ c, ?_, ?_⟩

142 · refine ⟨?_, ?_⟩

143 · intro t ht

144 rcases hcn with ⟨s, hs⟩

145 exact Set.mem_sUnion_of_mem ((hcS hs).1 ht) hs

146 · exact chain_sUnion_isRightPartialSchreierTransversal

147 (X := X) (L := L) hcn (fun {s} hs {t} ht hst => hc hs ht hst)

148 (fun {s} hs => (hcS hs).2)

149 · intro s hs

150 exact Set.subset_sUnion_of_mem hs)

151 T₀ hT₀S

152 have hTpartial : IsRightPartialSchreierTransversal (X := X) L T := hTmax.prop.2

153 have hTcover :

154 ∀ g : FreeGroup X,

155 ∃ t ∈ T,

156 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel L)) = Quotient.mk'' g := by

157 intro g

158 by_contra hnog

159 let Missing : FreeGroup X → Prop := fun w =>

160 ∀ t ∈ T,

161 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel L)) ≠ Quotient.mk'' w

162 have hmissing : Missing g := by

163 intro t ht hEq

164 exact hnog ⟨t, ht, hEq⟩

165 let P : ℕ → Prop := fun n =>

166 ∃ w : FreeGroup X, Missing w ∧ (FreeGroup.toWord w).length = n

167 have hP : ∃ n, P n := ⟨(FreeGroup.toWord g).length, g, hmissing, rfl⟩

168 let n := Nat.find hP

169 obtain ⟨w, hwmiss, hwlen⟩ := Nat.find_spec hP

170 have hmin : ∀ u : FreeGroup X, Missing u → n ≤ (FreeGroup.toWord u).length := by

171 intro u hu

172 exact Nat.find_min' hP ⟨u, hu, rfl⟩

173 have hw1 : w ≠ 1 := by

174 intro hw1

175 exact hwmiss 1 hTpartial.1 (by simp only [hw1])

176 have hwword : FreeGroup.toWord w ≠ [] := by

177 exact mt (FreeGroup.toWord_eq_nil_iff.mp) hw1

178 let y : X × Bool := (FreeGroup.toWord w).getLast hwword

179 let u : FreeGroup X := FreeGroup.prefixParent w

180 have huWitness :

181 ∃ t ∈ T,

182 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel L)) = Quotient.mk'' u := by

183 by_contra hu

184 have humiss : Missing u := by

185 intro t ht hEq

186 exact hu ⟨t, ht, hEq⟩

187 have hlt : (FreeGroup.toWord u).length < n := by

188 simpa [u, n, hwlen] using

189 Internal.FreeGroupWord.FreeGroup.toWord_length_prefixParent_lt (t := w) hw1

190 exact (Nat.not_lt_of_ge (hmin u humiss)) hlt

191 obtain ⟨t, htT, htq⟩ := huWitness

192 let z : FreeGroup X := t * FreeGroup.mk [y]

193 have hzq :

194 (Quotient.mk'' z : Quotient (QuotientGroup.rightRel L)) = Quotient.mk'' w := by

195 apply Quotient.sound'

196 have hrel : QuotientGroup.rightRel L t u := Quotient.exact' htq

197 rw [QuotientGroup.rightRel_apply] at hrel ⊢

198 have hwrep :

199 u * FreeGroup.mk [y] = w := by

200 exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_mk_singleton_of_last

201 w y hwword (by rfl)

202 have hzw : w * z⁻¹ = u * t⁻¹ := by

203 have hcancelWord :

204 FreeGroup.mk [y] * FreeGroup.mk (FreeGroup.invRev [y]) = (1 : FreeGroup X) := by

205 rw [← FreeGroup.inv_mk (L := [y])]

206 exact mul_inv_cancel (FreeGroup.mk [y])

207 have hcancelWord' :

208 FreeGroup.mk (y :: FreeGroup.invRev [y]) = (1 : FreeGroup X) := by

209 simpa using hcancelWord

210 have htail :

211 FreeGroup.mk [y] * (FreeGroup.mk (FreeGroup.invRev [y]) * t⁻¹) =

212 FreeGroup.mk (y :: FreeGroup.invRev [y]) * t⁻¹ := by

213 calc

214 FreeGroup.mk [y] * (FreeGroup.mk (FreeGroup.invRev [y]) * t⁻¹)

215 = (FreeGroup.mk [y] * FreeGroup.mk (FreeGroup.invRev [y])) * t⁻¹ := by

216 rw [mul_assoc]

217 _ = FreeGroup.mk (y :: FreeGroup.invRev [y]) * t⁻¹ := by

218 rw [FreeGroup.mul_mk]

219 rfl

220 calc

221 w * z⁻¹ = (u * FreeGroup.mk [y]) * z⁻¹ := by rw [hwrep]

222 _ = (u * FreeGroup.mk [y]) * (t * FreeGroup.mk [y])⁻¹ := by rfl

223 _ = (u * FreeGroup.mk [y]) * (FreeGroup.mk (FreeGroup.invRev [y]) * t⁻¹) := by

224 simp only [mul_inv_rev, FreeGroup.inv_mk]

225 _ = u * (FreeGroup.mk [y] * (FreeGroup.mk (FreeGroup.invRev [y]) * t⁻¹)) := by

226 rw [← mul_assoc, ← mul_assoc, mul_assoc]

227 _ = u * (FreeGroup.mk (y :: FreeGroup.invRev [y]) * t⁻¹) := by

228 exact congrArg (fun x => u * x) htail

229 _ = u * (1 * t⁻¹) := by rw [hcancelWord']

230 _ = u * t⁻¹ := by simp only [one_mul]

231 simpa [hzw] using hrel

232 by_cases hcancel :

233 ∃ hw' : FreeGroup.toWord t ≠ [],

234 (FreeGroup.toWord t).getLast hw' = (y.1, !y.2)

235 · rcases hcancel with ⟨hw', hlast'⟩

236 have hzEqPrefix : z = FreeGroup.prefixParent t := by

237 simpa [z, FreeGroup.prefixParent] using

238 Internal.FreeGroupWord.FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels

239 t y hw' hlast'

240 have hzT : z ∈ T := by

241 simpa [hzEqPrefix] using prefixParent_mem_of_partial (X := X) (L := L) hTpartial htT

242 exact hwmiss z hzT hzq

243 · have hzWord : FreeGroup.toWord z = FreeGroup.toWord t ++ [y] :=

244 Internal.FreeGroupWord.FreeGroup.toWord_mul_mk_singleton_of_not_cancels t y hcancel

245 let U : Set (FreeGroup X) := Set.insert z T

246 have hzPrefix : freeGroupInitialSegments z ⊆ U := by

247 intro v hv

248 rcases hv with ⟨m, hm, rfl⟩

249 have hlenz : (FreeGroup.toWord z).length = (FreeGroup.toWord t).length + 1 := by

250 rw [hzWord]

251 simp only [List.length_append, List.length_cons, List.length_nil, zero_add]

252 have hm' : m ≤ (FreeGroup.toWord t).length + 1 := by

253 simpa [hlenz] using hm

254 rcases Nat.eq_or_lt_of_le hm' with hmEq | hmLt

255 · left

256 have hmz : m = (FreeGroup.toWord z).length := by

257 simpa [hlenz] using hmEq

258 have htake : List.take m (FreeGroup.toWord z) = FreeGroup.toWord z := by

259 rw [hmz, List.take_length]

260 rw [htake]

261 exact FreeGroup.mk_toWord (x := z)

262 · right

263 have hmle : m ≤ (FreeGroup.toWord t).length := Nat.lt_succ_iff.mp hmLt

264 have htake : List.take m (FreeGroup.toWord z) = List.take m (FreeGroup.toWord t) := by

265 rw [hzWord, List.take_append_of_le_length hmle]

266 rw [htake]

267 exact hTpartial.2.1 htT ⟨m, hmle, rfl⟩

268 have hUin : U ∈ S := by

269 refine ⟨?_, ?_⟩

270 · intro s hs

271 exact Or.inr (hTmax.prop.1 hs)

272 · refine ⟨Or.inr hTpartial.1, ?_, ?_⟩

273 · intro s hs

274 rcases hs with rfl | hsT

275 · exact hzPrefix

276 · intro v hv

277 exact Or.inr (hTpartial.2.1 hsT hv)

278 · intro a b ha hb hab

279 rcases ha with rfl | haT

280 · rcases hb with rfl | hbT

281 · rfl

282 · exfalso

283 exact hwmiss b hbT (hab.symm.trans hzq)

284 · rcases hb with rfl | hbT

285 · exfalso

286 exact hwmiss a haT (hab.trans hzq)

287 · exact hTpartial.2.2 haT hbT hab

288 have hTU : T = U := hTmax.eq_of_subset hUin (by intro s hs; exact Or.inr hs)

289 have hzT : z ∈ T := by

290 have hzU : z ∈ U := by

291 change z ∈ Set.insert z T

292 exact Set.mem_insert z T

293 exact hTU.symm ▸ hzU

294 exact hwmiss z hzT hzq

295 refine ⟨T, hTmax.prop.1, ?_⟩

296 refine ⟨?_, hTpartial.1, hTpartial.2.1⟩

297 rw [Subgroup.isComplement_iff_existsUnique_mul_inv_mem]

298 intro g

299 rcases hTcover g with ⟨t, htT, htq⟩

300 refine ⟨⟨t, htT⟩, ?_, ?_⟩

301 · have hrel : QuotientGroup.rightRel L t g := Quotient.exact' htq

302 simpa [QuotientGroup.rightRel_apply] using hrel

303 · intro t' hmem

304 apply Subtype.ext

305 apply hTpartial.2.2 t'.2 htT

306 calc

307 (Quotient.mk'' (t' : FreeGroup X) :

308 Quotient (QuotientGroup.rightRel L)) =

309 Quotient.mk'' g := by

310 apply Quotient.sound'

311 rw [QuotientGroup.rightRel_apply]

312 simpa using hmem

313 _ = Quotient.mk'' t := htq.symm

314

315/-- Every subgroup of a free group admits a right Schreier transversal. -/

316theorem exists_rightSchreierTransversal {X : Type u} [DecidableEq X]

317 (L : Subgroup (FreeGroup X)) :

318 ∃ T : Set (FreeGroup X), IsRightSchreierTransversal (X := X) L T := by

319 let T₀ : Set (FreeGroup X) := {(1 : FreeGroup X)}

320 have hT₀ : IsRightPartialSchreierTransversal (X := X) L T₀ := by

321 refine ⟨by simp only [Set.mem_singleton_iff, T₀], ?_, ?_⟩

322 · intro t ht u hu

323 have ht1 : t = 1 := by

324 simpa [T₀] using ht

325 subst t

326 rcases hu with ⟨n, hn, hu⟩

327 have hn0 : n = 0 := Nat.eq_zero_of_le_zero (by simpa using hn)

328 subst hn0

329 change u = (1 : FreeGroup X)

330 exact hu.trans FreeGroup.one_eq_mk.symm

331 · intro a b ha hb _

332 have ha1 : a = 1 := by

333 simpa [T₀] using ha

334 have hb1 : b = 1 := by

335 simpa [T₀] using hb

336 subst a

337 subst b

338 rfl

339 rcases exists_rightSchreierTransversal_of_partial (X := X) (L := L) hT₀ with ⟨T, _, hT⟩

340 exact ⟨T, hT⟩

341

342/--

343If two generator powers determine the same right quotient, their difference lies in the

344subgroup.

345-/

346theorem generatorPower_sub_mem_of_rightQuotient_eq {X : Type u}

347 {L : Subgroup (FreeGroup X)} (x : X) {m n : ℕ} (hmn : m ≤ n)

348 (hEq :

349 (Quotient.mk'' ((FreeGroup.of x) ^ m) : Quotient (QuotientGroup.rightRel L)) =

350 Quotient.mk'' ((FreeGroup.of x) ^ n)) :

351 (FreeGroup.of x) ^ (n - m) ∈ L := by

352 have hrel : QuotientGroup.rightRel L ((FreeGroup.of x) ^ m) ((FreeGroup.of x) ^ n) :=

353 Quotient.exact' hEq

354 rw [QuotientGroup.rightRel_apply] at hrel

355 have hcalc :

356 (FreeGroup.of x) ^ n * (((FreeGroup.of x) ^ m)⁻¹) =

357 (FreeGroup.of x) ^ (n - m) := by

358 calc

359 (FreeGroup.of x) ^ n * (((FreeGroup.of x) ^ m)⁻¹)

360 = (FreeGroup.of x) ^ ((n - m) + m) * (((FreeGroup.of x) ^ m)⁻¹) := by

361 rw [Nat.sub_add_cancel hmn]

362 _ = (((FreeGroup.of x) ^ (n - m)) * (FreeGroup.of x) ^ m) *

363 (((FreeGroup.of x) ^ m)⁻¹) := by

364 rw [pow_add]

365 _ = (FreeGroup.of x) ^ (n - m) := by simp only [mul_assoc, mul_inv_cancel, mul_one]

366 exact hcalc ▸ hrel

367

368/--

369The representatives built from minimal generator powers form a right partial Schreier

370transversal.

371-/

372theorem isRightPartialSchreierTransversal_generatorPowers_of_minimalPower

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

374 (hN : 0 < N)

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

376 IsRightPartialSchreierTransversal (X := X) L

377 (Set.range fun i : Fin N => (FreeGroup.of x) ^ (i : ℕ)) := by

378 refine ⟨?_, ?_, ?_⟩

379 · exact ⟨⟨0, hN⟩, by simp only [pow_zero]⟩

380 · intro t ht u hu

381 rcases ht with ⟨i, rfl⟩

382 rcases hu with ⟨m, hm, rfl⟩

383 have hm' : m ≤ (i : ℕ) := by

384 simpa [FreeGroup.toWord_of_pow, List.length_replicate] using hm

385 refine ⟨⟨m, lt_of_le_of_lt hm' i.2⟩, ?_⟩

386 rw [FreeGroup.toWord_of_pow, List.take_replicate, min_eq_left hm',

387 ← FreeGroup.toWord_of_pow, FreeGroup.mk_toWord]

388 · intro a b ha hb hEq

389 rcases ha with ⟨i, rfl⟩

390 rcases hb with ⟨j, rfl⟩

391 have hij : (i : ℕ) = j := by

392 by_contra hij

393 rcases lt_or_gt_of_ne hij with hijlt | hjilt

394 · have hmem : (FreeGroup.of x) ^ ((j : ℕ) - i) ∈ L :=

395 generatorPower_sub_mem_of_rightQuotient_eq (X := X) (L := L) x

396 (Nat.le_of_lt hijlt) hEq

397 exact hmin ((j : ℕ) - i) (Nat.sub_pos_of_lt hijlt)

398 (lt_of_le_of_lt (Nat.sub_le _ _) j.2) hmem

399 · have hmem : (FreeGroup.of x) ^ ((i : ℕ) - j) ∈ L :=

400 generatorPower_sub_mem_of_rightQuotient_eq (X := X) (L := L) x

401 (Nat.le_of_lt hjilt) hEq.symm

402 exact hmin ((i : ℕ) - j) (Nat.sub_pos_of_lt hjilt)

403 (lt_of_le_of_lt (Nat.sub_le _ _) i.2) hmem

404 have hij' : i = j := Fin.ext hij

405 subst hij'

406 rfl

407

408/--

409Right multiplication on right cosets, expressed as a left action via \(g \cdot [t] = [t *

410g{}^{-1}]\). This is the action naturally compatible with Schreier generators of the form \(t x

411(\widetilde{t x}){}^{-1}\).

412-/

413instance rightCosetLeftMulActionByInverse {X : Type u} (L : Subgroup (FreeGroup X)) :

414 MulAction (FreeGroup X) (Quotient (QuotientGroup.rightRel L)) where

415 smul g :=

416 Quotient.map' (fun a => a * g⁻¹) fun a b hab => by

417 rw [QuotientGroup.rightRel_apply] at hab ⊢

418 simpa [mul_assoc] using hab

419 one_smul q := by

420 refine Quotient.inductionOn' q ?_

421 intro a

422 apply Quotient.sound'

423 rw [QuotientGroup.rightRel_apply]

424 simp only [inv_one, mul_one, mul_inv_cancel, one_mem]

425 mul_smul g h q := by

426 refine Quotient.inductionOn' q ?_

427 intro a

428 apply Quotient.sound'

429 rw [QuotientGroup.rightRel_apply]

430 simp only [mul_assoc, mul_inv_rev, inv_inv, inv_mul_cancel_left, mul_inv_cancel, one_mem]

431

432/-- The Schreier generator component of the corresponding rewriting map. -/

433@[simp] theorem rightCosetLeftMulActionByInverse_mk_smul {X : Type u}

434 (L : Subgroup (FreeGroup X)) (g a : FreeGroup X) :

435 g • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =

436 Quotient.mk'' (a * g⁻¹) :=

437 rfl

438

439end RightSchreierTransversals

440

441end ReidemeisterSchreier.Discrete.OpenSubgroups