background image

6.9. FUNCOIDAL PRODUCT OF FILTERS

115

Proposition

639

.

A ×

FCD

B

is really a funcoid and

A ×

FCD

B

X

=

(

B

if

X 6 A

F

(Base(

B

))

if

X  A

.

Proof.

Obvious.

Obvious

640

.

FCD

(

U

;

V

)

(

A

×

B

) =

U

A

× ↑

V

B

for sets

A

U

and

B

V

.

Proposition

641

.

f

v A ×

FCD

B ⇔

dom

f

v A ∧

im

f

v B

for every

f

FCD

(

A

;

B

) and

A ∈

F

(

A

),

B ∈

F

(

B

).

Proof.

If

f

v A×

FCD

B

then dom

f

v

dom(

FCD

B

)

v A

, im

f

v

im(

FCD

B

)

v B

. If dom

f

v A ∧

im

f

v B

then

∀X ∈

F

(

A

)

,

Y ∈

F

(

B

) : (

X

[

f

]

Y ⇒ X u A 6

=

F

(

A

)

∧ Y u B 6

=

F

(

B

)

);

consequently

f

v A ×

FCD

B

.

The following theorem gives a formula for calculating an important particular

case of a meet on the lattice of funcoids:

Theorem

642

.

f

u

(

A ×

FCD

B

) = id

FCD

B

f

id

FCD

A

for every funcoid

f

and

A ∈

F

(Src

f

),

B ∈

F

(Dst

f

).

Proof.

h

def

= id

FCD

B

f

id

FCD

A

. For every

X ∈

F

(Src

f

)

h

h

iX

=

D

id

FCD

B

E

h

f

i

D

id

FCD

A

E

X

=

B u h

f

i

(

A u X

)

.

From this, as easy to show,

h

v

f

and

h

v A ×

FCD

B

. If

g

v

f

g

v A ×

FCD

B

for a

g

FCD

(Src

f

; Dst

f

) then dom

g

v A

, im

g

v B

,

h

g

iX

=

B u h

g

i

(

A u X

)

v B u h

f

i

(

A u X

) =

D

id

FCD

B

E

h

f

i

D

id

FCD

A

E

X

=

h

h

iX

,

g

v

h

. So

h

=

f

u

(

A ×

FCD

B

).

Corollary

643

.

f

|

A

=

f

u

(

A ×

FCD

>

F

(Dst

f

)

) for every funcoid

f

and

A ∈

F

(Src

f

).

Proof.

f

u

(

A ×

FCD

>

F

(Dst

f

)

) = id

FCD

>

F

(Dst

f

)

f

id

FCD

A

=

f

id

FCD

A

=

f

|

A

.

Corollary

644

.

f

6 A ×

FCD

B ⇔ A

[

f

]

B

for every funcoid

f

and

A ∈

F

(Src

f

),

B ∈

F

(Dst

f

).

Proof.

f

6 A ×

FCD

B ⇔

f

u

(

A ×

FCD

B

)

(Src

f

)

6

=

F

(Dst

f

)

D

id

FCD

B

f

id

FCD

A

E

(Src

f

)

6

=

F

(Dst

f

)

D

id

FCD

B

E

h

f

i

D

id

FCD

A

E

>

F

(Src

f

)

6

=

F

(Dst

f

)

B u h

f

i

(

A u >

F

(Src

f

)

)

6

=

F

(Dst

f

)

B u h

f

iA 6

=

F

(Dst

f

)

A

[

f

]

B

.

Corollary

645

.

Every filtrator of funcoids is star-separable.

Proof.

The set of funcoidal products of principal filters is a separation subset

of the lattice of funcoids.