 Pointfree funcoids as a generalization of frames

by Victor Porton

Email:

porton@narod.ru

Web:

http://www.mathematics21.org

August 29, 2013

Abstract

I define an injection from the set of frames to the set of pointfree endo-funcoids.

1 Preliminaries

This article is a rough partial draft of a future longer writting.

Read my book  before this article. The preprint of  is not final, so theorem numbers may

change.

2 Confession of a non-professional

I am not a professional mathematician. I just recently started my study of pointfree topology by
the book “Stone Spaces”.

I don’t understand how to prove the statement I use below that every frame can be embedded

into a boolean lattice. (I take it below as granted, without understanding the proof.)

Despite of all that, this article presents a new branch of mathematics discovered by me: rela-

tionships between frames and locales on one side and pointfree funcoids (pointfree funcoids are
also my discovery) on an other side. (Frames and locales can be considered as a special kind of
pointfree funcoids.) I expect that analyzing pointfree funcoids will turn to be much more easy that
customary ways of doing pointfree topology.

3 Definitions

3.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 ,

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

A

}

.

Here

d

can be taken on either

L

or

B

(

L

)

as they are the same.

Obvious 1.

cl

L

B

(

L

)

.

cl

(

A

B

) =

d

{

X

L

|

X

A

B

}

=

d

{

X

L

|

X

A, X

B

}

=

d

{

X

1

X

2

|

X

1

A,

X

2

B

}

=

d

{

X

1

|

X

1

A

} ⊔

d

{

X

2

|

X

2

B

}

=

cl

A

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

=

l

F

(

B

(

L

))

h

cl

i

up

(

F

(

B

(

L

));

P

(

B

(

L

)))

X

for every filter

X ∈

F

(

B

(

L

))

.

1