**Algebraic General Topology. Vol 1**:
Paperback
/
E-book
||
**Axiomatic Theory of Formulas**:
Paperback
/
E-book

Distributivity of co mposition 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 boo k [1].

1.1 Decomposition of composition of binary relations

Remark 1. Sorry for unfortunate choice of termino logy: “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 ca n 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 tr ick 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 ﬁlter 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 ﬁlter base.

Propositio n 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

Let X ∈ dom

d

↑

RLD(Src f ×Dst g;℧)

(G ⊗ F ) | F ∈ GR f , G ∈ GR g

. Then there exist Y such that

X × Y ∈

d

↑

RLD(Src f ×Dst g;℧)

(G ⊗ F ) | F ∈ GR f , G ∈ GR g

. So because it is a generalized

ﬁlter base X × Y ⊇ G ⊗ F for some F ∈ GR f, G ∈ GR g. Thus X ∈ dom(G ⊗ F ), X ⊒

↑

RLD(Src f ;Dst g)

dom(G ⊗ F ), X ∈ GR(g ◦ f).

We can deﬁne g ⊗ f for reloids f , g:

g ⊗ f = {G ⊗ F | F ∈ GR f , G ∈ GR g}.

Then

g ◦ f =

l

↑

RLD(Src f ;Dst g)

hdomi(g ⊗ f ) = dom

l

↑

RLD(Src f ×Dst g;℧)

(g ⊗ f ).

2 Lemmas for the main resu lt

Let F = ↑

RLD(Src F ;Dst F )

f is a principal reloid.

Lemma 5. (g ⊗ f) ∪ (h ⊗ f) = (g ∪ h) ⊗ f for binary relations f , g, h.

Proof. (g ∪ h) ⊗ f = Θ

0

f ∩ Θ

1

(g ∪ h) = Θ

0

f ∩ (Θ

1

g ∪ Θ

1

h) = (Θ

0

f ∩ Θ

1

g) ∪ (Θ

0

f ∩ Θ

1

h) =

(g ⊗ f) ∪ (h ⊗ f).

Lemma 6.

d

↑

RLD(Src f ×Dst g;℧)

(G ⊗ f ) | G ∈

F

T

=

F

d

↑

RLD(Src f ×Dst g;℧)

(G ⊗ F ) | G ∈

T

.

Proof.

d

↑

RLD(Src f ×Dst g;℧)

(G ⊗ f ) | G ∈ GR

F

T

⊒

F

d

↑

RLD(Src f ×Dst g;℧)

(G ⊗ F ) | G ∈

T

is obvious.

Let K ∈

F

d

↑

RLD(Src f ×Dst g;℧)

(G ⊗ F ) | G ∈ T

. Then for each G ∈ T

K ∈

l

↑

RLD(Src f ×Dst g;℧)

(G ⊗ F );

K ∈

d

↑

RLD(Src f ×Dst g;℧)

{Γ ⊗ f | Γ ∈ GR G}.

K ∈ {(Γ

0

⊗ f ) ∩

∩ (Γ

n

⊗ f ) | n ∈ N, Γ

i

∈ GR G}.

∀G ∈ T : K ⊇ (Γ

G,0

⊗ f ) ∩

∩ (Γ

G,n

⊗ f ) for some n ∈ N, Γ

G,i

∈ G.

Let G ∈

T

T .

K ⊇ (Γ

0

⊗ f ) ∩

∩ (Γ

n

⊗ f ) where Γ

i

=

S

g∈G

Γ

g,i

∈ GR

F

T .

K ∈ {(Γ

0

⊗ f ) ∩

∩ (Γ

n

⊗ f ) | n ∈ N}.

So K ∈ {(Γ

0

′

⊗ f ) ∩

∩ (Γ

n

′

⊗ f ) | n ∈ N, Γ

i

′

∈ GR

F

T } =

d

↑

RLD(Src f ×Dst g;℧)

{G ⊗ f | G ∈

GR

F

T }.

3 Proof of the main result

Theorem 7. (

F

T ) ◦ F =

F

