 3.2 Co-frame induced by a pointfree funcoid

The co-frame

f

for some pointfree endo-funcoids

f

will be defined to be the reverse of

. See

below for exact meaning of being reverse.

Let restore the co-frame

L

from the pointfree funcoid

L

.

Let poset

f

for every pointfree funcoid

f

is defined by the formula:

f

=

{

X

Z

(

Ob

f

)

| h

f

i

X

=

X

}

.

Remark 2.

It seems that

is

not

a monovalued function from pf

FCD

to Ob

(

Frm

)

.

3.3 Isomorphism of co-frames through pointfree funcoids

Remark 3.

P

(

B

(

L

)) =

Z

(

F

(

B

(

L

)))

(theorem 4.137 in ).

Theorem 4.

L

⇓⇑

L

(where

L

ranges all small frames) is an order isomorphism.

Proof.

Let

A

∈ ⇓⇑

L

. Then there exists

A

∈ B

(

L

)

such that

A

=

B

(

L

)

A

.

h

f

i

A

=

B

(

L

)

cl

A

.

h

f

i

A

=

A

that is

B

(

L

)

cl

A

=

A

=

B

(

L

)

A

. So cl

A

=

A

and thus

A

L

.

Let now

A

L

. Then take

A

=

B

(

L

)

A

. We have

h

f

i

A

=

cl

A

=

B

(

L

)

A

=

A

. So

A

∈ ⇓⇑

L

.

We have proved that it is a bijection.
Because

A

and

A

are related by the equation

A

=

B

(

L

)

A

it is obvious that this is an order

embedding.

4 Postface

Pointfree funcoids are a

massive

generalization of locales and frames: They don’t only require the

lattice of filters to be boolean but these can be even not lattices of filters at all but just arbitrary
posets. I think a new era in pointfree topology starts.

Much work is yet needed to relate different properties of frames and locales with corresponding

properties of pointfree funcoids.

Bibliography



Peter T. Johnstone.

Stone Spaces

. Cambridge University Press, 1982.



Victor Porton.

Algebraic General Topology. Volume 1

. 2013.

2

Section