English
Let G be a free groupoid equipped with a spanning tree T of its generating quiver. For any monoid X and any monoid hom f from the vertex group End(root'(T)) to X, there exists a functor F: G → 1_X (the one-object category with object X) such that on arrows p, F(p) = f(loopOfHom T p) and F acts on the root object by the unique unit. In particular, a monoid hom from the root vertex extends to a functor on the entire free groupoid.
Русский
Пусть имеется свободная группоида G, снабжённая спаннинг-деревом T над её порождающей квиверой. Для любого моноидного множителя X и любого моноидного гомоморфизма f: End(root'(T)) →* X существует функтор F: G → 1_X (однообъектная категория с объектом X), такой что на стрелках p выполняется F(p) = f(loopOfHom T p) и F действует на объекте корня как единичный элемент. Таким образом, гомоморфизм из корневой вершины перестраивает весь группоид.
LaTeX
$$$$\exists F: G \to \mathbf{1}_X\quad\text{such that}\quad F(\ast)=(),\quad F(p)=f(\mathrm{loopOfHom}(T,p))\text{ for all arrows }p.$$$$
Lean4
/-- Since a hom gives a loop, any homomorphism from the vertex group at the root
extends to a functor on the whole groupoid. -/
@[simps]
def functorOfMonoidHom {X} [Monoid X] (f : End (root' T) →* X) : G ⥤ CategoryTheory.SingleObj X
where
obj _ := ()
map p := f (loopOfHom T p)
map_id := by
intro a
dsimp only [loopOfHom]
rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_one]
map_comp := by
intros
rw [comp_as_mul, ← f.map_mul]
simp only [IsIso.inv_hom_id_assoc, loopOfHom, End.mul_def, Category.assoc]
