 3.9. SOME PROPERTIES OF FRAMES

55

Proof.

concat(

J

x

K

) =

x

for a function

x

taking an ordinal number of argument

is obvious. It is remained to prove

concat(concat

S

) = concat(concat

S

);

We have, using the lemmas,

concat(concat

S

)

uncurry(concat

S

)

(by lemma

315

)

uncurry(uncurry

S

)

uncurry(uncurry

S

)

uncurry(concat

S

)

concat(concat

S

)

.

Consequently concat(concat

S

) = concat(concat

S

).

Corollary

318

.

Ordinated product is an infinitely associative function.

3.8. Galois surjections

Definition

319

.

Galois surjection

is the special case of Galois connection such

that

f

f

is identity.

Proposition

320

.

For Galois surjection

A

B

such that

A

is a join-

semilattice we have (for every

y

B

)

f

y

= max

x

A

f

x

=

y

.

Proof.

We need to prove (theorem

131

)

max

x

A

f

x

=

y

= max

x

A

f

x

v

y

.

To prove it, it’s enough to show that for each

f

x

v

y

there exists an

x

0

w

x

such

that

f

x

0

=

y

.

Really,

y

=

f

f

y

. It’s enough to prove

f

(

x

t

f

y

) =

y

.

Indeed (because lower adjoints preserve joins),

f

(

x

t

f

y

) =

f

x

t

f

f

y

=

f

x

t

y

=

y

.

3.9. Some properties of frames

This section is based on a

Todd Trimble

’s proof. A shorter but less elemen-

tary proof (also by

Todd Trimble

) is available at

http://ncatlab.org/toddtrimble/published/topogeny

I will abbreviate

join-semilattice with least element

as JSWLE.

Obvious

321

.

JSWLEs are the same as finitely join-closed posets (with nullary

joins included).

Definition

322

.

It is said that a function

f

from a poset

A

to a poset

B

preserves finite joins

, when for every finite set

S

P

A

such that

d

A

S

exists we

have

d

B

h

f

i

S

=

f

d

A

S

.

Obvious

323

.

A function between JSWLEs preserves finite joins iff it preserves

binary joins (

f

(

x

t

y

) =

f x

t

f y

) and nullary joins (

f

(

A

) =

B

).

Definition

324

.

A

fixed point

of a function

F

is such

x

that

F

(

x

) =

x

. We

will denote Fix(

F

) the set of all fixed points of a function

F

.