Free groupoid on a category

This file defines the free groupoid on a category, the lifting of a functor to its unique extension as a functor from the free groupoid, and proves uniqueness of this extension.

Main results

Given a type C and a category instance on C:

• CategoryTheory.FreeGroupoid C: the underlying type of the free groupoid on C.
• CategoryTheory.FreeGroupoid.instGroupoid: the Groupoid instance on FreeGroupoid C.
• CategoryTheory.FreeGroupoid.lift: the lifting of a functor C ⥤ G where G is a groupoid, to a functor CategoryTheory.FreeGroupoid C ⥤ G.
• CategoryTheory.FreeGroupoid.lift_spec and CategoryTheory.FreeGroupoid.lift_unique: the proofs that, respectively, CategoryTheory.FreeGroupoid.lift indeed is a lifting and is the unique one.
• CategoryTheory.Grpd.free: the free functor from Grpd to Cat
• CategoryTheory.Grpd.freeForgetAdjunction: that free is left adjoint to Grpd.forgetToCat.

Implementation notes

The free groupoid on a category C is first defined by taking the free groupoid G on the underlying quiver of C. Then the free groupoid on the category C is defined as the quotient of G by the relation that makes the inclusion prefunctor C ⥤q G a functor.

inductive CategoryTheory.FreeGroupoid.homRel (C : Type u) [Category.{v, u} C] : HomRel (Quiver.FreeGroupoid C)

The relation on the free groupoid on the underlying quiver of C that promotes the prefunctor C ⥤q FreeGroupoid C into a functor C ⥤ Quotient (FreeGroupoid.homRel C).

