Source: ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.PrefixTree

1import Mathlib.GroupTheory.Schreier

2import ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Generators

3import ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Words.NielsenSchreierCompat

4import ProCGroups.ReidemeisterSchreier.FreeGroup.Automorphisms

6/-!

7# Reidemeister Schreier / Discrete / Open Subgroups / Prefix Tree

9This module constructs the Schreier prefix tree from a right transversal,

10proves its positive and negative edge criteria, and relates its complement

11edges to the nontrivial Schreier generators.

12-/

14namespace ReidemeisterSchreier.Discrete.OpenSubgroups

16section SchreierPrefixTrees

18open scoped Pointwise

19open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj Quiver FreeGroup

21/--

22The parent vertex of a nontrivial prefix-parent edge of a Schreier transversal again lies in the

23transversal.

24-/

25theorem prefixParentEdge_mem_transversal {X : Type u} [DecidableEq X]

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

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

28 (t : T) (ht1 : (t : FreeGroup X) ≠ 1) :

29 (FreeGroup.prefixParentEdgeOfNeOne (X := X) (t := (t : FreeGroup X)) ht1).parent ∈ T := by

30 rw [FreeGroup.prefixParentEdgeOfNeOne_parent]

31 exact prefixParent_mem_of_mem (X := X) hT t.property

33/-- Every nonidentity transversal representative is reached from its prefix parent by an inverse-basis edge. -/

34theorem exists_inverseBasis_edge_of_ne_one {X : Type u} [DecidableEq X]

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

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

37 (t : T) (ht1 : (t : FreeGroup X) ≠ 1) :

38 ∃ x : X,

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

40 (FreeGroup.inverseBasis X x •

41 (⟨FreeGroup.prefixParent (t : FreeGroup X),

42 prefixParent_mem_of_mem (X := X) hT t.property⟩ : T) = t) ∨

43 (FreeGroup.inverseBasis X x • t =

44 (⟨FreeGroup.prefixParent (t : FreeGroup X),

45 prefixParent_mem_of_mem (X := X) hT t.property⟩ : T)) := by

46 let edge := FreeGroup.prefixParentEdgeOfNeOne (X := X) (t := (t : FreeGroup X)) ht1

47 have hlastEdge :

48 FreeGroup.lastLetter? (t : FreeGroup X) = some edge.letter :=

49 FreeGroup.prefixParentEdgeOfNeOne_lastLetter? (X := X) (t := (t : FreeGroup X)) ht1

50 rcases hletter : edge.letter with ⟨x, b⟩

51 cases b with

52 | false =>

53 have hlast? :

54 FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, false) : Internal.SignedLetter X) := by

55 simpa [edge, hletter] using hlastEdge

56 rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff

57 (g := (t : FreeGroup X)) (y := ((x, false) : Internal.SignedLetter X))).1 hlast? with

58 ⟨hw, hlast⟩

59 refine ⟨x, Or.inr ?_⟩

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

61 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),

62 prefixParent_mem_of_mem (X := X) hT t.property⟩

63 rw [FreeGroup.inverseBasis_apply,

64 schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ t]

65 simpa [p] using

66 schreierRepresentative_eq_prefixParent_of_cancels (X := X) hT t.property hw hlast

67 | true =>

68 have hlast? :

69 FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, true) : Internal.SignedLetter X) := by

70 simpa [edge, hletter] using hlastEdge

71 rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff

72 (g := (t : FreeGroup X)) (y := ((x, true) : Internal.SignedLetter X))).1 hlast? with

73 ⟨hw, hlast⟩

74 refine ⟨x, Or.inl ?_⟩

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

76 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),

77 prefixParent_mem_of_mem (X := X) hT t.property⟩

78 rw [FreeGroup.inverseBasis_apply,

79 schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ p]

80 simpa [p] using

81 schreierRepresentative_eq_of_prefixParent_last_pos (X := X) hT t.property hw hlast

83/--

84The canonical prefix tree on the Schreier transversal. Its unique incoming edge for a non-root

85vertex is determined by the last letter of the reduced word of that vertex.

86-/

87noncomputable def schreierPrefixTree {X : Type u} [DecidableEq X]

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

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

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

91 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

92 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

93 WideSubquiver

94 (Quiver.Symmetrify <| IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)) := by

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

96 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

97 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

98 exact fun a b =>

