The category of refl quivers

The category ReflQuiv of (bundled) reflexive quivers, and the free/forgetful adjunction between Cat and ReflQuiv.

def CategoryTheory.ReflQuiv : Type (max (u + 1) u (v + 1))

Category of refl quivers.

instance CategoryTheory.ReflQuiv.instCoeSortType : CoeSort ReflQuiv (Type u)

instance CategoryTheory.ReflQuiv.instReflQuiverα (C : ReflQuiv) : ReflQuiver ↑C

def CategoryTheory.ReflQuiv.toQuiv (C : ReflQuiv) : Quiv

The underlying quiver of a reflexive quiver

def CategoryTheory.ReflQuiv.of (C : Type u) [ReflQuiver C] : ReflQuiv

Construct a bundled ReflQuiv from the underlying type and the typeclass.

instance CategoryTheory.ReflQuiv.instInhabited : Inhabited ReflQuiv

@[simp]

theorem CategoryTheory.ReflQuiv.of_val (C : Type u) [ReflQuiver C] : ↑(of C) = C

instance CategoryTheory.ReflQuiv.category : LargeCategory ReflQuiv

Category structure on ReflQuiv

theorem CategoryTheory.ReflQuiv.id_eq_id (X : ReflQuiv) : CategoryStruct.id X = 𝟭rq ↑X

theorem CategoryTheory.ReflQuiv.comp_eq_comp {X Y Z : ReflQuiv} (F : X ⟶ Y) (G : Y ⟶ Z) : CategoryStruct.comp F G = F ⋙rq G

def CategoryTheory.ReflQuiv.forget : Functor Cat ReflQuiv

The forgetful functor from categories to quivers.

@[simp]

theorem CategoryTheory.ReflQuiv.forget_obj (C : Cat) : forget.obj C = of ↑C

@[simp]

theorem CategoryTheory.ReflQuiv.forget_map {X✝ Y✝ : Cat} (F : X✝ ⟶ Y✝) : forget.map F = Functor.toReflPrefunctor F

theorem CategoryTheory.ReflQuiv.forget_faithful {C D : Cat} (F G : Functor ↑C ↑D) (hyp : forget.map F = forget.map G) : F = G

instance CategoryTheory.ReflQuiv.forget.Faithful : forget.Faithful

def CategoryTheory.ReflQuiv.forgetToQuiv : Functor ReflQuiv Quiv

The forgetful functor from categories to quivers.

@[simp]

theorem CategoryTheory.ReflQuiv.forgetToQuiv_obj (V : ReflQuiv) : forgetToQuiv.obj V = Quiv.of ↑V

@[simp]

theorem CategoryTheory.ReflQuiv.forgetToQuiv_map {X✝ Y✝ : ReflQuiv} (F : X✝ ⟶ Y✝) : forgetToQuiv.map F = F.toPrefunctor

theorem CategoryTheory.ReflQuiv.forgetToQuiv_faithful {V W : ReflQuiv} (F G : ↑V ⥤rq ↑W) (hyp : forgetToQuiv.map F = forgetToQuiv.map G) : F = G

instance CategoryTheory.ReflQuiv.forgetToQuiv.Faithful : forgetToQuiv.Faithful

theorem CategoryTheory.ReflQuiv.forget_forgetToQuiv : forget.comp forgetToQuiv = Quiv.forget

def CategoryTheory.ReflQuiv.isoOfQuivIso {V W : Type u} [ReflQuiver V] [ReflQuiver W] (e : Quiv.of V ≅ Quiv.of W) (h_id : ∀ (X : V), e.hom.map (ReflQuiver.id X) = ReflQuiver.id (e.hom.obj X)) : of V ≅ of W

An isomorphism of quivers lifts to an isomorphism of reflexive quivers given a suitable compatibility with the identities.

def CategoryTheory.ReflQuiv.isoOfEquiv {V W : Type u} [ReflQuiver V] [ReflQuiver W] (e : V ≃ W) (he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)) (h_id : ∀ (X : V), (he X X) (ReflQuiver.id X) = ReflQuiver.id (e X)) : of V ≅ of W

Compatible equivalences of types and hom-types induce an isomorphism of reflexive quivers.

