background image

8.1. FUNCOID INDUCED BY A RELOID

149

So continuing the above equalities,

h

((

FCD

)

g

)

((

FCD

)

f

)

i

X

=

l

d

n

Dst

g

h

G

i

h

F

i

X

F

xyGR

f

o

G

xyGR

g

=

l

d

Dst

g

h

G

i

h

F

i

X

F

xyGR

f, G

xyGR

g

=

l

d

Dst

g

h

G

F

i

X

F

xyGR

f, G

xyGR

g

.

Combining these equalities we get

h

(

FCD

)(

g

f

)

i

X

=

h

((

FCD

)

g

)

((

FCD

)

f

)

i

X

for every set

X

P

(Src

f

).

Proposition

805

.

(

FCD

) id

RLD

A

= id

FCD

A

for every filter

A

.

Proof.

Recall that id

RLD

A

=

d

n

Base(

A

)

id

A

A

∈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

∈ A

:

X ×

RLD

Y 6↑

RLD

(Base(

A

);Base(

A

))

id

A

A

∈ A

:

X

h

FCD

(Base(

A

);Base(

A

))

id

A

i

Y ⇔

A

∈ A

:

X u Y 6↑

Base(

A

)

A

X u Y 6 A ⇔

X

h

id

FCD

A

i

Y

(used properties of generalized filter bases).

Proposition

806

.

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

monovalued reloid. Then

f

f

1

v

id

RLD

(Dst

f

)

; (

FCD

)(

f

f

1

)

v

id

FCD

(Dst

f

)

;

(

FCD

)

f

((

FCD

)

f

)

1

v

id

FCD

(Dst

f

)

that is (

FCD

)

f

is a monovalued funcoid.

Proposition

807

.

(

FCD

)(

A ×

RLD

B

) =

A ×

FCD

B

for every filters

A

,

B

.

Proof.

X

(

FCD

)(

A ×

RLD

B

)

Y ⇔ ∀

F

xyGR(

A ×

RLD

B

) :

X

FCD

F

Y

(for every

X ∈

F

(Base(

A

)),

Y ∈

F

(Base(

B

)).

Evidently

F

xyGR(

RLD

B

) :

X

FCD

F

Y ⇒ ∀

A

∈ A

, B

∈ B

:

X

h

FCD

(Base(

A

);Base(

B

))

(

A

×

B

)

i

Y

.

Let

A

∈ A

, B

∈ B

:

X

FCD

(Base(

A

);Base(

B

))

(

A

×

B

)

Y

. Then if

F

xyGR(

A ×

RLD

B

), there are

A

∈ A

,

B

∈ B

such that

F

A

×

B

. So

X

FCD

F

Y

.

We have proved

F

xyGR(

RLD

B

) :

X

FCD

F

Y ⇔ ∀

A

∈ A

, B

∈ B

:

X

h

FCD

(Base(

A

);Base(

B

))

(

A

×

B

)

i

Y

.