• map_id {C : Type u} [Category.{v, u} C] (X : C) : homRel C ((Quiver.FreeGroupoid.of C).map (CategoryStruct.id X)) (CategoryStruct.id ((Quiver.FreeGroupoid.of C).obj X))
• map_comp {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : homRel C ((Quiver.FreeGroupoid.of C).map (CategoryStruct.comp f g)) (CategoryStruct.comp ((Quiver.FreeGroupoid.of C).map f) ((Quiver.FreeGroupoid.of C).map g))

def CategoryTheory.FreeGroupoid (C : Type u) [Category.{v, u} C] : Type u

The underlying type of the free groupoid on a category, defined by quotienting the free groupoid on the underlying quiver of C by the relation that promotes the prefunctor C ⥤q FreeGroupoid C into a functor C ⥤ Quotient (FreeGroupoid.homRel C).

instance CategoryTheory.instNonemptyFreeGroupoid (C : Type u) [Category.{v, u} C] [Nonempty C] : Nonempty (FreeGroupoid C)

@[implicit_reducible]

instance CategoryTheory.instGroupoidFreeGroupoid (C : Type u) [Category.{v, u} C] : Groupoid (FreeGroupoid C)

def CategoryTheory.FreeGroupoid.of (C : Type u) [Category.{v, u} C] : Functor C (FreeGroupoid C)

The localization functor from the category C to the groupoid FreeGroupoid C

@[reducible, inline]

abbrev CategoryTheory.FreeGroupoid.mk {C : Type u} [Category.{v, u} C] (X : C) : FreeGroupoid C

Construct an object in the free groupoid on C by providing an object in C.

@[reducible, inline]

abbrev CategoryTheory.FreeGroupoid.homMk {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : mk X ⟶ mk Y

Construct a morphism in the free groupoid on C by providing a morphism in C.

theorem CategoryTheory.FreeGroupoid.eq_mk {C : Type u} [Category.{v, u} C] (X : FreeGroupoid C) : X = mk X.as.as

theorem CategoryTheory.FreeGroupoid.of_obj_bijective {C : Type u} [Category.{v, u} C] : Function.Bijective (of C).obj

def CategoryTheory.FreeGroupoid.lift {C : Type u} [Category.{v, u} C] {G : Type u₁} [Groupoid G] (φ : Functor C G) : Functor (FreeGroupoid C) G

The lift of a functor from C to a groupoid to a functor from FreeGroupoid C to the groupoid

theorem CategoryTheory.FreeGroupoid.lift_spec {C : Type u} [Category.{v, u} C] {G : Type u₁} [Groupoid G] (φ : Functor C G) : (of C).comp (lift φ) = φ

@[simp]

theorem CategoryTheory.FreeGroupoid.lift_obj_mk {C : Type u} [Category.{v, u} C] {E : Type u₂} [Groupoid E] (φ : Functor C E) (X : C) : (lift φ).obj (mk X) = φ.obj X

@[simp]

theorem CategoryTheory.FreeGroupoid.lift_map_homMk {C : Type u} [Category.{v, u} C] {E : Type u₂} [Groupoid E] (φ : Functor C E) {X Y : C} (f : X ⟶ Y) : (lift φ).map (homMk f) = φ.map f

theorem CategoryTheory.FreeGroupoid.lift_unique {C : Type u} [Category.{v, u} C] {G : Type u₁} [Groupoid G] (φ : Functor C G) (Φ : Functor (FreeGroupoid C) G) (hΦ : (of C).comp Φ = φ) : Φ = lift φ

theorem CategoryTheory.FreeGroupoid.lift_id_comp_of {G : Type u₁} [Groupoid G] : (lift (Functor.id G)).comp (of G) = Functor.id (FreeGroupoid G)

theorem CategoryTheory.FreeGroupoid.lift_comp {C : Type u} [Category.{v, u} C] {G : Type u₁} [Groupoid G] {H : Type u₂} [Groupoid H] (φ : Functor C G) (ψ : Functor G H) : lift (φ.comp ψ) = (lift φ).comp ψ

def CategoryTheory.FreeGroupoid.strictUniversalPropertyFixedTarget {C : Type u} [Category.{v, u} C] {G : Type u₁} [Groupoid G] : Localization.StrictUniversalPropertyFixedTarget (of C) ⊤ G

The universal property of the free groupoid.

instance CategoryTheory.FreeGroupoid.instIsLocalizationOfTopMorphismProperty {C : Type u} [Category.{v, u} C] : (of C).IsLocalization ⊤

noncomputable def CategoryTheory.FreeGroupoid.liftNatIso {C : Type u} [Category.{v, u} C] {G : Type u₁} [Groupoid G] (F₁ F₂ : Functor (FreeGroupoid C) G) (τ : (of C).comp F₁ ≅ (of C).comp F₂) : F₁ ≅ F₂

In order to define a natural isomorphism F ≅ G with F G : FreeGroupoid ⥤ D, it suffices to do so after precomposing with FreeGroupoid.of C.

@[simp]

theorem CategoryTheory.FreeGroupoid.liftNatIso_hom_app {C : Type u} [Category.{v, u} C] {G : Type u₁} [Groupoid G] (F₁ F₂ : Functor (FreeGroupoid C) G) (τ : (of C).comp F₁ ≅ (of C).comp F₂) (X : C) : (liftNatIso F₁ F₂ τ).hom.app (mk X) = τ.hom.app X

@[simp]

theorem CategoryTheory.FreeGroupoid.liftNatIso_inv_app {C : Type u} [Category.{v, u} C] {G : Type u₁} [Groupoid G] (F₁ F₂ : Functor (FreeGroupoid C) G) (τ : (of C).comp F₁ ≅ (of C).comp F₂) (X : C) : (liftNatIso F₁ F₂ τ).inv.app (mk X) = τ.inv.app X

def CategoryTheory.FreeGroupoid.map {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (φ : Functor C D) : Functor (FreeGroupoid C) (FreeGroupoid D)

The functor between free groupoids induced by a functor between categories.

theorem CategoryTheory.FreeGroupoid.of_comp_map {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) : (of C).comp (map F) = F.comp (of D)

def CategoryTheory.FreeGroupoid.ofCompMapIso {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) : (of C).comp (map F) ≅ F.comp (of D)

The operation of is natural.

noncomputable def CategoryTheory.FreeGroupoid.mapId (C : Type u) [Category.{v, u} C] : map (Functor.id C) ≅ Functor.id (FreeGroupoid C)

The functor induced by the identity is the identity.

@[simp]

theorem CategoryTheory.FreeGroupoid.mapId_hom_app {C : Type u} [Category.{v, u} C] (X : FreeGroupoid C) : (mapId C).hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.FreeGroupoid.mapId_inv_app {C : Type u} [Category.{v, u} C] (X : FreeGroupoid C) : (mapId C).inv.app X = CategoryStruct.id X

theorem CategoryTheory.FreeGroupoid.map_id (C : Type u) [Category.{v, u} C] : map (Functor.id C) = Functor.id (FreeGroupoid C)

noncomputable def CategoryTheory.FreeGroupoid.mapComp {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Category.{v₂, u₂} E] (φ : Functor C D) (φ' : Functor D E) : map (φ.comp φ') ≅ (map φ).comp (map φ')

The functor induced by a composition is the composition of the functors they induce.

@[simp]

theorem CategoryTheory.FreeGroupoid.mapComp_hom_app {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Category.{v₂, u₂} E] (φ : Functor C D) (φ' : Functor D E) (X : FreeGroupoid C) : (mapComp φ φ').hom.app X = CategoryStruct.id ((map (φ.comp φ')).obj X)

@[simp]

theorem CategoryTheory.FreeGroupoid.mapComp_inv_app {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Category.{v₂, u₂} E] (φ : Functor C D) (φ' : Functor D E) (X : FreeGroupoid C) : (mapComp φ φ').inv.app X = CategoryStruct.id (((map φ).comp (map φ')).obj X)

theorem CategoryTheory.FreeGroupoid.map_comp {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Category.{v₂, u₂} E] (φ : Functor C D) (φ' : Functor D E) : map (φ.comp φ') = (map φ).comp (map φ')

@[simp]

theorem CategoryTheory.FreeGroupoid.map_obj_mk {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (φ : Functor C D) (X : C) : (map φ).obj (mk X) = mk (φ.obj X)

@[simp]

theorem CategoryTheory.FreeGroupoid.map_map_homMk {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (φ : Functor C D) {X Y : C} (f : X ⟶ Y) : (map φ).map (homMk f) = homMk (φ.map f)

theorem CategoryTheory.FreeGroupoid.map_comp_lift {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Groupoid E] (F : Functor C D) (G : Functor D E) : (map F).comp (lift G) = lift (F.comp G)

noncomputable def CategoryTheory.FreeGroupoid.mapCompLift {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Groupoid E] (F : Functor C D) (G : Functor D E) : (map F).comp (lift G) ≅ lift (F.comp G)

The operation lift is natural.

@[simp]

theorem CategoryTheory.FreeGroupoid.mapCompLift_hom_app {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Groupoid E] (F : Functor C D) (G : Functor D E) (X : FreeGroupoid C) : (mapCompLift F G).hom.app X = CategoryStruct.id (((map F).comp (lift G)).obj X)

@[simp]

theorem CategoryTheory.FreeGroupoid.mapCompLift_inv_app {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {E : Type u₂} [Groupoid E] (F : Functor C D) (G : Functor D E) (X : FreeGroupoid C) : (mapCompLift F G).inv.app X = CategoryStruct.id ((lift (F.comp G)).obj X)

def CategoryTheory.FreeGroupoid.functorEquiv {C : Type u} [Category.{v, u} C] {D : Type u_1} [Groupoid D] : Functor (FreeGroupoid C) D ≃ Functor C D

Functors out of the free groupoid biject with functors out of the original category.

@[simp]

theorem CategoryTheory.FreeGroupoid.functorEquiv_apply {C : Type u} [Category.{v, u} C] {D : Type u_1} [Groupoid D] (G : Functor (FreeGroupoid C) D) : functorEquiv G = (of C).comp G

@[simp]

theorem CategoryTheory.FreeGroupoid.functorEquiv_symm_apply {C : Type u} [Category.{v, u} C] {D : Type u_1} [Groupoid D] (F : Functor C D) : functorEquiv.symm F = lift F

def CategoryTheory.Grpd.free : Functor Cat Grpd

The free groupoid construction on a category as a functor.

@[simp]

theorem CategoryTheory.Grpd.free_obj (C : Cat) : ↑(free.obj C) = FreeGroupoid ↑C

@[simp]

theorem CategoryTheory.Grpd.free_map {C D : Cat} (F : C ⟶ D) : free.map F = FreeGroupoid.map F.toFunctor

def CategoryTheory.Grpd.freeForgetAdjunction : free ⊣ forgetToCat

The free-forgetful adjunction between Grpd and Cat.

@[simp]

theorem CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_apply {C : Type u} [Category.{u, u} C] {D : Type u} [Groupoid D] (F : Functor (FreeGroupoid C) D) : ((freeForgetAdjunction.homEquiv (Cat.of C) (of D)) F).toFunctor = (FreeGroupoid.of C).comp F

@[simp]

theorem CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_symm_apply {C : Type u} [Category.{u, u} C] {D : Type u} [Groupoid D] (F : Functor C D) : (freeForgetAdjunction.homEquiv (Cat.of C) (of D)).symm F.toCatHom = (FreeGroupoid.map F).comp (FreeGroupoid.lift (Functor.id D))

@[simp]

theorem CategoryTheory.Grpd.freeForgetAdjunction_unit_app {C : Type u} [Category.{u, u} C] : (freeForgetAdjunction.unit.app (Cat.of C)).toFunctor = FreeGroupoid.of C

@[simp]

theorem CategoryTheory.Grpd.freeForgetAdjunction_counit_app {D : Type u} [Groupoid D] : freeForgetAdjunction.counit.app (of D) = FreeGroupoid.lift (Functor.id D)

@[implicit_reducible]

instance CategoryTheory.Grpd.instReflectiveCatForgetToCat : Reflective forgetToCat