99 { e |

100 ∃ hw : FreeGroup.toWord (((show ActionCategory (FreeGroup X) T from b).back : T) :

101 FreeGroup X) ≠ [],

102 let tb : T := (show ActionCategory (FreeGroup X) T from b).back

103 let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),

104 prefixParent_mem_of_mem (X := X) hT tb.property⟩

105 (show ActionCategory (FreeGroup X) T from a).back = pb ∧

106 match e with

107 | Sum.inl g => (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, true)

108 | Sum.inr g => (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, false) }

109

110/--

111Membership in the left branch of the Schreier prefix tree is equivalent to the displayed prefix

112condition.

113-/

114theorem mem_schreierPrefixTree_inl_iff {X : Type u} [DecidableEq X]

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

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

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

118 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

119 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

120 ∀ {a b : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)}

121 {g : a ⟶ b},

122 (Sum.inl g :

123 @Quiver.Hom

124 (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))

125 inferInstance a b) ∈

126 schreierPrefixTree (X := X) hT a b ↔

127 ∃ hw : FreeGroup.toWord ((((show ActionCategory (FreeGroup X) T from b).back : T)) :

128 FreeGroup X) ≠ [],

129 let tb : T := (show ActionCategory (FreeGroup X) T from b).back

130 let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),

131 prefixParent_mem_of_mem (X := X) hT tb.property⟩

132 (show ActionCategory (FreeGroup X) T from a).back = pb ∧

133 (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, true) := by

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

135 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

136 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

137 intro a b g

138 rfl

139

140/--

141Membership in the right branch of the Schreier prefix tree is equivalent to the displayed prefix

142condition.

143-/

144theorem mem_schreierPrefixTree_inr_iff {X : Type u} [DecidableEq X]

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

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

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

148 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

149 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

150 ∀ {a b : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)}

151 {g : b ⟶ a},

152 (Sum.inr g :

153 @Quiver.Hom

154 (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))

155 inferInstance a b) ∈

156 schreierPrefixTree (X := X) hT a b ↔

157 ∃ hw : FreeGroup.toWord ((((show ActionCategory (FreeGroup X) T from b).back : T)) :

158 FreeGroup X) ≠ [],

159 let tb : T := (show ActionCategory (FreeGroup X) T from b).back

160 let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),

161 prefixParent_mem_of_mem (X := X) hT tb.property⟩

162 (show ActionCategory (FreeGroup X) T from a).back = pb ∧

163 (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, false) := by

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

165 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

166 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

167 intro a b g

168 rfl

169

170/-- A positive final letter determines the forward edge from the prefix parent in the Schreier tree. -/

171theorem schreierPrefixTree_edge_of_last_pos {X : Type u} [DecidableEq X]

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

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

174 (t : T) {x : X} (hw : FreeGroup.toWord (t : FreeGroup X) ≠ [])

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

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

177 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

178 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

179 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),

180 prefixParent_mem_of_mem (X := X) hT t.property⟩

181 let pA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=

182 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from

183 ((p : T) : ActionCategory (FreeGroup X) T)

184 let tA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=

185 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from

186 ((t : T) : ActionCategory (FreeGroup X) T)

187 ∃ e : @Quiver.Hom

188 (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))

189 inferInstance pA tA,

190 e ∈ schreierPrefixTree (X := X) hT pA tA := by

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

192 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

193 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

194 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),

195 prefixParent_mem_of_mem (X := X) hT t.property⟩

196 refine ⟨Sum.inl ⟨x, ?_⟩, ?_⟩

197 · change (FreeGroup.of x)⁻¹ • p = t

198 rw [schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ p]

199 simpa [p] using

200 schreierRepresentative_eq_of_prefixParent_last_pos (X := X) hT t.property hw hlast

201 · rw [mem_schreierPrefixTree_inl_iff (X := X) (hT := hT)]

202 exact ⟨hw, rfl, by simpa using hlast⟩

203

204/-- A negative final letter determines the oppositely oriented edge from the prefix parent. -/

205theorem schreierPrefixTree_edge_of_last_neg {X : Type u} [DecidableEq X]

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

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

208 (t : T) {x : X} (hw : FreeGroup.toWord (t : FreeGroup X) ≠ [])

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

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

211 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

212 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

213 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),

214 prefixParent_mem_of_mem (X := X) hT t.property⟩

215 let pA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=

216 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from

217 ((p : T) : ActionCategory (FreeGroup X) T)

218 let tA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=

219 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from

220 ((t : T) : ActionCategory (FreeGroup X) T)

