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.

@[inline, reducible]

abbrev Quiver.Hom.toPosPath {V : Type u} [Quiver V] {X : V} {Y : V} (f : X ⟶ Y) : X ⟶ Y

Shorthand for the "forward" arrow corresponding to f in paths <| symmetrify V

Equations

• Quiver.Hom.toPosPath f = Quiver.Hom.toPath (Quiver.Hom.toPos f)

@[inline, reducible]

abbrev Quiver.Hom.toNegPath {V : Type u} [Quiver V] {X : V} {Y : V} (f : X ⟶ Y) : Y ⟶ X

Shorthand for the "forward" arrow corresponding to f in paths <| symmetrify V

Equations

• Quiver.Hom.toNegPath f = Quiver.Hom.toPath (Quiver.Hom.toNeg f)

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

The "reduction" relation

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

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 (CategoryTheory.FreeGroupoid V)

Equations

• (_ : Nonempty (CategoryTheory.FreeGroupoid V)) = (_ : Nonempty (CategoryTheory.FreeGroupoid V))

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

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

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

instance CategoryTheory.Groupoid.Free.instCategoryFreeGroupoid {V : Type u} [Quiver V] : CategoryTheory.Category.{max u v, u} (CategoryTheory.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 : CategoryTheory.FreeGroupoid V} {Y : CategoryTheory.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] : CategoryTheory.Groupoid (CategoryTheory.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 CategoryTheory.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] : CategoryTheory.Groupoid.Free.of V = Quiver.Symmetrify.of ⋙q CategoryTheory.Paths.of ⋙q (CategoryTheory.Quotient.functor CategoryTheory.Groupoid.Free.redStep).toPrefunctor

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

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

Equations

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

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

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

def CategoryTheory.freeGroupoidFunctor {V : Type u} [Quiver V] {V' : Type u'} [Quiver V'] (φ : V ⥤q V') : CategoryTheory.Functor (CategoryTheory.FreeGroupoid V) (CategoryTheory.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] : CategoryTheory.freeGroupoidFunctor (𝟭q V) = CategoryTheory.Functor.id (CategoryTheory.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'') : CategoryTheory.freeGroupoidFunctor (φ ⋙q φ') = CategoryTheory.Functor.comp (CategoryTheory.freeGroupoidFunctor φ) (CategoryTheory.freeGroupoidFunctor φ')