 CHAPTER 20

Alternative representations of binary relations

Theorem

1612

.

Let

A

and

B

be fixed sets. The diagram at the figure

1

is a commutative diagram (in category

Set

), every arrow in this diagram is an

isomorphism. Every cycle in this diagram is an identity. All “parallel” arrows are

mutually inverse.

For a Galois connection

f

I denote

f

0

the lower adjoint and

f

1

For simplicity, in the diagram I equate

P

A

and

T

A

.

Proof.

First, note that despite we use the notation Ψ

1

i

, it is not yet proved

that Ψ

1

i

is the inverse of Ψ

i

. We will prove it below.

Now prove a list of claims. First concentrate on the upper “triangle” of the

diagram (the lower one will be considered later).
Claim:

n

(

x,y

)

y

f

0

{

x

}

o

=

n

(

x,y

)

x

f

1

{

y

}

o

when

f

is an antitone Galois connection be-

tween

P

A

and

P

B

.

Proof:

y

f

0

{

x

} ⇔ {

y

} v

f

0

{

x

} ⇔ {

x

} v

f

1

{

y

} ⇔

x

f

1

{

y

}

.

Claim:

(

X

7→

d

x

T

X

\{⊥}

h

f

i

x,Y

7→

d

y

T

Y

\{⊥}

h

f

1

i

y

)

=

(

X

7→

d

x

X

h

f

i{

x

}

,Y

7→

d

y

Y

h

f

1

i

{

y

}

)

when

f

is a pointfree funcoid between

P

A

and

P

B

.

Proof: It is enough to prove

d

x

T

X

\{⊥}

h

f

i

x

=

d

x

X

h

f

i{

x

}

(the rest follows

from symmetry).

d

x

T

X

\{⊥}

h

f

i

x

v

d

x

X

h

f

i{

x

}

because

T

X

\ {⊥} ⊇

n

{

x

}

x

X

o

.

d

x

T

X

\{⊥}

h

f

i

x

w

d

x

X

h

f

i{

x

}

because if

x

T

X

\ {⊥}

then we can take

x

0

x

that is

{

x

0

} ⊆

x

and thus

h

f

i

x

w h

f

i{

x

0

}

, so

d

x

T

X

\{⊥}

h

f

i

x

w

d

x

T

X

\{⊥}

h

f

i{

x

0

} w

d

x

X

h

f

i{

x

}

.

Claim:

P

A,

P

B, X

7→

d

x

T

X

\{⊥}

f

0

x, Y

7→

d

y

T

Y

\{⊥}

f

1

y

=

P

A,

P

B, X

7→

d

x

X

f

0

{

x

}

, Y

7→

d

y

Y

f

1

{

y

}

when

f

is an antitone Galois

connection between

P

A

and

P

B

.

Proof: It is enough to prove

d

x

T

X

\{⊥}

f

0

x

=

d

x

X

f

0

{

x

}

(the rest follows from

symmetry). We have

d

x

T

X

\{⊥}

f

0

x

w

d

x

X

f

0

{

x

}

because

{

x

} ∈

T

X

\{⊥}

. Let

x

T

X

\ {⊥}

. Take

x

0

X

. We have

f

0

x

v

f

0

{

x

0

}

and thus

f

0

x

v

d

x

X

f

0

{

x

}

.

So

d

x

T

X

\{⊥}

f

0

x

v

d

x

X

f

0

{

x

}

.

Claim: Ψ

1

3

= Ψ

2

Ψ

1

.

Proof: Ψ

2

Ψ

1

f

=

P

A,

P

B, X

7→

n

y

x

X

:(

x,y

)

Ψ

1

f

o

, Y

7→

n

x

y

Y

:(

x,y

)

Ψ

1

f

o

=

P

A,

P

B, X

7→

n

y

x

X

:

y

f

0

{

x

}

o

, Y

7→

n

x

y

Y

:

x

f

1

{

y

}

o

=

P

A,

P

B, X

7→

d

x

X

f

0

{

x

}

, Y

7→

d

y

Y

f

1

{

y

}

= Ψ

1

3

f

.

Claim: Ψ

3

= Ψ

1

1

Ψ

1

2

.

Proof: Ψ

1

1

Ψ

1

2

f

=

X

7→

n

y

B

x

X

:

{

x

}

[

f

]

{

y

}

o

, Y

7→

n

x

A

y

Y

:

{

x

}

[

f

]

{

y

}

o

=

X

7→

n

y

B

x

X

:

y

∈h

f

i{

x

}

o

, Y

7→

n

x

A

y

Y

:

x

∈h

f

1

i{

y

}

o

=

X

7→

d

x

X

h

f

i{

x

}

, Y

7→

d

y

Y

f

1

{

y

}

= Ψ

3

f

.

312