background image

h

R

i

f

g

=

f

j

"

Src

f

f

g

f

g j

2

Src

f

 

=

h

f

i

f

g

for every

2

Src

f

and

R

is complete

as a join of complete funcoids.

Thus

R

is the completion of

f

.

Conjecture 6.132.

Compl

f

=

f

n

(

FCD

f

)

for every funcoid

f

.

This conjecture may be proved by considerations similar to these in the section Fréchet lter.

Lemma 6.133.

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

F

fh

f

i

f

x

g j

x

2

X

g

=

F

f

Cor

h

f

i

f

x

g j

x

2

X

g

=

F

fh

CoCompl

f

i

f

x

g j

x

2

X

g

for every set

X

. Thus CoCompl

f

is complete.

Theorem 6.134.

Compl CoCompl

f

=

CoCompl Compl

f

=

Cor

f

for every funcoid

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 fun-

coid under

f

and Compl CoCompl

f

is the greatest complete funcoid under CoCompl

f

. So

Compl CoCompl

f

is greater than any principal funcoid under CoCompl

f

which is greater than

any principal funcoid under

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 6.135.

Is Compl

FCD

(

A

;

B

)

a co-brouwerian lattice for every sets

A

,

B

?

[TODO: Solved.]

6.13.1 More on completion of funcoids

Proposition 6.136.

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 6.137.

For every composable funcoids

f

and

g

[TODO: Errors in this theorem,

corrected in the LyX version of this text.]

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.

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

for every

X

.

2.

(

CoCompl

(

g

f

))

¡

1

=

f

¡

1

(

CoCompl

g

)

¡

1

; Compl

(

g

f

)

¡

1

=

f

¡

1

Compl

g

¡

1

;

Compl

(

f

¡

1

g

¡

1

) =

f

¡

1

Compl

g

¡

1

. After variable replacement we get Compl

(

f

g

) =

f

Compl

g

(after the replacement

f

is a complete funcoid).

Corollary 6.138.

CoCompl

((

Compl

g

)

f

) =

Compl

(

g

(

CoCompl

f

)) = (

Compl

g

)

(

CoCompl

f

)

.

Proof.

By the theorem:

Compl

(

g

(

CoCompl

f

)) = (

Compl

g

)

(

CoCompl

f

)

;

CoCompl

((

Compl

f

)

g

) = (

Compl

f

)

(

CoCompl

g

)

.

After variable replacement CoCompl

((

Compl

g

)

f

) = (

Compl

g

)

(

CoCompl

f

)

.

116

Funcoids