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.

Equations

• CategoryTheory.ReflQuiv = CategoryTheory.Bundled CategoryTheory.ReflQuiver

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

Equations

• CategoryTheory.ReflQuiv.instCoeSortType = { coe := CategoryTheory.Bundled.α }

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

Equations

• C.instReflQuiverα = C.str

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

The underlying quiver of a reflexive quiver.

Equations

• C.toQuiv = CategoryTheory.Quiv.of ↑C

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

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

Equations

• CategoryTheory.ReflQuiv.of C = CategoryTheory.Bundled.of C

instance CategoryTheory.ReflQuiv.instInhabited : Inhabited CategoryTheory.ReflQuiv

Equations

• CategoryTheory.ReflQuiv.instInhabited = { default := CategoryTheory.ReflQuiv.of (CategoryTheory.Discrete default) }

@[simp]

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

instance CategoryTheory.ReflQuiv.category : CategoryTheory.LargeCategory CategoryTheory.ReflQuiv

Category structure on ReflQuiv

Equations

• CategoryTheory.ReflQuiv.category = CategoryTheory.Category.mk @CategoryTheory.ReflQuiv.category.proof_1 @CategoryTheory.ReflQuiv.category.proof_1 @CategoryTheory.ReflQuiv.category.proof_2

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

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

def CategoryTheory.ReflQuiv.forget : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.ReflQuiv

The forgetful functor from categories to quivers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

theorem CategoryTheory.ReflQuiv.forget.Faithful : CategoryTheory.ReflQuiv.forget.Faithful

def CategoryTheory.ReflQuiv.forgetToQuiv : CategoryTheory.Functor CategoryTheory.ReflQuiv CategoryTheory.Quiv

The forgetful functor from categories to quivers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

theorem CategoryTheory.ReflQuiv.forgetToQuiv.Faithful : CategoryTheory.ReflQuiv.forgetToQuiv.Faithful

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

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

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

Equations

• CategoryTheory.ReflPrefunctor.toFunctor F hyp = { obj := F.obj, map := fun {X Y : ↑C} => F.map, map_id := ⋯, map_comp := ⋯ }

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

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

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

