# mathlib3documentation

category_theory.groupoid.free_groupoid

# Free groupoid on a quiver #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

• free_groupoid V: a type synonym for V.
• free_groupoid_groupoid: the groupoid instance on free_groupoid V.
• lift: the lifting of a prefunctor from V to V' where V' is a groupoid, to a functor. free_groupoid V ⥤ V'.
• lift_spec and lift_unique: the proofs that, respectively, lift indeed is a lifting and is the unique one.

## 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_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

def category_theory.free_groupoid (V : Type u_1) [Q : quiver V] :
Type u_1

The underlying vertices of the free groupoid

Equations
Instances for category_theory.free_groupoid
@[protected, instance]
@[protected, instance]
Equations

The inverse of an arrow in the free groupoid

Equations
• = (λ (pp : X.as Y.as), category_theory.groupoid.free.quot_inv._proof_1
@[protected, instance]
Equations

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

Equations
def category_theory.groupoid.free.lift {V : Type u} [quiver V] {V' : Type u'} (φ : V ⥤q V') :

The lift of a prefunctor to a groupoid, to a functor from free_groupoid V

Equations
theorem category_theory.groupoid.free.lift_spec {V : Type u} [quiver V] {V' : Type u'} (φ : V ⥤q V') :
theorem category_theory.groupoid.free.lift_unique {V : Type u} [quiver V] {V' : Type u'} (φ : V ⥤q V') (Φ : V') (hΦ : = φ) :
def category_theory.free_groupoid_functor {V : Type u} [quiver V] {V' : Type u'} [quiver V'] (φ : V ⥤q V') :

The functor of free groupoid induced by a prefunctor of quivers

Equations
theorem category_theory.groupoid.free.free_groupoid_functor_comp {V : Type u} [quiver V] {V' : Type u'} [quiver V'] {V'' : Type u''} [quiver V''] (φ : V ⥤q V') (φ' : V' ⥤q V'') :