Source: ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis

1import ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.PrefixTree

2import ProCGroups.ReidemeisterSchreier.Quiver

3import ProCGroups.ReidemeisterSchreier.Schreier

5/-!

6# Reidemeister Schreier / Discrete / Open Subgroups / Free Basis

8Using the action groupoid and Schreier prefix tree, this module constructs a

9free basis indexed by complement edges and transports it to the canonical

10type of nontrivial Schreier pairs.

11-/

13namespace ReidemeisterSchreier.Discrete.OpenSubgroups

16/--

17The total generator arrows in the action groupoid attached to a chosen free basis are indexed by

18a pair consisting of a vertex and a basis element.

19-/

20noncomputable def FreeGroupBasis.actionGroupoidGeneratorTotalEquiv

21 {ι G A : Type u} [Group G] [MulAction G A] (b : FreeGroupBasis ι G) :

22 letI : IsFreeGroupoid (CategoryTheory.ActionCategory G A) :=

23 FreeGroupBasis.actionGroupoidIsFree b

24 Quiver.Total (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory G A)) ≃ A × ι := by

25 letI : IsFreeGroupoid (CategoryTheory.ActionCategory G A) :=

26 FreeGroupBasis.actionGroupoidIsFree b

27 refine

28 { toFun := fun e => (e.left.back, e.hom.1)

29 invFun := fun ai =>

30 { left := show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory G A) from

31 ((ai.1 : A) : CategoryTheory.ActionCategory G A)

32 right := show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory G A) from

33 ((b ai.2 • ai.1 : A) : CategoryTheory.ActionCategory G A)

34 hom := ⟨ai.2, rfl⟩ }

35 left_inv := ?_

36 right_inv := ?_ }

37 · intro e

38 cases e with

39 | mk left right hom =>

40 cases left with

41 | mk _ a =>

42 cases right with

43 | mk _ a' =>

44 cases hom with

45 | mk i hi =>

46 dsimp

47 cases hi

48 rfl

49 · intro ai

50 rfl

52/--

53Complement edges of the symmetrized Schreier prefix tree. These are the canonical indexing

54objects for the Schreier free basis.

55-/

56noncomputable abbrev schreierComplementEdges

57 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

58 (hT : IsRightSchreierTransversal (X := X) L T) : Type u := by

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

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

61 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

62 exact

63 ↥(((Quiver.wideSubquiverEquivSetTotal <|

64 Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT))ᶜ :

65 Set (Quiver.Total

66 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)))))

68/-- The Schreier basis indexed by complement edges of the prefix tree. -/

69noncomputable def schreierComplementEdgesBasis

70 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

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

72 FreeGroupBasis (schreierComplementEdges (X := X) hT) L := by

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

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

75 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

76 exact

77 (ReidemeisterSchreier.Groupoid.endBasis (schreierPrefixTree (X := X) hT)).map

78 (schreierRootEndMulEquiv (X := X) hT)

80/--

81Auxiliary bridge from nontrivial Schreier pairs to the classical Schreier generator value set.

82-/

83private noncomputable def nontrivialSchreierPairsEquivSchreierGeneratorSet

84 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

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

86 NontrivialSchreierPair (X := X) hT ≃ ↥(schreierGeneratorSet (X := X) hT) := by

87 classical

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

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

90 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

91 let C :

92 Set (Quiver.Total

93 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))) :=

94 ((Quiver.wideSubquiverEquivSetTotal <|

95 Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT))ᶜ : Set _)

96 let toSch : ↑C → ↥(schreierGeneratorSet (X := X) hT) := fun i =>

97 ⟨schreierGenerator (X := X) hT (((i.1.left.back : T) : FreeGroup X)) i.1.hom.1,

98 by

99 refine ⟨

100 ((i.1.left.back : T) : FreeGroup X), (i.1.left.back : T).property,

101 i.1.hom.1, rfl, ?_⟩

102 intro hgen

103 exact i.2 (show i.1 ∈ Quiver.wideSubquiverEquivSetTotal

104 (Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)) from

105 schreierGenerator_eq_one_implies_mem_prefixTree (X := X) hT i.1.hom hgen)⟩

106 let b : FreeGroupBasis ↑C L :=

