Source: ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Words.NielsenSchreierCompat
1import ProCGroups.ReidemeisterSchreier.Groupoid
3/-!
4# Reidemeister Schreier / Discrete / Open Subgroups / Words / Nielsen Schreier Compat
6This module connects the local word conventions with Mathlib's
7Nielsen--Schreier action-groupoid basis and establishes the edge and back-edge
8identities needed to transport that basis.
9-/
11namespace ReidemeisterSchreier.Discrete.OpenSubgroups
13section NielsenSchreierCompat
15open scoped Pointwise
16open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj Quiver FreeGroup
18/--
19An explicit free-group basis makes the corresponding action groupoid free with controlled
20generator labels.
21-/
22@[reducible] noncomputable def FreeGroupBasis.actionGroupoidIsFree
23 {ι G A : Type u} [Group G] [MulAction G A] (b : FreeGroupBasis ι G) :
24 IsFreeGroupoid (ActionCategory G A) where
25 quiverGenerators :=
26 ⟨fun a b' => { i : ι // b i • a.back = b'.back }⟩
27 of := fun (e : Subtype _) => ⟨b e, e.property⟩
28 unique_lift := by
29 intro X _ f
30 let f' : ι → (A → X) ⋊[mulAutArrow] G := fun i =>
31 ⟨fun a =>
32 @f ⟨(), (b i)⁻¹ • a⟩ ⟨(), a⟩
33 ⟨i, smul_inv_smul (b i) a⟩,
34 b i⟩
35 let F' : G →* (A → X) ⋊[mulAutArrow] G := b.lift f'
36 have hF' : ∀ i, F' (b i) = f' i := congrFun (b.lift.left_inv f')
37 refine ⟨uncurry F' ?_, ?_, ?_⟩
38 · intro g
39 suffices SemidirectProduct.rightHom.comp F' = MonoidHom.id G by
40 exact DFunLike.ext_iff.mp this g
41 apply b.ext_hom
42 intro i
43 rw [MonoidHom.comp_apply, hF' i]
44 rfl
45 · rintro ⟨⟨⟩, a : A⟩ ⟨⟨⟩, b'⟩ ⟨i, h : b i • a = b'⟩
46 change (F' (b i)).left _ = _
47 rw [hF' i]
48 cases inv_smul_eq_iff.mpr h.symm
49 rfl
50 · intro E hE
51 have hcurried : curry E = F' := by
52 apply b.ext_hom
53 intro i
54 rw [hF' i]
55 apply SemidirectProduct.ext
56 · funext a
57 exact hE ⟨(), (b i)⁻¹ • a⟩ ⟨(), a⟩ ⟨i, smul_inv_smul (b i) a⟩
58 · rfl
59 apply Functor.hext
60 · intro
61 apply Unit.ext
62 · refine ActionCategory.cases ?_
63 intro t g
64 simp only [← hcurried, uncurry_map, curry_apply_left, coe_back, homOfPair.val]
65 rfl
67/-- Two action-category objects are equal when their underlying points are equal. -/
68lemma actionCategory_eq_of_back_eq {M X : Type u} [Monoid M] [MulAction M X]
69 {u v : ActionCategory M X} (h : u.back = v.back) : u = v := by
70 cases u
71 cases v
72 cases h
73 rfl
75end NielsenSchreierCompat
77end ReidemeisterSchreier.Discrete.OpenSubgroups