Obvious 7.49.

Principal reloids are complete and co-complete.

Obvious 7.50.

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

Corollary 7.51.

Compl

RLD

(with the induced order) is a complete lattice.

Theorem 7.52.

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

f"

Src

f

f

RLD

G

(

)

j

2

Src

f

g

and

f

=

G

f

H

(

)

RLD

"

Dst

f

f

g j

2

Dst

f

g

for some functions

G

:

Src

f

!

F

(

Dst

f

)

and

H

:

Dst

f

!

F

(

Src

f

)

. For every

2

Src

f

we have

G

(

) =

im

f

j

"

Src

f

f

g

=

im

¡

f

u

¡

"

Src

f

f

RLD

1

F

(

Dst

f

)

=

(*)

im

(

H

(

)

RLD

"

Dst

f

f

g

)

u

¡

"

Src

f

f

RLD

1

F

(

Dst

f

)

j

2

Dst

f

=

im

G

f

(

H

(

)

u "

Src

f

f

g

)

RLD

"

Dst

f

f

g j

2

Dst

f

g

=

im

G

( (

"

Src

f

f

RLD

"

Dst

f

f

g

if

H

(

)

/

"

Src

f

f

g

0

RLD

(

Src

f

;

Dst

f

)

if

H

(

)

"

Src

f

f

g

!

j

2

Dst

f

)

=

im

G

f"

Src

f

f

RLD

"

Dst

f

f

g j

2

Dst

f ; H

(

)

/

"

Src

f

f

gg

=

im

"

RLD

(

Src

f

;

Dst

f

)

f

(

;

)

g j

2

Dst

f ; H

(

)

/

"

Src

f

f

g

=

G

f"

Dst

f

f

g j

2

Dst

f ; H

(

)

/

"

Src

f

f

gg

* proposition

4.194

was used.

Thus

G

(

)

is a principal lter that is

G

(

) =

"

Dst

f

g

(

)

for some

g

:

Src

f

!

Dst

f

;

"

Src

f

f

RLD

G

(

) =

"

RLD

(

Src

f

;

Dst

f

)

(

f

g

(

))

;

f

is principal as a join of principal reloids.

Conjecture 7.53.

Composition of complete reloids is complete.

[TODO: Solved.]

Theorem 7.54.

1. For a complete reloid

f

there exists exactly one function

F

2

F

(

Dst

f

)

Src

f

such that

f

=

G

f"

Src

f

f

RLD

F

(

)

j

2

Src

f

g

:

2. For a co-complete reloid

f

there exists exactly one function

F

2

F

(

Src

f

)

Dst

f

such that

f

=

G

f

F

(

)

RLD

"

Dst

f

f

g j

2

Dst

f

g

:

Proof.

We will prove only the rst as the second is similar. Let

f

=

G

f"

Src

f

f

RLD

F

(

)

j

2

Src

f

g

=

G

f"

Src

f

f

RLD

G

(

)

j

2

Src

f

g

for some

F ; G

2

F

(

Dst

f

)

Src

f

. We need to prove

F

=

G

. Let

2

Src

f

.

f

u

¡

"

Src

f

f

RLD

1

F

(

Dst

f

)

=

(proposition

4.194

)

(

"

Src

f

f

RLD

F

(

))

u

¡

"

Src

f

f

RLD

1

F

(

Dst

f

)

j

2

Src

f

=

"

Src

f

f

RLD

F

(

)

:

Similarly

f

u

¡

"

Src

f

f

RLD

1

F

(

Dst

f

)

=

"

Src

f

f

RLD

G

(

)

. Thus

"

Src

f

f

RLD

F

(

) =

"

Src

f

f

RLD

G

(

)

and so

F

(

) =

G

(

)

.

Denition 7.55.

Completion

and

co-completion

of a reloid

f

2

RLD

(

A

;

B

)

are dened by the

formulas:

Compl

f

=

Cor

(

RLD

(

A

;

B

);

Compl

RLD

(

A

;

B

))

f

;

CoCompl

f

=

Cor

(

RLD

(

A

;

B

);

CoCompl

RLD

(

A

;

B

))

f :

128

Reloids