107 (ReidemeisterSchreier.Groupoid.endBasis (schreierPrefixTree (X := X) hT)).map

108 (schreierRootEndMulEquiv (X := X) hT)

109 have hval : ∀ i : ↑C, (b i : L) = (((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) := by

110 intro i

111 rw [FreeGroupBasis.map_apply, ReidemeisterSchreier.Groupoid.endBasis_apply]

112 have htree : ∀ {a b : IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)}

113 (e : a ⟶ b),

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

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

116 intro a b e he

117 exact schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he

118 have hloop := ReidemeisterSchreier.Groupoid.map_loopOfHom_eq_map

119 (T := schreierPrefixTree (X := X) hT)

120 (F := schreierLabelFunctor (X := X) hT)

121 (hTree := by

122 intro a b e he

123 exact htree e he)

124 (q := IsFreeGroupoid.of i.1.hom)

125 let loop := ReidemeisterSchreier.Groupoid.rootLoopOfHom (schreierPrefixTree (X := X) hT)

126 (IsFreeGroupoid.of i.1.hom)

127 have hrootEq : (schreierRootEndMulEquiv (X := X) hT loop : L) =

128 (schreierLabelFunctor (X := X) hT).map loop := by

129 apply Subtype.ext

130 change loop.1 = (1 : FreeGroup X) * loop.1 * (1 : FreeGroup X)⁻¹

131 simp only [one_mul, inv_one, mul_one]

132 exact hrootEq.trans <| hloop.trans <| schreierLabelFunctor_map_of (X := X) hT i.1.hom

133 have hto_inj : Function.Injective toSch := by

134 intro i j hij

135 apply b.injective

136 have hz : ((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L) =

137 ((toSch j : ↥(schreierGeneratorSet (X := X) hT)) : L) := congrArg Subtype.val hij

138 have hz_inv : (((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) =

139 (((toSch j : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) := congrArg Inv.inv hz

140 exact (hval i).trans (hz_inv.trans (hval j).symm)

141 have hto_surj : Function.Surjective toSch := by

142 intro z

143 rcases z.2 with ⟨t, ht, x, hz, hne⟩

144 let a : CategoryTheory.ActionCategory (FreeGroup X) T :=

145 ((⟨t, ht⟩ : T) : CategoryTheory.ActionCategory (FreeGroup X) T)

146 let b0 : CategoryTheory.ActionCategory (FreeGroup X) T :=

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

148 let e :

149 ((show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from a) ⟶

150 b0) :=

151 ⟨x, by

152 rw [FreeGroup.inverseBasis_apply]

153 change (FreeGroup.of x)⁻¹ • (show T from CategoryTheory.ActionCategory.back a) =

154 (show T from CategoryTheory.ActionCategory.back b0)

155 simpa [a, b0] using

156 (schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ (⟨t, ht⟩ : T))⟩

157 have he_not : ⟨a, b0, e⟩ ∈ C := by

158 change ¬ e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b0

159 intro he

160 have hgen1_inv :

161 (schreierGenerator (X := X) hT

162 ((show T from CategoryTheory.ActionCategory.back a) : FreeGroup X) e.1)⁻¹ = 1 := by

163 have htreeLabel :=

164 schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he

165 rw [schreierLabelFunctor_map_of (X := X) hT e] at htreeLabel

166 exact htreeLabel

167 have hgen1 :

168 schreierGenerator (X := X) hT

169 ((show T from CategoryTheory.ActionCategory.back a) : FreeGroup X) e.1 = 1 :=

170 inv_eq_one.mp hgen1_inv

171 exact hne (by simpa [a, e, hz] using hgen1)

172 refine ⟨⟨⟨a, b0, e⟩, he_not⟩, ?_⟩

173 apply Subtype.ext

174 simpa [toSch, a, e] using hz.symm

175 let eC : ↑C ≃ ↥(schreierGeneratorSet (X := X) hT) := Equiv.ofBijective toSch ⟨hto_inj, hto_surj⟩

176 let ePair :

177 ↑C ≃ NontrivialSchreierPair (X := X) hT := by

178 let eTotal :

179 Quiver.Total (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)) ≃

180 T × X :=

181 FreeGroupBasis.actionGroupoidGeneratorTotalEquiv (FreeGroup.inverseBasis X)

182 refine

183 { toFun := fun i =>

184 ⟨eTotal i.1, by

185 intro hgen

186 have hgen' :

187 schreierGenerator (X := X) hT

188 (((show T from CategoryTheory.ActionCategory.back i.1.left) : T) : FreeGroup X)

189 i.1.hom.1 = 1 := by

190 simpa [eTotal, FreeGroupBasis.actionGroupoidGeneratorTotalEquiv] using hgen

191 exact i.2 (show i.1 ∈ Quiver.wideSubquiverEquivSetTotal

192 (Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)) from

193 schreierGenerator_eq_one_implies_mem_prefixTree (X := X) hT i.1.hom hgen')⟩

194 invFun := fun p =>

195 let e := eTotal.symm p.1

196 ⟨e, by

197 intro he

198 have htreeLabel :=

199 schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e.hom

200 (show e.hom ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)

201 e.left e.right from he)

202 rw [schreierLabelFunctor_map_of (X := X) hT e.hom] at htreeLabel

203 have hgen' :

204 schreierGenerator (X := X) hT

205 (((show T from CategoryTheory.ActionCategory.back e.left) : T) : FreeGroup X)

206 e.hom.1 = 1 := inv_eq_one.mp htreeLabel

207 have hgen'' :

208 schreierGenerator (X := X) hT

209 (((eTotal e).1 : T) : FreeGroup X) (eTotal e).2 = 1 := by

210 simpa [eTotal, FreeGroupBasis.actionGroupoidGeneratorTotalEquiv] using hgen'

211 rw [eTotal.apply_symm_apply p.1] at hgen''

212 exact p.2 hgen''⟩

213 left_inv := by

214 intro i

215 apply Subtype.ext

216 simp only [Equiv.symm_apply_apply, eTotal]

217 right_inv := by

218 intro p

219 apply Subtype.ext

220 simp only [ne_eq, Equiv.apply_symm_apply, eTotal]}

221 exact ePair.symm.trans eC

222

223/-- Complement edges are equivalent to nontrivial Schreier pairs. -/

224noncomputable def schreierComplementEdgesEquivNontrivialPairs

225 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

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

227 schreierComplementEdges (X := X) hT ≃ NontrivialSchreierPair (X := X) hT := by

228 classical

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

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

231 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

232 let C :

233 Set (Quiver.Total

234 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))) :=

235 ((Quiver.wideSubquiverEquivSetTotal <|

236 Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT))ᶜ : Set _)

237 change ↑C ≃ NontrivialSchreierPair (X := X) hT

238 let eTotal :

239 Quiver.Total (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)) ≃

