nLab connected relation

Connected relations

Connected relations


A (binary) relation \sim on a set AA is connected if any two elements that are related in neither order are equal:

(x,y:A),xyyxx=y. \forall (x, y: A),\; x \nsim y \;\wedge\; y \nsim x \;\Rightarrow\; x = y .

This is a basic property of strict total orders.

Every tight relation is a connected relation. Every connected symmetric relation is a tight relation.

Constructive aspects

Using excluded middle, it is equivalent to say that every two elements are related in some order or equal:

(x,y:A),xyyxx=y. \forall (x, y: A),\; x \sim y \;\vee\; y \sim x \;\vee\; x = y .

However, this version is too strong for the intended applications to constructive mathematics. (In particular, <\lt on the located Dedekind real numbers satisfies the first definition but not this one.)

On the other hand, there is a stronger notion that may be used in constructive mathematics, if AA is already equipped with a tight apartness #\#. In that case, we say that \sim is strongly connected if any two distinct elements are related in one order or the other:

(x,y:A),x#yxyyx. \forall (x, y: A),\; x \# y \;\Rightarrow\; x \sim y \;\vee\; y \sim x .

Since #\# is connected itself, every strongly connected relation is connected; the converse holds with excluded middle (through which every set has a unique tight apartness).

We can do a similar thing if AA is equipped with any inequality #\#, except that in the general case, this is not necessarily stronger than being connected, and so we should call it #\#-connected.

In dependent type theory

In dependent type theory, an irreflexive relation \sim with terms a:Airr(a):(aa)a:A \vdash \mathrm{irr}(a):(a \sim a) \to \emptyset is connected if the canonical function

idtosymnotrel(a,b):(a= Ab)(((ab))×((ba)))\mathrm{idtosymnotrel}(a, b):(a =_A b) \to (((a \sim b) \to \emptyset) \times ((b \sim a) \to \emptyset))

inductively defined by

β(a):idtosymnotrel(a,a)(refl A(a))= ((aa))×((aa))(irr(a),irr(a))\beta(a):\mathrm{idtosymnotrel}(a, a)(\mathrm{refl}_A(a)) =_{((a \sim a) \to \emptyset) \times ((a \sim a) \to \emptyset)} (\mathrm{irr}(a), \mathrm{irr}(a))

is an equivalence of types

conn(a,b):isEquiv(idtosymnotrel(a,b))\mathrm{conn}(a, b):\mathrm{isEquiv}(\mathrm{idtosymnotrel}(a, b))

 See also

Last revised on December 26, 2023 at 04:34:51. See the history of this page for a list of all contributions to it.