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:

• Quiver.FreeGroupoid V: a type synonym for V.
• Quiver.FreeGroupoid.instGroupoid: the Groupoid instance on Quiver.FreeGroupoid V.
• lift: the lifting of a prefunctor from V to V' where V' is a groupoid, to a functor. Quiver.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 Quiver.FreeGroupoid.redStep {V : Type u} [Quiver V] : HomRel (CategoryTheory.Paths (Symmetrify V))

The "reduction" relation

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

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

The underlying vertices of the free groupoid

Equations

• Quiver.FreeGroupoid V = CategoryTheory.Quotient Quiver.FreeGroupoid.redStep

instance Quiver.FreeGroupoid.instNonempty {V : Type u_1} [Quiver V] [Nonempty V] : Nonempty (Quiver.FreeGroupoid V)

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

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

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

@[instance_reducible]

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

Equations

• Quiver.FreeGroupoid.instCategory = CategoryTheory.Quotient.category Quiver.FreeGroupoid.redStep

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

The inverse of an arrow in the free groupoid

Equations

• Quiver.FreeGroupoid.quotInv f = Quot.liftOn f (fun (pp : X.as ⟶ Y.as) => Quot.mk (CategoryTheory.HomRel.CompClosure Quiver.FreeGroupoid.redStep) (Quiver.Path.reverse pp)) ⋯

@[instance_reducible]

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

Equations

• Quiver.FreeGroupoid.instGroupoid = { toCategory := Quiver.FreeGroupoid.instCategory, inv := fun {X Y : Quiver.FreeGroupoid V} => Quiver.FreeGroupoid.quotInv, inv_comp := ⋯, comp_inv := ⋯ }

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

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

Equations

• Quiver.FreeGroupoid.of V = { obj := fun (X : V) => { as := X }, map := fun {X Y : V} (f : X ⟶ Y) => Quot.mk (CategoryTheory.HomRel.CompClosure Quiver.FreeGroupoid.redStep) f.toPosPath }

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

theorem Quiver.FreeGroupoid.hom_rec {V : Type u} [Quiver V] {motive : {x y : Quiver.FreeGroupoid V} → (x ⟶ y) → Prop} (of_map : ∀ {x y : V} (f : x ⟶ y), motive ((of V).map f)) (inv_of_map : ∀ {x y : V} (f : x ⟶ y), motive (CategoryTheory.inv ((of V).map f))) (id : ∀ (x : V), motive (CategoryTheory.CategoryStruct.id ((of V).obj x))) (comp : ∀ {x y z : Quiver.FreeGroupoid V} (f : x ⟶ y) (g : y ⟶ z), motive f → motive g → motive (CategoryTheory.CategoryStruct.comp f g)) {x y : Quiver.FreeGroupoid V} (f : x ⟶ y) : motive f

Induction principle for proving a property for all the morphisms in the free groupoid of a quiver V: it suffices to prove the property for morphisms (of V).map f coming for the quiver V and their inverses, and that the property is multiplicative (i.e. stable under composition and satisfied by identities).

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

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

Equations

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

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

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

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

The functor of free groupoid induced by a prefunctor of quivers

Equations

• Quiver.freeGroupoidFunctor φ = Quiver.FreeGroupoid.lift (φ ⋙q Quiver.FreeGroupoid.of V')

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

theorem Quiver.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 φ')