240 T × X :=

241 FreeGroupBasis.actionGroupoidGeneratorTotalEquiv (FreeGroup.inverseBasis X)

242 refine

243 { toFun := fun i =>

244 ⟨eTotal i.1, by

245 intro hgen

246 have hgen' :

247 schreierGenerator (X := X) hT

248 (((show T from CategoryTheory.ActionCategory.back i.1.left) : T) : FreeGroup X)

249 i.1.hom.1 = 1 := by

250 simpa [eTotal, FreeGroupBasis.actionGroupoidGeneratorTotalEquiv] using hgen

251 exact i.2 (show i.1 ∈ Quiver.wideSubquiverEquivSetTotal

252 (Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)) from

253 (schreierGenerator_eq_one_iff_mem_prefixTree (X := X) (hT := hT) (e := i.1.hom)).1

254 hgen')⟩

255 invFun := fun p =>

256 let e := eTotal.symm p.1

257 ⟨e, by

258 intro he

259 have hgen' :

260 schreierGenerator (X := X) hT

261 (((show T from CategoryTheory.ActionCategory.back e.left) : T) : FreeGroup X)

262 e.hom.1 = 1 :=

263 (schreierGenerator_eq_one_iff_mem_prefixTree (X := X) (hT := hT) (e := e.hom)).2

264 (show e.hom ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)

265 e.left e.right from he)

266 have hgen'' :

267 schreierGenerator (X := X) hT

