 19.17. BINARY RELATIONS ARE POINTFREE FUNCOIDS

310

Conjecture

1608

.

Let

A

,

B

be boolean lattices.

A function

α

B

A

is equal to the component

h

f

i

of a pointfree funcoid

f

pFCD

(

A

,

B

) iff

α

is a lower adjoint.

It is tempting to conclude that

h

f

i

is a lower adjoint to

f

1

. But that’s false:

We should disprove that

h

f

i

X

v

Y

X

v

f

1

Y

.

For a counter-example, take

f

=

{

0

} ×

N

. Then our condition takes form

Y

=

N

X

v {

0

}

for

X

3

0,

Y

3

0 what obviously does not hold.

19.17. Binary relations are pointfree funcoids

Below for simplicity we will equate

T

A

with

P

A

.

Theorem

1609

.

Pointfree funcoids

f

between powerset posets

T

A

and

T

B

bijectively (moreover this bijection is an order-isomorphism) correspond to mor-

phisms

p

Rel

(

A, B

) by the formulas:

h

f

i

=

h

p

i

,

f

1

=

p

1

;

(30)

(

x, y

)

GR

p

y

∈ h

f

i{

x

} ⇔

x

f

1

{

y

}

.

(31)

Proof.

Suppose

p

Rel

(

A, B

) and prove that there is a pointfree funcoid

f

conforming to (

30

). Really, for every

X

T

A

,

Y

T

B

Y

6 h

f

i

X

Y

6 h

p

i

X

Y

6 h

p

i

X

X

6

p

1

Y

X

6

p

1

Y

X

6

f

1

Y.

Now suppose

f

pFCD

(

T

A,

T

B

) and prove that the relation defined by the

formula (

31

exists. To prove it, it’s enough to show that

y

∈ h

f

i{

x

} ⇔

x

f

1

{

y

}

. Really,

y

∈ h

f

i{

x

} ⇔ {

y

} 6 h

f

i{

x

} ⇔ {

x

} 6

f

1

{

y

} ⇔

x

f

1

{

y

}

.

It remains to prove that functions defined by (

30

and (

31

are mutually inverse.

(That these functions are monotone is obvious.)

Let

p

0

Rel

(

A, B

) and

f

pFCD

(

T

A,

T

B

) corresponds to

p

0

by the for-

mula (

30

); let

p

1

Rel

(

A, B

) corresponds to

f

by the formula (

31

). Then

p

0

=

p

1

because

(

x, y

)

GR

p

0

y

∈ h

p

0

i

{

x

} ⇔

y

∈ h

f

i{

x

} ⇔

(

x, y

)

GR

p

1

.

Let now

f

0

pFCD

(

T

A,

T

B

) and

p

Rel

(

A, B

) corresponds to

f

0

by the

formula (

31

); let

f

1

pFCD

(

T

A,

T

B

) corresponds to

p

by the formula (

30

). Then

(

x, y

)

GR

p

y

∈ h

f

0

i{

x

}

and

h

f

1

i

=

h

p

i

; thus

y

∈ h

f

1

i{

x

} ⇔

y

∈ h

p

i

{

x

} ⇔

(

x, y

)

GR

p

y

∈ h

f

0

i{

x

}

.

So

h

f

0

i

=

h

f

1

i

. Similarly

f

1

0

=

f

1

1

.

Proposition

1610

.

The bijection defined by the theorem

1609

preserves com-

position and identities, that is is a functor between categories

Rel

and (

A, B

)

7→

pFCD

(

T

A,

T

B

).

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 it 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 it preserves identities.

Proposition

1611

.

The bijection defined by theorem

1609

preserves reversal.

Proof.

f

1

=

p

1

.