**Algebraic General Topology. Vol 1**:
Paperback
/
E-book
||
**Axiomatic Theory of Formulas**:
Paperback
/
E-book

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 fK

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.

Deﬁnition 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 02"(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 hf iX =/ 0 ,

d

hhf iX u i

∗

S =/ 0 , (by properties of generalized ﬁlter

bases),9Y 2 hhf iX u i

∗

S: Y =/ 0 , 9Y 2 S: hf 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 hf i = '. [TODO: Deﬁne ﬁltered meets. Say about empty join 0.]

1

Proof. Backward implication is easy.

Let = 'j

PA

. Then preserves bottom element and binary joins. Thus there exists a funcoid f

such that hf i

∗

= .

It remains to prove that hf i = '.

Really, hf iX =

d

hhf i

∗

i

∗

X =

d

h i

∗

X =

d

h'i

∗

X = '

d

X = ' X for every X 2 F(A).

Corollary 6. Funcoids f from A to B bijectively correspond by the formula hf i = ' to functions

': F(A) ! F(B) preserving ﬁnite joins and ﬁltered meets.

2 Representing funcoids as binary relations

Deﬁnition 7. The binary relation ξ

~

2 P(F(Src ξ) × F(Dst ξ)) for a funcoid ξ is deﬁned by the

formula A ξ

~

B ,B w hξ iA.

Deﬁnition 8. The binary relation ξ

∗

2 P(P Src ξ × P Dst ξ) for a funcoid ξ is deﬁned by the

formula

A ξ

∗

B ,B w hξiA , B 2 up hξiA:

Proposition 9. Funcoid ξ can be restored from

1. the value of ξ

~

;

2. the value of ξ

∗

.

Proof.

1. The value of hξi can be restored from ξ

~

.

2. The value of hξi

∗

can be restored from ξ

∗

.

Theorem 10. Let ν and ξ be composable funcoids. Then:

1. ξ

~

◦ ν

~

= (ξ ◦ ν)

~

;

2. ξ

∗

◦ ν

∗

= (ξ ◦ ν)

∗

.

Proof.

1. A [ξ

~

◦ ν

~

] C , 9B:(A ν

~

B ^B ξ

~

C ), 9B 2 F(Dstν):(B w hν iA^ C whξiB) ,C whξ ihνiA,

C w hξ ◦ ν iA , A [(ξ ◦ ν)

~

] C.

2. A [ξ

∗

◦ ν

∗

] C , 9B: (A ν

∗

B ^B ξ

∗

C ) , 9B: (B 2 up hν iA ^ C 2 up hξiB) , 9B 2 up hν iA:

C 2 up hξiB.

A [(ξ ◦ ν)

∗

] C , C 2 up hξ ◦ ν iB , C 2 up hξ ihν iB.

It remains to prove

9B 2 up hν iA: C 2 up hξiB , C 2 up hξ ihνiA:

9B 2 up hν iA: C 2 up hξiB ) C 2 up hξihν iA is obvious.

Let C 2 up hξ ihν iA. Then C 2 up

d

hhξ ii

∗

up hν iA; so by properties of generalized ﬁlter

bases, 9P 2 hhξii

∗

up hν iA: C 2 up P ; 9B 2 up hν iA: C 2 up hξ iB.

Remark 11. The above theorem is interesting by the fact that composition of funcoids is repre-

sented as relational composition of binary relations.

Bibliography

[1] Victor Porton. Algebraic General Topology. Volume 1. 2014.

2