background image

16.5. THE DIAGRAM

264

Proof.

Let

a

be an an atomic filter object. We need to prove

h

(

FCD

)

f

i

a

=

*

FCD

l

(Γ(

A, B

)

GR

f

)

+

a

that is

*

FCD

l

up

f

+

a

=

*

FCD

l

(Γ(

A, B

)

GR

f

)

+

a

that is

F

l

F

up

f

h

F

i

a

=

F

l

F

Γ(

A,B

)

up

f

h

F

i

a.

For this it’s enough to prove that

Y

up

h

F

i

a

for some

F

up

f

implies

Y

up

h

F

0

i

a

for some

F

0

Γ(

A, B

)

GR

f

.

Let

Y

up

h

F

i

a

. Then (proposition above) there exists

A

up

a

such that

Y

up

h

F

i

A

.

Y

up

A

×

FCD

Y

t

A

×

FCD

>

a

;

A

×

FCD

Y

t

A

×

FCD

>

X

=

Y

up

h

F

iX

if

⊥ 6

=

X v

A

and

A

×

FCD

Y

t

A

×

FCD

>

X

=

> ∈

up

h

F

iX

if

X 6v

A

.

Thus

A

×

FCD

Y

t

A

×

FCD

> w

F

. So

A

×

FCD

Y

t

A

×

FCD

>

is the sought

for

F

0

.

16.5. The diagram

Theorem

1396

.

The diagram at the figure

1

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, composition, and reversal (

f

7→

f

1

).

Figure 1.

funcoids

funcoidal reloids

filters on Γ

up

Γ

(

RLD

)

in

(

FCD

)

f

7→

f

Γ

d

FCD

d

RLD

Proof.

First we need to show that

d

RLD

f

is a funcoidal reloid. But it follows

from lemma

1389

.

Next, we need to show that all morphisms depicted on the diagram are bijec-

tions 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.

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

they preserve reversal is obvious.

So it remains to apply lemma

193

(taking into account lemma

1389

).

Another proof that (

FCD

)(

RLD

)

in

f

=

f

for every funcoid

f

: