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:

• Quiver.FreeGroupoid V: a type synonym for V.
• Quiver.FreeGroupoid.instGroupoid: the Groupoid instance on Quiver.FreeGroupoid V.
• lift: the lifting of a prefunctor from V to V' where V' is a groupoid, to a functor. Quiver.FreeGroupoid 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, inline]

abbrev Quiver.Hom.toPosPath {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, inline]

abbrev Quiver.Hom.toNegPath {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 Quiver.FreeGroupoid.redStep {V : Type u} [Quiver V] : HomRel (CategoryTheory.Paths (Symmetrify V))

The "reduction" relation

• step {V : Type u} [Quiver V] (X Z : Symmetrify V) (f : X ⟶ Z) : redStep (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of (Symmetrify V)).obj X)) (CategoryTheory.CategoryStruct.comp f.toPath (reverse f).toPath)

def Quiver.FreeGroupoid (V : Type u_1) [Q : Quiver V] : Type u_1

The underlying vertices of the free groupoid

instance Quiver.FreeGroupoid.instNonempty {V : Type u_1} [Quiver V] [Nonempty V] : Nonempty (Quiver.FreeGroupoid V)

theorem Quiver.FreeGroupoid.congr_reverse {V : Type u} [Quiver V] {X Y : CategoryTheory.Paths (Symmetrify V)} (p q : X ⟶ Y) : CategoryTheory.HomRel.CompClosure redStep p q → CategoryTheory.HomRel.CompClosure redStep (Path.reverse p) (Path.reverse q)

theorem Quiver.FreeGroupoid.congr_comp_reverse {V : Type u} [Quiver V] {X Y : CategoryTheory.Paths (Symmetrify V)} (p : X ⟶ Y) : Quot.mk (CategoryTheory.HomRel.CompClosure redStep) (CategoryTheory.CategoryStruct.comp p (Path.reverse p)) = Quot.mk (CategoryTheory.HomRel.CompClosure redStep) (CategoryTheory.CategoryStruct.id X)

theorem Quiver.FreeGroupoid.congr_reverse_comp {V : Type u} [Quiver V] {X Y : CategoryTheory.Paths (Symmetrify V)} (p : X ⟶ Y) : Quot.mk (CategoryTheory.HomRel.CompClosure redStep) (CategoryTheory.CategoryStruct.comp (Path.reverse p) p) = Quot.mk (CategoryTheory.HomRel.CompClosure redStep) (CategoryTheory.CategoryStruct.id Y)

instance Quiver.FreeGroupoid.instCategory {V : Type u} [Quiver V] : CategoryTheory.Category.{max u v, u} (Quiver.FreeGroupoid V)

def Quiver.FreeGroupoid.quotInv {V : Type u} [Quiver V] {X Y : Quiver.FreeGroupoid V} (f : X ⟶ Y) : Y ⟶ X

The inverse of an arrow in the free groupoid

instance Quiver.FreeGroupoid.instGroupoid {V : Type u} [Quiver V] : CategoryTheory.Groupoid (Quiver.FreeGroupoid V)

def Quiver.FreeGroupoid.of (V : Type u_1) [Quiver V] : V ⥤q Quiver.FreeGroupoid V

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

theorem Quiver.FreeGroupoid.of_eq {V : Type u} [Quiver V] : of V = Symmetrify.of ⋙q CategoryTheory.Paths.of (Symmetrify V) ⋙q (CategoryTheory.Quotient.functor redStep).toPrefunctor

def Quiver.FreeGroupoid.lift {V : Type u} [Quiver V] {V' : Type u'} [CategoryTheory.Groupoid V'] (φ : V ⥤q V') : CategoryTheory.Functor (Quiver.FreeGroupoid V) V'

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

theorem Quiver.FreeGroupoid.lift_spec {V : Type u} [Quiver V] {V' : Type u'} [CategoryTheory.Groupoid V'] (φ : V ⥤q V') : of V ⋙q (lift φ).toPrefunctor = φ

theorem Quiver.FreeGroupoid.lift_unique {V : Type u} [Quiver V] {V' : Type u'} [CategoryTheory.Groupoid V'] (φ : V ⥤q V') (Φ : CategoryTheory.Functor (Quiver.FreeGroupoid V) V') (hΦ : of V ⋙q Φ.toPrefunctor = φ) : Φ = lift φ

def Quiver.freeGroupoidFunctor {V : Type u} [Quiver V] {V' : Type u'} [Quiver V'] (φ : V ⥤q V') : CategoryTheory.Functor (Quiver.FreeGroupoid V) (Quiver.FreeGroupoid V')

The functor of free groupoid induced by a prefunctor of quivers

theorem Quiver.freeGroupoidFunctor_id {V : Type u} [Quiver V] : freeGroupoidFunctor (𝟭q V) = CategoryTheory.Functor.id (Quiver.FreeGroupoid V)

theorem Quiver.freeGroupoidFunctor_comp {V : Type u} [Quiver V] {V' : Type u'} [Quiver V'] {V'' : Type u''} [Quiver V''] (φ : V ⥤q V') (φ' : V' ⥤q V'') : freeGroupoidFunctor (φ ⋙q φ') = (freeGroupoidFunctor φ).comp (freeGroupoidFunctor φ')