Reflexive Quivers

This module defines reflexive quivers. A reflexive quiver, or "refl quiver" for short, extends a quiver with a specified endoarrow on each term in its type of objects.

We also introduce morphisms between reflexive quivers, called reflexive prefunctors or "refl prefunctors" for short.

Note: Currently Category does not extend ReflQuiver, although it could. (TODO: do this)

class CategoryTheory.ReflQuiver (obj : Type u) extends Quiver obj : Type (max u v)

A reflexive quiver extends a quiver with a specified arrow id X : X ⟶ X for each X in its type of objects. We denote these arrows by id since categories can be understood as an extension of refl quivers.

• Hom : obj → obj → Sort v
• id (X : obj) : X ⟶ X

  The identity morphism on an object.

def CategoryTheory.«term𝟙rq» : Lean.ParserDescr

Notation for the identity morphism in a category.

Equations

• CategoryTheory.«term𝟙rq» = Lean.ParserDescr.node `CategoryTheory.«term𝟙rq» 1024 (Lean.ParserDescr.symbol "𝟙rq")

@[simp]

theorem CategoryTheory.ReflQuiver.homOfEq_id {V : Type u_1} [CategoryTheory.ReflQuiver V] {X X' : V} (hX : X = X') : Quiver.homOfEq (CategoryTheory.ReflQuiver.id X) hX hX = CategoryTheory.ReflQuiver.id X'

instance CategoryTheory.catToReflQuiver {C : Type u} [inst : CategoryTheory.Category.{v, u} C] : CategoryTheory.ReflQuiver C

Equations

• CategoryTheory.catToReflQuiver = CategoryTheory.ReflQuiver.mk CategoryTheory.CategoryStruct.id

@[simp]

theorem CategoryTheory.ReflQuiver.id_eq_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) : CategoryTheory.ReflQuiver.id X = CategoryTheory.CategoryStruct.id X

structure CategoryTheory.ReflPrefunctor (V : Type u₁) [CategoryTheory.ReflQuiver V] (W : Type u₂) [CategoryTheory.ReflQuiver W] extends V ⥤q W : Sort (max (max (max (u₁ + 1) (u₂ + 1)) v₁) v₂)

A morphism of reflexive quivers called a ReflPrefunctor.

• obj : V → W
• map {X Y : V} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• map_id (X : V) : self.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (self.obj X)

  A functor preserves identity morphisms.

theorem CategoryTheory.ReflPrefunctor.mk_obj {V : Type u_1} {W : Type u_2} [CategoryTheory.ReflQuiver V] [CategoryTheory.ReflQuiver W] {obj : V → W} {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X : V} : { obj := obj, map := map }.obj X = obj X

theorem CategoryTheory.ReflPrefunctor.mk_map {V : Type u_1} {W : Type u_2} [CategoryTheory.ReflQuiver V] [CategoryTheory.ReflQuiver W] {obj : V → W} {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X Y : V} {f : X ⟶ Y} : { obj := obj, map := map }.map f = map f

theorem CategoryTheory.ReflPrefunctor.ext {V : Type u} [CategoryTheory.ReflQuiver V] {W : Type u₂} [CategoryTheory.ReflQuiver W] {F G : V ⥤rq W} (h_obj : ∀ (X : V), F.obj X = G.obj X) (h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))) : F = G

Proving equality between reflexive prefunctors. This isn't an extensionality lemma, because usually you don't really want to do this.

theorem CategoryTheory.ReflPrefunctor.ext' {V W : Type u} [CategoryTheory.ReflQuiver V] [CategoryTheory.ReflQuiver W] {F G : V ⥤rq W} (h_obj : ∀ (X : V), F.obj X = G.obj X) (h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯) : F = G

This may be a more useful form of ReflPrefunctor.ext.

def CategoryTheory.ReflPrefunctor.id (V : Type u_1) [CategoryTheory.ReflQuiver V] : V ⥤rq V

The identity morphism between reflexive quivers.

Equations

• 𝟭rq V = { toPrefunctor := 𝟭q V, map_id := ⋯ }

@[simp]

theorem CategoryTheory.ReflPrefunctor.id_obj (V : Type u_1) [CategoryTheory.ReflQuiver V] (X : V) : (𝟭rq V).obj X = X

@[simp]

theorem CategoryTheory.ReflPrefunctor.id_map (V : Type u_1) [CategoryTheory.ReflQuiver V] {X✝ Y✝ : V} (f : X✝ ⟶ Y✝) : (𝟭rq V).map f = f

instance CategoryTheory.ReflPrefunctor.instInhabited (V : Type u_1) [CategoryTheory.ReflQuiver V] : Inhabited (V ⥤rq V)

Equations

• CategoryTheory.ReflPrefunctor.instInhabited V = { default := 𝟭rq V }

def CategoryTheory.ReflPrefunctor.comp {U : Type u_1} [CategoryTheory.ReflQuiver U] {V : Type u_2} [CategoryTheory.ReflQuiver V] {W : Type u_3} [CategoryTheory.ReflQuiver W] (F : U ⥤rq V) (G : V ⥤rq W) : U ⥤rq W

Composition of morphisms between reflexive quivers.

Equations

• F ⋙rq G = { toPrefunctor := F.toPrefunctor ⋙q G.toPrefunctor, map_id := ⋯ }

@[simp]

theorem CategoryTheory.ReflPrefunctor.comp_obj {U : Type u_1} [CategoryTheory.ReflQuiver U] {V : Type u_2} [CategoryTheory.ReflQuiver V] {W : Type u_3} [CategoryTheory.ReflQuiver W] (F : U ⥤rq V) (G : V ⥤rq W) (X : U) : (F ⋙rq G).obj X = G.obj (F.obj X)

@[simp]

theorem CategoryTheory.ReflPrefunctor.comp_map {U : Type u_1} [CategoryTheory.ReflQuiver U] {V : Type u_2} [CategoryTheory.ReflQuiver V] {W : Type u_3} [CategoryTheory.ReflQuiver W] (F : U ⥤rq V) (G : V ⥤rq W) {X✝ Y✝ : U} (f : X✝ ⟶ Y✝) : (F ⋙rq G).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.ReflPrefunctor.comp_id {U : Type u_1} {V : Type u_2} [CategoryTheory.ReflQuiver U] [CategoryTheory.ReflQuiver V] (F : U ⥤rq V) : F ⋙rq 𝟭rq V = F

@[simp]

theorem CategoryTheory.ReflPrefunctor.id_comp {U : Type u_1} {V : Type u_2} [CategoryTheory.ReflQuiver U] [CategoryTheory.ReflQuiver V] (F : U ⥤rq V) : 𝟭rq U ⋙rq F = F

@[simp]

theorem CategoryTheory.ReflPrefunctor.comp_assoc {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [CategoryTheory.ReflQuiver U] [CategoryTheory.ReflQuiver V] [CategoryTheory.ReflQuiver W] [CategoryTheory.ReflQuiver Z] (F : U ⥤rq V) (G : V ⥤rq W) (H : W ⥤rq Z) : F ⋙rq G ⋙rq H = F ⋙rq (G ⋙rq H)

def CategoryTheory.ReflPrefunctor.«term_⥤rq_» : Lean.TrailingParserDescr

Notation for a prefunctor between reflexive quivers.

Equations

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

def CategoryTheory.ReflPrefunctor.«term_⋙rq_» : Lean.TrailingParserDescr

Notation for composition of reflexive prefunctors.

Equations

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

def CategoryTheory.ReflPrefunctor.«term𝟭rq» : Lean.ParserDescr

Notation for the identity prefunctor on a reflexive quiver.

Equations

• CategoryTheory.ReflPrefunctor.«term𝟭rq» = Lean.ParserDescr.node `CategoryTheory.ReflPrefunctor.«term𝟭rq» 1024 (Lean.ParserDescr.symbol "𝟭rq")

