It’s enough to prove

l

RLD

(

Src

f

×

Dst

g

;

)

(

G

f

)

|

G

GR

G

T

=

l

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

G

T

but this is the statement of the lemma.

4 Embedding reloids into funcoids

Definition 8.

Let

f

is a reloid. The funcoid

ρf

FCD

(

Src

f

;

Dst

f

)

is defined by the formulas:

h

ρf

i

x

=

f

x

and

h

ρ f

1

i

y

=

f

1

y

where

x

are endo-reloids on Src

f

and

y

are endo-reloids on Dst

f

.

Proposition 9.

It is really a funcoid (if we equate reloids

x

and

y

with corresponding filters on

cartesian products of sets).

Proof.

y

h

ρf

i

x

y

f

x

f

1

y

x

⇔ h

ρ f

1

i

y

x

.

Corollary 10.

(

ρf

)

1

=

ρ f

1

.

Definition 11.

It can be continued to arbitrary funcoids

x

having source Src

f

by the formula

h

ρ

f

i

x

=

h

ρf

i

id

Src

f

x

.

Proposition 12.

ρ

is an injection.

Proof.

Consider

x

=

id

Src

f

.

Proposition 13.

ρ

(

g

f

) = (

ρg

)

(

ρf

)

.

Proof.

h

ρ

(

g

f

)

i

x

=

g

f

x

=

h

ρ g

ih

ρ f

i

x

= (

h

ρ g

i ◦ h

ρ f

i

)

x

. Thus

h

ρ

(

g

f

)

i

=

h

ρ g

i ◦ h

ρ f

i

=

h

(

ρg

)

(

ρf

)

i

and so

ρ

(

g

f

) = (

ρg

)

(

ρf

)

.

Theorem 14.

ρ

F

F

=

F

h

ρ

i

F

for a set

F

of reloids.

Proof.

It’s enough to prove

h

ρ

F

F

i

X

=

h

F

h

ρ

i

F

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

ρ

i

F

i

X

.

Conjecture 15.

ρ

d

F

=

d

h

ρ

i

F

for a set

F

of reloids.

Proposition 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 reloids into funcoids for

researching of properties of reloids.

Theorem 17.

Reloid

f

is monovalued iff 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.

Bibliography

[1]

Victor Porton.

Algebraic General Topology. Volume 1

. 2013.

Bibliography

3