background image

Definition 4.

I call a

Pos

-morphism

monovalued

when it maps atoms to atoms or least element.

Definition 5.

I call a

Pos

-morphism

entirely defined

when its value is non-least on every non-

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. mefp

FCD

is the subcategory of

fp

FCD

with only monovalued and entirely defined

morphisms.

Remark 10.

In the two above definitions different definitions of monovaluedness and entire

definedness from different articles.

4 Definition of the categories

Definition 11.

A

(pointfree) endo-funcoid

is a (pointfree) funcoid with the same source and

destination (an endomorphism of the category of (pointfree) funcoids). I will denote Ob

f

the

object of an endomorphism

f

.

Obvious 12.

The

category of continuous pointfree funcoids

cont

(

fp

FCD

)

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 from

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 pointfree funcoids.

Identity for an object

a

is

(

I

Ob

a

FCD

;

a

;

a

)

.

5 Isomorphisms

Theorem 13.

If

f

is an isomorphism

a

b

of the category

cont

(

fp

FCD

)

, 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 preserve structure of objects. I will show that (under certain con-

ditions) isomorphisms of

cont

(

fp

FCD

)

really preserve structure of objects.

First we will consider an isomorphism between objects

a

and

b

which are funcoids (not the

general case of pointfree funcoids). 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