background image

Theorem 7.32.

id

A

RLD

=

d

"

RLD

(

Base

(

A

);

Base

(

A

))

id

A

j

A

2 A

 

for every lter

A

.

Proof.

Let

K

2

GR

d

"

RLD

(

Base

(

A

);

Base

(

A

))

id

A

j

A

2 A

 

, then there exists

A

2 A

such that

K

id

A

. Then

id

A

RLD

v "

RLD

(

Base

(

A

);

Base

(

A

))

id

Base

(

A

)

u

¡

RLD

1

F

(

Base

(

A

))

v "

RLD

(

Base

(

A

);

Base

(

A

))

id

Base

(

A

)

u

¡

"

Base

(

A

)

A

RLD

1

F

(

Base

(

A

))

=

"

RLD

(

Base

(

A

);

Base

(

A

))

id

Base

(

A

)

u "

RLD

(

Base

(

A

);

Base

(

A

))

(

A

Base

(

A

)) =

"

RLD

(

Base

(

A

);

Base

(

A

))

(

id

Base

(

A

)

\

(

A

Base

(

A

))) =

"

RLD

(

Base

(

A

);

Base

(

A

))

id

A

v "

RLD

(

Base

(

A

);

Base

(

A

))

K

.

Thus

K

2

GR id

A

RLD

.

Reversely let

K

2

GR id

A

RLD

=

GR

¡

id

RLD

(

Base

(

A

))

u

¡

RLD

1

F

(

Base

(

A

))

, then there exists

A

2 A

such that

K

2

GR

"

RLD

(

Base

(

A

);

Base

(

A

))

(

id

Base

(

A

)

\

(

A

Base

(

A

))) =

GR

"

RLD

(

Base

(

A

);

Base

(

A

))

id

A

w

GR

d

"

RLD

(

Base

(

A

);

Base

(

A

))

id

A

j

A

2 A

 

.

Corollary 7.33.

(

id

A

RLD

)

¡

1

=

id

A

RLD

.

Theorem 7.34.

f

j

A

=

f

id

A

RLD

for every reloid

f

and

A 2

F

(

Src

f

)

.

Proof.

We need to prove that

f

u

¡

RLD

1

F

(

Dst

f

)

=

f

d

"

RLD

(

Src

f

;

Src

f

)

id

A

j

A

2 A

 

.

We have

f

d

"

RLD

(

Src

f

;

Src

f

)

id

A

j

A

2 A

 

=

d

"

RLD

(

Src

f

;

Dst

f

)

(

F

id

A

)

j

F

2

GR

f ; A

2 A

 

=

d

"

RLD

(

Src

f

;

Dst

f

)

(

F

j

A

)

j

F

2

GR

f ; A

2 A

 

=

d

"

RLD

(

Src

f

;

Dst

f

)

(

F

\

(

A

Dst

f

))

j

F

2

GR

f ;

A

2 A

 

=

d

"

RLD

(

Src

f

;

Dst

f

)

F

j

F

2

GR

f

 

u

d

"

RLD

(

Src

f

;

Dst

f

)

(

A

Dst

f

)

j

A

2 A

 

=

f

u

¡

RLD

1

F

(

Dst

f

)

.

Theorem 7.35.

(

g

f

)

j

A

=

g

(

f

j

A

)

for every composable reloids

f

and

g

and

A 2

F

(

Src

f

)

.

Proof.

(

g

f

)

j

A

=(

g

f

)

id

A

RLD

=

g

(

f

id

A

RLD

) =

g

(

f

j

A

)

.

Theorem 7.36.

f

u

(

RLD

B

) =

id

B

RLD

f

id

A

RLD

for every reloid

f

and

A 2

F

(

Src

f

)

,

B 2

F

(

Dst

f

)

.

Proof.

f

u

(

RLD

B

) =

f

u

¡

RLD

1

F

(

Dst

f

)

u

¡

1

F

(

Src

f

)

RLD

B

=

f

j

A

u

¡

1

F

(

Src

f

)

RLD

B

=

(

f

id

A

RLD

)

u

¡

1

F

(

Src

f

)

RLD

B

=

¡

(

f

id

A

RLD

)

¡

1

u

¡

1

F

(

Src

f

)

RLD

B

¡

1

¡

1

=

¡

(

id

A

RLD

f

¡

1

)

u

¡

RLD

1

F

(

Src

f

)

¡

1

= (

id

A

RLD

f

¡

1

id

B

RLD

)

¡

1

=

id

B

RLD

f

id

A

RLD

.

Theorem 7.37.

f

j

"

Src

f

g

=

"

Src

f

RLD

im

(

f

j

"

Src

f

g

)

for every reloid

f

and

2

Src

f

.

Proof.

First,

im

(

f

j

"

Src

f

g

) =

l

h"

Dst

f

ih

im

i

GR

(

f

j

"

Src

f

g

) =

l

h"

Dst

f

ih

im

i

GR

¡

f

u

¡

"

Src

f

f

RLD

1

F

(

Dst

f

)

=

l

f"

Dst

f

im

(

F

\

(

f

Dst

f

))

j

F

2

GR

f

g

=

l

f"

Dst

f

im

(

F

j

f

g

)

j

F

2

GR

f

g

:

Taking this into account we have:

"

Src

f

RLD

im

(

f

j

"

Src

f

g

) =

l

"

RLD

(

Src

f

;

Dst

f

)

(

f

K

)

j

K

2

im

(

f

j

"

Src

f

g

)

 

=

l

"

RLD

(

Src

f

;

Dst

f

)

(

f

im

(

F

j

f

g

))

j

F

2

GR

f

 

=

l

"

RLD

(

Src

f

;

Dst

f

)

(

F

j

f

g

)

j

F

2

GR

f

 

=

l

"

RLD

(

Src

f

;

Dst

f

)

(

F

\

(

f

Dst

f

))

j

F

2

GR

f

 

=

l

"

RLD

(

Src

f

;

Dst

f

)

F

j

F

2

GR

f

 

u "

RLD

(

Src

f

;

Dst

f

)

(

f

Dst

f

) =

f

u "

RLD

(

Src

f

;

Dst

f

)

(

f

Dst

f

) =

f

j

"

Src

f

g

:

7.4 Restricting reloid to a filter. Domain and image

125