background image

funcoidal reloids

(

RLD

)

in

(

FCD

)

funcoids

d

RLD

lters on

¡

f

7!

f

\

¡

up

¡

d

FCD

Proof.

First we need to show that

d

RLD

f

is a funcoidal reloid. But it follows from lemma

25

.

Next, we need to show that all morphisms depicted on the diagram are bijections and the

depicted opposite morphisms are mutually inverse.

That

(

FCD

)

and

(

RLD

)

in

are mutually inverse was proved above in the book.

That

d

RLD

and

f

7!

f

\

¡

are mutually inverse was proved above.

That

d

FCD

and up

¡

are mutually inverse was proved above.

It remains to prove that three-element cycles are identities. But this follows from lemma

25

.

That the morphisms preserve order and composition was proved above. That they preserve

reversal is obvious.

6 Some additional properties

Proposition 36.

For every funcoid

f

2

FCD

(

A

;

B

)

(for sets

A

,

B

):

1. dom

f

=

d

F

(

A

)

h

dom

i

up

¡(

A

;

B

)

f

;

2. im

f

=

d

F

(

A

)

h

im

i

up

¡(

A

;

B

)

f

.

Proof.

Take

f

X

Y

j

X

2

P

A; Y

2

P

A; X

Y

f

up

¡(

A

;

B

)

f

. I leave the rest reasoning as

an exercise.

Proposition 37.

(

RLD

)

¡

f

w

(

RLD

)

in

f

w

(

RLD

)

out

f

for every funcoid

f

.

Proof.

We already know that

(

RLD

)

in

f

w

(

RLD

)

out

f

(see above in the book).

The formula

(

RLD

)

¡

f

w

(

RLD

)

in

f

follows from

8

G

2

up

¡(

Src

f

;

Dst

f

)

f

:

G

w

f

.

Example 38.

(

RLD

)

¡

f

A

(

RLD

)

in

f

A

(

RLD

)

out

f

for some funcoid

f

.

Proof.

Take

f

= (=)

j

R

. We already know that

(

RLD

)

in

f

A

(

RLD

)

out

f

(see above in the book).

It remains to prove

(

RLD

)

¡

f

=

/ (

RLD

)

in

f

.

Take

F

=

S

i

2

Z

([

i

;

i

+ 1[

[

i

;

i

+ 1[)

.

Then

F

2

f

=

up

(

RLD

)

in

f

(because

h

F

i

a

w h

f

i

a

for both principal ultralter

a

=

f

i

g

and every

other ultralter

a

).

It remains to prove

F

2

/

up

(

RLD

)

¡

f

.

Some additional properties

7