 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.

h

f

i

A

⊓ h

f

i

((

Src

f

)

\

A

) = 0

Dst

f

because

f

is monovalued.

h

f

i

A

⊔ h

f

i

((

Src

f

)

\

A

) = 1

Dst

f

.

Therefore

h

f

i

A

is a principal filter (theorem 49 in ). So

f

is co-complete.

That

f

is complete follows from symmetry.

For wider class of pointfree funcoids the concept of bijection does not make sense. Instead we

would want a structure preserving map to be

order isomorphism

.

Actually, for mapping between

P

A

and

P

B

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 isomorphisms

f

between

P

A

and

P

B

by the formula

f

=

h

F

i

.

Proof.

Let

F

is a bijection. Then

X

Y

⇒ h

F

i

X

⊆ h

F

i

Y

and

h

F

1

ih

F

i

X

=

X

for every sets

X ,

Y

P

A

. Thus

f

=

h

F

i

is an order isomorphism.

Let now

f

is an order isomorphism between

P

A

and

P

B

. 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

=

h

F

i

.

For arbitrary pointfree funcoids isomorphisms do not necessarily preserve structure. It holds

only for

increasing pointfree funcoids

:

Definition 16.

I call a pointfree funcoid

f

increasing

iff

h

f

i

and

h

f

1

i

are monotone functions.

Proposition 17.

If

f

is an increasing isomorphism of the category of pointfree funcoids then

h

f

i

is an order isomorphism.

Proof.

We have:

h

f

i ◦ h

f

1

i

=

h

f

f

1

i

=

h

id

B

FCD

i

=

id

B

and

h

f

1

i ◦ h

f

i

=

h

f

1

f

i

=

h

id

A

FCD

i

=

id

A

.

Thus

h

f

i

is a bijection.

h

f

i

is increasing and bijective.

Remark 18.

Non-increasing isomorphisms of the category of pointfree funcoids are against sound

mind, they don’t preserve the structure of the source, that is for them

h

f

i

or

h

f

1

i

are not order

isomorphisms.

Obvious 19.

Isomorphisms of

cont

(

Pos

)

and

cont

(

mePos

)

are order isomorphisms.

6 Direct products

[TODO: Now this section is a complete mess. Clean it up.]

Consider the category

contFcd

which is the full subcategory

cont

(

mePos

)

restricted to

objects 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 formula

f

1

×

(

D

)

f

2

y

=

f

1

y

×

FCD

f

2

y

.

f

1

×

(

D

)

f

2

is monovalued and entirely defined because so are

f

1

and

f

2

.

f

1

×

(

D

2)

f

2

y

=

[

{

f

1

x

×

FCD

f

2

x

|

x

atoms

A

y

}

.

[TODO: Is

f

1

×

(

D

2)

f

2

a pointfree funcoid?]

Direct products

3