 CHAPTER 9

Relationships between funcoids and reloids

9.1. Funcoid induced by a reloid

Every reloid

f

induces a funcoid (

FCD

)

f

FCD

(Src

f,

Dst

f

) by the following

formulas (for every

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

)):

X

[(

FCD

)

f

]

Y ⇔ ∀

F

up

f

:

X

FCD

F

Y

;

h

(

FCD

)

f

iX

=

F

l

F

up

f

FCD

F

X

.

We should prove that (

FCD

)

f

is really a funcoid.

Proof.

We need to prove that

X

[(

FCD

)

f

]

Y ⇔ Y u h

(

FCD

)

f

iX 6

=

⊥ ⇔ X u

(

FCD

)

f

1

Y 6

=

.

The above formula is equivalent to:

F

up

f

:

X

FCD

F

Y ⇔

Y u

l

F

up

f

FCD

F

X 6

=

⊥ ⇔

X u

l

F

up

f

FCD

F

1

Y 6

=

.

We have

Y u

d

F

up

f

FCD

F

X

=

d

F

up

f

(

Y u

FCD

F

X

).

Let’s denote

W

=

Yu

h

FCD

F

i

X

F

up

f

.

F

up

f

:

X

FCD

F

Y ⇔ ∀

F

up

f

:

Y u

FCD

F

X 6

=

⊥ ⇔ ⊥

/

W.

We need to prove only that

/

W

d

W

6

=

. (The rest follows from

symmetry.) To prove it is enough to show that

W

is a generalized filter base.

Let’s prove that

W

is a generalized filter base. For this it’s enough to prove that

V

=

h

FCD

F

i

X

F

up

f

is a generalized filter base. Let

A

,

B ∈

V

that is

A

=

FCD

P

X

,

B

=

FCD

Q

X

where

P, Q

up

f

. Then for

C

=

FCD

(

P

u

Q

)

X

is true both

C ∈

V

and

C v A

,

B

. So

V

is a generalized filter base and thus

W

is a generalized

filter base.

Proposition

1064

.

(

FCD

)

RLD

f

=

FCD

f

for every

Rel

-morphism

f

.

Proof.

X

(

FCD

)

RLD

f

Y ⇔ ∀

F

up

RLD

f

:

X

FCD

F

Y ⇔

X

FCD

f

Y

(for every

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

)).

Theorem

1065

.

X

[(

FCD

)

f

]

Y ⇔ X ×

RLD

Y 6

f

for every reloid

f

and

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

).

197