6. DIRECT PRODUCTS

33

Proof.

h

f

i

A

u h

f

i

((Src

f

)

\

A

) = 0

Dst

f

because

f

is monovalued.

h

f

i

A

t h

f

i

((Src

f

)

\

A

) = 1

Dst

f

.

Therefore

h

f

i

A

is a principal filter (theorem 49 in [

4

]). 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

2076

.

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 struc-

ture. It holds only for

increasing pointfree funcoids

:

Definition

2077

.

I call a pointfree funcoid

f

increasing

iff

h

f

i

and

h

f

1

i

are

monotone functions.

Proposition

2078

.

If

f

is an increasing isomorphism of the category of point-

free 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

FCD

B

i

= id

B

and

h

f

1

i ◦ h

f

i

=

h

f

1

f

i

=

h

id

FCD

A

i

= id

A

. Thus

h

f

i

is a bijection.

h

f

i

is increasing and bijective.

Remark

2079

.

Non-increasing isomorphisms of the category of pointfree fun-

coids 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

2080

.

Isomorphisms of cont(

Pos

) and cont(

mePos

) are order iso-

morphisms.

6. Direct products

FiXme

: 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

Y

×

FCD

f

2

Y

|

Y

atoms

A

y

.

FiXme

: Is (

f

1

×

(

D

2)

f

2

) a pointfree funcoid?

To prove that it is really a morphism we need to show

(

f

1

×

(

D

)

f

2

)

Y

v

(

X

1

×

(

C

)

X

2

)

(

f

1

×

(

D

)

f

2

)