Documentation

Mathlib.CategoryTheory.Groupoid.FreeGroupoid

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:

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

The inverse of an arrow in the free groupoid

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

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

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.