 5. ISOMORPHISMS

32

Obvious

2067

.

A morphism is both monovalued and entirely defined iff it

maps atoms into atoms.

FiXme

: Show how it relates with dagger categories.

Definition

2068

.

mePos

is the subcategory of

Pos

with only monovalued

and entirely defined morphisms.

Obvious

2069

.

This is a well defined category.

Definition

2070

.

mefp

FCD

is the subcategory of

fp

FCD

with only monoval-

ued and entirely defined morphisms.

Remark

2071

.

In the two above definitions different definitions of monoval-

uedness and entire definedness from different articles.

4. Definition of the categories

Definition

2072

.

A

(pointfree) endo-funcoid

is a (pointfree) funcoid with the

same source and destination (an endomorphism of the category of (pointfree) fun-
coids). I will denote Ob

f

the object of an endomorphism

f

.

Obvious

2073

.

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

v

b

f

, or equivalently

a

v

f

1

b

f

, or

equivalently

f

a

f

1

v

f

).

Composition is the composition of pointfree funcoids.

Identity for an object

a

is (

I

FCD

Ob

a

, a, a

).

5. Isomorphisms

Theorem

2074

.

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

v

b

f

and

f

1

b

v

a

f

1

. Consequently

f

1

f

a

v

f

1

b

f

;

a

v

f

1

b

f

;

a

f

1

v

f

1

b

f

f

1

;

a

f

1

v

f

1

b

. Similarly

b

f

v

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 conditions) isomorphisms of cont(

fp

FCD

) really preserve structure

of objects.

First we will consider an isomorphism between objects

a

and

b

which are fun-

coids (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:

Theorem

2075

.

If

f

is an isomorphism of the category of funcoids then

f

is a discrete funcoid (so, it is essentially a bijection).

FiXme

: Split it into two

propositions: about completeness and co-completeness.