 20. ALTERNATIVE REPRESENTATIONS OF BINARY RELATIONS

316

That Φ

1

2

preserves composition and identities follows from the fact that it is

an isomorphism.

That is preserves reversal follows from the formula

f

1

=

p

1

.

Proposition

1617

.

The bijections Ψ

2

and Ψ

1

2

from the diagram at figure

11

preserves monovaluedness and injectivity.

Proof.

Because it is a functor which preserves reversal.

Proposition

1618

.

The bijections Ψ

2

and Ψ

1

2

from the diagram at figure

11

preserves domain an image.

Proof.

im

f

=

h

f

i>

=

h

p

i

>

= im

p

, likewise for domain.

Proposition

1619

.

The bijections Ψ

2

and Ψ

1

2

from the diagram at figure

11

maps cartesian products to corresponding funcoidal products.

Proof.

A

×

FCD

B

X

=

(

B

if

X

6

A

if

X

A

=

h

A

×

B

i

X

.

Likewise

(

A

×

FCD

B

)

1

Y

=

(

A

×

B

)

1

Y

.

Let Φ map a pointfree funcoid whose first component is

c

into the Galois con-

nection whose lower adjoint is

c

. Then Φ is an isomorphism (theorem

1607

and

Φ

1

maps a Galois connection whose lower adjoint is

c

into the pointfree funcoid

whose first component is

c

.

Informally speaking, Φ replaces a relation

r

with its complement relations

¬

r

.

Formally:

Proposition

1620

.

1

. For every path

P

in the diagram at figure

11

from binary relations between

A

and

B

to pointfree funcoids between

P

A

and

P

B

and every path

Q

in

the diagram at figure

11

from Galois connections between

P

A

and

P

B

to binary relations between

A

and

B

, we have

Q

Φ

P r

=

¬

r

.

2

. For every path

Q

in the diagram at figure

11

from binary relations between

A

and

B

to pointfree funcoids between

P

A

and

P

B

and every path

P

in

the diagram at figure

11

from Galois connections between

P

A

and

P

B

to binary relations between

A

and

B

, we have

P

Φ

1

Qr

=

¬

r

.

Proof.

We will prove only the second (

P

Φ

1

Q

=

¬

), because the first

(

Q

Φ

P

=

¬

) can be obtained from it by inverting the morphisms (and variable

replacement).

Because the diagram is commutative, it is enough to prove it for some fixed

P

and

Q

. For example, we will prove Ψ

1

2

Φ

1

Ψ

4

Ψ

2

r

=

¬

r

.

Ψ

4

Ψ

2

r

=

X

7→ ¬

d

x

X

h

r

i

{

x

}

, Y

7→

d

y

Y

h

r

i

¬{

y

}

.

Φ

1

Ψ

4

Ψ

2

r

is pointfree funcoid

f

with

h

f

i

=

X

7→ ¬

d

x

X

h

r

i

{

x

}

.

Ψ

1

2

Φ

1

Ψ

4

Ψ

2

r

is the relation consisting of (

x, y

) such that

{

x

}

[

f

]

{

y

}

what is

equivalent to:

{

y

} 6 h

f

i{

x

}

;

{

y

} 6 ¬h

r

i

{

x

}

;

{

y

} 6v h

r

i

{

x

}

;

y /

∈ h

r

i

{

x

}

.

So Ψ

1

2

Φ

1

Ψ

4

Ψ

2

r

=

¬

r

.

Proposition

1621

.

Φ and Φ

1

preserve composition.

Proof.

By definitions of compositions and the fact that both pointfree fun-

coids and Galois connections are determined by the first component.