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 ReflQuiv (Type u)

Equations

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

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

Equations

• C.instReflQuiverα = C.str

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

The underlying quiver of a reflexive quiver

Equations

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

def CategoryTheory.ReflQuiv.of (C : Type u) [ReflQuiver C] : 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 ReflQuiv

Equations

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

@[simp]

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

instance CategoryTheory.ReflQuiv.category : LargeCategory ReflQuiv

Category structure on ReflQuiv

Equations

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

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

@[simp]

theorem CategoryTheory.ReflQuiv.id_obj (X : ReflQuiv) (x : ↑X) : (CategoryStruct.id X).obj x = x

@[simp]

theorem CategoryTheory.ReflQuiv.id_map {X : ReflQuiv} {x y : ↑X} (f : x ⟶ y) : (CategoryStruct.id X).map f = f

@[simp]

theorem CategoryTheory.ReflQuiv.comp_obj {X Y Z : ReflQuiv} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) : (CategoryStruct.comp f g).obj x = g.obj (f.obj x)

@[simp]

theorem CategoryTheory.ReflQuiv.comp_map {X Y Z : ReflQuiv} (f : X ⟶ Y) (g : Y ⟶ Z) {x y : ↑X} (a : x ⟶ y) : (CategoryStruct.comp f g).map a = g.map (f.map a)

def CategoryTheory.ReflQuiv.forget : Functor Cat 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_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.

Equations

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

@[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.

Equations

• CategoryTheory.ReflQuiv.isoOfQuivIso e h_id = { hom := { toPrefunctor := e.hom, map_id := h_id }, inv := { toPrefunctor := e.inv, map_id := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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.

Equations

• CategoryTheory.ReflQuiv.isoOfEquiv e he h_id = CategoryTheory.ReflQuiv.isoOfQuivIso (CategoryTheory.Quiv.isoOfEquiv e he) h_id

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.

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) [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 V 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 a 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 V)

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

Equations

• CategoryTheory.Cat.FreeRefl.instCategory = inferInstanceAs (CategoryTheory.Category.{max ?u.14 ?u.13, ?u.14} (CategoryTheory.Quotient (CategoryTheory.Cat.FreeReflRel V)))

def CategoryTheory.Cat.FreeRefl.mk {V : Type u_1} [ReflQuiver V] (v : V) : FreeRefl V

Constructor for objects in the free category on a reflexive quiver.

Equations

• CategoryTheory.Cat.FreeRefl.mk v = (CategoryTheory.Quotient.functor (CategoryTheory.Cat.FreeReflRel V)).obj v

def CategoryTheory.Cat.FreeRefl.induction {V : Type u_1} [ReflQuiver V] {motive : FreeRefl V → Sort u_2} (mk : (v : V) → motive (mk v)) (x : FreeRefl V) : motive x

Induction principle for the objects of the free category on a reflexive quiver.

Equations

• CategoryTheory.Cat.FreeRefl.induction mk x = mk x.as

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.

Equations

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

instance CategoryTheory.Cat.FreeRefl.instFullPathsQuotientFunctor {V : Type u_1} [ReflQuiver V] : (quotientFunctor V).Full

def CategoryTheory.Cat.FreeRefl.homMk {V : Type u_1} [ReflQuiver V] {v w : V} (f : v ⟶ w) : mk v ⟶ mk w

Constructor for morphisms in FreeRefl.

Equations

• CategoryTheory.Cat.FreeRefl.homMk f = (CategoryTheory.Cat.FreeRefl.quotientFunctor V).map f.toPath

@[simp]

theorem CategoryTheory.Cat.FreeRefl.homMk_id {V : Type u_1} [ReflQuiver V] (v : V) : homMk (ReflQuiver.id v) = CategoryStruct.id (mk v)

@[simp]

theorem CategoryTheory.Cat.FreeRefl.quotientFunctor_map_nil {V : Type u_1} [ReflQuiver V] (x : Paths V) : (quotientFunctor V).map Quiver.Path.nil = CategoryStruct.id ((quotientFunctor V).obj x)

@[simp]

theorem CategoryTheory.Cat.FreeRefl.quotientFunctor_map_cons {V : Type u_1} [ReflQuiver V] {x y z : Paths V} (p : x ⟶ y) (q : y ⟶ z) : (quotientFunctor V).map (Quiver.Path.cons p q) = CategoryStruct.comp ((quotientFunctor V).map p) (homMk q)

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

The property of morphisms in FreeRefl V which are of the form homMk f for some morphism f : x ⟶ y in V.

Equations

• CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk V = CategoryTheory.MorphismProperty.ofHoms fun (e : (x : V) × (y : V) × (x ⟶ y)) => CategoryTheory.Cat.FreeRefl.homMk e.snd.snd

theorem CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk_homMk {V : Type u_1} [ReflQuiver V] {x y : V} (e : x ⟶ y) : morphismPropertyHomMk V (homMk e)

theorem CategoryTheory.Cat.FreeRefl.hom_induction {V : Type u_1} [ReflQuiver V] {motive : {x y : FreeRefl V} → (x ⟶ y) → Prop} (id : ∀ (x : V), motive (homMk (ReflQuiver.id x))) (comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (CategoryStruct.comp f (homMk g))) {x y : FreeRefl V} (f : x ⟶ y) : motive f

theorem CategoryTheory.Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk {V : Type u_1} [ReflQuiver V] : (morphismPropertyHomMk V).multiplicativeClosure = ⊤

theorem CategoryTheory.Cat.FreeRefl.morphismProperty_eq_top {V : Type u_1} [ReflQuiver V] {W : MorphismProperty (FreeRefl V)} [W.IsMultiplicative] (hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)) : W = ⊤

def CategoryTheory.Cat.FreeRefl.lift {V : Type u_1} [ReflQuiver V] {D : Type u_2} [Category.{u_4, u_2} D] (F : V ⥤rq D) : Functor (FreeRefl V) D

Constructor for functors from FreeRefl. (See also lift' for which the data is unbundled.)

Equations

• CategoryTheory.Cat.FreeRefl.lift F = CategoryTheory.Quotient.lift (CategoryTheory.Cat.FreeReflRel V) (CategoryTheory.Paths.lift F.toPrefunctor) ⋯

@[simp]

theorem CategoryTheory.Cat.FreeRefl.lift_obj {V : Type u_1} [ReflQuiver V] {D : Type u_2} [Category.{u_4, u_2} D] (F : V ⥤rq D) (v : V) : (lift F).obj (mk v) = F.obj v

@[simp]

theorem CategoryTheory.Cat.FreeRefl.lift_map {V : Type u_1} [ReflQuiver V] {D : Type u_2} [Category.{u_4, u_2} D] (F : V ⥤rq D) {v w : V} (f : v ⟶ w) : (lift F).map (homMk f) = F.map f

def CategoryTheory.Cat.FreeRefl.lift' {V : Type u_1} [ReflQuiver V] {D : Type u_2} [Category.{u_4, u_2} D] (obj : V → D) (map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w)) (map_id : ∀ (v : V), map (ReflQuiver.id v) = CategoryStruct.id (obj v)) : Functor (FreeRefl V) D

Constructor for functors from FreeRefl. (See also lift for which the data is bundled.)

Equations

• CategoryTheory.Cat.FreeRefl.lift' obj map map_id = CategoryTheory.Cat.FreeRefl.lift { obj := obj, map := fun {X Y : V} => map, map_id := map_id }

@[simp]

theorem CategoryTheory.Cat.FreeRefl.lift'_obj {V : Type u_1} [ReflQuiver V] {D : Type u_2} [Category.{u_4, u_2} D] (obj : V → D) (map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w)) (map_id : ∀ (v : V), map (ReflQuiver.id v) = CategoryStruct.id (obj v)) (v : V) : (lift' obj (fun {v w : V} => map) map_id).obj (mk v) = obj v

@[simp]

theorem CategoryTheory.Cat.FreeRefl.lift'_map {V : Type u_1} [ReflQuiver V] {D : Type u_2} [Category.{u_4, u_2} D] (obj : V → D) (map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w)) (map_id : ∀ (v : V), map (ReflQuiver.id v) = CategoryStruct.id (obj v)) {v w : V} (f : v ⟶ w) : (lift' obj (fun {v w : V} => map) map_id).map (homMk f) = map f