def CategoryTheory.ReflPrefunctor.toFunctor {C D : Cat} (F : ReflQuiv.of ↑C ⟶ ReflQuiv.of ↑D) (hyp : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), F.map (CategoryStruct.comp f g) = CategoryStruct.comp (F.map f) (F.map g)) : Functor ↑C ↑D

A refl prefunctor can be promoted to a functor if it respects composition.

inductive CategoryTheory.Cat.FreeReflRel {V : Type u_1} [ReflQuiver V] (X Y : Paths V) (f g : X ⟶ Y) : Prop

The hom relation that identifies the specified reflexivity arrows with the nil paths

• mk {V : Type u_1} [ReflQuiver V] {X : V} : FreeReflRel X X (ReflQuiver.id X).toPath Quiver.Path.nil

def CategoryTheory.Cat.FreeRefl (V : Type u_1) [ReflQuiver V] : Type u_1

A reflexive quiver generates a free category, defined as as quotient of the free category on its underlying quiver (called the "path category") by the hom relation that uses the specified reflexivity arrows as the identity arrows.

instance CategoryTheory.Cat.instCategoryFreeRefl (V : Type u_1) [ReflQuiver V] : Category.{max u_1 u_2, u_1} (FreeRefl V)

def CategoryTheory.Cat.FreeRefl.quotientFunctor (V : Type u_1) [ReflQuiver V] : Functor (Paths V) (FreeRefl V)

The quotient functor associated to a quotient category defines a natural map from the free category on the underlying quiver of a refl quiver to the free category on the reflexive quiver.

theorem CategoryTheory.Cat.FreeRefl.lift_unique' {V : Type u_1} [ReflQuiver V] {D : Type u_3} [Category.{u_4, u_3} D] (F₁ F₂ : Functor (FreeRefl V) D) (h : (quotientFunctor V).comp F₁ = (quotientFunctor V).comp F₂) : F₁ = F₂

This is a specialization of Quotient.lift_unique' rather than Quotient.lift_unique, hence the prime in the name.

@[simp]

theorem CategoryTheory.Cat.FreeRefl.quotientFunctor_map_id (V : Type u_1) [ReflQuiver V] (X : V) : (quotientFunctor V).map (ReflQuiver.id X).toPath = CategoryStruct.id ((quotientFunctor V).obj X)

instance CategoryTheory.Cat.instUniqueFreeRefl (V : Type u_1) [ReflQuiver V] [Unique V] : Unique (FreeRefl V)

instance CategoryTheory.Cat.instUniqueHomFreeRefl (V : Type u_1) [ReflQuiver V] [Unique V] [(x y : V) → Unique (x ⟶ y)] (x y : FreeRefl V) : Unique (x ⟶ y)

def CategoryTheory.Cat.freeReflMap {V : Type u_1} {W : Type u_2} [ReflQuiver V] [ReflQuiver W] (F : V ⥤rq W) : Functor (FreeRefl V) (FreeRefl W)

A refl prefunctor V ⥤rq W induces a functor FreeRefl V ⥤ FreeRefl W defined using freeMap and the quotient functor.

@[simp]

theorem CategoryTheory.Cat.freeReflMap_obj_as {V : Type u_1} {W : Type u_2} [ReflQuiver V] [ReflQuiver W] (F : V ⥤rq W) (a : Quotient FreeReflRel) : ((freeReflMap F).obj a).as = F.obj a.as

@[simp]

theorem CategoryTheory.Cat.freeReflMap_map {V : Type u_1} {W : Type u_2} [ReflQuiver V] [ReflQuiver W] (F : V ⥤rq W) (a b : Quotient FreeReflRel) (hf : a ⟶ b) : (freeReflMap F).map hf = Quot.liftOn hf (fun (f : a.as ⟶ b.as) => (FreeRefl.quotientFunctor W).map (F.mapPath f)) ⋯

theorem CategoryTheory.Cat.freeReflMap_naturality {V : Type u_1} {W : Type u_2} [ReflQuiver V] [ReflQuiver W] (F : V ⥤rq W) : (FreeRefl.quotientFunctor V).comp (freeReflMap F) = (freeMap F.toPrefunctor).comp (FreeRefl.quotientFunctor W)

def CategoryTheory.Cat.freeRefl : Functor ReflQuiv Cat

The functor sending a reflexive quiver to the free category it generates, a quotient of its path category

@[simp]

