7.7. COMPLETE RELOIDS AND COMPLETION OF RELOIDS

142

Obvious

779

.

Principal reloids are complete and co-complete.

Obvious

780

.

Join (on the lattice of reloids) of complete reloids is complete.

Corollary

781

.

ComplRLD

(with the induced order) is a complete lattice.

Theorem

782

.

A reloid which is both complete and co-complete is principal.

Proof.

Let

f

be a complete and co-complete reloid. We have

f

=

G

Src

f

{

α

} ×

RLD

G

(

α

)

α

Src

f

and

f

=

G

H

(

β

)

×

RLD

Dst

f

{

β

}

β

Dst

f

for some functions

G

: Src

f

F

(Dst

f

) and

H

: Dst

f

F

(Src

f

). For every

α

Src

f

we have

G

(

α

) =

im

f

|

Src

f

{

α

}

=

im(

f

u

(

Src

f

{

α

} ×

RLD

>

F

(Dst

f

)

)) = (*)

im

G

(

H

(

β

)

×

RLD

Dst

f

{

β

}

)

u

(

Src

f

{

α

} ×

RLD

>

F

(Dst

f

)

)

β

Dst

f

=

im

G

(

H

(

β

)

u ↑

Src

f

{

α

}

)

×

RLD

Dst

f

{

β

}

β

Dst

f

=

im

G

(

Src

f

{

α

RLD

Dst

f

{

β

}

if

H

(

β

)

6↑

Src

f

{

α

}

RLD

(Src

f

;Dst

f

)

if

H

(

β

)

Src

f

{

α

}

!

β

Dst

f

=

im

G

Src

f

{

α

RLD

Dst

f

{

β

}

β

Dst

f, H

(

β

)

6↑

Src

f

{

α

}

=

im

G

RLD

(Src

f

;Dst

f

)

{

(

α

;

β

)

}

β

Dst

f, H

(

β

)

6↑

Src

f

{

α

}

=

G

Dst

f

{

β

}

β

Dst

f, H

(

β

)

6↑

Src

f

{

α

}

* proposition (

461

was used.

Thus

G

(

α

) is a principal filter that is

G

(

α

) =

Dst

f

g

(

α

) for some

g

: Src

f

Dst

f

;

Src

f

{

α

} ×

RLD

G

(

α

) =

RLD

(Src

f

;Dst

f

)

(

{

α

} ×

g

(

α

));

f

is principal as a join

of principal reloids.

Conjecture

783

.

Composition of complete reloids is complete.

FiXme

: Solved.

Theorem

784

.

1

. For a complete reloid

f

there exists exactly one function

F

F

(Dst

f

)

Src

f

such that

f

=

G

Src

f

{

α

} ×

RLD

F

(

α

)

α

Src

f

.

2

. For a co-complete reloid

f

there exists exactly one function

F

F

(Src

f

)

Dst

f

such that

f

=

G

F

(

α

)

×

RLD

Dst

f

{

α

}

α

Dst

f

.