 6.13. COMPLETION OF FUNCOIDS

127

Conjecture

697

.

Compl is not an upper adjoint (in general).

Proposition

698

.

Compl

f

=

F

n

f

|

Src

f

{

α

}

α

Src

f

o

for every funcoid

f

.

Proof.

Let denote

R

the right part of the equality to prove.

h

R

i

{

β

}

=

F

f

|

Src

f

{

α

}

{

β

}

α

Src

f

=

h

f

i

{

β

}

for every

β

Src

f

and

R

is com-

plete as a join of complete funcoids.

Thus

R

is the completion of

f

.

Conjecture

699

.

Compl

f

=

f

\

(Ω

×

FCD

f

).

This conjecture may be proved by considerations similar to these in the section

“Fréchet filter”.

Lemma

700

.

Co-completion of a complete funcoid is complete.

Proof.

Let

f

be a complete funcoid.

h

CoCompl

f

i

X

= Cor

h

f

i

X

=

Cor

G

h

f

i

{

x

}

x

X

=

G

Cor

h

f

i

{

x

}

x

X

=

G

h

CoCompl

f

i

{

x

}

x

X

for every set

X

. Thus CoCompl

f

is complete.

Theorem

701

.

Compl CoCompl

f

= CoCompl Compl

f

= Cor

f

for every fun-

coid

f

.

Proof.

Compl CoCompl

f

is co-complete since (used the lemma) CoCompl

f

is co-complete. Thus Compl CoCompl

f

is a principal funcoid. CoCompl

f

is the

greatest co-complete funcoid under

f

and Compl CoCompl

f

is the greatest com-

plete funcoid under CoCompl

f

. So Compl CoCompl

f

is greater than any prin-

cipal funcoid under CoCompl

f

which is greater than any principal funcoid un-

der

f

. Thus Compl CoCompl

f

is the greatest principal funcoid under

f

. Thus

Compl CoCompl

f

= Cor

f

. Similarly CoCompl Compl

f

= Cor

f

.

Question

702

.

FiXme

: Solved.

Is

ComplFCD

(

A

;

B

) a co-brouwerian lattice for

every sets

A

,

B

?

6.13.1. More on completion of funcoids.

Proposition

703

.

For every composable funcoids

f

and

g

1

. Compl(

g

f

)

w

Compl

g

Compl

f

;

2

. CoCompl(

g

f

)

w

CoCompl

g

CoCompl

f

.

Proof.

1

Compl

g

Compl

f

= Compl(Compl

g

Compl

f

)

v

Compl(

g

f

).

2

CoCompl

g

CoCompl

f

= CoCompl(CoCompl

g

CoCompl

f

)

v

CoCompl(

g

f

).

Proposition

704

.

For every composable funcoids

f

and

g

1

. CoCompl(

g

f

) = (CoCompl

g

)

f

if

f

is a co-complete funcoid.

2

. Compl(

f

g

) =

f

Compl

g

if

f

is a complete funcoid.