 Proof.

For every

y

2

Dst

f

we have

y

/

h

f

i

(

x

u

dom

f

)

,

x

u

dom

f

u h

f

¡

1

i

y

=

/ 0

Src

f

,

x

u

im

f

¡

1

u h

f

¡

1

i

y

=

/ 0

Src

f

,

x

u h

f

¡

1

i

y

=

/ 0

Src

f

,

y

/

h

f

i

x

. Thus

h

f

i

x

=

h

f

i

(

x

u

dom

f

)

by

separability of Dst

f

.

Proposition 15.50.

x

/

dom

f

,

(

h

f

i

x

is not least

)

for every pointfree funcoid

f

and

x

2

Src

f

if Dst

f

has greatest element

1

and Src

f

is a separable poset.

Proof.

x

/

dom

f

,

x

/

h

f

¡

1

i

1

Dst

f

,

1

Dst

f

/

h

f

i

x

,

(

h

f

i

x

is not least

)

.

Corollary 15.51.

dom

f

=

F

f

a

2

atoms

Src

f

j h

f

i

a

=

/ 0

Dst

f

g

for every pointfree funcoid

f

whose

destination is a bounded poset and source is a separable atomistic meet-semilattice.

Proof.

For every

a

2

atoms

Src

f

we have

a

/

dom

f

,

a

/

h

f

¡

1

i

1

Dst

f

,

1

Dst

f

/

h

f

i

a

,h

f

i

a

=

/ 0

Dst

f

.

So

dom

f

=

F

f

a

2

atoms

Src

f

j

a

/

dom

f

g

=

F

f

a

2

atoms

Src

f

j h

f

i

a

=

/ 0

Dst

f

g

.

Proposition 15.52.

dom

(

f

j

a

) =

a

u

dom

f

for every pointfree funcoid

f

and

a

2

Src

f

where Src

f

is a separable meet-semilattice and Dst

f

has greatest element.

Proof.

dom

(

f

j

a

) =

im

id

a

FCD

(

Src

f

)

f

¡

1

=

D

id

a

FCD

(

Src

f

)

E

h

f

¡

1

i

1

Dst

f

=

a

u h

f

¡

1

i

1

Dst

f

=

a

u

dom

f

.

Proposition 15.53.

For every composable pointfree funcoids

f

and

g

where the posets Src

f

and

Dst

f

=

Src

g

have greatest elements and Dst

f

and Dst

g

are separable:

1. If im

f

w

dom

g

then im

(

g

f

) =

im

g

.

2. If im

f

v

dom

g

then dom

(

g

f

) =

dom

g

.

Proof.

1. im

(

g

f

) =

h

g

f

i

1

Src

f

=

h

g

ih

f

i

1

Src

f

=

h

g

i

im

f

=

h

g

i

dom

g

=

h

g

i

1

Src

g

=

im

g

.

2. dom

(

g

f

) =

im

(

f

¡

1

g

¡

1

)

what by the proved is equal to im

f

¡

1

that is dom

f

.

15.6 Category of pointfree funcoids

I will dene the category

p

FCD

of pointfree funcoids:

The class of objects are small posets.

The set of morphisms from

A

to

B

is

FCD

(

A

;

B

)

.

The composition is the composition of pointfree funcoids.

Identity morphism for an object

A

is

(

A

;

A

;

id

A

;

id

A

)

.

To prove that it is really a category is trivial.

The

category of pointfree funcoid triples

is dened as follows:

Objects are pairs

(

A

;

A

)

where

A

is a small poset and

A 2

A

.

The morphisms from an object

(

A

;

A

)

to an object

(

B

;

B

)

are tuples

(

A

;

B

;

A

;

B

;

f

)

where

f

2

FCD

(

A

;

B

)

and dom

f

v A ^

im

f

v B

.

[FIXME: Domain and image are not always

dened. Even if it's dened, the composition law may not hold. We can require instead

f

v A

FCD

B

, but this is dened only for posets with least elements.]

The composition is dened by the formula

(

B

;

C

;

g

)

(

A

;

B

;

f

) = (

A

;

C

;

g

f

)

.

Identity morphism for an object

(

A

;

A

)

is id

A

FCD

(

A

)

.

[FIXME: Dened only for meet-semi-

lattices. We can also dene a wider precategory without identity.]

To prove that it is really a category is trivial.

184

Pointfree funcoids