background image

3.9. SOME PROPERTIES OF FRAMES

60

Proof.

a

Fix(Join(

P, F

))

a

F

P

F

a

=

a

a

F

P

∧ ∀

x

P

:

F

(

a

(

x

)) =

a

(

x

).

a

Join(

P,

Fix(

F

))

a

Fix(

F

)

P

a

F

P

∧ ∀

x

P

:

F

(

a

(

x

)) =

a

(

x

).

Thus Fix(Join(

P, F

)) = Join(

P,

Fix(

F

)). That the order of the left and right

sides of the equality agrees is obvious.

Definition

349

.

Pos

(

A

,

B

) is the pointwise ordered poset of monotone maps

from a poset

A

to a poset

B

.

Lemma

350

.

If

Q

,

R

are JSWLEs and

P

is a poset, then

Pos

(

P, R

) is a JSWLE

and

Pos

(

P,

Join(

Q, R

)) is isomorphic to Join(

Q,

Pos

(

P, R

)). If

R

is a co-frame,

then also

Pos

(

P, R

) is a co-frame.

Proof.

Let

f, g

Pos

(

P, R

). Then

λx

P

: (

f x

t

gx

) is obviously monotone

and then it is evident that

f

t

Pos

(

P,R

)

g

=

λx

P

: (

f x

t

gx

).

λx

P

:

R

is also

obviously monotone and it is evident that

Pos

(

P,R

)

=

λx

P

:

R

.

Obviously both

Pos

(

P,

Join(

Q, R

)) and Join(

Q,

Pos

(

P, R

)) are sets of order

preserving maps.

Let

f

be a monotone map.

f

Pos

(

P,

Join(

Q, R

)) iff

f

Join(

Q, R

)

P

iff

f

n

g

R

Q

g

preserves finite joins

o

P

iff

f

(

R

Q

)

P

and every

g

=

f

(

x

) (for

x

P

) preserving finite joins. This is bijectively

equivalent (

f

7→

f

0

) to

f

0

(

R

P

)

Q

preserving finite joins.

f

0

Join(

Q,

Pos

(

P, R

)) iff

f

0

preserves finite joins and

f

0

Pos

(

P, R

)

Q

iff

f

0

preserves finite joins and

f

0

n

g

(

R

P

)

Q

g

(

x

) is monotone

o

iff

f

0

preserves finite joins and

f

0

(

R

P

)

Q

.

So we have proved that

f

7→

f

0

is a bijection between

Pos

(

P,

Join(

Q, R

)) and

Join(

Q,

Pos

(

P, R

)). That it preserves order is obvious.

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

P

Pos

(

P, R

) we have

λx

P

:

d

f

S

f

(

x

) and

λx

P

:

d

f

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

)

Pos

(

P,R

)

l

S

=

Pos

(

P,R

)

l

D

b

t

Pos

(

P,R

)

E

S.

Really (for every

x

P

),

b

t

Pos

(

P,R

)

Pos

(

P,R

)

l

S

x

=

b

(

x

)

t

Pos

(

P,R

)

l

S

x

=

b

(

x

)

t

l

f

S

f

(

x

) =

l

f

S

(

b

(

x

)

t

f

(

x

)) =

l

f

S

b

t

Pos

(

P,R

)

f

x

=

Pos

(

P,R

)

l

f

S

b

t

Pos

(

P,R

)

f

x.

Thus

b

t

Pos

(

P,R

)

d

Pos

(

P,R

)

S

=

d

Pos

(

P,R

)

f

S

b

t

Pos

(

P,R

)

f

=

d

Pos

(

P,R

)

b

t

Pos

(

P,R

)

S

.

Definition

351

.

P

=

Q

means that posets

P

and

Q

are isomorphic.