7.14. COMPLETION OF FUNCOIDS

175

Theorem

942

.

h

CoCompl

f

i

X

= Cor

h

f

i

X

for every funcoid

f

and typed

set

X

T

(Src

f

).

Proof.

CoCompl

f

v

f

thus

h

CoCompl

f

i

X

v h

f

i

X

but

h

CoCompl

f

i

X

is a principal filter thus

h

CoCompl

f

i

X

v

Cor

h

f

i

X

.

Let

αX

= Cor

h

f

i

X

. Then

α

T

(Src

f

)

=

F

(Dst

f

)

and

α

(

X

t

Y

) = Cor

h

f

i

(

X

t

Y

) = Cor(

h

f

i

X

t h

f

i

Y

) =

Cor

h

f

i

X

t

Cor

h

f

i

Y

=

αX

t

αY

(used theorem

603

). Thus

α

can be continued till

h

g

i

for some funcoid

g

. This

funcoid is co-complete.

Evidently

g

is the greatest co-complete element of

FCD

(Src

f,

Dst

f

) which is

lower than

f

.

Thus

g

= CoCompl

f

and Cor

h

f

i

X

=

αX

=

h

g

i

X

=

h

CoCompl

f

i

X

.

Theorem

943

.

ComplFCD

(

A, B

) is an atomistic lattice.

Proof.

Let

f

ComplFCD

(

A, B

),

X

T

(Src

f

).

h

f

i

X

=

l

x

atoms

X

h

f

i

x

=

l

x

atoms

X

h

f

|

x

i

x

=

l

x

atoms

X

h

f

|

x

i

X,

thus

f

=

d

x

atoms

X

(

f

|

x

). It is trivial that every

f

|

x

is a join of atoms of

ComplFCD

(

A, B

).

Theorem

944

.

A funcoid is complete iff it is a join (on the lattice

FCD

(

A, B

))

of atomic complete funcoids.

Proof.

It follows from the theorem

922

and the previous theorem.

Corollary

945

.

ComplFCD

(

A, B

) is join-closed.

Theorem

946

.

Compl

d

R

=

d

h

Compl

i

R

for every

R

P

FCD

(

A, B

) (for

every sets

A

,

B

).

Proof.

For every typed set

X

D

Compl

l

R

E

X

=

l

x

atoms

X

D

l

R

E

x

=

l

x

atoms

X

l

f

R

h

f

i

x

=

l

f

R

l

x

atoms

X

h

f

i

x

=

l

f

R

h

Compl

f

i

X

=

D

l

h

Compl

i

R

E

X.

Corollary

947

.

Conjecture

948

.

Compl is not an upper adjoint (in general).

Proposition

949

.

Compl

f

=

d

α

Src

f

(

f

|

↑{

α

}

) for every funcoid

f

.