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
:
free_groupoid V
: a type synonym forV
.free_groupoid_groupoid
: thegroupoid
instance onfree_groupoid V
.lift
: the lifting of a prefunctor fromV
toV'
whereV'
is a groupoid, to a functor.free_groupoid V ⥤ V'
.lift_spec
andlift_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.
- step : ∀ {V : Type u} [_inst_1 : quiver V] (X Z : quiver.symmetrify V) (f : X ⟶ Z), category_theory.groupoid.free.red_step (𝟙 X) (f.to_path ≫ (quiver.reverse f).to_path)
The "reduction" relation
The underlying vertices of the free groupoid
Equations
@[protected, instance]
def
category_theory.groupoid.free.category_theory.free_groupoid.nonempty
{V : Type u_1}
[Q : quiver V]
[h : nonempty V] :
theorem
category_theory.groupoid.free.congr_reverse
{V : Type u}
[quiver V]
{X Y : category_theory.paths (quiver.symmetrify V)}
(p q : X ⟶ Y) :
theorem
category_theory.groupoid.free.congr_comp_reverse
{V : Type u}
[quiver V]
{X Y : category_theory.paths (quiver.symmetrify V)}
(p : X ⟶ Y) :
theorem
category_theory.groupoid.free.congr_reverse_comp
{V : Type u}
[quiver V]
{X Y : category_theory.paths (quiver.symmetrify V)}
(p : X ⟶ Y) :
@[protected, instance]
def
category_theory.groupoid.free.quot_inv
{V : Type u}
[quiver V]
{X Y : category_theory.free_groupoid V}
(f : X ⟶ Y) :
Y ⟶ X
The inverse of an arrow in the free groupoid
Equations
- category_theory.groupoid.free.quot_inv f = quot.lift_on f (λ (pp : X.as ⟶ Y.as), quot.mk (category_theory.quotient.comp_closure category_theory.groupoid.free.red_step) (quiver.path.reverse pp)) category_theory.groupoid.free.quot_inv._proof_1
@[protected, instance]
def
category_theory.groupoid.free.category_theory.free_groupoid.category_theory.groupoid
{V : Type u}
[quiver V] :
Equations
- category_theory.groupoid.free.category_theory.free_groupoid.category_theory.groupoid = {to_category := {to_category_struct := category_theory.category.to_category_struct category_theory.groupoid.free.category_theory.free_groupoid.category_theory.category, id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (X Y : category_theory.free_groupoid V) (f : X ⟶ Y), category_theory.groupoid.free.quot_inv f, inv_comp' := _, comp_inv' := _}
The inclusion of the quiver on V
to the underlying quiver on free_groupoid V
Equations
- category_theory.groupoid.free.of V = {obj := λ (X : V), {as := X}, map := λ (X Y : V) (f : X ⟶ Y), quot.mk (category_theory.quotient.comp_closure category_theory.groupoid.free.red_step) (category_theory.groupoid.free.quiver.hom.to_pos_path f)}
def
category_theory.groupoid.free.lift
{V : Type u}
[quiver V]
{V' : Type u'}
[category_theory.groupoid V']
(φ : V ⥤q V') :
The lift of a prefunctor to a groupoid, to a functor from free_groupoid V
theorem
category_theory.groupoid.free.lift_spec
{V : Type u}
[quiver V]
{V' : Type u'}
[category_theory.groupoid V']
(φ : V ⥤q V') :
theorem
category_theory.groupoid.free.lift_unique
{V : Type u}
[quiver V]
{V' : Type u'}
[category_theory.groupoid V']
(φ : V ⥤q V')
(Φ : category_theory.free_groupoid V ⥤ V')
(hΦ : category_theory.groupoid.free.of V ⋙q Φ.to_prefunctor = φ) :