 7.14. COMPLETION OF FUNCOIDS

176

Proof.

Let denote

R

the right part of the equality to prove.

h

R

i

@

{

β

}

=

d

α

Src

f

f

|

↑{

α

}

@

{

β

}

=

h

f

i

@

{

β

}

for every

β

Src

f

and

R

is

complete as a join of complete funcoids.

Thus

R

is the completion of

f

.

Conjecture

947

.

Compl

f

=

f

\

(Ω

×

FCD

f

).

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

“Fréchet filter”.

Lemma

948

.

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

l

x

atoms

X

h

f

i

x

=

l

x

atoms

X

Cor

h

f

i

x

=

l

x

atoms

X

h

CoCompl

f

i

x

for every set typed

X

T

(Src

f

). Thus CoCompl

f

is complete.

Theorem

949

.

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

.

7.14.1. More on completion of funcoids.

Proposition

950

.

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

951

.

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.

Proof.

1

For every

X

T

(Src

f

)

h

CoCompl(

g

f

)

i

X

=

Cor

h

g

f

i

X

=

Cor

h

g

ih

f

i

X

=

h

CoCompl

g

ih

f

i

X

=

h

(CoCompl

g

)

f

i

X.