 CHAPTER 10

On distributivity of composition with a principal

reloid

10.1. Decomposition of composition of binary relations

Remark

1157

.

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.

10.2. Decomposition of composition of reloids

A similar thing for reloids:

In this chapter we will equate reloids with filters on cartesian products of sets.

For composable reloids

f

and

g

we have

g

f

=

RLD

(Src

f,

Dst

g

)

l

G

F

F

GR

f, G

GR

g

=

RLD

(Src

f,

Dst

g

)

l

dom(

G

F

)

F

GR

f, G

GR

g

.

Lemma

1158

.

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

up

f

,

G

0

G

1

up

g

and thus

P

Q

(

F

0

F

1

)

(

G

0

G

1

)

G

F

F

GR

f, G

GR

g

.

Corollary

1159

.

n

F

(Src

f

×

Dst

g

)

(

G

F

)

F

GR

f,G

GR

g

o

is a generalized filter base.

Proposition

1160

.

g

f

= dom

d

F

(Src

f

×

Dst

g

)

n

G

F

F

GR

f,G

GR

g

o

.

215