 3.9. SOME PROPERTIES OF FRAMES

59

Finally, we have

a

w

a

0

if and only if

a

⊆↑

a

0

, so that

:

A

Up(

A

) maps

A

isomorphically onto its image

h↑i

A

. This image is Fix(

F

) because if

D

is any

fixed point (i.e. if

D

=

d

D

), then

D

clearly belongs to

h↑i

A

; and conversely

a

is always a fixed point of

F

=

↑ ◦

d

since

F

(

a

) =

d

a

=

a

.

Definition

344

.

If

A

,

B

are two JSWLEs, then Join(

A

,

B

) is the (ordered

pointwise) set of finite joins preserving maps

A

B

.

Obvious

345

.

Join(

A

,

B

) is a JSWLE, where

f

t

g

is given by the formula

(

f

t

g

)(

p

) =

f

(

p

)

t

g

(

p

),

Join(

A

,

B

)

is given by the formula

Join(

A

,

B

)

(

p

) =

B

.

Definition

346

.

Let

h

:

Q

R

be a finite joins preserving map. Then

by definition Join(

P, h

) : Join(

P, Q

)

Join(

P, R

) takes

f

Join(

P, Q

) into the

composition

h

f

Join(

P, R

).

Lemma

347

.

Above defined Join(

P, h

) is a finite joins preserving map.

Proof.

(

h

(

f

t

f

0

))

x

=

h

(

f

t

f

0

)

x

=

h

(

f x

t

f

0

x

) =

hf x

t

hf

0

x

= (

h

f

)

x

t

(

h

f

0

)

x

= ((

h

f

)

t

(

h

f

0

))

x.

Thus

h

(

f

t

f

0

) = (

h

f

)

t

(

h

f

0

).

(

h

◦ ⊥

Join(

P,Q

)

)

x

=

h

Join(

P,Q

)

x

=

h

Q

=

R

.

Proposition

348

.

If

h, h

0

:

Q

R

are finite join preserving maps and

h

w

h

0

,

then Join(

P, h

)

w

Join(

P, h

0

).

Proof.

Join(

P, h

)(

f

)(

x

) = (

h

f

)(

x

) =

hf x

w

h

0

f x

= (

h

0

f

)(

x

) =

Join(

P, h

0

)(

f

)(

x

).

Lemma

349

.

If

g

:

Q

R

and

h

:

R

S

are finite joins preserving, then the

composition Join(

P, h

)

Join(

P, g

) is equal to Join(

P, h

g

). Also Join(

P,

id

Q

) for

identity map id

Q

on

Q

is the identity map id

Join(

P,Q

)

on Join(

P, Q

).

Proof.

Join(

P, h

) Join(

P, g

)

f

= Join(

P, h

)(

g

f

) =

h

g

f

= Join(

P, h

g

)

f

.

Join(

P,

id

Q

)

f

= id

Q

f

=

f

.

Corollary

350

.

If

Q

is a JSWLE and

F

:

Q

Q

is a co-nucleus, then for

any JSWLE

P

we have that

Join(

P, F

) : Join(

P, Q

)

Join(

P, Q

)

is also a co-nucleus.

Proof.

From id

Q

w

F

(co-nucleus axiom

1

we have Join(

P,

id

Q

)

w

Join(

P, F

) and since by the last lemma the left side is the identity on Join(

P, Q

),

we see that Join(

P, F

) also satisfies co-nucleus axiom

1

.

Join(

P, F

)

Join(

P, F

) = Join(

P, F

F

) by the same lemma and thus

Join(

P, F

)

Join(

P, F

) = Join(

P, F

) by the second co-nucleus axiom for

F

, showing

that Join(

P, F

) satisfies the second co-nucleus axiom.

By an other lemma, we have that Join(

P, F

) preserves binary joins, given that

F

preserves binary joins, which is the third co-nucleus axiom.

Lemma

351

.

Fix(Join(

P, F

)) = Join(

P,

Fix(

F

)) for every JSWLEs

P

,

Q

and

a join preserving function

F

:

Q

Q

.