nLab reflexive graph

Idea

A graph is reflexive if for each vertex $v$ there is a (specified) edge $v \to v$.

Since the word “graph” has many meanings, while category theorists often use it to mean a quiver, they often use “reflexive graph” to mean what we could more precisely call a “reflexive quiver”: a quiver with a specified edge $i_X: X \to X$ on each vertex $v$.

More formally, a reflexive quiver consists of a set $V$ of vertices, a set $E$ of edges, two maps $s: E \to V$ and $t: E \to V$, and a map $i: V \to E$ such that

$$s \circ i = t \circ i = 1_V.$$

The category $RefGph$ of reflexive quivers is a presheaf topos. So is the category of quivers, $Gph$. One advantage of $RefGph$ is that the set of vertices of a reflexive quiver $G$ is representable: it is naturally isomorphic to $\text{hom}(1,G)$. In $Gph$, there may be many or no morphisms from the terminal object $1$ to a quiver $G$ sending the only vertex of $1$ to a given vertex of $G$.

The free category on a reflexive quiver has the same objects, identity morphisms corresponding to the identity edges, and non-identity morphisms consisting of paths of non-identity edges.

Properties

Proposition

The category of reflexive quivers $RefGph$, equipped with the functor $U: RefGph \to Set$ which sends a graph to its set of edges, is monadic over $Set$.

Proof

$RefGph$ is the category of functors $R \to Set$ where $R$ is the walking reflexive fork, consisting of two objects $0, 1$ and generated by arrows $i: 0 \to 1$ and $s, t: 1 \to 0$ subject to $s i = 1_0 = t i$ and no other relations. This $R$ is in turn the Cauchy completion of a monoid $M$ consisting of two elements $e_0 = i s, e_1 = i t$ and an identity, with multiplication $e_0 e_0 = e_0 = e_1 e_0$ and $e_1 e_1 = e_1 = e_0 e_1$, and therefore $RefGph$ is equivalent to the category of functors $M \to Set$, i.e., the category of $M$-sets $Set^M$. This is the category of algebras of the monad $M \times -$ whose monad structure is induced from the monoid structure of $M$.

$Cat$ is monadic over $RefGph$ and $RefGph$ is monadic over $Set$ but $Cat$ is not monadic over $Set$; this is a nice example of how the relation “being monadic over” is not transitive.

In dependent type theory

In dependent type theory, a graph $(A; x:A, y:A \vdash R(x, y))$ is reflexive if

• it comes with a family of elements $x:A \vdash \mathrm{refl}_A^R(x):R(x, x)$.
• it comes with a family of functions $\mathrm{idtofam}(x, y):(x =_A y) \to R(x, y)$.

These two definitions are the same. From $\mathrm{refl}_A^R(x)$, we can inductively define $\mathrm{idtofam}(x, y)$ on reflexivity:

$$\mathrm{idtofam}(x, x)(\mathrm{refl}_A(x)) \coloneqq \mathrm{refl}_A^R(x)$$

From $\mathrm{idtofam}(x, y)$ we define $\mathrm{refl}_A^R(x)$ to be

$$\mathrm{refl}_A^R(x) \coloneqq \mathrm{idtofam}(x, x)(\mathrm{refl}_A(x))$$

Related concepts

• reflexive relation

• univalent reflexive graph

References

Classifying the closed symmetric monoidal-structures on the category of reflexive graphs:

• Krzysztof Kapulkin, Nathan Kershaw: Closed symmetric monoidal structures on the category of graphs, Theory and Applications of Categories 41 23 (2024) 760-784 [tac:41-23, arXiv:2310.00493]