 Proof.

Let

R

be a set of co-complete pointfree funcoids. Then for every

X

2

Z

0

G

R

X

=

G

B

fh

f

i

X

j

f

2

R

g

=

G

Z

1

fh

f

i

X

j

f

2

R

g 2

Z

1

(used the theorem

15.33

and corollary

4.96

).

Let

A

and

B

be posets with least elements. I will denote Compl

FCD

(

A

;

B

)

and CoCompl

FCD

(

A

;

B

)

the sets of complete and co-complete funcoids correspondingly from a poset

A

to a poset

B

.

Proposition 15.94.

1. Let

f

2

Compl

FCD

(

A

;

B

)

and

g

2

Compl

FCD

(

B

;

C

)

where

A

and

C

are posets with least

elements and

B

is a complete lattice. Then

g

f

2

Compl

FCD

(

A

;

C

)

.

2. Let

f

2

CoCompl

FCD

(

A

;

B

)

and

g

2

CoCompl

FCD

(

B

;

C

)

where

A

,

B

and

C

are posets with

least elements and

(

A

;

Z

0

)

,

(

B

;

Z

1

)

,

(

C

;

Z

2

)

are ltrators. Then

g

f

2

CoCompl

FCD

(

A

;

C

)

.

Proof.

1. Let

F

S

and

F

hh

g

f

ii

S

be dened. Then

[FIXME: Is

F

hh

f

ii

S

dened?]

h

g

f

i

G

S

=

h

g

ih

f

i

G

S

=

h

g

i

G

hh

f

ii

S

=

G

hh

g

iihh

f

ii

S

=

G

hh

g

f

ii

S:

2.

h

g

f

i

Z

0

=

h

g

ih

f

i

Z

0

2

Z

2

because

h

f

i

Z

0

2

Z

1

.

Proposition 15.95.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over boolean lattices. Then

CoCompl

FCD

(

A

;

B

)

(with induced order) is a complete lattice.

Proof.

Follows from the theorem

15.93

.

Theorem 15.96.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators where

Z

0

and

Z

1

are boolean lattices.

Let

R

be a set of pointfree funcoids from

A

to

B

.

g

(

F

R

) =

F

f

g

f

j

g

2

R

g

=

F

h

g

i

R

if

g

is a complete pointfree funcoid from

B

.

Proof.

h

g

(

F

R

)

i

X

=

h

g

ih

F

R

i

X

=

h

g

i

F

fh

f

i

X

j

f

2

R

g

=

F

fh

g

ih

f

i

X

j

f

2

R

g

=

F

fh

g

f

i

X

j

f

2

R

g

=

h

F

f

g

f

j

f

2

R

gi

X

=

h

F

h

g

i

R

i

X

for every

X

2

A

. So

g

(

F

R

) =

F

h

g

i

R

.

15.12 Completion and co-completion

Denition 15.97.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over boolean lattices and

Z

1

is a

complete atomistic lattice.

Co-completion

of a pointfree funcoid

f

2

FCD

(

A

;

B

)

is pointfree funcoid CoCompl

f

dened

by the formula (for every

X

2

Z

0

)

h

CoCompl

f

i

X

=

Cor

h

f

i

X:

Proposition 15.98.

Above dened co-completion always exists.

Proof.

Existence of Cor

h

f

i

X

follows from completeness of

Z

1

.

We may apply the theorem

15.26

because

Cor

h

f

i

(

X

t

Z

0

Y

) =

Cor

(

h

f

i

X

t

B

h

f

i

Y

) =

Cor

h

f

i

X

t

Z

1

Cor

h

f

i

Y

by proposition

4.156

.

Obvious 15.99.

Co-completion is always co-complete.

Proposition 15.100.

For above dened always CoCompl

f

v

f

.

Proof.

By proposition

4.101

.

194

Pointfree funcoids