268 (((eTotal e).1 : T) : FreeGroup X) (eTotal e).2 = 1 := by

269 simpa [eTotal, FreeGroupBasis.actionGroupoidGeneratorTotalEquiv] using hgen'

270 rw [eTotal.apply_symm_apply p.1] at hgen''

271 exact p.2 hgen''⟩

272 left_inv := by

273 intro i

274 apply Subtype.ext

275 simp only [Equiv.symm_apply_apply, eTotal]

276 right_inv := by

277 intro p

278 apply Subtype.ext

279 simp only [ne_eq, Equiv.apply_symm_apply, eTotal]}

280

281/--

282The Schreier free basis indexed by nontrivial Schreier pairs. This is the preferred

283Schreier-basis formulation; the classical value-set basis is a reindexing of this one.

284-/

285noncomputable def nontrivialSchreierPairBasis

286 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

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

288 FreeGroupBasis (NontrivialSchreierPair (X := X) hT) L :=

289 (schreierComplementEdgesBasis (X := X) hT).reindex

290 (schreierComplementEdgesEquivNontrivialPairs (X := X) hT)

291

292/-- The free group equivalence obtained directly from the preferred pair-indexed Schreier basis. -/

293noncomputable def nontrivialSchreierPairBasisEquiv

294 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

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

296 FreeGroup (NontrivialSchreierPair (X := X) hT) ≃* L :=

297 (nontrivialSchreierPairBasis (X := X) hT).repr.symm

298

299/--

300The preferred pair-indexed basis equivalence sends each free generator to its Schreier basis

301element.

302-/

303@[simp] theorem nontrivialSchreierPairBasisEquiv_of

304 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

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

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

307 nontrivialSchreierPairBasisEquiv (X := X) hT (FreeGroup.of p) =

308 nontrivialSchreierPairBasis (X := X) hT p := by

309 apply (nontrivialSchreierPairBasis (X := X) hT).repr.injective

310 calc

311 (nontrivialSchreierPairBasis (X := X) hT).repr

312 (nontrivialSchreierPairBasisEquiv (X := X) hT (FreeGroup.of p))

313 = FreeGroup.of p := by simp only [nontrivialSchreierPairBasisEquiv,

314 MulEquiv.apply_symm_apply]

315 _ = (nontrivialSchreierPairBasis (X := X) hT).repr

316 (nontrivialSchreierPairBasis (X := X) hT p) :=

317 (FreeGroupBasis.repr_apply_coe (nontrivialSchreierPairBasis (X := X) hT) p).symm

318

319/--

320The Reidemeister--Schreier equivalence is evaluated by the chosen nontrivial Schreier pair and

321its associated generator.

322-/

323private theorem nontrivialSchreierPairsEquivSchreierGeneratorSet_apply

324 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

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

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

327 ((nontrivialSchreierPairsEquivSchreierGeneratorSet (X := X) hT p :

328 ↥(schreierGeneratorSet (X := X) hT)) : L) =

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

330 rfl

331

332/-- The Schreier-generator map is injective on nontrivial Schreier pairs. -/

333theorem schreierGenerator_injective_of_nontrivial

334 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}

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

336 Function.Injective

337 (nontrivialSchreierPairGenerator (X := X) hT) := by

338 intro p q hpq

339 apply (nontrivialSchreierPairsEquivSchreierGeneratorSet (X := X) hT).injective

340 apply Subtype.ext

341 simpa [nontrivialSchreierPairsEquivSchreierGeneratorSet_apply,

342 nontrivialSchreierPairGenerator] using hpq

343

344/-- A right Schreier transversal has cardinality equal to the corresponding right-coset index. -/

345theorem natCard_schreierTransversal_eq_index

346 {X : Type u} [DecidableEq X]

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

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

349 Nat.card T = Nat.card (Quotient (QuotientGroup.rightRel L)) := by

350 exact Nat.card_congr hT.1.rightQuotientEquiv.symm

351

352/--

353The direct combinatorial count of complement edges in the Schreier prefix tree: all labelled

354edges minus tree edges.

355-/

356theorem natCard_schreierComplementEdges_eq_rankTransform_direct

357 {X : Type u} [DecidableEq X] [Finite X]

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

359 [Finite T]

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

