8.4. RESTRICTING RELOID TO A FILTER. DOMAIN AND IMAGE

188

8.4. Restricting reloid to a filter. Domain and image

Definition

1016

.

Identity reloid

for a set

A

is defined by the formula

1

RLD

A

=

RLD

(

A,A

)

id

A

.

Obvious

1017

.

(1

RLD

A

)

1

= 1

RLD

A

.

Definition

1018

.

I define

restricting

a reloid

f

to a filter

A

as

f

|

A

=

f

u

(

A ×

RLD

>

F

(Dst

f

)

).

Definition

1019

.

Domain

and

image

of a reloid

f

are defined as follows:

dom

f

=

F

l

h

dom

i

up

f

; im

f

=

F

l

h

im

i

up

f.

Proposition

1020

.

f

v A ×

RLD

B ⇔

dom

f

v A ∧

im

f

v B

for every reloid

f

and filters

A ∈

F

(Src

f

),

B ∈

F

(Dst

f

).

Proof.

. It follows from dom(

A ×

RLD

B

)

v A ∧

im(

A ×

RLD

B

)

v B

.

. dom

f

v A ⇔ ∀

A

up

A∃

F

up

f

: dom

F

v

A

. Analogously

im

f

v B ⇔ ∀

B

up

B∃

G

up

f

: im

G

v

B

.

Let dom

f

v A ∧

im

f

v B

,

A

up

A

,

B

up

B

. Then there exist

F, G

up

f

such that dom

F

v

A

im

G

v

B

. Consequently

F

u

G

up

f

,

dom(

F

u

G

)

v

A

, im(

F

u

G

)

v

B

that is

F

u

G

v

A

×

B

. So there exists

H

up

f

such that

H

v

A

×

B

for every

A

up

A

,

B

up

B

. So

f

v A ×

RLD

B

.

Definition

1021

.

I call

restricted identity reloid

for a filter

A

the reloid

id

RLD

A

= (1

RLD

Base(

A

)

)

|

A

.

Theorem

1022

.

id

RLD

A

=

d

RLD

(Base(

A

)

,

Base(

A

))

A

up

A

id

A

for every filter

A

.

Proof.

Let

K

up

d

RLD

(Base(

A

)

,

Base(

A

))

A

up

A

id

A

, then there exists

A

up

A

such

that GR

K

id

A

. Then

id

RLD

A

v

RLD

(Base(

A

)

,

Base(

A

))

id

Base(

A

)

u

(

A ×

RLD

>

)

v

RLD

(Base(

A

)

,

Base(

A

))

id

Base(

A

)

u

(

A

×

RLD

>

) =

RLD

(Base(

A

)

,

Base(

A

))

id

Base(

A

)

u ↑

RLD

(

A

× >

) =

RLD

(Base(

A

)

,

Base(

A

))

(id

Base(

A

)

GR(

A

× >

)) =

RLD

(Base(

A

)

,

Base(

A

))

id

A

v

K.

Thus

K

up id

RLD

A

.

Reversely let

K

up id

RLD

A

= up(1

RLD

Base(

A

)

u

(

A ×

RLD

>

)), then there exists

A

up

A

such that

K

up

RLD

(Base(

A

)

,

Base(

A

))

(id

Base(

A

)

GR(

A

× >

)) =

up

RLD

(Base(

A

)

,

Base(

A

))

id

A

w

up

RLD

(Base(

A

)

,

Base(

A

))

l

A

up

A

id

A

.