221 ∃ e : @Quiver.Hom

222 (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))

223 inferInstance pA tA,

224 e ∈ schreierPrefixTree (X := X) hT pA tA := by

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

226 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

227 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

228 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),

229 prefixParent_mem_of_mem (X := X) hT t.property⟩

230 refine ⟨Sum.inr ⟨x, ?_⟩, ?_⟩

231 · change (FreeGroup.of x)⁻¹ • t = p

232 rw [schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ t]

233 simpa [p] using

234 schreierRepresentative_eq_prefixParent_of_cancels (X := X) hT t.property hw hlast

235 · rw [mem_schreierPrefixTree_inr_iff (X := X) (hT := hT)]

236 exact ⟨hw, rfl, by simpa using hlast⟩

237

238/-- Every nonroot vertex has a Schreier-tree edge from its canonical prefix parent. -/

239theorem schreierPrefixTree_parent_edge_of_ne_one {X : Type u} [DecidableEq X]

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

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

242 (t : T) (ht1 : (t : FreeGroup X) ≠ 1) :

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

244 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

245 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

246 let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),

247 prefixParent_mem_of_mem (X := X) hT t.property⟩

248 let pA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=

249 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from

250 ((p : T) : ActionCategory (FreeGroup X) T)

251 let tA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=

252 show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from

253 ((t : T) : ActionCategory (FreeGroup X) T)

254 ∃ e : @Quiver.Hom

255 (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))

256 inferInstance pA tA,

257 e ∈ schreierPrefixTree (X := X) hT pA tA := by

258 let edge := FreeGroup.prefixParentEdgeOfNeOne (X := X) (t := (t : FreeGroup X)) ht1

259 have hlastEdge :

260 FreeGroup.lastLetter? (t : FreeGroup X) = some edge.letter :=

261 FreeGroup.prefixParentEdgeOfNeOne_lastLetter? (X := X) (t := (t : FreeGroup X)) ht1

262 rcases hletter : edge.letter with ⟨x, b⟩

263 cases b with

264 | false =>

265 have hlast? :

266 FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, false) : Internal.SignedLetter X)

267 := by

268 simpa [edge, hletter] using hlastEdge

269 rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff

270 (g := (t : FreeGroup X)) (y := ((x, false) : Internal.SignedLetter X))).1 hlast? with

271 ⟨hw, hlast⟩

272 exact schreierPrefixTree_edge_of_last_neg (X := X) hT t hw hlast

273 | true =>

274 have hlast? :

275 FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, true) : Internal.SignedLetter X) := by

276 simpa [edge, hletter] using hlastEdge

277 rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff

278 (g := (t : FreeGroup X)) (y := ((x, true) : Internal.SignedLetter X))).1 hlast? with

279 ⟨hw, hlast⟩

280 exact schreierPrefixTree_edge_of_last_pos (X := X) hT t hw hlast

281

282/-- Every Schreier-tree vertex is either the identity root or the target of an incoming edge. -/

283lemma schreierPrefixTree_root_or_arrow {X : Type u} [DecidableEq X]

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

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

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

287 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

288 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

289 ∀ b : schreierPrefixTree (X := X) hT,

290 b = ((((⟨(1 : FreeGroup X), hT.2.1⟩ : T) : ActionCategory (FreeGroup X) T) :

291 schreierPrefixTree (X := X) hT)) ∨

292 ∃ a, Nonempty (a ⟶ b) := by

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

294 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

295 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

296 intro b

297 let tb : T := (show ActionCategory (FreeGroup X) T from b).back

298 by_cases hb1 : (tb : FreeGroup X) = 1

299 · left

300 cases b with

301 | mk fst snd =>

302 cases fst

303 cases snd with

304 | mk val hval =>

305 have hb1' : val = 1 := by

306 simpa [tb] using hb1

307 cases hb1'

308 rfl

309 · right

310 let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),

311 prefixParent_mem_of_mem (X := X) hT tb.property⟩

312 refine ⟨((pb : T) : ActionCategory (FreeGroup X) T), ?_⟩

313 rcases schreierPrefixTree_parent_edge_of_ne_one (X := X) hT tb hb1 with ⟨e, he⟩

314 exact ⟨⟨e, he⟩⟩

315

316/-- Two Schreier-tree arrows with the same target have equal sources and agree as quiver edges. -/

317lemma schreierPrefixTree_unique_arrow {X : Type u} [DecidableEq X]

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

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

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

321 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

