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.

@[reducible, inline]
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
  • f.toPosPath = f.toPos.toPath
Instances For
    @[reducible, inline]
    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
    • f.toNegPath = f.toNeg.toPath
    Instances For

      The "reduction" relation

      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