CHAPTER 9

On distributivity of composition with a principal

reloid

9.1. Decomposition of composition of binary relations

Remark

849

.

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

=

((

x

;

z

);

y

)

x f y

y g z

.

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

=

((

x

;

z

);

y

)

x f y, z

f

and Θ

1

f

=

((

x

;

z

);

y

)

y f z, x

f

.

(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

)

F

GR

f, G

GR

g

=

l

RLD

(Src

f

;Dst

g

)

dom(

G

F

)

F

GR

f, G

GR

g

.

Lemma

850

.

n

G

F

F

GR

f,G

GR

g

o

is a filter base.

Proof.

Let

P, Q

n

G

F

F

GR

f,G

GR

g

o

. Then

P

=

G

0

F

0

,

Q

=

G

1

F

1

for

some

F

0

, F

1

f

,

G

0

, G

1

g

. Then

F

0

F

1

GR

f

,

G

0

G

1

GR

g

and thus

P

Q

(

F

0

F

1

)

(

G

0

G

1

)

G

F

F

GR

f, G

GR

g

.

Corollary

851

.

n

RLD

(Src

f

×

Dst

g

)

(

G

F

)

F

GR

f,G

GR

g

o

is a generalized filter base.

Proposition

852

.

g

f

= dom

d

n

RLD

(Src

f

×

Dst

g

)

(

G

F

)

F

GR

f,G

GR

g

o

.

Proof.

RLD

(Src

f

;Dst

g

)

dom(

G

F

)

w

dom

d

n

RLD

(Src

f

×

Dst

g

)

(

G

F

)

F

GR

f,G

GR

g

o

. Thus

g

f

w

dom

l

RLD

(Src

f

×

Dst

g

)

(

G

F

)

F

GR

f, G

GR

g

.

157