 20. ALTERNATIVE REPRESENTATIONS OF BINARY RELATIONS

315

Claim:

X

7→

d

x

T

X

\{⊥}

¬

f

0

x, Y

7→

d

y

T

Y

\{⊥}

f

1

¬

y

=

X

7→

d

x

X

¬

f

0

{

x

}

, Y

7→

d

y

Y

f

1

¬{

y

}

.

Proof: It is enough to prove

d

x

T

X

\{⊥}

¬

f

0

x

=

d

x

X

¬

f

0

{

x

}

for a Galois connec-

tion

f

(the rest follows from symmetry).

d

x

T

X

\{⊥}

¬

f

0

x

w

d

x

X

¬

f

0

{

x

}

because

{

x

} ∈

T

X

\ {⊥}

. If

x

T

X

\ {⊥}

then there exists

x

0

∈ {

x

}

and thus

¬

f

0

{

x

0

} w ¬

f

0

x

. Thus

¬

f

0

x

v

d

x

X

¬

f

0

{

x

}

and so

d

x

T

X

\{⊥}

¬

f

0

x

v

d

x

X

¬

f

0

{

x

}

.

Claim: Ψ

5

is self-inverse.

Proof: Obvious.

Claim: Ψ

4

= Ψ

5

Ψ

3

.

Proof: Easily follows from symmetry.

Claim: Ψ

1

4

= Ψ

1

3

Ψ

1

5

.

Proof: Easily follows from symmetry.

Claim: Ψ

4

and Ψ

1

4

are mutually inverse.

Proof: From two above claims and the fact that Ψ

1

3

is the inverse of Ψ

3

and Ψ

1

5

is the inverse of Ψ

5

proved above.

Note that now we have proved that Ψ

i

and Ψ

1

i

are mutually inverse for all

i

= 1

,

2

,

3

,

4

,

5.

Claim: For every path of the diagram on figure

2

started with the circled node, the

corresponding morphism is with which the node is labeled.

Figure 2.

1

Ψ

2

Ψ

1

1

Ψ

5

Ψ

1

1

Ψ

1

1

Ψ

2

Ψ

1

2

Ψ

3

Ψ

4

Ψ

1

Ψ

1

3

Ψ

5

1

5

Ψ

1

4

Proof: Take into account that Ψ

1

3

= Ψ

2

Ψ

1

, Ψ

4

= Ψ

5

Ψ

3

and thus also Ψ

4

Ψ

2

=

Ψ

5

Ψ

1

1

. Now prove it by induction on path length.

Claim: Every cycle in the diagram at figure

1

is identity.

Proof: For cycles starting at the top node it follows from the previous claim. For

arbitrary cycles it follows from theorem

192

.

Claim: The diagram at figure

1

is commutative.

Proof: From the previous claim.

Proposition

1613

.

We equate the set of binary relations between

A

and

B

with

Rld

(

A, B

). Ψ

2

and Ψ

1

2

from the diagram at figure

1

preserve composition and

identities (that are functors between categories

Rel

and (

A, B

)

7→

pFCD

(

T

A,

T

B

))

and also reversal (

f

7→

f

1

).

Proof.

Let

h

f

i

=

h

p

i

and

h

g

i

=

h

q

i

. Then

h

g

f

i

=

h

g

i ◦ h

f

i

=

h

q

i

◦ h

p

i

=

h

q

p

i

. Likewise

(

g

f

)

1

=

(

q

p

)

1

. So Φ

2

preserves composition.

Let

p

= 1

A

Rel

for some set

A

. Then

h

f

i

=

h

p

i

=

1

A

Rel

= id

P

A

and likewise

f

1

= id

P

A

, that is

f

is an identity pointfree funcoid. So Φ

2

preserves identities.