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

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 .

Deﬁnition 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 deﬁned 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 inﬁnitely small is less than inﬁnitely

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 deﬁned.

1

Deﬁnition 4. I call a Pos-morphism monovalued when it maps atoms to a toms or least element.

Deﬁnition 5. I call a Pos-morphism entirely deﬁned when its value is non-least on every n on-

least element.

Obvious 6. A morphism is both monovalued and entirely deﬁned iﬀ it maps atoms into atoms.

[TODO: Show how it relates with dagger categories.]

Deﬁnition 7. mePos is the subcategory of Pos with only monovalued and entirely deﬁned

morphisms.

Obvious 8. This is a well deﬁned category.

Deﬁnition 9. mefpFCD is the subcategory of fpFCD with only monovalued and entirely deﬁned

morphisms.

Remark 10. In the two above deﬁnitions diﬀerent deﬁnitions of monovalue dness and entire

deﬁnedness from diﬀerent articles.

4 Deﬁnition o f t he cat egories

Deﬁnition 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 deﬁned.

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 deﬁnition 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 ﬁlter ( 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:

Deﬁnition 16. I call a pointfree funco id f increasing iﬀ 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 deﬁned 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 deﬁned 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 deﬁne ??

[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