{G ◦ F | G ∈ T } for every prin cipal reloid F = ↑

RLD(Src f ;Dst g)

f.

Proof.

G

T

◦ F =

l

↑

RLD(Src f ;Dst g)

hdomi

G

T

⊗ F

= dom

l

↑

RLD(Src f ×Dst g;℧)

G

T

⊗ F

= dom

l

↑

RLD(Src f ×Dst g;℧)

G ⊗ f | G ∈ GR

G

T

G

{G ◦ F | G ∈ T } =

G

l

↑

RLD(Src f ;Dst g)

hdomi(G ⊗ F ) | G ∈ T

=

G

dom

l

↑

RLD(Src f ×Dst g;℧)

(G ⊗ F ) | G ∈ T

= dom

G

l

↑

RLD(Src f ×Dst g;℧)

(G ⊗ F ) | G ∈ T

.

2 Section 3

It’s enough to prove

l

↑

RLD(Src f ×Dst g;℧)

(G ⊗ f ) | G ∈ GR

G

T

=

G

l

↑

RLD(Src f ×Dst g;℧)

(G ⊗ F ) | G ∈ T

but this is the statement of the lemma.

4 Embedding reloids into funcoids

Deﬁnition 8. Let f is a reloid. The funcoid ρf ∈ FCD(Src f; Dst f ) is deﬁned by the formulas:

hρf ix = f ◦ x and hρ f

−1

iy = f

−1

◦ y

where x are endo-reloids on Src f a nd y are endo-reloids on Dst f .

Propositio n 9. It is really a funcoid (if we equate reloids x and y with corresponding ﬁlters on

cartesian products of sets).

Proof. y

hρf ix ⇔ y

f ◦ x ⇔ f

−1

◦ y

x ⇔ hρ f

−1

iy

x.

Corollary 10. (ρf )

−1

= ρ f

−1

.

Deﬁnition 11. It can be continued to arbitrary funcoi ds x having source Src f by the formula

hρ

∗

f ix = hρf iid

Src f

◦ x.

Propositio n 12. ρ is an injection.

Proof. Consider x = id

Src f

.

Propositio n 13. ρ(g ◦ f) = (ρg) ◦ (ρf ).

Proof. hρ(g ◦ f )ix = g ◦ f ◦ x = hρgihρf ix = (hρ gi ◦ hρf i)x. Thus hρ(g ◦ f)i = hρgi ◦ hρf i =

h(ρg) ◦ (ρf)i and so ρ(g ◦ f) = (ρg) ◦ (ρf).

Theorem 14. ρ

F

F =

F

hρiF f or a set F of reloids.

Proof. It’s enough to prove hρ

F

F i

∗

X = h

F

hρiF i

∗

X for a set X.

Really, hρ

F

F i

∗

X = hρ

F

F i↑X =

F

F ◦ ↑X =

F

{f ◦ ↑X | f ∈ F } =

F

{hρf i↑X | f ∈ F } =

h

F

{ρf | f ∈ F }i↑X = h

F

hρiF i

∗

X.

Conjecture 1 5. ρ

d

F =

d

hρiF f or a set F of reloids.

Propositio n 16. ρid

RLD(A)

= id

FCD(A)

.

Proof.

ρid

RLD(A)

x = id

RLD(A)

◦ x = x.

We can try to develop further theory by applying embedding of rel oids into funcoids for

researching of properties of reloids.

Theorem 17. Reloid f is monovalued iﬀ funcoid ρf is monovalued.

Proof. ρf is monovalued⇔(ρf) ◦ (ρf )

−1

⊑ 1

Dst ρf

⇔ ρ(f ◦ f

−1

) ⊑ 1

Dst f

⇔ ρ(f ◦ f

−1

) ⊑ id

RLD(A)

⇔

ρ(f ◦ f

−1

) ⊑ ρid

FCD(A)

⇔ f ◦ f

−1

⊑ id

FCD(A)

⇔ f is monovalued.

Bib liogr aphy

[1] Victor Porton. Algebraic General Topology. Volume 1. 2013.

Bibliography 3