 19.12. COMPLETION AND CO-COMPLETION

305

Proposition

1581

.

1

. Let

f

ComplpFCD

(

A

,

B

) and

g

ComplpFCD

(

B

,

C

) where

A

and

C

are

posets with least elements and

B

is a complete lattice. Then

g

f

ComplpFCD

(

A

,

C

).

2

. Let

f

CoComplpFCD

(

A

,

B

) and

g

CoComplpFCD

(

B

,

C

) where (

A

,

Z

0

),

(

B

,

Z

1

), (

C

,

Z

2

) are filtrators. Then

g

f

CoComplpFCD

(

A

,

C

).

Proof.

1

Let

d

S

and

d

hh

g

f

ii

S

be defined. Then

h

g

f

i

l

S

=

h

g

ih

f

i

l

S

=

h

g

i

l

hh

f

ii

S

=

l

hh

g

ii

hh

f

ii

S

=

l

hh

g

f

ii

S.

2

.

h

g

f

i

Z

0

=

h

g

ih

f

i

Z

0

Z

2

because

h

f

i

Z

0

Z

1

.

Proposition

1582

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices. Then

CoComplpFCD

(

A

,

B

) (with induced order) is a complete lattice.

Proof.

Follows from the theorem

1580

.

Theorem

1583

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators where

Z

0

and

Z

1

are boolean lattices. Let

R

be a set of pointfree funcoids from

A

to

B

.

g

(

d

R

) =

d

g

R

(

g

f

) =

d

h

g

◦i

R

if

g

is a complete pointfree funcoid from

B

.

Proof.

For every

X

A

D

g

l

R

E

X

=

h

g

i

D

l

R

E

X

=

h

g

i

l

f

R

h

f

i

X

=

l

f

R

h

g

ih

f

i

X

=

l

f

R

h

g

f

i

X

=

*

l

f

R

(

g

f

)

+

X

=

D

l

h

g

◦i

R

E

X.

So

g

(

d

R

) =

d

h

g

◦i

R

.

19.12. Completion and co-completion

Definition

1584

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices and

Z

1

is a complete atomistic lattice.

Co-completion

of a pointfree funcoid

f

pFCD

(

A

,

B

) is pointfree funcoid

CoCompl

f

defined by the formula (for every

X

Z

0

)

h

CoCompl

f

i

X

= Cor

h

f

i

X.

Proposition

1585

.

Above defined co-completion always exists.

Proof.

Existence of Cor

h

f

i

X

follows from completeness of

Z

1

.

We may apply the theorem

1510

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 theorem

600

.