theorem CategoryTheory.Cat.FreeRefl.lift_unique' {V : Type u_2} [ReflQuiver V] {D : Type u_4} [Category.{u_5, u_4} 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.

theorem CategoryTheory.Cat.FreeRefl.functor_ext {V : Type u_1} [ReflQuiver V] {D : Type u_2} [Category.{u_3, u_2} D] {F G : Functor (FreeRefl V) D} (h₁ : ∀ (v : V), F.obj (mk v) = G.obj (mk v)) (h₂ : ∀ {v w : V} (f : v ⟶ w), F.map (homMk f) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G.map (homMk f)) (eqToHom ⋯))) : F = G

@[simp]

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

instance CategoryTheory.Cat.FreeRefl.instUnique (V : Type u_2) [ReflQuiver V] [Unique V] : Unique (FreeRefl V)

Equations

• CategoryTheory.Cat.FreeRefl.instUnique V = inferInstanceAs (Unique (CategoryTheory.Quotient (CategoryTheory.Cat.FreeReflRel V)))

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

Equations

• CategoryTheory.Cat.FreeRefl.instUniqueHom V x y = { default := CategoryTheory.Cat.FreeRefl.homMk default, uniq := ⋯ }

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

Given a refl quiver V, this is the refl functor V ⥤rq FreeRefl V which is the counit of the adjunction between reflexive quivers and categories.

Equations