theorem CategoryTheory.Cat.freeRefl_obj_str_id (V : ReflQuiv) (a : Quotient FreeReflRel) : CategoryStruct.id a = Quot.mk (Quotient.CompClosure FreeReflRel) (CategoryStruct.id a.as)

@[simp]

theorem CategoryTheory.Cat.freeRefl_map_map {X✝ Y✝ : ReflQuiv} (F : X✝ ⟶ Y✝) (a b : Quotient FreeReflRel) (hf : a ⟶ b) : (freeRefl.map F).map hf = Quot.liftOn hf (fun (f : a.as ⟶ b.as) => (FreeRefl.quotientFunctor ↑Y✝).map (F.mapPath f)) ⋯

@[simp]

theorem CategoryTheory.Cat.freeRefl_obj_α (V : ReflQuiv) : ↑(freeRefl.obj V) = FreeRefl ↑V

@[simp]

theorem CategoryTheory.Cat.freeRefl_map_obj_as {X✝ Y✝ : ReflQuiv} (F : X✝ ⟶ Y✝) (a : Quotient FreeReflRel) : ((freeRefl.map F).obj a).as = F.obj a.as

@[simp]

theorem CategoryTheory.Cat.freeRefl_obj_str_comp (V : ReflQuiv) ⦃a b c : Quotient FreeReflRel⦄ (a✝ : Quotient.Hom FreeReflRel a b) (a✝¹ : Quotient.Hom FreeReflRel b c) : CategoryStruct.comp a✝ a✝¹ = Quotient.comp FreeReflRel a✝ a✝¹

def CategoryTheory.Cat.freeReflNatTrans : ReflQuiv.forgetToQuiv.comp free ⟶ freeRefl

We will make use of the natural quotient map from the free category on the underlying quiver of a refl quiver to the free category on the reflexive quiver.

def CategoryTheory.ReflQuiv.adj.unit.app (V : Type u) [ReflQuiver V] : V ⥤rq ↑(forget.obj (Cat.freeRefl.obj (of V)))

The unit components are defined as the composite of the corresponding unit component for the adjunction between categories and quivers with the map underlying the quotient functor.

@[simp]

theorem CategoryTheory.ReflQuiv.adj.unit.app_map (V : Type u) [ReflQuiver V] {X✝ Y✝ : V} (f : X✝ ⟶ Y✝) : (app V).map f = (Cat.FreeRefl.quotientFunctor V).map f.toPath

@[simp]

theorem CategoryTheory.ReflQuiv.adj.unit.app_obj (V : Type u) [ReflQuiver V] (X : V) : (app V).obj X = (Cat.FreeRefl.quotientFunctor V).obj X

@[simp]

theorem CategoryTheory.ReflQuiv.adj.unit.app_toPrefunctor (V : Type u) [ReflQuiver V] : (app V).toPrefunctor = Paths.of V ⋙q (Cat.FreeRefl.quotientFunctor V).toPrefunctor

theorem CategoryTheory.ReflQuiv.adj.unit.map_app_eq (V : ReflQuiv) : forgetToQuiv.map (app ↑V) = CategoryStruct.comp (Quiv.adj.unit.app V.toQuiv) (Quiv.forget.map (Cat.FreeRefl.quotientFunctor ↑V))

This is used in the proof of both triangle equalities.

def CategoryTheory.ReflQuiv.adj.counit.app (C : Type u) [Category.{max u v, u} C] : Functor (↑(Cat.freeRefl.obj (of C))) C

The counit components are defined using the universal property of the quotient from the corresponding counit component for the adjunction between categories and quivers.

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.app_obj (C : Type u) [Category.{max u v, u} C] (a : Quotient Cat.FreeReflRel) : (app C).obj a = a.as

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.app_map (C : Type u) [Category.{max u v, u} C] (a b : Quotient Cat.FreeReflRel) (hf : a ⟶ b) : (app C).map hf = Quot.liftOn hf (fun (f : a.as ⟶ b.as) => composePath f) ⋯

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.comp_app_eq (C : Type u) [Category.{max u u_1, u} C] : (Cat.FreeRefl.quotientFunctor C).comp (app C) = pathComposition ↑(Cat.of C)

The counit of ReflQuiv.adj is closely related to the counit of Quiv.adj.

def CategoryTheory.ReflQuiv.adj : Cat.freeRefl ⊣ forget

The adjunction between forming the free category on a reflexive quiver, and forgetting a category to a reflexive quiver.