English
In a free groupoid, every morphism a → b gives rise to a zigzag from symgen a to symgen b in the generating quiver; i.e., there exists a path from symgen(a) to symgen(b).
Русский
В свободном группоиде каждый морфизм a → b порождает зигзаг от symgen(a) к symgen(b) в порождающей квивере; то есть существует путь между symgen(a) и symgen(b).
LaTeX
$$$$\text{If } a \to b, \text{ then } \exists \pi: \mathrm{Path}(\mathrm{symgen}(a), \mathrm{symgen}(b)).$$$$
Lean4
/-- If there exists a morphism `a → b` in a free groupoid, then there also exists a zigzag
from `a` to `b` in the generating quiver. -/
theorem path_nonempty_of_hom {G} [Groupoid.{u, u} G] [IsFreeGroupoid G] {a b : G} :
Nonempty (a ⟶ b) → Nonempty (Path (symgen a) (symgen b)) :=
by
rintro ⟨p⟩
rw [← @WeaklyConnectedComponent.eq (Generators G), eq_comm, ← FreeGroup.of_injective.eq_iff, ← mul_inv_eq_one]
let X := FreeGroup (WeaklyConnectedComponent <| Generators G)
let f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
let F : G ⥤ CategoryTheory.SingleObj.{u} (X : Type u) := SingleObj.differenceFunctor f
change (F.map p) = ((@CategoryTheory.Functor.const G _ _ (SingleObj.category X)).obj ()).map p
congr; ext
rw [Functor.const_obj_map, id_as_one, differenceFunctor_map, @mul_inv_eq_one _ _ (f _)]
apply congr_arg FreeGroup.of
apply (WeaklyConnectedComponent.eq _ _).mpr
exact ⟨Hom.toPath (Sum.inr (by assumption))⟩
