background image

Distributivity of composition with a principal reloid

over join of reloids

by Victor Porton

Email:

porton@narod.ru

Web:

http://www.mathematics21.org

September 23, 2013

1 Introduction

It is a draft.

I present a proof of the equation

(

F

T

)

F

=

F

{

G

F

|

G

T

}

for a principal reloid

F

and a

set

T

of reloids (provided their sources and destination match each other).

First read my book [1].

1.1 Decomposition of composition of binary relations

Remark 1.

Sorry for unfortunate choice of terminology: “composition” and “decomposisiton” 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

)

|

xfy

ygz

}

.

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

)

|

xfy, z

}

and

Θ

1

f

=

{

((

x

;

z

);

y

)

|

yfz, x

}

.

(Here

is the Grothendieck universe.)

Now we will do a similar trick with reloids.

1.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 2.

{

G

F

|

F

f , G

g

}

is a filter base.

Proof.

Let

P , Q

∈ {

G

F

|

F

f , G

g

}

. 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

f

,

G

0

G

1

g

and thus

P

Q

(

F

0

F

1

)

(

G

0

G

1

)

∈ {

G

F

|

F

f , G

g

}

.

Corollary 3.

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

F

GR

f , G

GR

g

 

is a generalized filter base.

Proposition 4.

g

f

=

dom

d

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

F

GR

f , G

GR

g

 

.

Proof.

RLD

(

Src

f

;

Dst

g

)

dom

(

G

F

)

dom

d

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

F

GR

f , G

GR

g

 

.

Thus

g

f

dom

l

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

F

GR

f , G

GR

g

 

.

1