Proposition 6.122.

The ltrator

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

is ltered.

Proof.

Because the ltrator of funcoids is ltered.

Theorem 6.123.

Compl

f

=

Cor

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

f

=

Cor

0

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

f

for

every funcoid

f

2

FCD

(

A

;

B

)

.

Proof.

Cor

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

f

=

Cor

0

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

f

using theorem

4.34

since the

ltrator

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

is ltered.

Let

g

2

up

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

f

. Then

g

2

Compl

FCD

(

A

;

B

)

and

g

w

f

. Thus

g

=

Compl

g

w

Compl

f

.

Thus

8

g

2

up

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

f

:

g

w

Compl

f

.

Let

8

g

2

up

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

f

:

h

v

g

for some

h

2

Compl

FCD

(

A

;

B

)

.

Then

h

v

d

up

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

f

=

f

and consequently

h

=

Compl

h

v

Compl

f

.

Thus

Compl

f

=

l

Compl

FCD

(

A

;

B

)

up

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

f

=

Cor

(

FCD

(

A

;

B

);

Compl

FCD

(

A

;

B

))

f :

Theorem 6.124.

h

CoCompl

f

i

X

=

Cor

h

f

i

X

for every funcoid

f

and set

X

2

P

(

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 lter

thus

h

CoCompl

f

i

X

v

Cor

h

f

i

X

.

Let

X

=

Cor

h

f

i

X

. Then

;

= 0

F

(

Dst

f

)

and

(

X

[

Y

) =

Cor

h

f

i

(

X

[

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

4.223

). 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 6.125.

Compl

FCD

(

A

;

B

)

is an atomistic lattice.

Proof.

Let

f

2

Compl

FCD

(

A

;

B

)

.

h

f

i

X

=

F

fh

f

i

f

x

g j

x

2

X

g

=

f

j

"

Src

f

f

x

g

f

x

g j

x

2

X

=

f

j

"

Src

f

f

x

g

X

j

x

2

X

, thus

f

=

f

j

"

Src

f

f

x

g

j

x

2

X

. It is trivial that every

f

j

"

Src

f

f

x

g

is a join of atoms of Compl

FCD

(

A

;

B

)

.

Theorem 6.126.

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

FCD

(

A

;

B

)

) of atomic complete

funcoids.

Proof.

It follows from the theorem

6.106

and the previous theorem.

Corollary 6.127.

Compl

FCD

(

A

;

B

)

is join-closed.

Theorem 6.128.

Compl

F

R

=

F

h

Compl

i

R

for every

R

2

P

FCD

(

A

;

B

)

(for every sets

A

,

B

).

Proof.

h

Compl

F

R

i

X

=

F

fh

F

R

i

f

g j

2

X

g

=

F

f

F

fh

f

i

f

g j

f

2

R

g j

2

X

g

=

F

f

F

fh

f

i

f

g j

2

X

g j

f

2

R

g

=

F

fh

Compl

f

i

X

j

f

2

R

g

=

h

F

h

Compl

i

R

i

X

for every set

X

.

Corollary 6.129.

Conjecture 6.130.

Compl is not an upper adjoint (in general).

Proposition 6.131.

Compl

f

=

f

j

"

Src

f

f

g

j

2

Src

f

for every funcoid

f

.

Proof.

Let denote

R

the right part of the equality to prove.

6.13 Completion of funcoids

115