322 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

323 ∀ ⦃a b c : schreierPrefixTree (X := X) hT⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f := by

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

325 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

326 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

327 intro a b c e f

328 rcases e with ⟨e0, hme⟩

329 rcases f with ⟨f0, hmf⟩

330 have hme0 := hme

331 have hmf0 := hmf

332 rcases hme with ⟨hwe, hsrca, hlast_e⟩

333 rcases hmf with ⟨hwf, hsrcb, hlast_f⟩

334 let tc : T := (show ActionCategory (FreeGroup X) T from c).back

335 let pc : T := ⟨FreeGroup.prefixParent (tc : FreeGroup X),

336 prefixParent_mem_of_mem (X := X) hT tc.property⟩

337 have ha_back : (show ActionCategory (FreeGroup X) T from a).back = pc := by

338 simpa [tc, pc] using hsrca

339 have hb_back : (show ActionCategory (FreeGroup X) T from b).back = pc := by

340 simpa [tc, pc] using hsrcb

341 have hab : a = b := actionCategory_eq_of_back_eq (h := ha_back.trans hb_back.symm)

342 refine ⟨hab, ?_⟩

343 subst hab

344 have hUnder : e0 = f0 := by

345 cases e0 with

346 | inl ge =>

347 cases f0 with

348 | inl gf =>

349 have hxeq : ge.1 = gf.1 := by

350 have hlast : (ge.1, true) = (gf.1, true) := by

351 calc

352 (ge.1, true) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by

353 simpa [tc] using hlast_e.symm

354 _ = (gf.1, true) := by simpa [tc] using hlast_f

355 exact congrArg Prod.fst hlast

356 have hgegf : ge = gf := Subtype.ext hxeq

357 subst hgegf

358 rfl

359 | inr gf =>

360 exfalso

361 have hlast : (ge.1, true) = (gf.1, false) := by

362 calc

363 (ge.1, true) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by

364 simpa [tc] using hlast_e.symm

365 _ = (gf.1, false) := by simpa [tc] using hlast_f

366 have : (true : Bool) = false := congrArg Prod.snd hlast

367 cases this

368 | inr ge =>

369 cases f0 with

370 | inl gf =>

371 exfalso

372 have hlast : (ge.1, false) = (gf.1, true) := by

373 calc

374 (ge.1, false) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by

375 simpa [tc] using hlast_e.symm

376 _ = (gf.1, true) := by simpa [tc] using hlast_f

377 have : (false : Bool) = true := congrArg Prod.snd hlast

378 cases this

379 | inr gf =>

380 have hxeq : ge.1 = gf.1 := by

381 have hlast : (ge.1, false) = (gf.1, false) := by

382 calc

383 (ge.1, false) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by

384 simpa [tc] using hlast_e.symm

385 _ = (gf.1, false) := by simpa [tc] using hlast_f

386 exact congrArg Prod.fst hlast

387 have hgegf : ge = gf := Subtype.ext hxeq

388 subst hgegf

389 rfl

390 have hEq : (⟨e0, hme0⟩ : a ⟶ c) = ⟨f0, hmf0⟩ := by

391 apply Subtype.ext

392 exact hUnder

393 cases hEq

394 rfl

395

396/-- The reduced-word length strictly increases along every oriented Schreier-tree edge. -/

397lemma schreierPrefixTree_height_lt {X : Type u} [DecidableEq X]

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

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

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

401 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

402 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

403 ∀ ⦃a b : schreierPrefixTree (X := X) hT⦄ (_ : a ⟶ b),

404 (FreeGroup.toWord (((show ActionCategory (FreeGroup X) T from a).back : T) :

405 FreeGroup X)).length <

406 (FreeGroup.toWord (((show ActionCategory (FreeGroup X) T from b).back : T) :

407 FreeGroup X)).length := by

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

409 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

410 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

411 intro a b e

412 rcases e with ⟨_, hmem⟩

413 rcases hmem with ⟨hw, hsrc, _⟩

414 let tb : T := (show ActionCategory (FreeGroup X) T from b).back

415 have htb1 : (tb : FreeGroup X) ≠ 1 := by

416 exact mt (FreeGroup.toWord_eq_nil_iff.mpr) hw

417 have hlt :=

418 Internal.FreeGroupWord.FreeGroup.toWord_length_prefixParent_lt (t := (tb : FreeGroup X)) htb1

419 have hsrc' : (show ActionCategory (FreeGroup X) T from a).back =