theorem CategoryTheory.ReflPrefunctor.congr_map {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y} (h : f = g) : F.map f = F.map g

def CategoryTheory.Functor.toReflPrefunctor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) : C ⥤rq D

A functor has an underlying refl prefunctor.

Equations

• F.toReflPrefunctor = { toPrefunctor := F.toPrefunctor, map_id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.toReflPrefunctor_toPrefunctor {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑C ↑D) : F.toReflPrefunctor.toPrefunctor = F.toPrefunctor

instance CategoryTheory.ReflQuiver.opposite {V : Type u_1} [CategoryTheory.ReflQuiver V] : CategoryTheory.ReflQuiver Vᵒᵖ

Vᵒᵖ reverses the direction of all arrows of V.

Equations

• CategoryTheory.ReflQuiver.opposite = CategoryTheory.ReflQuiver.mk fun (X : Vᵒᵖ) => Opposite.op (CategoryTheory.ReflQuiver.id (Opposite.unop X))

instance CategoryTheory.ReflQuiver.discreteReflQuiver (V : Type u) : CategoryTheory.ReflQuiver (CategoryTheory.Discrete V)

Equations

• CategoryTheory.ReflQuiver.discreteReflQuiver V = CategoryTheory.ReflQuiver.mk CategoryTheory.CategoryStruct.id