361 Nat.card (schreierComplementEdges (X := X) hT) =

362 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T) := by

363 classical

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

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

366 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)

367 let Ttree :

368 WideSubquiver

369 (Quiver.Symmetrify

370 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))) :=

371 schreierPrefixTree (X := X) hT

372 letI : Quiver.Arborescence Ttree := by

373 dsimp [Ttree]

374 infer_instance

375 let totalGen :=

376 Quiver.Total (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))

377 let covered : Set totalGen :=

378 Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify Ttree)

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

380 let root : CategoryTheory.ActionCategory (FreeGroup X) T :=

381 CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T rootT

382 have hroot : Quiver.root Ttree = root := by

383 change root = root

384 rfl

385 letI : Fintype X := Fintype.ofFinite X

386 letI : Fintype T := Fintype.ofFinite T

387 haveI : Finite (CategoryTheory.ActionCategory (FreeGroup X) T) :=

388 Finite.of_equiv T (CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T)

389 haveI : Finite Ttree :=

390 Finite.of_equiv (CategoryTheory.ActionCategory (FreeGroup X) T)

391 (show _ ≃ Ttree from Equiv.refl _)

392 haveI : Finite totalGen :=

393 Finite.of_equiv (T × X)

394 (FreeGroupBasis.actionGroupoidGeneratorTotalEquiv (FreeGroup.inverseBasis X)).symm

395 letI : Fintype totalGen := Fintype.ofFinite totalGen

396 letI : Fintype (schreierComplementEdges (X := X) hT) :=

397 Fintype.ofFinite (schreierComplementEdges (X := X) hT)