420 ⟨FreeGroup.prefixParent (tb : FreeGroup X),

421 prefixParent_mem_of_mem (X := X) hT tb.property⟩ := by

422 simpa [tb] using hsrc

423 simpa [tb, hsrc', Internal.FreeGroupWord.FreeGroup.toWord_prefixParent] using hlt

424

425/-- The prefix-closed Schreier quiver is an arborescence rooted at the identity representative. -/

426noncomputable instance schreierPrefixTree_arborescence {X : Type u} [DecidableEq X]

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

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

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

430 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

431 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

432 Quiver.Arborescence (schreierPrefixTree (X := X) hT) := by

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

434 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

435 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

436 refine Quiver.arborescenceMk

437 ((((⟨(1 : FreeGroup X), hT.2.1⟩ : T) : ActionCategory (FreeGroup X) T) :

438 schreierPrefixTree (X := X) hT))

439 (fun a =>

440 (FreeGroup.toWord (((show ActionCategory (FreeGroup X) T from a).back : T) :

441 FreeGroup X)).length)

442 ?_ ?_ ?_

443 · intro a b e

444 exact schreierPrefixTree_height_lt (X := X) hT e

445 · intro a b c e f

446 exact schreierPrefixTree_unique_arrow (X := X) hT e f

447 · intro b

448 exact schreierPrefixTree_root_or_arrow (X := X) hT b

449

450/--

451The classical Schreier generators attached to a right Schreier transversal algebraically

452generate the subgroup.

453-/

454theorem closure_schreierGeneratorSet_eq_top {X : Type u} [DecidableEq X]

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

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

457 Subgroup.closure (schreierGeneratorSet (X := X) hT : Set L) = ⊤ := by

458 let U : Set L :=

459 (T * Set.range (FreeGroup.of : X → FreeGroup X)).image fun g =>

460 ⟨g * (hT.1.toRightFun g : FreeGroup X)⁻¹, hT.1.mul_inv_toRightFun_mem g⟩

461 have hUtop : Subgroup.closure U = ⊤ := by

462 simpa [U] using

463 (Subgroup.closure_mul_image_eq_top

464 (H := L) (R := T) (S := Set.range (FreeGroup.of : X → FreeGroup X))

465 hT.1 hT.2.1 (FreeGroup.closure_range_of X))

466 have hSchreier_le :

467 (schreierGeneratorSet (X := X) hT : Set L) ⊆ U := by

468 intro z hz

469 rcases hz with ⟨t, ht, x, rfl, _hz1⟩

470 refine ⟨t * FreeGroup.of x, ⟨t, ht, FreeGroup.of x, ⟨x, rfl⟩, rfl⟩, ?_⟩

471 apply Subtype.ext

472 rfl

473 have hU_le :

474 U ⊆ insert 1 (schreierGeneratorSet (X := X) hT : Set L) := by

475 intro z hz

476 rcases hz with ⟨g, hg, rfl⟩

477 rcases hg with ⟨t, ht, y, hy, rfl⟩

478 rcases hy with ⟨x, rfl⟩

479 by_cases hgen : schreierGenerator (X := X) hT t x = 1

480 · left

481 simpa [schreierGenerator, schreierRepresentative] using congrArg Subtype.val hgen

482 · right

483 exact ⟨t, ht, x, rfl, hgen⟩

484 have hclosureU_le :

485 Subgroup.closure U ≤

486 Subgroup.closure (schreierGeneratorSet (X := X) hT : Set L) := by

487 refine (Subgroup.closure_mono hU_le).trans ?_

488 exact le_of_eq (Subgroup.closure_insert_one

489 (schreierGeneratorSet (X := X) hT : Set L))

490 apply top_unique

491 calc

492 ⊤ = Subgroup.closure U := hUtop.symm

493 _ ≤ Subgroup.closure (schreierGeneratorSet (X := X) hT : Set L) := hclosureU_le

494

495/--

496The root vertex group in the Schreier action groupoid is canonically the subgroup L, via the

497action label of an endomorphism.

498-/

499noncomputable def schreierRootEndMulEquiv {X : Type u} [DecidableEq X]

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

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

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

503 CategoryTheory.End

504 (show ActionCategory (FreeGroup X) T from ((⟨(1 : FreeGroup X), hT.2.1⟩ : T) :

505 ActionCategory (FreeGroup X) T)) ≃* L := by

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

507 let rootT : T := ⟨(1 : FreeGroup X), hT.2.1⟩

508 let eStab : MulAction.stabilizer (FreeGroup X) rootT ≃* L := by

509 refine MulEquiv.subgroupCongr ?_

510 ext g

511 constructor

512 · intro hg

513 have hfix : g • rootT = rootT := hg

514 have hrep : schreierRepresentative (X := X) hT (g⁻¹) = rootT := by

515 simpa [rootT] using (schreierTransversalRightCosetAction_smul (X := X) hT g

516 rootT).symm.trans hfix

517 have hmemInv : g⁻¹ ∈ L := by

518 have hm : g⁻¹ *

519 (((schreierRepresentative (X := X) hT (g⁻¹) : T) : FreeGroup X))⁻¹ ∈ L :=

520 hT.1.mul_inv_toRightFun_mem (g⁻¹)

521 simpa [hrep, rootT] using hm

522 simpa using L.inv_mem hmemInv

523 · intro hg

524 change g • rootT = rootT

525 rw [schreierTransversalRightCosetAction_smul (X := X) hT g rootT]

526 simpa [rootT] using schreierRepresentative_eq_one_of_mem (X := X) hT (L.inv_mem hg)

527 let eSubmonoid : MulAction.stabilizerSubmonoid (FreeGroup X) rootT ≃* L :=

528 { toFun := fun g => eStab ⟨g.1, g.2⟩

529 invFun := fun l => ⟨(eStab.symm l).1, (eStab.symm l).2⟩

530 left_inv := by intro g; rfl

531 right_inv := by intro l; rfl

532 map_mul' := by intro g h; rfl }

533 exact (CategoryTheory.ActionCategory.stabilizerIsoEnd (FreeGroup X) rootT).symm.trans eSubmonoid

534

535/--

536The cocycle functor on the Schreier action groupoid. It sends a morphism \(a\to b\) labelled by

537\(g\) to the subgroup element \(b g a^{-1}\), the inverse of the corresponding classical

538Schreier generator.

539-/

540noncomputable def schreierLabelFunctor {X : Type u} [DecidableEq X]

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

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

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

544 ActionCategory (FreeGroup X) T ⥤ CategoryTheory.SingleObj L := by

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

546 refine

547 { obj := fun _ => ()

548 map := fun {a b} p => ?_

549 map_id := ?_

550 map_comp := ?_ }

551 · let g : FreeGroup X := p.1

552 refine ⟨((b.back : T) : FreeGroup X) * g * (((a.back : T) : FreeGroup X))⁻¹, ?_⟩

553 have hp : schreierRepresentative (X := X) hT

554 ((((a.back : T) : FreeGroup X)) * g⁻¹) = b.back := by

555 rw [← schreierTransversalRightCosetAction_smul (X := X) hT g a.back]

556 exact p.2

557 have hmem : (((a.back : T) : FreeGroup X)) * g⁻¹ *

558 (((b.back : T) : FreeGroup X))⁻¹ ∈ L := by

559 have hmem0 : (((a.back : T) : FreeGroup X)) * g⁻¹ *

560 (((schreierRepresentative (X := X) hT

561 ((((a.back : T) : FreeGroup X)) * g⁻¹) : T) : FreeGroup X))⁻¹ ∈ L := by

562 simpa [schreierRepresentative] using

563 hT.1.mul_inv_toRightFun_mem ((((a.back : T) : FreeGroup X)) * g⁻¹)

564 rw [hp] at hmem0

565 exact hmem0

566 simpa [mul_assoc] using L.inv_mem hmem

567 · intro a

568 apply Subtype.ext

569 change (((a.back : T) : FreeGroup X) * (1 : FreeGroup X) *

570 (((a.back : T) : FreeGroup X))⁻¹) = 1

571 simp only [mul_one, mul_inv_cancel]

572 · intro a b c p q

573 let gp : FreeGroup X := p.1

574 let gq : FreeGroup X := q.1

575 apply Subtype.ext

576 change (((c.back : T) : FreeGroup X) * (gq * gp) *

577 (((a.back : T) : FreeGroup X))⁻¹) =

578 ((((c.back : T) : FreeGroup X) * gq * (((b.back : T) : FreeGroup X))⁻¹) *

579 (((b.back : T) : FreeGroup X) * gp * (((a.back : T) : FreeGroup X))⁻¹))

580 simp only [mul_assoc, inv_mul_cancel_left]

581

582/-- The Schreier label functor respects the corresponding map of generators. -/

583@[simp 900] theorem schreierLabelFunctor_map_of {X : Type u} [DecidableEq X]

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

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

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

587 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

588 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

589 ∀ {a b : ActionCategory (FreeGroup X) T}

590 (e : ((show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from a) ⟶ b)),

591 ((schreierLabelFunctor (X := X) hT).map (IsFreeGroupoid.of e) : L) =

592 (schreierGenerator (X := X) hT (((a.back : T) : FreeGroup X)) e.1)⁻¹ := by

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

594 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

595 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

596 intro a b e

597 have hb : schreierRepresentative (X := X) hT

598 ((((a.back : T) : FreeGroup X)) * FreeGroup.of e.1) = b.back := by

599 have hp : FreeGroup.inverseBasis X e.1 • a.back = b.back := e.property

600 rw [FreeGroup.inverseBasis_apply,

601 schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of e.1)⁻¹ a.back] at hp

602 simpa using hp

603 apply Subtype.ext

604 change (((b.back : T) : FreeGroup X) * (FreeGroup.of e.1)⁻¹ *

605 (((a.back : T) : FreeGroup X))⁻¹) =

606 ((((schreierGenerator (X := X) hT (((a.back : T) : FreeGroup X)) e.1 : L) :

607 FreeGroup X))⁻¹)

608 simp only [Lean.Elab.WF.paramLet, mul_assoc, schreierGenerator, hb, mul_inv_rev, inv_inv]

609

610/-- The corresponding Schreier representative satisfies the stated membership criterion. -/

611lemma schreierLabelFunctor_map_of_eq_one_of_mem_tree {X : Type u} [DecidableEq X]

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

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

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

615 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

616 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

617 ∀ {a b : ActionCategory (FreeGroup X) T}

618 (e : ((show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from a) ⟶ b)),

619 e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b →

620 (schreierLabelFunctor (X := X) hT).map (IsFreeGroupoid.of e) = (1 : L) := by

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

622 letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=

623 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

624 intro a b e he

625 rw [schreierLabelFunctor_map_of (X := X) hT e]

626 rcases he with htree | htree

627 · rcases htree with ⟨hw, hsrc, hlast⟩

628 let tb : T := b.back

629 have hsrc' : a.back = ⟨FreeGroup.prefixParent (tb : FreeGroup X),

630 prefixParent_mem_of_mem (X := X) hT tb.property⟩ := by

631 simpa [tb] using hsrc

632 have hgen :

633 schreierGenerator (X := X) hT

634 (FreeGroup.prefixParent (tb : FreeGroup X)) e.1 = (1 : L) := by

635 exact schreierGenerator_eq_one_of_prefixParent_last_pos (X := X) hT

636 (t := (tb : FreeGroup X)) tb.property hw hlast

637 have hgen' : schreierGenerator (X := X) hT (((a.back : T) : FreeGroup X)) e.1 = (1 : L) := by

638 simpa [hsrc'] using hgen

639 exact inv_eq_one.mpr hgen'

640 · rcases htree with ⟨hw, hsrc, hlast⟩

641 let ta : T := a.back

642 have hgen : schreierGenerator (X := X) hT (ta : FreeGroup X) e.1 = (1 : L) := by

643 exact schreierGenerator_eq_one_of_cancels (X := X) hT

644 (t := (ta : FreeGroup X)) ta.property hw hlast

645 exact inv_eq_one.mpr (by simpa [ta] using hgen)

646

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

648lemma schreierGenerator_eq_one_implies_mem_prefixTree {X : Type u} [DecidableEq X]

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

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

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

652 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=

653 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

654 ∀ {a b : CategoryTheory.ActionCategory (FreeGroup X) T}

655 (e :

656 (show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from

657 a) ⟶ b),

658 schreierGenerator (X := X) hT (a.back : FreeGroup X) e.1 = 1 →

659 e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b := by

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

661 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=

662 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

663 intro a b e hgen

664 let ta : T := a.back

665 have hrep : schreierRepresentative (X := X) hT

666 ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) = b.back := by

667 have hp : FreeGroup.inverseBasis X e.1 • a.back = b.back := e.property

668 rw [FreeGroup.inverseBasis_apply,

669 schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of e.1)⁻¹ a.back] at hp

