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
Instances For
    @[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
    Instances For
      def CategoryTheory.FreeGroupoid (V : Type u_1) [Q : Quiver V] :
      Type u_1

      The underlying vertices of the free groupoid

      Equations
      Instances For
        Equations

        The inverse of an arrow in the free groupoid

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          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.
          Instances For
            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
            Instances For