mathlib3 documentation

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

inductive category_theory.groupoid.free.red_step {V : Type u} [quiver V] :

hom_rel (category_theory.paths (quiver.symmetrify V))

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

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

Type u_1

The underlying vertices of the free groupoid

Equations

category_theory.free_groupoid V = category_theory.quotient category_theory.groupoid.free.red_step

Instances for category_theory.free_groupoid

@[protected, instance]

def category_theory.groupoid.free.category_theory.free_groupoid.nonempty {V : Type u_1} [Q : quiver V] [h : nonempty V] :

nonempty (category_theory.free_groupoid 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) :

category_theory.quotient.comp_closure category_theory.groupoid.free.red_step p q → category_theory.quotient.comp_closure category_theory.groupoid.free.red_step (quiver.path.reverse p) (quiver.path.reverse q)

theorem category_theory.groupoid.free.congr_comp_reverse {V : Type u} [quiver V] {X Y : category_theory.paths (quiver.symmetrify V)} (p : X ⟶ Y) :

quot.mk (category_theory.quotient.comp_closure category_theory.groupoid.free.red_step) (p ≫ quiver.path.reverse p) = quot.mk (category_theory.quotient.comp_closure category_theory.groupoid.free.red_step) (𝟙 X)

theorem category_theory.groupoid.free.congr_reverse_comp {V : Type u} [quiver V] {X Y : category_theory.paths (quiver.symmetrify V)} (p : X ⟶ Y) :

quot.mk (category_theory.quotient.comp_closure category_theory.groupoid.free.red_step) (quiver.path.reverse p ≫ p) = quot.mk (category_theory.quotient.comp_closure category_theory.groupoid.free.red_step) (𝟙 Y)

@[protected, instance]

def category_theory.groupoid.free.category_theory.free_groupoid.category_theory.category {V : Type u} [quiver V] :

category_theory.category (category_theory.free_groupoid V)

Equations

category_theory.groupoid.free.category_theory.free_groupoid.category_theory.category = category_theory.quotient.category category_theory.groupoid.free.red_step

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] :

category_theory.groupoid (category_theory.free_groupoid 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' := _}

def category_theory.groupoid.free.of (V : Type u_1) [quiver V] :

V ⥤q category_theory.free_groupoid V

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)}

theorem category_theory.groupoid.free.of_eq {V : Type u} [quiver V] :

category_theory.groupoid.free.of V = quiver.symmetrify.of ⋙q category_theory.paths.of ⋙q (category_theory.quotient.functor category_theory.groupoid.free.red_step).to_prefunctor

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

category_theory.free_groupoid V ⥤ V'

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

Equations

category_theory.groupoid.free.lift φ = category_theory.quotient.lift category_theory.groupoid.free.red_step (category_theory.paths.lift (quiver.symmetrify.lift φ)) _

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

category_theory.groupoid.free.of V ⋙q (category_theory.groupoid.free.lift φ).to_prefunctor = φ

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 = φ) :

Φ = category_theory.groupoid.free.lift φ

def category_theory.free_groupoid_functor {V : Type u} [quiver V] {V' : Type u'} [quiver V'] (φ : V ⥤q V') :

category_theory.free_groupoid V ⥤ category_theory.free_groupoid V'

The functor of free groupoid induced by a prefunctor of quivers

Equations

category_theory.free_groupoid_functor φ = category_theory.groupoid.free.lift (φ ⋙q category_theory.groupoid.free.of V')

theorem category_theory.groupoid.free.free_groupoid_functor_id {V : Type u} [quiver V] :

category_theory.free_groupoid_functor (𝟭q V) = 𝟭 (category_theory.free_groupoid V)

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'') :

category_theory.free_groupoid_functor (φ ⋙q φ') = category_theory.free_groupoid_functor φ ⋙ category_theory.free_groupoid_functor φ'