background image

15.12. COMPLETION AND CO-COMPLETION

222

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

1151

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices. Then

CoComplFCD

(

A

;

B

) (with induced order) is a complete lattice.

Proof.

Follows from the theorem

1149

.

Theorem

1152

.

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

(

F

R

) =

F

n

g

f

g

R

o

=

F

h

g

◦i

R

if

g

is a complete pointfree funcoid from

B

.

Proof.

For every

X

A

D

g

G

R

E

X

=

h

g

i

DG

R

E

X

=

h

g

i

G

h

f

i

X

f

R

=

G

h

g

ih

f

i

X

f

R

=

G

h

g

f

i

X

f

R

=

G

g

f

f

R

X

=

DG

h

g

◦i

R

E

X.

So

g

(

F

R

) =

F

h

g

◦i

R

.

15.12. Completion and co-completion

Definition

1153

.

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

FCD

(

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

1154

.

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

1082

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

423

.

Obvious

1155

.

Co-completion is always co-complete.

Proposition

1156

.

For above defined always CoCompl

f

v

f

.

Proof.

By proposition

368

.

Proposition

1157

.

Monovalued pointfree funcoids between sets of filters on

boolean lattices are metamonovalued.

FiXme

: Monovalued is defined below that used

here. Is there a similar error in “Funcoids” chapter?