Categories related with funcoids
by Victor Porton
Web: http://www.mathematics21.org
July 26, 2012
Abstract
I consider some categories related with pointfree funcoids.
1 Draft status
This is a rough partial draft.
2 Topic of this article
In this article are considered some categories related to pointfree funcoids [1].
3 Category of co ntinuous morphism s
I will denote Ob f the object (source and destination) of an endomorphism f .
Definition 1. Let C is a partially ordered category. The category cont(C) (which I call the
category of continuous morphism over C) is:
• Objects are endomorphisms of category C.
• Morphisms are triples (f; a; b) where a and b are objects and f : Ob a → Ob b is a morphism
of th e category C such that f ◦ a ⊑ b ◦ f .
• Composition of morphisms is defined by the formula (g; b; c) ◦ (f ; a; b) = (g ◦ f; a; c).
• Identity morphisms are (a; a; 1
a
C
).
It is really a category:
Proof. We need to prove that: composition of morphisms is a morphism, composition is associative,
and identity morphisms can be canceled on the left and on the right.
That co mposition of morphisms is a morphism follows from these implications:
f ◦ a ⊑ b ◦ f ∧ g ◦ b ⊑ c ◦ g ⇒ g ◦ f ◦ a ⊑ g ◦ b ◦ f ⊑ c ◦ g ◦ f .
That co mposition is associative is obvious.
That identity morphisms can be canceled on the left and on the right is obvious.
Remark 2. The “physical” meaning of this category is:
• Objects (endomor phis ms of C) are spaces.
• Morphisms are continuous functions between spaces.
• f ◦ a ⊑ b ◦ f intuitively means that f combined with an infinitely small is less than infinitely
small combined with f (that is f is continuous).
Remark 3. Every Hom(A;B) of Pos is partially ordered by the formula a6 b⇔ ∀x ∈ A: a(x) 6 b(x).
So cont(Pos) is defined.
1
Definition 4. I call a Pos-morphism monovalued when it maps atoms to a toms or least element.
Definition 5. I call a Pos-morphism entirely defined when its value is non-least on every n on-
least element.
Obvious 6. A morphism is both monovalued and entirely defined iff it maps atoms into atoms.
[TODO: Show how it relates with dagger categories.]
Definition 7. mePos is the subcategory of Pos with only monovalued and entirely defined
morphisms.
Obvious 8. This is a well defined category.
Definition 9. mefpFCD is the subcategory of fpFCD with only monovalued and entirely defined
morphisms.
Remark 10. In the two above definitions different definitions of monovalue dness and entire
definedness from different articles.
4 Definition o f t he cat egories
Definition 11. A (pointfree) endo-funcoid is a (pointfree) funcoid with the same source and
destination (an endomorphism of t he category of (pointfree) funcoids). I will denote Ob f the
object of an endom orphism f .
Obvious 12. The category of continuous pointfree fun coids cont(fpFCD) is:
• Objects are small pointfree endo-funcoids.
• Morphisms from an object a to an object b are triples (f ; a;b) where f is a pointfree funcoid
from Ob a to Ob b such that f is a continuous morphism fro m a to b (that is f ◦ a ⊑ b ◦ f ,
or equivalently a ⊑ f
−1
◦ b ◦ f, or equivalently f ◦ a ◦ f
−1
⊑ f ).
• Composition is the composition of po intfree funcoids.
• Identity for an object a is (I
Ob a
FCD
; a; a).
5 Isomorphisms
Theorem 13. If f is an isomorphism a → b o f the category cont(fpFCD), then:
1. f ◦ a = b ◦ f ;
2. a = f
−1
◦ b ◦ f ;
3. f ◦ a ◦ f
−1
= b.
Proof. Note that f is monovalued and entirely defined.
1. We have f ◦ a ⊑ b ◦ f and f
−1
◦ b ⊑ a ◦ f
−1
. Consequently f
−1
◦ f ◦ a ⊑ f
−1
◦ b ◦ f ;
a ⊑ f
−1
◦ b ◦ f; a ◦ f
−1
⊑ f
−1
◦ b ◦ f ◦ f
−1
; a ◦ f
−1
⊑ f
−1
◦ b. Similarly b ◦ f ⊑ f ◦ a. So f ◦ a = b ◦ f .
2 and 3. Follow from the definition of isomorphism.
Isomorphisms are meant to pre serve structure of objects. I will show that (under certain con-
ditions) isomorphisms of cont(fpFCD) really preserve structure of objects.
First we will co nsider an isomorphism between objects a and b which are funcoids (not the
general case of pointfree funco ids). In this case a map which preserves structure of objects is a
bijection. It is really a bijection as the following theorem says:
2 Section 5
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
To prove that it is really a morphism we need to show
f
1
×
(D)
f
2
◦ Y ⊑
X
1
×
(C)
X
2
◦
f
1
×
(D)
f
2
that is (for every y)
f
1
×
(D)
f
2
Yy ⊑
X
1
×
(C)
X
2
f
1
×
(D)
f
2
y.
Really,
f
1
×
(D)
f
2
Yy = f
1
Yy ×
FCD
f
2
Yy;
X
1
×
(C)
X
2
f
1
×
(D)
f
2
y =
X
1
×
(C)
X
2
(f
1
y ×
FCD
f
2
y) = X
1
f
1
y ×
FCD
X
2
f
2
y;
but it is easy to show f
1
Yy ×
FCD
f
2
Yy ⊑ X
1
f
1
y ×
FCD
X
2
f
2
y.
??
I define ??
[TODO: Prove that it is a direct product in contFcd.]
??
Bib liography
[1] Victor Porton. Pointfree funcoids. At http://www.mathematics21.org/binaries/pointfree.pdf.
[2] Victor Porton. Filters on posets and generalizations. International Journal of Pure and Applied Mathe-
matics, 74(1):55–119, 2012.
4 Section
