 CHAPTER 12

Pointfree funcoids as a generalization of frames

I define an injection from the set of frames to the set of pointfree endo-funcoids.
This article is a rough partial draft of a future longer writing.

1. Definitions

1.1. Pointfree funcoid induced by a co-frame.

Let

L

is a co-frame.

We will define pointfree funcoid

L

.

Let

B

(

L

) is a boolean lattice whose co-subframe

L

is. (That this mapping exists

follows from [

3

], page 53.) There may be probably more than one such mapping,

but we just choose one

B

arbitrarily.

Define cl(

A

) =

d

{

X

L

|

X

w

A

}

.

Here

d

can be taken on either

L

or

B

(

L

) as they are the same.

Obvious

2111

.

cl

L

B

(

L

)

.

cl(

A

t

B

) =

d

{

X

L

|

X

w

A

t

B

}

=

d

{

X

L

|

X

w

A, X

w

B

}

=

d

{

X

1

t

X

2

|

X

1

w

A, X

2

w

B

}

=

d

{

X

1

|

X

1

w

A

} t

d

{

X

2

|

X

2

w

B

}

=

cl

A

t

cl

B

.

cl 0 = 0 is obvious.
Hence we are under conditions of the theorem 14.26 in my book.
So there exists a unique pointfree endo-funcoid

L

FCD

(

F

(

B

(

L

))

,

F

(

B

(

L

)))

such that

h⇑

L

iX

=

F

(

B

(

L

))

l

h

cl

i

up

(

F

(

B

(

L

))

,

P

(

B

(

L

)))

X

for every filter

X ∈

F

(

B

(

L

)).

1.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

2112

.

It seems that

is

not

a monovalued function from

pFCD

to

Ob(

Frm

).

1.3. Isomorphism of co-frames through pointfree funcoids.

Remark

2113

.

P

(

B

(

L

)) =

Z

(

F

(

B

(

L

))) (theorem 4.137 in [

5

]).

Theorem

2114

.

L

7→⇓⇑

L

(where

L

ranges all small frames) is an order iso-

morphism.

Proof.

Let

A

0

∈⇓⇑

L

. Then there exists

A

∈ B

(

L

) such that

A

0

=

B

(

L

)

A

.

h

f

i

A

0

=

B

(

L

)

cl

A

.

h

f

i

A

0

=

A

0

that is

B

(

L

)

cl

A

=

A

0

=

B

(

L

)

A

. So cl

A

=

A

and thus

A

L

.

Let now

A

L

. Then take

A

0

=

B

(

L

)

A

. We have

h

f

i

A

0

= cl

A

=

B

(

L

)

A

=

A

0

.

So

A

0

∈⇓⇑

L

.

41