**Algebraic General Topology. Vol 1**:
Paperback
/
E-book
||
**Axiomatic Theory of Formulas**:
Paperback
/
E-book

Pointfree binary relations

Victor Porton

November 24, 2015

Abstract

I deﬁne pointfree binary relations, a way to describe binary rela-

tions and more general structures without referring to particular “points”

(elements).

In this short article I deﬁne pointfree binary relations, that is a way

to describe binary relations and more general structures without referring to

particular “points” (elements).

Deﬁnition. Remind that binary relations (also called morphisms of the cat-

egory Rel) are triples (A, B, f) where A, B are sets and f ∈ P(A × B).

Deﬁnition. Endo-relations are relations of the form (A, A, f ) for some set A

and f ∈ P(A × A).

Deﬁnition. Isomorphism between relations µ ∈ P(A

0

×A

0

) and ν ∈ P(A

1

×

A

1

) is a bijection f : A

1

→ A

0

such that ν = f

−1

◦ µ ◦ f.

I remind that precategory is deﬁned as category without requirement of

existence of identity morphisms.

Deﬁnition. Ordered precategory is a precategory, each Hom-set of which

is a poset, subject to the inequalities

f

0

≤ f

1

∧ g

0

≤ g

1

⇒ g

0

◦ f

0

≤ g

1

◦ f

1

.

Deﬁnition. Isomorphism of ordered precategories is a map which is both

precategory isomorphism and order isomorphism.

Deﬁnition. System of pointfree relations is:

• an ordered precategory (I call morphisms of which pointfree (binary)

relations; the composition is denoted ◦);

• for each Hom-sets two posets: possible domains and possible images;

• domain dom and image im (maps from pointfree relations to possible

domains and possible images of its Hom-set), subject to the inequalities

f ≤ g ⇒ dom f ≤ dom g ∧ im f ≤ im g.

1

Deﬁnition. System of pointfree relations induced by binary relations is the

system of pointfree relations whose precategory is the category Rel of binary

relations, possible domains and images for Rel(A, B) are P A and P B corre-

spondingly and domain and image are domain and image as usually deﬁned for

binary relations.

The pointfree relation induced by a binary relation is this binary relation

considered as a pointfree binary relation.

Deﬁnition. Pointfree endo-relations are endo-relations whose source and

destination (in our precategory) is the same.

Obvious 1. System of pointfree relations induced by binary relations is really

a system of pointfree relations.

Remark. The category of pointfree relations induced by binary relations is a

large category (its set of objects is a proper class).

Deﬁnition. The isomorphism between pointfree endo-relations µ and ν of

a system of pointfree relations is an isomorphism f of the precategory of this

system such that ν = f

−1

◦ µ ◦ f.

Obvious 2. The precategory for the system of pointfree relations induced by

binary relations is a category.

Let describe reversal f 7→ f

−1

of a binary relation f in pointfree terms:

f is a join (i.e., supremum) of atomic binary relation. Reversal of an atomic

relation t is deﬁned as the unique relation t

−1

conforming to the formulas

dom t

−1

= im t, im t

−1

= dom t. So f

−1

is the supremum of such t

−1

. Trivially

combining these steps we get reversal of a binary relation described in pointfree

terms.

Thus we have proved:

Proposition 1. Reversal of binary relations can be restored, knowing only in-

duced pointfree relations (up to isomorphism of systems of pointfree relations).

Proposition 2. Identity relation for binary relations can be restored, know-

ing only induced pointfree relations (up to isomorphism of systems of pointfree

relations).

Proof. Identity relation id is the identity element of our semigroup (and thus

does not depend on the isomorphism).

Proposition 3. The set of bijections for relations Rel(A, B) can be restored,

knowing only induced pointfree relations (up to isomorphism of systems of point-

free relations).

Proof. Bijections f : A → B are characterized by the formulas f ◦ f

−1

= id

B

and f

−1

◦ f = id

A

.

2

The following theorem states that pointfree endo-relations induced by bi-

nary endo-relations are essentially the same as these binary endo-relations them-

selves. Thus pointfree binary endo-relations are a generalization of binary endo-

relations.

Theorem 1. Having speciﬁed up to isomorphism (of systems of pointfree re-

lations) the system of pointfree relations induced by binary relations, we can

restore the endo-relation to which corresponds a given pointfree endo-relation

up to isomorphism (of binary relations).

Proof. Fix a set A.

Let µ ∈ Rel(A, A) be a binary relation (which we are going to restore up to

isomorphism from the corresponding pointfree relation).

We will consider possible domains and possible images D = PA.

Let A

0

be the set of atoms of D, that is one-element sets.

Take (using axiom of choice) an arbitrary bijection f : A

0

→ A. (Note that

it can be done using only the system of pointfree relations induced by the binary

relations up to isomorphism.)

Let y

0

, y

1

∈ A

0

be atoms. Take elements p, q ∈ Rel(A

0

, A

0

) such that im p =

y

0

, dom q = y

1

(they exist because our system of pointfree relations is induced

by binary relations).

Deﬁne binary relation µ

0

∈ Rel(A

0

, A

0

) as: y

0

µ

0

y

1

iﬀ q ◦ f

−1

◦ µ ◦ f ◦ p 6= ⊥

(for all y

0

, y

1

∈ A

0

).

Thus we have restored relation µ

0

from the corresponding pointfree relation.

µ

0

was deﬁned using only properties of orders and the precategory. Thus it is

invariant under isomorphism (of systems of pointfree relations).

Let’s prove that µ

0

= f

−1

◦ µ ◦ f (and thus µ

0

is isomorphic to µ). Really,

y

0

µ

0

y

1

⇔ q ◦ f

−1

◦ µ ◦ f ◦ p 6= ⊥ ⇔

∃x ∈ im p, y ∈ dom q : (x, y) ∈ f

−1

◦ µ ◦ f ⇔

(im p × dom q) ∩ f

−1

◦ µ ◦ f 6= ∅ ⇔ y

0

(f

−1

◦ µ ◦ f ) y

1

.

If we take another isomorphism f

2

instead of f, then the induced binary

relation

µ

0

2

= f

−1

2

◦ µ ◦ f

2

= f

−1

2

◦ f ◦ µ

0

◦ f

−1

◦ f

2

= (f

−1

2

◦ f) ◦ µ

0

◦ (f

−1

2

◦ f)

−1

.

Thus µ

0

2

is isomorphic to µ

0

(and therefore isomorphic to µ), because the com-

position f

−1

2

◦ f is a bijection. We have determined µ

0

up to isomorphism of

binary relations.

If µ

2

is a binary relation isomorphic to µ

0

, then µ

2

is isomorphic to µ and

thus µ

2

= f

−1

◦ µ ◦ f for some bijection f , so obviously µ

2

induces the same

(up to isomorphism) pointfree binary relation as µ. So we have determined

the sought-for class of pairwise isomorphic binary relations which induce (up

to isomorphism) the same pointfree binary relation as induced by µ as these

binary endo-relations which are isomorphic to µ

0

.

3

Now to the topic of both rationale and applications of this idea: I seriously

research ([1]) what I call reloids, that is ﬁlters on binary cartesian products of

sets. This seems promising to generalize for ﬁlters on pointfree relations instead

of that special case of ﬁlters on binary relations. This research is both the source

of the idea and an application of systems of pointfree relations.

Remark. Funcoids and reloids (see [1]) also are systems of pointfree relations.

References

[1] Victor Porton. Algebraic General Topology. Volume 1. 2015.

4