
Proof. Join(P ; h)(f)(x) = (h ◦ f )(x) = hfx w h
0
fx = (h
0
◦ f)(x) = Join(P ; h
0
)(f )(x).
Lemma 26. 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 27. If Q is a join-semilattice and F : Q! Q is a co-nucleus, then for any join-semilattice
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 finite joins, given that F preserves finite
joins, which is the third co-nucleus axiom.
Lemma 28. Fix(Join(P ; F )) = Join(P ; Fix(F )) for every join-semilattices P , Q and a join
preserving function F : Q ! Q.
Proof. a 2 Fix(Join(P ; F )) , a 2 F
P
^ F ◦ a = a , a 2 F
P
^ 8x 2 P : F (a(x)) = a(x) .
a 2 Join(P ; Fix(F )) , a 2 Fix(F )
P
, a 2 F
P
^ 8x 2 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 29. Pos(A; B) is the pointwise ordered poset of monotone maps from a poset A to a
poset B.
Lemma 30. If Q, R are join-semilattices and P is a poset, then Pos(P ; R) is a join-semilattice 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 2 Pos(P; R). Then λx 2 P : (fx t gx) is obviously monotone and then it is evident
that f t
Pos(P ;R)
g = λx 2 P : (fx t gx). λx 2 P : ?
R
is also obviously monotone and it is evident
that ?
Pos(P ;R)
= λx 2 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 2 Pos(P ; Join(Q; R)) iff f 2 Join(Q; R)
P
iff f 2 fg 2 R
Q
j g preserves finite joinsg
P
iff f 2 (R
Q
)
P
and every g = f(x) (for x 2 P ) preserving finite joins. This is bijectively equivalent (f 7! f
0
) to
f
0
2 (R
P
)
Q
preserving finite joins.
f
0
2 Join(Q; Pos(P ; R)) iff f
0
preserves finite joins and f
0
2 Pos(P ; R)
Q
iff f
0
preserves finite joins
and f
0
2 fg 2 (R
P
)
Q
j g(x) is monotoneg iff f
0
preserves finite joins and f
0
2 (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.
5