background image

Definition.

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 defined for
binary relations.

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

considered as a pointfree binary relation.

Definition. 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).

Definition.

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 defined 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