670 simpa [ta] using hp

671 have hraw :

672 (((schreierRepresentative (X := X) hT

673 ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) : T) : FreeGroup X)) =

674 ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := by

675 exact (schreierGenerator_eq_one_iff (X := X) (hT := hT)

676 (t := ((ta : T) : FreeGroup X)) (x := e.1)).mp hgen

677 by_cases hcancel : ∃ hw : FreeGroup.toWord ((ta : T) : FreeGroup X) ≠ [],

678 (FreeGroup.toWord ((ta : T) : FreeGroup X)).getLast hw = (e.1, false)

679 · rcases hcancel with ⟨hw, hlast⟩

680 have hb : (b.back : FreeGroup X) = FreeGroup.prefixParent ((ta : T) : FreeGroup X) := by

681 calc

682 (b.back : FreeGroup X)

683 = (((schreierRepresentative (X := X) hT

684 ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) : T) : FreeGroup X)) := by

685 exact congrArg Subtype.val hrep.symm

686 _ = ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := hraw

687 _ = FreeGroup.prefixParent ((ta : T) : FreeGroup X) :=

688 Internal.FreeGroupWord.FreeGroup.mul_of_eq_prefixParent_of_cancels

689 ((ta : T) : FreeGroup X) e.1 hw hlast

690 refine Or.inr ?_