398 letI : Fintype {e : totalGen // e ∈ covered} :=

399 Fintype.ofFinite {e : totalGen // e ∈ covered}

400 letI : Fintype {a : CategoryTheory.ActionCategory (FreeGroup X) T // a ≠ root} :=

401 Fintype.ofFinite {a : CategoryTheory.ActionCategory (FreeGroup X) T // a ≠ root}

402 letI : Fintype {v : Ttree // v ≠ Quiver.root Ttree} :=

403 Fintype.ofFinite {v : Ttree // v ≠ Quiver.root Ttree}

404 haveI : Finite (Quiver.Total Ttree) :=

405 Finite.of_equiv {v : Ttree // v ≠ Quiver.root Ttree}

406 (Quiver.Arborescence.totalEquivNonRoot Ttree).symm

407 letI : Fintype (Quiver.Total Ttree) := Fintype.ofFinite (Quiver.Total Ttree)

408 have hYcard :

409 Fintype.card (schreierComplementEdges (X := X) hT) =

410 Fintype.card totalGen - Fintype.card {e : totalGen // e ∈ covered} := by

411 change

412 Fintype.card {e : totalGen // e ∈ ((covered : Set totalGen)ᶜ)} =

413 Fintype.card totalGen - Fintype.card {e : totalGen // e ∈ covered}

414 simpa only [Set.mem_compl_iff] using

415 (Fintype.card_subtype_compl (fun e : totalGen => e ∈ covered) :

416 Fintype.card {e : totalGen // ¬ e ∈ covered} =

417 Fintype.card totalGen - Fintype.card {e : totalGen // e ∈ covered})

418 have hTotal :

419 Fintype.card totalGen = Fintype.card T * Fintype.card X := by

420 simpa [totalGen, Fintype.card_prod] using

421 Fintype.card_congr

422 (FreeGroupBasis.actionGroupoidGeneratorTotalEquiv

423 (ι := X) (G := FreeGroup X) (A := T) (FreeGroup.inverseBasis X))

424 let eObjNonRoot :

425 {a : CategoryTheory.ActionCategory (FreeGroup X) T // a ≠ root} ≃

426 {t : T // t ≠ rootT} := {

427 toFun := fun a => ⟨(CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T).symm a.1, by

428 intro h

429 apply a.2

430 simpa [root] using congrArg (CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T) h⟩

431 invFun := fun t => ⟨CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T t.1, by

432 intro h

433 apply t.2

434 simpa [root] using

435 congrArg (CategoryTheory.ActionCategory.objEquiv (FreeGroup X) T).symm h⟩

436 left_inv := by

437 intro a

438 apply Subtype.ext

439 simp only [ne_eq, Equiv.apply_symm_apply]

440 right_inv := by

441 intro t

442 apply Subtype.ext

443 simp only [ne_eq, Equiv.symm_apply_apply]}

444 haveI : Subsingleton {t : T // t = rootT} :=

445 ⟨fun t t' => Subtype.ext (by simp only [t.property, t'.property])⟩

446 have hOne :

447 Fintype.card {t : T // t = rootT} = 1 := by

448 exact Fintype.card_ofSubsingleton (⟨rootT, rfl⟩ : {t : T // t = rootT})

449 have hTcompl :

450 Fintype.card {t : T // t ≠ rootT} = Fintype.card T - 1 := by

451 calc

452 Fintype.card {t : T // t ≠ rootT}

453 = Fintype.card T - Fintype.card {t : T // t = rootT} := by

454 exact Fintype.card_subtype_compl (fun t : T => t = rootT)

455 _ = Fintype.card T - 1 := by rw [hOne]

456 have hNonRoot :

457 Fintype.card {v : Ttree // v ≠ Quiver.root Ttree} = Fintype.card T - 1 := by

458 let eRootNonRoot :

459 {v : Ttree // v ≠ Quiver.root Ttree} ≃

460 {a : CategoryTheory.ActionCategory (FreeGroup X) T // a ≠ root} := {

461 toFun v := ⟨v.1, fun hv => v.2 (hv.trans hroot.symm)⟩

462 invFun a := ⟨a.1, fun ha => a.2 (ha.trans hroot)⟩

463 left_inv v := by

464 apply Subtype.ext

465 rfl

466 right_inv a := by

467 apply Subtype.ext

468 rfl }

469 exact (Fintype.card_congr eRootNonRoot).trans

470 ((Fintype.card_congr eObjNonRoot).trans hTcompl)

471 have hCovered :

472 Fintype.card {e : totalGen // e ∈ covered} = Fintype.card T - 1 := by

473 calc

474 Fintype.card {e : totalGen // e ∈ covered}

475 = Fintype.card (Quiver.Total Ttree) := by

476 simpa [totalGen, covered] using

477 Fintype.card_congr (Quiver.coveredArrowEquivTotal Ttree)

478 _ = Fintype.card {v : Ttree // v ≠ Quiver.root Ttree} := by

479 simpa using Fintype.card_congr (Quiver.Arborescence.totalEquivNonRoot Ttree)

480 _ = Fintype.card T - 1 := hNonRoot

481 have hYcalcF :

482 Fintype.card (schreierComplementEdges (X := X) hT) =

483 Fintype.card T * Fintype.card X - (Fintype.card T - 1) := by

484 rw [hYcard, hTotal, hCovered]

485 have hYcalc :

486 Nat.card (schreierComplementEdges (X := X) hT) =

487 Nat.card T * Nat.card X - (Nat.card T - 1) := by

488 simpa [Nat.card_eq_fintype_card] using hYcalcF

489 by_cases hX0 : Nat.card X = 0

490 · have hX0F : Fintype.card X = 0 := by

491 simpa [Nat.card_eq_fintype_card] using hX0

492 calc

493 Nat.card (schreierComplementEdges (X := X) hT)

494 = Nat.card T * Nat.card X - (Nat.card T - 1) := hYcalc

495 _ = 0 := by simp only [Nat.card_eq_fintype_card, hX0F, mul_zero, zero_tsub]

496 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T) := by

497 simp only [Schreier.rankTransform, Nat.card_eq_fintype_card, hX0F, ↓reduceIte]

498 · obtain ⟨r, hr⟩ := Nat.exists_eq_succ_of_ne_zero hX0

499 rw [hr] at hYcalc ⊢

500 calc

501 Nat.card (schreierComplementEdges (X := X) hT)

502 = Nat.card T * (r + 1) - (Nat.card T - 1) := hYcalc

503 _ = Nat.card T * r + Nat.card T - (Nat.card T - 1) := by

504 rw [Nat.mul_succ]

505 _ = Nat.card T * r + (Nat.card T - (Nat.card T - 1)) := by

506 rw [Nat.add_sub_assoc (Nat.sub_le _ _)]

507 _ = Nat.card T * r + 1 := by

508 have hTpos : 0 < Nat.card T := by

509 simpa [Nat.card_eq_fintype_card] using

510 (Fintype.card_pos_iff.mpr ⟨rootT⟩)

511 obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hTpos)

512 rw [hn]

513 simp only [Nat.succ_eq_add_one, add_tsub_cancel_right, add_tsub_cancel_left]

514 _ = 1 + Nat.card T * r := by

515 rw [Nat.add_comm]

516 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (r + 1) (Nat.card T) := by

517 rw [_root_.ReidemeisterSchreier.Schreier.rankTransform_succ]

518

519/--

520The preferred pair-indexed generator type has cardinality equal to the Schreier rank-transform

521count.

522-/

523theorem natCard_nontrivialSchreierPairs_eq_rankTransform_direct

524 {X : Type u} [DecidableEq X] [Finite X]

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

526 [Finite T]

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

528 Nat.card (NontrivialSchreierPair (X := X) hT) =

529 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T) := by

530 calc

531 Nat.card (NontrivialSchreierPair (X := X) hT)

532 = Nat.card (schreierComplementEdges (X := X) hT) := by

533 exact Nat.card_congr

534 (schreierComplementEdgesEquivNontrivialPairs (X := X) hT).symm

535 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T) :=

536 natCard_schreierComplementEdges_eq_rankTransform_direct (X := X) (L := L) hT

537

538/--

539The number of nontrivial Schreier pairs equals the Schreier rank-transform count, with the index

540written as the usual left-coset quotient.

541-/

542theorem natCard_nontrivialSchreierPairs_eq_rankTransform

543 {X : Type u} [DecidableEq X] [Finite X]

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

545 [Finite (FreeGroup X ⧸ L)]

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

547 Nat.card (NontrivialSchreierPair (X := X) hT) =

548 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (FreeGroup X ⧸

549 L)) := by

550 classical

551 haveI : Finite (Quotient (QuotientGroup.rightRel L)) :=

552 Finite.of_equiv (FreeGroup X ⧸ L)

553 (QuotientGroup.quotientRightRelEquivQuotientLeftRel L).symm

554 haveI : Finite T :=

555 Finite.of_equiv (Quotient (QuotientGroup.rightRel L)) hT.1.rightQuotientEquiv

556 have hTcard :

557 Nat.card T = Nat.card (FreeGroup X ⧸ L) := by

558 calc

559 Nat.card T = Nat.card (Quotient (QuotientGroup.rightRel L)) := by

560 exact (Nat.card_congr hT.1.rightQuotientEquiv).symm

561 _ = Nat.card (FreeGroup X ⧸ L) := by

562 exact Nat.card_congr (QuotientGroup.quotientRightRelEquivQuotientLeftRel L)

563 calc

564 Nat.card (NontrivialSchreierPair (X := X) hT)

565 = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T) :=

566 natCard_nontrivialSchreierPairs_eq_rankTransform_direct (X := X) (L := L) hT

567 _ = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (FreeGroup X ⧸

568 L)) := by

569 rw [hTcard]

570

571/--

572A finite-index subgroup of a free group admits a free basis of Schreier-transformed cardinality.

573-/

574theorem exists_freeBasis_subgroupOfFreeGroup_of_rankTransform

575 {X : Type u} {L : Subgroup (FreeGroup X)} [Finite X] [Finite (FreeGroup X ⧸ L)] :

576 ∃ Y : Type u, Nonempty (FreeGroupBasis Y L) ∧

577 Nat.card Y = _root_.ReidemeisterSchreier.Schreier.rankTransform

578 (Nat.card X) (Nat.card (FreeGroup X ⧸ L)) := by

579 classical

580 rcases exists_rightSchreierTransversal L with ⟨T, hT⟩

581 exact ⟨NontrivialSchreierPair (X := X) hT,

582 ⟨nontrivialSchreierPairBasis (X := X) hT⟩,

583 natCard_nontrivialSchreierPairs_eq_rankTransform (X := X) hT⟩

584

585

586end ReidemeisterSchreier.Discrete.OpenSubgroups