 On Todd Trimble's notes on topogeny

by Victor Porton

Web:

http://www.mathematics21.org

This short article is written as a response on Todd Trimble's notes:

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

In this my article I am going to reprise these Todd's theorems which are new for me, converted
into terminology and notation of my book [

1

and of

http://www.mathematics21.org/binaries/rewrite-plan.pdf

Now this article is a partial draft. I am going to integrate materials of this article into my book.

1 Misc

The following theorem is a strenghtening suggested by Todd of my theorem:

Theorem 1.

d

F

S

=

S

f"

(

K

0

u

Z

:::

u

Z

K

n

)

j

K

i

2

S

S

where

i

= 0

; :::; n

for

n

2

N

g

for

every nonempty set

S

of lters on a meet-semilattice.

[TODO: Strengthen my theorems requiring

distributivity of lattice with this result which does not require it even to be a lattice.]

Proof.

It follows from the fact that

l

F

S

=

l

F

K

0

u

Z

:::

u

Z

K

n

j

K

i

2

[

S

where

i

= 0

; :::; n

for

n

2

N

and that

f

K

0

u

Z

:::

u

Z

K

n

j

K

i

2

S

S

where

i

= 0

; :::; n

for

n

2

N

g

is a lter base.

Denition 2.

A complete lattice is

co-compact

i

d

S

= 0

for a set

S

of elements of this lattice

implies that there is its nite subset

T

S

such that

d

T

= 0

.

[TODO: Remove the requirement

to have least.]

Proposition 3.

The poset of lters on a meet-semilattice

Z

with least element is co-compact.

Proof.

If

0

2

d

F

S

then there are

K

i

2

S

S

such that

0

2"

(

K

0

u

Z

:::

u

Z

K

n

)

that is

K

0

u

Z

:::

u

Z

K

n

= 0

from which easily follows

F

0

u

F

:::

u

F

F

n

= 0

for some

F

i

2

S

.

Proposition 4.

X

[

f

]

d

S

, 9Y 2

S

:

X

[

f

]

Y

if

S

is a generalized lter base on Dst

f

.

[TODO:

Pointfree funcoids.]

Proof.

X

[

f

]

d

S

,

d

S

u h

f

iX

=

/ 0

,

d

hh

f

iX u i

S

=

/ 0

,

(by properties of generalized lter

bases)

,9Y 2 hh

f

iX u i

S

:

Y

=

/ 0

, 9Y 2

S

:

h

f

iX u Y

=

/ 0

, 9Y 2

S

:

X

[

f

]

Y

.

The following theorem was easy to prove, but I would not discovered it without Todd's help:

Theorem 5.

A function

'

:

F

(

A

)

!

F

(

B

)

preserves nite joins and ltered meets i there exists a

funcoid

f

such that

h

f

i

=

'

.

[TODO: Dene ltered meets. Say about empty join

0

.]

1