background image

9.5. COMPLETE FUNCOIDS AND RELOIDS

210

Proof.

Really,

g

=

d

x

Src

f

(

Src

f

{

x

} ×

RLD

h

f

i

@

{

x

}

) for a complete reloid

g

and thus
(

FCD

)

g

=

l

x

Src

f

(

FCD

)(

Src

f

{

x

RLD

h

f

i

@

{

x

}

) =

l

x

Src

f

(

Src

f

{

x

FCD

h

f

i

@

{

x

}

) =

θg.

Lemma

1121

.

(

RLD

)

out

f

=

θ

1

f

for every complete funcoid

f

.

Proof.

We have

f

=

d

x

Src

f

(

Src

f

{

x

} ×

FCD

h

f

i

@

{

x

}

). We need to prove

(

RLD

)

out

f

=

d

x

Src

f

(

Src

f

{

x

} ×

RLD

h

f

i

@

{

x

}

).

Really, (

RLD

)

out

f

w

d

x

Src

f

(

Src

f

{

x

} ×

RLD

h

f

i

@

{

x

}

).

It remains to prove that

d

x

Src

f

(

Src

f

{

x

} ×

RLD

h

f

i

@

{

x

}

)

w

(

RLD

)

out

f

.

Let

L

up

d

x

Src

f

(

Src

f

{

x

} ×

RLD

h

f

i

@

{

x

}

).

We will prove

L

up(

RLD

)

out

f

.

We have

L

\

x

Src

f

up(

Src

f

{

x

} ×

RLD

h

f

i

@

{

x

}

)

.

h

L

i

{

x

}

=

G

(

x

) for some

G

(

x

)

up

h

f

i

@

{

x

}

(because

L

up(

Src

f

{

x

} ×

RLD

h

f

i

@

{

x

}

).

Thus

L

=

G

up

f

(because

f

is complete). Thus

L

up

f

and so

L

up(

RLD

)

out

f

.

Proposition

1122

.

(

FCD

) and (

RLD

)

out

form mutually inverse bijections be-

tween complete reloids and complete funcoids.

Proof.

From two last lemmas.

Theorem

1123

.

The diagram at the figure

1

(with the “unnamed” arrow from

ComplRLD

(

A, B

) to

F

(

B

)

A

defined

as the inverse isomorphism of its opposite ar-

row) is a commutative diagram (in category

Set

), every arrow in this diagram is

an isomorphism. Every cycle in this diagram is an identity (therefore “parallel”

arrows are mutually inverse). The arrows preserve order.

Figure 1.

F

(

B

)

A

ComplFCD

(

A, B

)

ComplRLD

(

A, B

)

G

7→

d

n

{

α

RLD

G

(

α

)

α

A

o

G

7→

d

n

{

α

FCD

G

(

α

)

α

A

o

f

7→

(

α

7→h

f

i

{

α

}

)

(

RLD

)

out

(

FCD

)