def CategoryTheory.Cat.FreeRefl (V : Type u_1) [CategoryTheory.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.

Equations

• CategoryTheory.Cat.FreeRefl V = CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel

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

Equations

• CategoryTheory.Cat.instCategoryFreeRefl V = inferInstanceAs (CategoryTheory.Category.{max ?u.19 ?u.18, ?u.19} (CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel))

def CategoryTheory.Cat.FreeRefl.quotientFunctor (V : Type u_1) [CategoryTheory.ReflQuiver V] : CategoryTheory.Functor (↑(CategoryTheory.Cat.free.obj (CategoryTheory.Quiv.of V))) (CategoryTheory.Cat.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.

Equations

• CategoryTheory.Cat.FreeRefl.quotientFunctor V = CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel

theorem CategoryTheory.Cat.FreeRefl.lift_unique' {V : Type u_1} [CategoryTheory.ReflQuiver V] {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (F₁ : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) D) (F₂ : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) D) (h : (CategoryTheory.Cat.FreeRefl.quotientFunctor V).comp F₁ = (CategoryTheory.Cat.FreeRefl.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.

def CategoryTheory.Cat.freeRefl : CategoryTheory.Functor CategoryTheory.ReflQuiv CategoryTheory.Cat

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Cat.freeRefl_obj_str_comp (V : CategoryTheory.ReflQuiv) ⦃a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel⦄ ⦃b : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel⦄ ⦃c : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel⦄ : ∀ (a_1 : CategoryTheory.Quotient.Hom CategoryTheory.Cat.FreeReflRel a b) (a_2 : CategoryTheory.Quotient.Hom CategoryTheory.Cat.FreeReflRel b c), CategoryTheory.CategoryStruct.comp a_1 a_2 = CategoryTheory.Quotient.comp CategoryTheory.Cat.FreeReflRel a_1 a_2

@[simp]

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

@[simp]

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

theorem CategoryTheory.Cat.freeRefl_naturality {X : Type u_1} {Y : Type u_1} [CategoryTheory.ReflQuiver X] [CategoryTheory.ReflQuiver Y] (f : X ⥤rq Y) : CategoryTheory.Functor.comp (CategoryTheory.Cat.free.map f.toPrefunctor) (CategoryTheory.Cat.FreeRefl.quotientFunctor Y) = (CategoryTheory.Cat.FreeRefl.quotientFunctor X).comp (CategoryTheory.Cat.freeRefl.map f)

def CategoryTheory.Cat.freeReflNatTrans : CategoryTheory.ReflQuiv.forgetToQuiv.comp CategoryTheory.Cat.free ⟶ CategoryTheory.Cat.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.

Equations

• CategoryTheory.Cat.freeReflNatTrans = { app := fun (V : CategoryTheory.ReflQuiv) => CategoryTheory.Cat.FreeRefl.quotientFunctor ↑V, naturality := CategoryTheory.Cat.freeReflNatTrans.proof_1 }

def CategoryTheory.ReflQuiv.adj.unit.app (V : CategoryTheory.ReflQuiv) : ↑V ⥤rq ↑(CategoryTheory.ReflQuiv.forget.obj (CategoryTheory.Cat.freeRefl.obj 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ReflQuiv.adj.unit.app_toPrefunctor (V : CategoryTheory.ReflQuiv) : (CategoryTheory.ReflQuiv.adj.unit.app V).toPrefunctor = CategoryTheory.Quiv.adj.unit.app V.toQuiv ⋙q (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑V).toPrefunctor

@[simp]

theorem CategoryTheory.ReflQuiv.adj.unit.app_obj (V : CategoryTheory.ReflQuiv) (X : ↑V) : (CategoryTheory.ReflQuiv.adj.unit.app V).obj X = (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑V).obj ((CategoryTheory.Quiv.adj.unit.app V.toQuiv).obj X)

@[simp]

theorem CategoryTheory.ReflQuiv.adj.unit.app_map (V : CategoryTheory.ReflQuiv) : ∀ {X Y : ↑V} (f : X ⟶ Y), (CategoryTheory.ReflQuiv.adj.unit.app V).map f = (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑V).map ((CategoryTheory.Quiv.adj.unit.app V.toQuiv).map f)

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

This is used in the proof of both triangle equalities.

def CategoryTheory.ReflQuiv.adj.counit.app (C : CategoryTheory.Cat) : CategoryTheory.Functor ↑(CategoryTheory.Cat.freeRefl.obj (CategoryTheory.ReflQuiv.forget.obj 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.

Equations

• CategoryTheory.ReflQuiv.adj.counit.app C = CategoryTheory.Quotient.lift CategoryTheory.Cat.FreeReflRel (CategoryTheory.Quiv.adj.counit.app C) ⋯

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.app_map (C : CategoryTheory.Cat) (a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) (b : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) (hf : a ⟶ b) : (CategoryTheory.ReflQuiv.adj.counit.app C).map hf = Quot.liftOn hf (fun (f : a.as ⟶ b.as) => (CategoryTheory.Quiv.adj.counit.app C).map f) ⋯

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.app_obj (C : CategoryTheory.Cat) (a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) : (CategoryTheory.ReflQuiv.adj.counit.app C).obj a = (CategoryTheory.Quiv.adj.counit.app C).obj a.as

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.component_eq (C : CategoryTheory.Cat) : (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑C).comp (CategoryTheory.ReflQuiv.adj.counit.app C) = CategoryTheory.Quiv.adj.counit.app C

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

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.component_eq' (C : Type u_1) [CategoryTheory.Category.{max u_1 u_2, u_1} C] : (CategoryTheory.Cat.FreeRefl.quotientFunctor C).comp (CategoryTheory.ReflQuiv.adj.counit.app (CategoryTheory.Cat.of C)) = CategoryTheory.Quiv.adj.counit.app (CategoryTheory.Cat.of C)

The counit of ReflQuiv.adj is closely related to the counit of Quiv.adj. For ease of use, we introduce primed version for unbundled categories.

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

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

Equations

• One or more equations did not get rendered due to their size.