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:

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

Equations

• f.toPosPath = f.toPos.toPath

@[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

Equations

• f.toNegPath = f.toNeg.toPath

inductive CategoryTheory.Groupoid.Free.redStep {V : Type u} [Quiver V] : HomRel (Paths (Quiver.Symmetrify V))

The "reduction" relation

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

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

The underlying vertices of the free groupoid

Equations

• CategoryTheory.FreeGroupoid V = CategoryTheory.Quotient CategoryTheory.Groupoid.Free.redStep

instance CategoryTheory.Groupoid.Free.instNonemptyFreeGroupoid {V : Type u_1} [Quiver V] [Nonempty V] : Nonempty (FreeGroupoid V)

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

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

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

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

Equations

• CategoryTheory.Groupoid.Free.instCategoryFreeGroupoid = CategoryTheory.Quotient.category CategoryTheory.Groupoid.Free.redStep

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

The inverse of an arrow in the free groupoid

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.FreeGroupoid.instGroupoid = CategoryTheory.Groupoid.mk (fun {X Y : CategoryTheory.FreeGroupoid V} => CategoryTheory.Groupoid.Free.quotInv) ⋯ ⋯

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

Equations

• CategoryTheory.Groupoid.Free.lift φ = CategoryTheory.Quotient.lift CategoryTheory.Groupoid.Free.redStep (CategoryTheory.Paths.lift (Quiver.Symmetrify.lift φ)) ⋯

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

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

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

The functor of free groupoid induced by a prefunctor of quivers

Equations

• CategoryTheory.freeGroupoidFunctor φ = CategoryTheory.Groupoid.Free.lift (φ ⋙q CategoryTheory.Groupoid.Free.of V')

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

theorem CategoryTheory.Groupoid.Free.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 φ')