691 refine ⟨hw, ?_⟩

692 constructor

693 · apply Subtype.ext

694 simpa [ta] using hb

695 · simpa [ta] using hlast

696 · have hword : FreeGroup.toWord (((ta : T) : FreeGroup X) * FreeGroup.of e.1) =

697 FreeGroup.toWord ((ta : T) : FreeGroup X) ++ [(e.1, true)] :=

698 Internal.FreeGroupWord.FreeGroup.toWord_mul_of_of_not_cancels

699 ((ta : T) : FreeGroup X) e.1 hcancel

700 have hb : (b.back : FreeGroup X) = ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := by

701 calc

702 (b.back : FreeGroup X)

703 = (((schreierRepresentative (X := X) hT

704 ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) : T) : FreeGroup X)) := by

705 exact congrArg Subtype.val hrep.symm

706 _ = ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := hraw

707 have hbw : FreeGroup.toWord (b.back : FreeGroup X) =

708 FreeGroup.toWord ((ta : T) : FreeGroup X) ++ [(e.1, true)] := by

709 simpa [hb] using hword

710 have hbw_ne : FreeGroup.toWord (b.back : FreeGroup X) ≠ [] := by

711 rw [hbw]

712 simp only [Lean.Elab.WF.paramLet, ne_eq, List.append_eq_nil_iff, FreeGroup.toWord_eq_nil_iff,

713 List.cons_ne_self, and_false, not_false_eq_true]

