background image

CHAPTER 15

Relationships are pointfree funcoids

Theorem

2422

.

((

FCD

)

,

(

RLD

)

in

) are components of a complete pointfree fun-

coid.

Proof.

For every ultrafilters

x

and

y

we have

x

[(

FCD

)(

f

u

(

RLD

)

in

g

)]

y

x

×

RLD

y

6

f

u

(

RLD

)

in

g

x

×

RLD

y

v

(

RLD

)

in

g

x

×

RLD

y

6

f

u

(

RLD

)

in

g

x

×

FCD

y

atoms

g

:

x

×

RLD

y

6

f

u

(

RLD

)

in

g

x

×

FCD

y

atoms

g

:

x

×

RLD

y

6

f

x

×

FCD

y

atoms

g

x

×

FCD

y

v

(

FCD

)

f

x

[

g

u

(

FCD

)

f

]

y

.

Thus (

FCD

)(

f

u

(

RLD

)

in

g

) =

g

u

(

FCD

)

f

. Consequently

f

u

(

RLD

)

in

g

=

⊥ ⇔

g

u

(

FCD

)

f

=

that is

g

6

(

FCD

)

f

f

6

(

RLD

)

in

g

.

It is complete by theorem 1198.

We will also prove in another way that (

FCD

), (

RLD

)

in

are components of

pointfree funcoids:

Theorem

2423

.

(

RLD

)

in

is a component of a pointfree funcoid (between filters

on boolean lattices).

Proof.

Consider the pointfree funcoid

R

defined by the formula

h

R

i

F

=

(

RLD

)

in

F

for binary relations

F

(obviously it does exists).

Then

h

R

i

f

=

h

R

i

d

FCD

up

Γ

f

=

d

RLD

F

up

Γ

f

h

R

i

F

=

d

RLD

F

up

Γ

f

(

RLD

)

in

F

= (

RLD

)

in

d

FCD

F

up

Γ

f

F

=

(

RLD

)

in

f

.

Theorem

2424

.

(

FCD

) is a component of a complete pointfree funcoid (be-

tween filters on boolean lattices).

Proof.

Consider

the

pointfree

funcoid

Q

defined

by

the

formula

h

Q

i

F

= (

FCD

)

F

for binary relations

F

(obviously it does exists).

Then

h

Q

i

f

=

h

Q

i

d

RLD

up

f

= (because up

f

is a filter base) =

d

FCD

F

up

f

h

Q

i

F

=

d

FCD

F

up

f

(

FCD

)

F

=

d

FCD

F

up

f

F

=

d

FCD

up

f

= (

FCD

)

f

.

Proposition

2425

.

(

FCD

)

d

S

=

d

f

S

(

FCD

)

f

if

S

is a filter base of reloids

(with the same sources and destinations).

Proof.

Theorem 831.

Conjecture

2426

.

(

RLD

)

in

d

S

=

d

f

S

(

RLD

)

in

f

if

S

is a filter base of fun-

coids (with the same sources and destinations).

74