• CategoryTheory.Cat.toFreeRefl V = { obj := CategoryTheory.Cat.FreeRefl.mk, map := fun {X Y : V} => CategoryTheory.Cat.FreeRefl.homMk, map_id := ⋯ }

@[simp]

theorem CategoryTheory.Cat.toFreeRefl_map (V : Type u_1) [ReflQuiver V] {X✝ Y✝ : V} (f : X✝ ⟶ Y✝) : (toFreeRefl V).map f = FreeRefl.homMk f

@[simp]

theorem CategoryTheory.Cat.toFreeRefl_obj (V : Type u_1) [ReflQuiver V] (v : V) : (toFreeRefl V).obj v = FreeRefl.mk v

theorem CategoryTheory.Cat.FreeRefl.lift_spec {V : Type u_1} [ReflQuiver V] {D : Type u_2} [Category.{u_3, u_2} D] (F : V ⥤rq D) : toFreeRefl V ⋙rq (lift F).toReflPrefunctor = F

Constructor for functors from FreeRefl.

def CategoryTheory.Cat.freeReflMap {V : Type u_1} [ReflQuiver V] {W : Type u_2} [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.

Equations

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

@[simp]

theorem CategoryTheory.Cat.freeReflMap_obj {V : Type u_1} [ReflQuiver V] {W : Type u_2} [ReflQuiver W] (F : V ⥤rq W) (v : V) : (freeReflMap F).obj (FreeRefl.mk v) = FreeRefl.mk (F.obj v)

@[simp]

theorem CategoryTheory.Cat.freeReflMap_map {V : Type u_1} [ReflQuiver V] {W : Type u_2} [ReflQuiver W] (F : V ⥤rq W) {v w : V} (f : v ⟶ w) : (freeReflMap F).map (FreeRefl.homMk f) = FreeRefl.homMk (F.map f)

theorem CategoryTheory.Cat.freeReflMap_naturality {V : Type u_3} {W : Type u_4} [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

Equations

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

@[simp]

theorem CategoryTheory.Cat.freeRefl_obj (V : ReflQuiv) : freeRefl.obj V = of (FreeRefl ↑V)

@[simp]

theorem CategoryTheory.Cat.freeRefl_map {X✝ Y✝ : ReflQuiv} (F : X✝ ⟶ Y✝) : freeRefl.map F = freeReflMap F

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.

Equations

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

def CategoryTheory.ReflQuiv.adj.homEquiv {V : Type u_1} [ReflQuiver V] {C : Type u_3} [Category.{u_6, u_3} C] : Functor (Cat.FreeRefl V) C ≃ V ⥤rq C

Given a reflexive quiver V and a category C, this is the bijection between functors Cat.FreeRefl V ⥤ C and refl functors V ⥤rq C.

Equations

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

@[simp]

theorem CategoryTheory.ReflQuiv.adj.homEquiv_apply {V : Type u_1} [ReflQuiver V] {C : Type u_3} [Category.{u_6, u_3} C] (F : Functor (Cat.FreeRefl V) C) : homEquiv F = Cat.toFreeRefl V ⋙rq F.toReflPrefunctor

@[simp]

theorem CategoryTheory.ReflQuiv.adj.homEquiv_symm_apply {V : Type u_1} [ReflQuiver V] {C : Type u_3} [Category.{u_6, u_3} C] (F : V ⥤rq C) : homEquiv.symm F = Cat.FreeRefl.lift F

theorem CategoryTheory.ReflQuiv.adj.homEquiv_naturality_left_symm {V : Type u_1} {W : Type u_2} [ReflQuiver W] [ReflQuiver V] {C : Type u_3} [Category.{u_7, u_3} C] (F : V ⥤rq W) (G : W ⥤rq C) : homEquiv.symm (F ⋙rq G) = (Cat.freeReflMap F).comp (homEquiv.symm G)

theorem CategoryTheory.ReflQuiv.adj.homEquiv_naturality_right {V : Type u_1} [ReflQuiver V] {C : Type u_3} {D : Type u_4} [Category.{u_6, u_3} C] [Category.{u_7, u_4} D] (F : Functor (Cat.FreeRefl V) C) (G : Functor C D) : homEquiv (F.comp G) = homEquiv F ⋙rq G.toReflPrefunctor

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.

Equations

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

@[simp]

theorem CategoryTheory.ReflQuiv.adj_unit_app (V : Type u_1) [ReflQuiver V] : adj.unit.app (of V) = Cat.toFreeRefl V

theorem CategoryTheory.ReflQuiv.adj_counit_app (D : Type u_1) [Category.{max u_1 u_2, u_1} D] : adj.counit.app (Cat.of D) = Cat.FreeRefl.lift (𝟭rq D)

theorem CategoryTheory.ReflQuiv.adj_homEquiv (V : Type u) [ReflQuiver V] (C : Type u) [Category.{max u v, u} C] : adj.homEquiv (of V) (Cat.of C) = adj.homEquiv

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

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