714 have hprefix : FreeGroup.prefixParent (b.back : FreeGroup X) = ((ta : T) : FreeGroup X) := by

715 apply FreeGroup.toWord_injective

716 rw [Internal.FreeGroupWord.FreeGroup.toWord_prefixParent, hbw]

717 simp only [Lean.Elab.WF.paramLet, ne_eq, List.cons_ne_self, not_false_eq_true,

718 List.dropLast_append_of_ne_nil,

719 List.dropLast_singleton, List.append_nil]

720 refine Or.inl ?_

721 refine ⟨hbw_ne, ?_⟩

722 constructor

723 · apply Subtype.ext

724 exact hprefix.symm

725 · simp only [hbw, Lean.Elab.WF.paramLet, ne_eq, List.cons_ne_self, not_false_eq_true,

726 List.getLast_append_of_ne_nil, List.getLast_singleton]

727

728/--

729A generator edge lies in the symmetrized prefix tree exactly when the associated Schreier

730generator is trivial.

731-/

732theorem schreierGenerator_eq_one_iff_mem_prefixTree {X : Type u} [DecidableEq X]

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

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

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

736 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=

737 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

738 ∀ {a b : CategoryTheory.ActionCategory (FreeGroup X) T}

739 {e :

740 (show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from

741 a) ⟶ b},

742 schreierGenerator (X := X) hT (a.back : FreeGroup X) e.1 = 1 ↔

743 e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b := by

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

745 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=

746 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

747 intro a b e

748 constructor

749 · exact schreierGenerator_eq_one_implies_mem_prefixTree (X := X) hT e

750 · intro he

751 have hmap :=

752 schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he

753 rw [schreierLabelFunctor_map_of (X := X) hT e] at hmap

754 exact inv_eq_one.mp hmap

755

756

757end SchreierPrefixTrees

758

759end ReidemeisterSchreier.Discrete.OpenSubgroups