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)
Notation for the identity morphism in a category.
Equations
- CategoryTheory.«term𝟙rq» = Lean.ParserDescr.node `CategoryTheory.«term𝟙rq» 1024 (Lean.ParserDescr.symbol "𝟙rq")
Instances For
Equations
- CategoryTheory.catToReflQuiver = CategoryTheory.ReflQuiver.mk CategoryTheory.CategoryStruct.id
A morphism of reflexive quivers called a ReflPrefunctor
.
- obj : V → W
- map_id (X : V) : self.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (self.obj X)
A functor preserves identity morphisms.
Instances For
Proving equality between reflexive prefunctors. This isn't an extensionality lemma, because usually you don't really want to do this.
This may be a more useful form of ReflPrefunctor.ext
.
The identity morphism between reflexive quivers.
Instances For
Equations
- CategoryTheory.ReflPrefunctor.instInhabited V = { default := 𝟭rq V }
Composition of morphisms between reflexive quivers.
Instances For
Notation for a prefunctor between reflexive quivers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Notation for composition of reflexive prefunctors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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")
Instances For
A functor has an underlying refl prefunctor.
Equations
- F.toReflPrefunctor = { toPrefunctor := F.toPrefunctor, map_id := ⋯ }
Instances For
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))
Equations
- CategoryTheory.ReflQuiver.discreteReflQuiver V = CategoryTheory.ReflQuiver.mk CategoryTheory.CategoryStruct.id