background image

7.4. RESTRICTING RELOID TO A FILTER. DOMAIN AND IMAGE

139

Proof.

f

u

(

A ×

RLD

B

) =

f

u

(

A ×

RLD

>

F

(Dst

f

)

)

u

(

>

F

(Src

f

)

×

RLD

B

) =

f

|

A

u

(

>

F

(Src

f

)

×

RLD

B

) =

(

f

id

RLD

A

)

u

(

>

F

(Src

f

)

×

RLD

B

) =

((

f

id

RLD

A

)

1

u

(

>

F

(Src

f

)

×

RLD

B

)

1

)

1

=

((id

RLD

A

f

1

)

u

(

B ×

RLD

>

F

(Src

f

)

))

1

=

(id

RLD

A

f

id

RLD

B

)

1

=

id

RLD

B

f

id

RLD

A

.

Theorem

767

.

f

|

Src

f

{

α

}

=

Src

f

{

α

} ×

RLD

im(

f

|

Src

f

{

α

}

) for every reloid

f

and

α

Src

f

.

Proof.

First,

im(

f

|

Src

f

{

α

}

) =

l

Dst

f

h

im

i

GR(

f

|

Src

f

{

α

}

) =

l

Dst

f

h

im

i

GR(

f

u

(

Src

f

{

α

} × >

F

(Dst

f

)

)) =

l

Dst

f

im(

F

(

{

α

} ×

Dst

f

))

F

GR

f

=

l

(

Dst

f

im(

F

|

{

α

}

)

F

GR

f

)

.

Taking this into account we have:

Src

f

{

α

} ×

RLD

im(

f

|

Src

f

{

α

}

) =

l

RLD

(Src

f

;Dst

f

)

(

{

α

} ×

K

)

K

im(

f

|

Src

f

{

α

}

)

=

l

(

RLD

(Src

f

;Dst

f

)

(

{

α

} ×

im(

F

|

{

α

}

))

F

GR

f

)

=

l

(

RLD

(Src

f

;Dst

f

)

(

F

|

{

α

}

)

F

GR

f

)

=

l

RLD

(Src

f

;Dst

f

)

(

F

(

{

α

} ×

Dst

f

))

F

GR

f

=

l

RLD

(Src

f

;Dst

f

)

F

F

GR

f

u ↑

RLD

(Src

f

;Dst

f

)

(

{

α

} ×

Dst

f

) =

f

u ↑

RLD

(Src

f

;Dst

f

)

(

{

α

} ×

Dst

f

) =

f

|

Src

f

{

α

}

.

Lemma

768

.

λ

B ∈

F

(

B

) :

>

F

×

RLD

B

is an upper adjoint of

λf

RLD

(

A

;

B

) :

im

f

(for every sets

A

,

B

).

Proof.

We need to prove im

f

v B ⇔ >

F

×

RLD

B

what is obvious.