background image

9.1. FUNCOID INDUCED BY A RELOID

200

Proof.

Recall that id

RLD

A

=

d

n

Base(

A

)

id

A

A

up

A

o

. For every

X

,

Y ∈

F

(Base(

A

))

we have

X

h

(

FCD

) id

RLD

A

i

Y ⇔

X ×

RLD

Y 6

id

RLD

A

A

up

A

:

X ×

RLD

Y 6↑

RLD

(Base(

A

)

,

Base(

A

))

id

A

A

up

A

:

X

h

FCD

(Base(

A

)

,

Base(

A

))

id

A

i

Y ⇔

A

up

A

:

X u Y 6

A

X u Y 6 A ⇔

X

h

id

FCD

A

i

Y

(used properties of generalized filter bases).

Corollary

1068

.

(

FCD

)1

RLD

A

= 1

FCD

A

for every set

A

.

Proposition

1069

.

(

FCD

) is a functor from

RLD

to

FCD

.

Proof.

Preservation of composition and of identity is proved above.

Proposition

1070

.

1

. (

FCD

)

f

is a monovalued funcoid if

f

is a monovalued reloid.

2

. (

FCD

)

f

is an injective funcoid if

f

is an injective reloid.

Proof.

We will prove only the first as the second is dual. Let

f

be a monoval-

ued reloid. Then

f

f

1

v

1

RLD

Dst

f

; (

FCD

)(

f

f

1

)

v

1

FCD

Dst

f

; (

FCD

)

f

((

FCD

)

f

)

1

v

1

FCD

Dst

f

that is (

FCD

)

f

is a monovalued funcoid.

Proposition

1071

.

(

FCD

)(

A ×

RLD

B

) =

A ×

FCD

B

for every filters

A

,

B

.

Proof.

X

(

FCD

)(

A ×

RLD

B

)

Y ⇔ ∀

F

up(

A ×

RLD

B

) :

X

FCD

F

Y

(for

every

X ∈

F

(Base(

A

)),

Y ∈

F

(Base(

B

)).

Evidently

F

up(

A ×

RLD

B

) :

X

FCD

F

Y ⇒ ∀

A

up

A

, B

up

B

:

X

[

A

×

B

]

Y

.

Let

A

up

A

, B

up

B

:

X

[

A

×

B

]

Y

. Then if

F

up(

A ×

RLD

B

), there are

A

up

A

,

B

up

B

such that

F

w

A

×

B

. So

X

FCD

F

Y

. We have proved

F

up(

A ×

RLD

B

) :

X

FCD

F

Y ⇔ ∀

A

up

A

, B

up

B

:

X

[

A

×

B

]

Y

.

Further

A

up

A

, B

up

B

:

X

[

A

×

B

]

Y ⇔

A

up

A

, B

up

B

: (

X 6

A

∧ Y 6

B

)

X 6 A ∧ Y 6 B ⇔ X

A ×

FCD

B

Y

.

Thus

X

(

FCD

)(

A ×

RLD

B

)

Y ⇔ X

A ×

FCD

B

Y

.

Proposition

1072

.

dom(

FCD

)

f

= dom

f

and im(

FCD

)

f

= im

f

for every

reloid

f

.