background image

5.2

Reloids induced by funcoid

Every funcoid

f

FCD

(

A

;

B

) induces a reloid from

A

to

B

in two ways, in-

tersection of

outward

relations and union of

inward

direct products of filter

objects:

(

RLD

)

out

f

def

=

RLD

(

A

;

B

)

up

f

;

(

RLD

)

in

f

def

=

A ×

RLD

B

| A ∈

F

(

A

)

,

B ∈

F

(

B

)

,

A ×

FCD

B ⊆

f

 

.

Theorem 64

(

RLD

)

in

f

=

a

×

RLD

b

|

a

atoms 1

F

(Src

f

)

, b

atoms 1

F

(Dst

f

)

, a

×

FCD

b

f

 

.

Proof

It follows from the theorem 46.

Remark 6

It seems that (

RLD

)

in

has smoother properties and is more im-

portant than (

RLD

)

out

. (However see also the exercize below for (

RLD

)

in

not

preserving identities.)

Proposition 37

(

RLD

)

out

FCD

(

A

;

B

)

f

=

RLD

(

A

;

B

)

f

for every small sets

A

,

B

and binary relation

f

A

×

B

.

Proof

(

RLD

)

out

FCD

(

A

;

B

)

f

=

RLD

(

A

;

B

)

up

FCD

(

A

;

B

)

f

=

RLD

(

A

;

B

)

min up

FCD

(

A

;

B

)

f

=

RLD

(

A

;

B

)

f

.

Surprisingly a funcoid is greater inward than outward:

Theorem 65

(

RLD

)

out

f

(

RLD

)

in

f

for every funcoid

f

.

Proof

We need to prove

\ D

RLD

(Src

f

;Dst

f

)

E

up

f

A ×

RLD

B

| A

,

B ∈

F

,

A ×

FCD

B ⊆

f

 

.

Let

K

up

A ×

RLD

B

| A

,

B ∈

F

,

A ×

FCD

B ⊆

f

 

.

Then

K

=

RLD

(Src

f

;Dst

f

)

X

A

×

Y

B

| A

,

B ∈

F

,

A ×

FCD

B ⊆

f

 

=

[ n

RLD

(Src

f

;Dst

f

)

(

X

A

×

Y

B

)

| A

,

B ∈

F

,

A ×

FCD

B ⊆

f

o

f

where

X

A

up

A

,

Y

B

up

B

. So

K

up

f

;

K

up

RLD

(Src

f

;Dst

f

)

up

f

.

Theorem 66

(

FCD

)(

RLD

)

in

f

=

f

for every funcoid

f

.

56