ReidemeisterSchreier/Groupoid.lean
1import Mathlib.GroupTheory.FreeGroup.NielsenSchreier
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Groupoid.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free groupoids and spanning tree bases
14Groupoid-level free basis and spanning-tree constructions underlying the Nielsen-Schreier proof.
15-/
17open CategoryTheory CategoryTheory.SingleObj Quiver
20/-- The complement of a chosen spanning tree in a free connected groupoid gives an explicit free
21group basis of the root vertex group. This is the basis-level version of mathlib's
22`SpanningTree.endIsFree`. -/
23noncomputable def IsFreeGroupoid.SpanningTree.endBasis
24 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
25 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T] :
26 FreeGroupBasis
27 (((Quiver.wideSubquiverEquivSetTotal <| Quiver.wideSubquiverSymmetrify T)ᶜ : Set _))
28 (End (show G from Quiver.root T)) := by
29 classical
30 refine FreeGroupBasis.ofUniqueLift
31 (((Quiver.wideSubquiverEquivSetTotal <| Quiver.wideSubquiverSymmetrify T)ᶜ : Set _))
32 (fun e => IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e.val.hom))
33 ?_
34 intro X _ f
35 let f' : Quiver.Labelling (IsFreeGroupoid.Generators G) X := fun a b e =>
36 if h : e ∈ Quiver.wideSubquiverSymmetrify T a b then 1 else f ⟨⟨a, b, e⟩, h⟩
37 rcases IsFreeGroupoid.unique_lift f' with ⟨F', hF', uF'⟩
38 refine ⟨F'.mapEnd _, ?_, ?_⟩
39 · suffices
40 ∀ {x y} (q : x ⟶ y),
41 F'.map (IsFreeGroupoid.SpanningTree.loopOfHom T q) = (F'.map q : X) by
42 rintro ⟨⟨a, b, e⟩, h⟩
43 erw [Functor.mapEnd_apply]
44 rw [this, hF']
45 exact dif_neg h
46 intro x y q
47 suffices
48 ∀ {a} (p : Quiver.Path (Quiver.root T) a),
49 F'.map (IsFreeGroupoid.SpanningTree.homOfPath T p) = 1 by
50 simp only [this, IsFreeGroupoid.SpanningTree.treeHom,
51 CategoryTheory.SingleObj.comp_as_mul, inv_as_inv,
52 IsFreeGroupoid.SpanningTree.loopOfHom, inv_one, mul_one, one_mul,
53 Functor.map_inv, Functor.map_comp]
54 intro a p
55 induction p with
56 | nil =>
57 rw [IsFreeGroupoid.SpanningTree.homOfPath, F'.map_id, id_as_one]
58 | cons p e ih =>
59 rw [IsFreeGroupoid.SpanningTree.homOfPath, F'.map_comp,
60 CategoryTheory.SingleObj.comp_as_mul, ih, mul_one]
61 rcases e with ⟨e | e, eT⟩
62 · rw [hF']
63 have he : e ∈ Quiver.wideSubquiverSymmetrify T _ _ := by
64 change T _ _ (Sum.inl e) ∨ T _ _ (Sum.inr e)
65 exact Or.inl eT
66 simp only [he, ↓reduceDIte, f']
67 · rw [F'.map_inv, inv_as_inv, inv_eq_one, hF']
68 have he : e ∈ Quiver.wideSubquiverSymmetrify T _ _ := by
69 change T _ _ (Sum.inl e) ∨ T _ _ (Sum.inr e)
70 exact Or.inr eT
71 simp only [he, ↓reduceDIte, f']
72 · intro E hE
73 ext x
74 change E x = F'.map x
75 suffices
76 (IsFreeGroupoid.SpanningTree.functorOfMonoidHom T E).map x = F'.map x by
77 change E (IsFreeGroupoid.SpanningTree.loopOfHom T x) = F'.map x at this
78 have hroot : IsFreeGroupoid.SpanningTree.treeHom T (Quiver.root T) = 𝟙 _ := by
79 rw [IsFreeGroupoid.SpanningTree.treeHom_eq T Quiver.Path.nil]
80 rfl
81 have hx : E (IsFreeGroupoid.SpanningTree.loopOfHom T x) = E x := by
82 have hloop :
83 IsFreeGroupoid.SpanningTree.loopOfHom T x = x ≫ 𝟙 _ := by
84 simp only [IsFreeGroupoid.SpanningTree.loopOfHom, hroot, IsIso.inv_id,
85 Category.id_comp]
86 rfl
87 exact (congrArg E hloop).trans (congrArg E (Category.comp_id x))
88 exact hx.symm.trans this
89 congr
90 apply uF'
91 intro a b e
92 change E (IsFreeGroupoid.SpanningTree.loopOfHom T _) = dite _ _ _
93 split_ifs with h
94 · rw [IsFreeGroupoid.SpanningTree.loopOfHom_eq_id T e h, ← End.one_def, E.map_one]
95 · exact hE ⟨⟨a, b, e⟩, h⟩
98 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
99 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
100 {X : Type u} [Group X] (F : G ⥤ CategoryTheory.SingleObj X)
101 (hTree : ∀ {a b : IsFreeGroupoid.Generators G} (e : a ⟶ b),
102 e ∈ Quiver.wideSubquiverSymmetrify T a b → F.map (IsFreeGroupoid.of e) = 1) :
103 ∀ {a b} (q : a ⟶ b), F.map (IsFreeGroupoid.SpanningTree.loopOfHom T q) = (F.map q : X) := by
104 suffices
105 ∀ {a} (p : Quiver.Path (Quiver.root T) a),
106 F.map (IsFreeGroupoid.SpanningTree.homOfPath T p) = 1 by
107 intro x y q
108 simp only [this, IsFreeGroupoid.SpanningTree.treeHom,
109 CategoryTheory.SingleObj.comp_as_mul, inv_as_inv,
110 IsFreeGroupoid.SpanningTree.loopOfHom, inv_one, mul_one, one_mul,
111 Functor.map_inv, Functor.map_comp]
112 intro a p
113 induction p with
114 | nil =>
115 rw [IsFreeGroupoid.SpanningTree.homOfPath, F.map_id, id_as_one]
116 | cons p e ih =>
117 rw [IsFreeGroupoid.SpanningTree.homOfPath, F.map_comp,
118 CategoryTheory.SingleObj.comp_as_mul, ih, mul_one]
119 rcases e with ⟨e | e, eT⟩
120 · rw [hTree e (Or.inl eT)]
121 · rw [F.map_inv, inv_as_inv, inv_eq_one, hTree e (Or.inr eT)]
123@[simp] theorem FreeGroupBasis.ofUniqueLift_apply {X G : Type u} [Group G] (of : X → G)
124 (h : ∀ {H : Type u} [Group H] (f : X → H), ∃! F : G →* H, ∀ a, F (of a) = f a)
125 (x : X) :
126 FreeGroupBasis.ofUniqueLift X of h x = of x := by
127 unfold FreeGroupBasis.ofUniqueLift
128 change FreeGroup.lift of (FreeGroup.of x) = of x
129 simp only [FreeGroup.lift_apply_of]
131@[simp] lemma IsFreeGroupoid.SpanningTree.endBasis_apply
132 {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
133 (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
134 (e : (((Quiver.wideSubquiverEquivSetTotal <| Quiver.wideSubquiverSymmetrify T)ᶜ : Set _))) :
136 IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e.1.hom) := by
137 unfold IsFreeGroupoid.SpanningTree.endBasis FreeGroupBasis.ofUniqueLift
138 change
139 FreeGroup.lift (fun e =>
140 IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e.1.hom))
141 (FreeGroup.of e) = IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e.1.hom)
142 simp only [Lean.Elab.WF.paramLet, FreeGroup.lift_apply_of]