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
A functor preserves identity morphisms.
Proving equality between reflexive prefunctors. This isn't an extensionality lemma, because usually you don't really want to do this.
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