Source: ProCGroups.ReidemeisterSchreier.Groupoid
1import Mathlib.GroupTheory.FreeGroup.NielsenSchreier
3/-!
4# Reidemeister Schreier / Groupoid
6This module rebuilds the spanning-tree loop construction using public conversion functions between
7mathlib's vertex type synonyms. No private-root declaration or backward elaboration option enters
8the public API.
9-/
11open CategoryTheory CategoryTheory.SingleObj Quiver
13namespace ReidemeisterSchreier.Groupoid
15/-- A generator-quiver vertex viewed in the ambient groupoid. -/
16abbrev generatorObject
17 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
18 (a : IsFreeGroupoid.Generators G) : G :=
19 a
21/-- A generating arrow with both endpoints expressed through `generatorObject`. -/
22abbrev generatorHom
23 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
24 {a b : IsFreeGroupoid.Generators G} (e : a ⟶ b) :
25 generatorObject a ⟶ generatorObject b :=
26 IsFreeGroupoid.of e
28/-- A spanning-tree vertex viewed in the ambient groupoid. -/
29abbrev treeVertexObject
30 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
31 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G))
32 (a : T) : G :=
33 generatorObject a
35/-- An ambient groupoid vertex viewed as a vertex of the wide spanning subquiver. -/
36abbrev treeVertexOfObject
37 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
38 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G))
39 (a : G) : T :=
40 a
42/-- The root vertex of a spanning tree, explicitly returned in the ambient groupoid type. -/
43noncomputable abbrev rootObject
44 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
45 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G))
46 [Quiver.Arborescence T] : G :=
47 treeVertexObject T (Quiver.root T)
49/-- A tree edge viewed as an arrow of the ambient groupoid. -/
50noncomputable abbrev treeEdgeHom
51 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
52 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G))
53 {a b : T} (e : a ⟶ b) : treeVertexObject T a ⟶ treeVertexObject T b :=
54 Sum.recOn e.val (fun f => generatorHom f) (fun f => inv (generatorHom f))
56/-- A path in the chosen spanning tree gives an arrow from its explicit root. -/
57noncomputable def rootHomOfPath
58 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
59 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T] :
60 ∀ {a : T}, Quiver.Path (Quiver.root T) a →
61 (rootObject T ⟶ treeVertexObject T a)
62 | _, Quiver.Path.nil => 𝟙 _
63 | _, Quiver.Path.cons p e => rootHomOfPath T p ≫ treeEdgeHom T e
65/-- The canonical spanning-tree arrow from the explicit root to a tree vertex. -/
66noncomputable def rootTreeHom
67 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
68 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
69 (a : T) : rootObject T ⟶ treeVertexObject T a :=
70 rootHomOfPath T default
72/-- Any spanning-tree path computes the canonical root arrow. -/
73theorem rootTreeHom_eq
74 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
75 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
76 {a : T} (p : Quiver.Path (Quiver.root T) a) :
77 rootTreeHom T a = rootHomOfPath T p := by
78 rw [rootTreeHom, Unique.default_eq]
80/-- The canonical tree arrow at the explicit root is the identity. -/
81@[simp] theorem rootTreeHom_root
82 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
83 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T] :
84 rootTreeHom T (Quiver.root T) = 𝟙 _ :=
85 (rootTreeHom_eq T Quiver.Path.nil).trans rfl
87/-- The loop associated to a groupoid arrow, based at the explicit spanning-tree root. -/
88noncomputable def rootLoopOfHom
89 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
90 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
91 {a b : G} (p : a ⟶ b) : End (rootObject T) :=
92 rootTreeHom T (treeVertexOfObject T a) ≫ p ≫
93 inv (rootTreeHom T (treeVertexOfObject T b))
95/-- A tree edge gives the identity explicit-root loop. -/
96@[simp] theorem rootLoopOfHom_eq_id
97 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
98 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
99 {a b : IsFreeGroupoid.Generators G} (e : a ⟶ b)
100 (h : e ∈ Quiver.wideSubquiverSymmetrify T a b) :
101 rootLoopOfHom T (generatorHom e) = 𝟙 (rootObject T) := by
102 rcases h with h | h
103 · have htb :
104 rootTreeHom T (treeVertexOfObject T (generatorObject b)) =
105 rootTreeHom T (treeVertexOfObject T (generatorObject a)) ≫ generatorHom e := by
106 rw [rootTreeHom_eq T (Quiver.Path.cons default ⟨Sum.inl e, h⟩), rootHomOfPath,
107 treeEdgeHom]
108 rfl
109 unfold rootLoopOfHom
110 rw [← Category.assoc, ← htb, IsIso.hom_inv_id]
111 · have hta :
112 rootTreeHom T (treeVertexOfObject T (generatorObject a)) =
113 rootTreeHom T (treeVertexOfObject T (generatorObject b)) ≫ inv (generatorHom e) := by
114 rw [rootTreeHom_eq T (Quiver.Path.cons default ⟨Sum.inr e, h⟩), rootHomOfPath,
115 treeEdgeHom]
116 rfl
117 unfold rootLoopOfHom
118 rw [hta]
119 simp only [Category.assoc, IsIso.inv_hom_id_assoc, IsIso.hom_inv_id]
121/-- The functor induced by a homomorphism from the explicit root vertex group. -/
122noncomputable def rootFunctorOfMonoidHom
123 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
124 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
125 {X : Type u} [Monoid X] (f : End (rootObject T) →* X) :
126 G ⥤ CategoryTheory.SingleObj X where
127 obj _ := ()
128 map p := f (rootLoopOfHom T p)
129 map_id := by
130 intro a
131 dsimp only [rootLoopOfHom]
132 rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_one]
133 map_comp := by
134 intros
135 rw [CategoryTheory.SingleObj.comp_as_mul, ← f.map_mul]
136 simp only [IsIso.inv_hom_id_assoc, rootLoopOfHom, End.mul_def, Category.assoc]
138/--
139The explicit-root induced functor applies the supplied homomorphism to the explicit-root loop.
140-/
141@[simp] theorem rootFunctorOfMonoidHom_map
142 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
143 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
144 {X : Type u} [Monoid X] (f : End (rootObject T) →* X)
145 {a b : G} (p : a ⟶ b) :
146 (rootFunctorOfMonoidHom T f).map p = f (rootLoopOfHom T p) := rfl
148/-- At the root, turning an endomorphism into a loop does nothing. -/
149@[simp] theorem rootLoopOfHom_end
150 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
151 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
152 (p : End (rootObject T)) : rootLoopOfHom T p = p := by
153 simp only [rootLoopOfHom, treeVertexOfObject, rootObject, rootTreeHom_root,
154 IsIso.inv_id, Category.id_comp, Category.comp_id]
156/-- A functor trivial on the spanning tree maps every explicit-root loop to the original arrow. -/
157lemma map_loopOfHom_eq_map
158 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
159 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
160 {X : Type u} [Group X] (F : G ⥤ CategoryTheory.SingleObj X)
161 (hTree : ∀ {a b : IsFreeGroupoid.Generators G} (e : a ⟶ b),
162 e ∈ Quiver.wideSubquiverSymmetrify T a b → F.map (generatorHom e) = 1) :
163 ∀ {a b} (q : a ⟶ b), F.map (rootLoopOfHom T q) = (F.map q : X) := by
164 suffices
165 ∀ {a : T} (p : Quiver.Path (Quiver.root T) a),
166 F.map (rootHomOfPath T p) = 1 by
167 intro x y q
168 simp only [this, rootTreeHom, CategoryTheory.SingleObj.comp_as_mul, inv_as_inv,
169 rootLoopOfHom, inv_one, mul_one, one_mul, Functor.map_inv, Functor.map_comp]
170 intro a p
171 induction p with
172 | nil =>
173 simpa only [rootHomOfPath, id_as_one] using F.map_id (rootObject T)
174 | cons p e ih =>
175 rw [rootHomOfPath, F.map_comp, CategoryTheory.SingleObj.comp_as_mul, ih, mul_one]
176 rcases e with ⟨e | e, eT⟩
177 · rw [treeEdgeHom, hTree e (Or.inl eT)]
178 · rw [treeEdgeHom, F.map_inv, inv_as_inv, inv_eq_one, hTree e (Or.inr eT)]
180/-- The complement of a chosen spanning tree in a free connected groupoid gives
181an explicit free group basis of the root vertex group. -/
182noncomputable def endBasis
183 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
184 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T] :
185 FreeGroupBasis
186 (((Quiver.wideSubquiverEquivSetTotal <| Quiver.wideSubquiverSymmetrify T)ᶜ : Set _))
187 (End (rootObject T)) := by
188 classical
189 refine FreeGroupBasis.ofUniqueLift
190 (((Quiver.wideSubquiverEquivSetTotal <| Quiver.wideSubquiverSymmetrify T)ᶜ : Set _))
191 (fun e => rootLoopOfHom T (generatorHom e.val.hom))
192 ?_
193 intro X _ f
194 let f' : Quiver.Labelling (IsFreeGroupoid.Generators G) X := fun a b e =>
195 if h : e ∈ Quiver.wideSubquiverSymmetrify T a b then 1 else f ⟨⟨a, b, e⟩, h⟩
196 rcases IsFreeGroupoid.unique_lift f' with ⟨F', hF', uF'⟩
197 refine ⟨F'.mapEnd _, ?_, ?_⟩
198 · have hloop :
199 ∀ {a b} (q : a ⟶ b), F'.map (rootLoopOfHom T q) = (F'.map q : X) :=
200 map_loopOfHom_eq_map T F' (by
201 intro a b e he
202 rw [hF']
203 simp only [f', he, ↓reduceDIte])
204 rintro ⟨⟨a, b, e⟩, h⟩
205 simp only [Functor.mapEnd, DFunLike.coe, hloop, hF']
206 exact dif_neg h
207 · intro E hE
208 ext x
209 change E x = (F'.map x : X)
210 suffices (rootFunctorOfMonoidHom T E).map x = F'.map x by
211 simpa only [rootFunctorOfMonoidHom_map, rootLoopOfHom_end] using this
212 congr
213 apply uF'
214 intro a b e
215 rw [rootFunctorOfMonoidHom_map]
216 change E (rootLoopOfHom T (IsFreeGroupoid.of e)) = dite _ _ _
217 split_ifs with h
218 · rw [rootLoopOfHom_eq_id T e h, ← End.one_def, E.map_one]
219 · exact hE ⟨⟨a, b, e⟩, h⟩
221/-- The explicit spanning-tree basis evaluates to the corresponding explicit-root loop. -/
222@[simp] theorem endBasis_apply
223 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
224 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
225 (e : (((Quiver.wideSubquiverEquivSetTotal <| Quiver.wideSubquiverSymmetrify T)ᶜ : Set _))) :
226 endBasis T e = rootLoopOfHom T (generatorHom e.1.hom) := by
227 unfold endBasis FreeGroupBasis.ofUniqueLift
228 change
229 FreeGroup.lift (fun e => rootLoopOfHom T (generatorHom e.1.hom))
230 (FreeGroup.of e) = rootLoopOfHom T (generatorHom e.1.hom)
231 simp only [FreeGroup.lift_apply_of]
233end ReidemeisterSchreier.Groupoid