Theorem 14. If f is an isomorphism of the category of funcoids then f is a discrete funcoid (so,
it is essentially a bijection). [TODO: Split it into two propositions: about completeness and co-
completeness.]
Proof. hf i
∗
A ⊓ hf i
∗
((Src f ) \ A) = 0
Dst f
because f is monovalued.
hf i
∗
A ⊔ hf i
∗
((Src f) \ A) = 1
Dst f
.
Therefore hf i
∗
A is a principal filter ( theorem 49 in [2]). So f is co-complete.
That f is complete follows f rom symmetr y.
For wider class of pointfree funcoids the concept of bijection does not ma ke sense. Instead we
would want a structure preserving map to be order isomorphism.
Actually, for mapping between PA a nd PB where A and B are some sets (including the above
considered case of funcoids from A to B) bijection and order isomorphism are essentially the same:
Proposition 15. Bijections F between sets A and B bijectively correspond to order isomor phis ms
f between PA and PB by the formula f = hF i.
Proof. Let F is a bijection. Then X ⊆ Y ⇒ hF iX ⊆ hF iY and hF
−1
ihF iX = X for every sets X ,
Y ∈ PA. Thus f = hF i is an order isomorphism.
Let now f is an order isomorphism between PA and PB. Then f ({x}) is a singleton for every
x ∈ A. Take F (x) to the unique y such that f({x})= {y }. Obviously f is a bijection and f = hF i.
For arbitrary pointfree funcoids isomorphisms do not necessarily preserve structure. It holds
only for increasing pointfree funcoids:
Definition 16. I call a pointfree funco id f increasing iff hf i and hf
−1
i are monotone functions.
Proposition 17. If f is an increasing isomorphism of the category of pointfree funcoids then hf i
is an order isomorphism.
Proof. We have: hf i ◦ hf
−1
i = hf ◦ f
−1
i = hid
B
FCD
i = id
B
and hf
−1
i ◦ hf i = hf
−1
◦ f i= hid
A
FCD
i = id
A
.
Thus hf i is a bijection.
hf i is increasing and bijective.
Remark 18. Non-increasing isomorphisms of the category of pointfree funcoid s are against sound
mind, they don’t preserve the structure of the source, that is for them hf i or hf
−1
i are not order
isomorphisms.
Obvious 19. Isomorphisms of cont(Pos) and cont(mePos) are order is omorphisms.
6 Direct products
[TODO: Now this section is a complete mess. Clean it up.]
Consider the category contFcd which is the full subcategory co nt(mePos) restricted to
object s which are essentially increasing pointfree funcoids.
Let f
1
: Y → X
1
and f
2
: Y → X
2
are morphisms of contFcd.
The product object is X
1
×
(C)
X
2
(cross composition product of funcoids used). It is easy to
see that X
1
×
(C)
X
2
is an object of contFcd that is an endo-funcoid.
The morphism f
1
×
(D)
f
2
: Y → X
1
×
(C)
X
2
is defined by the for mula
f
1
×
(D)
f
2
y =
f
1
y ×
FCD
f
2
y.
f
1
×
(D)
f
2
is monovalued and entir e ly defined because so are f
1
and f
2
.
f
1
×
(D2)
f
2
y =
[
{f
1
x ×
FCD
f
2
x | x ∈ atoms
A
y}.
[TODO: Is
f
1
×
(D2)
f
2
a pointfree funcoid?]
Direct products 3