nLab dense relation

Redirected from "dense directed loop graph".
Contents

Contents

 Definition

A binary endorelation RR on a set AA is dense if for all xAx \in A and yAy \in A such that R(x,y)R(x, y) there exists an element zAz \in A such that R(x,z)R(x, z) and R(z,y)R(z, y). Equivalently, a binary relation RR on AA is dense if RR is a subset of the composite RRR \circ R in Rel, RRRR \subseteq R \circ R.

In the graph theoretic representation of relations as (directed loop) graphs, a graph is dense if for every pair of vertices a:Va:V and b:Vb:V with an edge aba \to b, there exists a vertex c:Vc:V with edges aca \to c and cbc \to b.

 Examples

 Generalizations

The notion of dense relation in Rel can in theory be generalized to the notion of a dense morphism of an arbitrary 2-poset: Given a 2-poset CC and an object AOb(C)A \in \mathrm{Ob}(C), a morphism RHom(A,A)R \in \mathrm{Hom}(A, A) is dense if RRRR \leq R \circ R.

Dense relation structures

In dependent type theory, the usual definition of a dense relation above use the phrase “there exists…”. This existence in the definitions is mere existence; i.e. using the existential quantifier rather than the dependent sum type.

The untruncated version of the dense relation using dependent sum types can be called dense relation structure, and fields states that

  • for all x:Ax:A and y:Ay:A such that R(x,y)R(x, y), there exists as structure an element z:Az:A such that R(x,z)R(x, z) and R(z,y)R(z, y).
x:A y:AR(x,y) z:AR(x,z)×R(z,y)\prod_{x:A} \prod_{y:A} R(x, y) \to \sum_{z:A} R(x, z) \times R(z, y)

References

See also:

Last revised on January 18, 2024 at 03:17:12. See the history of this page for a list of all contributions to it.