ncatlab.org

reflexive graph (changes) in nLab

  • ️Invalid Date

Showing changes from revision #9 to #10: Added | Removed | Changed

Context

Graph theory

Contents

Idea

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

A Since the word “graph” has many meanings, while category theorists often use it to mean areflexive quiverquiver , has they often use “reflexive graph” to mean what we could more precisely call a “reflexive quiver”: a quiver with a specified identity edgei X:X→Xi_X: X \to X on each object vertex (vertex) X v X v.

More formally, a reflexive quiver consists of a set VV of vertices, a set EE of edges, two maps s:E→Vs: E \to V and t:E→Vt: E \to V, and a map i:V→Ei: V \to E such that

s∘i=t∘i=1 V.s \circ i = t \circ i = 1_V.

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

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 directed quivers graphsRefGphRefGph , i.e., equipped reflexive with the functorquiversU:RefGph→SetU: RefGph \to Set , equipped which with sends the a functor graph to its set of edges, isU:RefGph→SetU: RefGph \to Set which sends a graph to its set of edges, is monadic over SetSet.

Proof

RefGphRefGph is the category of functors R→SetR \to Set where RR is the walking reflexive fork, consisting of two objects 0,10, 1 and generated by arrows i:0→1i: 0 \to 1 and s,t:1→0s, 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 M→SetM \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 “being monadic over’ over” is not transitive.

In dependent type theory

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

  • it comes with a family of elements x:A⊢refl 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))

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](http://www.tac.mta.ca/tac/volumes/41/23/41-23abs.html), arXiv:2310.00493]

Last revised on January 22, 2025 at 15:49:17. See the history of this page for a list of all contributions to it.