nLab reflexive graph




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

A reflexive quiver has a specified identity edge i X:XXi_X: X \to X on each object (vertex) XX. 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.



The category of reflexive directed graphs RefGphRefGph, i.e., reflexive quivers, equipped with the functor U:RefGphSetU: RefGph \to Set which sends a graph to its set of edges, is monadic over SetSet.


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

CatCat is monadic over RefGphRefGph and RefGphRefGph is monadic over SetSet but CatCat is not monadic over SetSet; 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:AR(x,y))(A; x:A, y:A \vdash R(x, y)) is reflexive if

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

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

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

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

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

Last revised on January 11, 2023 at 21:36:54. See the history of this page for a list of all contributions to it.