 8.7. COMPLETE RELOIDS AND COMPLETION OF RELOIDS

193

Denote

f

=

d

n

A

{

α

RLD

G

(

α

)

α

A

o

. Then

im(

f

|

↑{

α

0

}

) = im(

f

u

(

A

{

α

0

} × >

T

(

B

)

)) =

(because

A

{

α

0

} × >

T

(

B

)

is principal) =

im

l

(

A

{

α

} ×

RLD

G

(

α

))

u

(

A

{

α

0

} × >

T

(

B

)

)

α

Src

f

=

im(

A

{

α

0

} ×

RLD

G

(

α

0

)) =

G

(

α

0

)

.

Corollary

1043

.

G

7→

d

n

G

(

α

)

×

RLD

A

{

α

}

α

A

o

is an order isomorphism from the

set of functions

G

F

(

B

)

A

to the set

CoComplRLD

(

A, B

).

The inverse isomorphism is described by the formula

G

(

α

) = im(

f

1

|

↑{

α

}

)

where

f

is a co-complete reloid.

Corollary

1044

.

ComplRLD

(

A, B

) and

ComplFCD

(

A, B

) are a co-frames.

Obvious

1045

.

Complete and co-complete reloids are convex.

Obvious

1046

.

Principal reloids are complete and co-complete.

Obvious

1047

.

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

Theorem

1048

.

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

Proof.

Let

f

be a complete and co-complete reloid. We have

f

=

l

Src

f

{

α

} ×

RLD

G

(

α

)

α

Src

f

and

f

=

l

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

|

↑{

α

}

=

im(

f

u

(

Src

f

{

α

} ×

RLD

>

F

(Dst

f

)

)) = (*)

im

l

(

H

(

β

)

×

RLD

Dst

f

{

β

}

)

u

(

Src

f

{

α

} ×

RLD

>

F

(Dst

f

)

)

β

Dst

f

=

im

l

(

H

(

β

)

u ↑

Src

f

{

α

}

)

×

RLD

Dst

f

{

β

}

β

Dst

f

=

im

l

(

Src

f

{

α

RLD

Dst

f

{

β

}

if

H

(

β

)

6↑

Src

f

{

α

}

RLD

(Src

f,

Dst

f

)

if

H

(

β

)

Src

f

{

α

}

!

β

Dst

f

=

im

l

Src

f

{

α

RLD

Dst

f

{

β

}

β

Dst

f, H

(

β

)

6↑

Src

f

{

α

}

=

im

l

RLD

(Src

f,

Dst

f

)

{

(

α, β

)

}

β

Dst

f, H

(

β

)

6↑

Src

f

{

α

}

=

l

Dst

f

{

β

}

β

Dst

f, H

(

β

)

6↑

Src

f

{

α

}

* theorem

610

was used.