background image

It remains to prove that if

R

is a co-frame, then also

Pos

(

P

;

R

)

is a co-frame.

First, we need to prove that

Pos

(

P

;

R

)

is a complete lattice. But it is easy to prove that for every

set

S

2

P

Pos

(

P

;

R

)

we have

x

2

P

:

F

f

2

S

f

(

x

)

and

x

2

P

:

d

f

2

S

f

(

x

)

are monotone and thus

are the joins and meets on

Pos

(

P

;

R

)

.

Next we need to prove that

b

t

Pos

(

P

;

R

)

d

Pos

(

P

;

R

)

S

=

d

Pos

(

P

;

R

)

b

t

Pos

(

P

;

R

)

S

. Really (for every

x

2

P

),

b

t

Pos

(

P

;

R

)

d

Pos

(

P

;

R

)

S

x

=

b

(

x

)

t

d

Pos

(

P

;

R

)

S

x

=

b

(

x

)

t

d

f

2

S

f

(

x

) =

d

f

2

S

(

b

(

x

)

t

f

(

x

)) =

d

f

2

S

¡

b

t

Pos

(

P

;

R

)

f

x

=

d

f

2

S

Pos

(

P

;

R

)

¡

b

t

Pos

(

P

;

R

)

f

x

.

Thus

b

t

Pos

(

P

;

R

)

d

Pos

(

P

;

R

)

S

=

d

f

2

S

Pos

(

P

;

R

)

¡

b

t

Pos

(

P

;

R

)

f

=

d

Pos

(

P

;

R

)

b

t

Pos

(

P

;

R

)

S

.

Denition 31.

P

=

Q

means that posets

P

and

Q

are isomorphic.

Theorem 32.

If

A

is a co-frame and

L

is a distributive lattice with greatest element, then

Join

(

L

;

A

)

is also a co-frame.

Proof.

Let

F

=

d

:

Up

(

A

)

!

Up

(

A

)

;

F

is a co-nucleus by above.

Since Up

(

A

) =

Pos

(

A

; 2)

by proposition

17

we may regard

F

as a co-nucleus on

Pos

(

A

; 2)

.

Join

(

L

;

A

) =

Join

(

L

;

Fix

(

F

))

by corollary

20

.

Join

(

L

;

Fix

(

F

)) =

Fix

(

Join

(

L

;

F

))

by lemma

28

.

By corollary

27

the function Join

(

L

;

F

)

is a co-nucleus on Join

(

L

;

Pos

(

A

; 2))

.

Join

(

L

;

Pos

(

A

; 2)) =

(by lemma

30

)

Pos

(

A

;

Join

(

L

; 2)) =

Pos

(

A

;

F

(

X

))

:

But

Pos

(

A

;

F

(

X

))

is a co-frame by lemma

30

.

Thus Join

(

L

;

A

)

is isomorphic to a poset of xed points of a co-nucleus on the co-frame

Pos

(

A

;

F

(

X

))

. By lemma

13

Join

(

L

;

A

)

is also a co-frame.

Theorem 33.

The set of funcoids from a set

A

to a set

B

is a co-frame.

[TODO: Generalize for

pointfree funcoids.]

Proof.

Take

A

=

F

(

B

)

in the previous theorem and use the fact that

FCD

(

A

;

B

)

is isomorphic to

nite join preserving maps

P

A

!

F

(

B

)

.

Remark 34.

The last theorem was proved without using axiom of choice.

6