mathlib documentation

category_theory.groupoid.free_groupoid

Free groupoid on a quiver #

This file defines the free groupoid on a quiver, the lifting of a prefunctor to its unique extension as a functor from the free groupoid, and proves uniqueness of this extension.

Main results #

Given the type V and a quiver instance on V:

Implementation notes #

The free groupoid is first defined by symmetrifying the quiver, taking the induced path category and finally quotienting by the reducibility relation.

@[reducible]
def category_theory.groupoid.free.quiver.hom.to_pos {V : Type u} [quiver V] {X Y : V} (f : X Y) :
X Y

Shorthand for the "forward" arrow corresponding to f in symmetrify V

@[reducible]
def category_theory.groupoid.free.quiver.hom.to_neg {V : Type u} [quiver V] {X Y : V} (f : X Y) :
Y X

Shorthand for the "backward" arrow corresponding to f in symmetrify V

@[reducible]
def category_theory.groupoid.free.quiver.hom.to_pos_path {V : Type u} [quiver V] {X Y : V} (f : X Y) :
X Y

Shorthand for the "forward" arrow corresponding to f in paths $ symmetrify V

@[reducible]
def category_theory.groupoid.free.quiver.hom.to_neg_path {V : Type u} [quiver V] {X Y : V} (f : X Y) :
Y X

Shorthand for the "forward" arrow corresponding to f in paths $ symmetrify V

The "reduction" relation

The inverse of an arrow in the free groupoid

Equations

The inclusion of the quiver on V to the underlying quiver on free_groupoid V

Equations