 Chapter 9
On distributivity of composition with a prin-

cipal reloid

9.1 Decomposition of composition of binary relations

Remark 9.1.

Sorry for an unfortunate choice of terminology: composition and decomposition

are unrelated.

The idea of the proof below is that composition of binary relations can be decomposed into two

operations:

and dom:

g

f

=

f

((

x

;

z

);

y

)

j

xfy

^

ygz

g

:

Composition of binary relations can be decomposed:

g

f

=

dom

(

g

f

)

.

It can be decomposed even further:

g

f

0

f

\

1

g

where

0

f

=

f

((

x

;

z

);

y

)

j

xfy; z

2

f

g

and

1

f

=

f

((

x

;

z

);

y

)

j

yfz; x

2

f

g

:

(Here

f

is the Grothendieck universe.)

Now we will do a similar trick with reloids.

9.2 Decomposition of composition of reloids

A similar thing for reloids:

g

f

=

l

"

RLD

(

Src

f

;

Dst

g

)

(

G

F

)

j

F

2

GR

f ; G

2

GR

g

=

l

"

RLD

(

Src

f

;

Dst

g

)

dom

(

G

F

)

j

F

2

GR

f ; G

2

GR

g

:

Lemma 9.2.

f

G

F

j

F

2

GR

f ; G

2

GR

g

g

is a lter base.

Proof.

Let

P ; Q

2 f

G

F

j

F

2

GR

f ; G

2

GR

g

g

. Then

P

=

G

0

F

0

,

Q

=

G

1

F

1

for some

F

0

;

F

1

2

f

,

G

0

; G

1

2

g

. Then

F

0

\

F

1

2

GR

f

,

G

0

\

G

1

2

GR

g

and thus

P

\

Q

(

F

0

\

F

1

)

(

G

0

\

G

1

)

2 f

G

F

j

F

2

GR

f ; G

2

GR

g

g

:

Corollary 9.3.

"

RLD

(

Src

f

Dst

g

;

f

)

(

G

F

)

j

F

2

GR

f ; G

2

GR

g

is a generalized lter base.

Proposition 9.4.

g

f

=

dom

d

"

RLD

(

Src

f

Dst

g

;

f

)

(

G

F

)

j

F

2

GR

f ; G

2

GR

g

.

Proof.

"

RLD

(

Src

f

;

Dst

g

)

dom

(

G

F

)

w

dom

d

"

RLD

(

Src

f

Dst

g

;

f

)

(

G

F

)

j

F

2

GR

f ; G

2

GR

g

.

Thus

g

f

w

dom

l

"

RLD

(

Src

f

Dst

g

;

f

)

(

G

F

)

j

F

2

GR

f ; G

2

GR

g

:

Let

X

2

dom

d

"

RLD

(

Src

f

Dst

g

;

f

)

(

G

F

)

j

F

2

GR

f ; G

2

GR

g

. Then there exist

Y

such that

X

Y

2

GR

d

"

RLD

(

Src

f

Dst

g

;

f

)

(

G

F

)

j

F

2

GR

f ; G

2

GR

g

. So because it is a generalized

lter base

X

Y

G

F

for some

F

2

GR

f

,

G

2

GR

g

. Thus

X

2

dom

(

G

F

)

,

X

2

GR

(

g

f

)

.

139