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 filters 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 filter base.
Definition 2. A complete lattice is co-compact iff
d
S = 0 for a set S of elements of this lattice
implies that there is its finite subset T ⊆ S such that
d
T = 0. [TODO: Remove the requirement
to have least.]
Proposition 3. The poset of filters 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 filter 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 filter
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 finite joins and filtered meets iff there exists a
funcoid f such that hf i = '. [TODO: Define filtered 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 finite joins and filtered meets.
2 Representing funcoids as binary relations
Definition 7. The binary relation ξ
~
2 P(F(Src ξ) × F(Dst ξ)) for a funcoid ξ is defined by the
formula A ξ
~
B ,B w hξ iA.
Definition 8. The binary relation ξ
∗
2 P(P Src ξ × P Dst ξ) for a funcoid ξ is defined 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 filter
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
