background image

7.10. FUNCOIDAL PRODUCT OF FILTERS

164

Proof.

g

f

6

h

a

atoms

F

(

A

)

, c

atoms

F

(

C

)

:

a

[(

g

f

)

u

h

]

c

a

atoms

F

(

A

)

, c

atoms

F

(

C

)

: (

a

[

g

f

]

c

a

[

h

]

c

)

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, c

atoms

F

(

C

)

: (

a

[

f

]

b

b

[

g

]

c

a

[

h

]

c

)

b

atoms

F

(

B

)

, c

atoms

F

(

C

)

: (

b

[

g

]

c

b

h

f

1

c

)

b

atoms

F

(

B

)

, c

atoms

F

(

C

)

:

b

g

u

(

h

f

1

)

c

g

6

h

f

1

.

7.10. Funcoidal product of filters

A generalization of Cartesian product of two sets is funcoidal product of two

filters:

Definition

883

.

Funcoidal product

of filters

A

and

B

is such a funcoid

A ×

FCD

B ∈

FCD

(Base(

A

)

,

Base(

B

)) that for every

X ∈

Base(

A

),

Y ∈

Base(

B

)

X

A ×

FCD

B

Y ⇔ X 6 A ∧ Y 6 B

.

Proposition

884

.

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

885

.

• ↑

FCD

(

U,V

)

(

A

×

B

) =

U

A

× ↑

V

B

for sets

A

U

and

B

V

.

• ↑

FCD

(

A

×

B

) =

A

× ↑

B

for typed sets

A

and

B

.

Proposition

886

.

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

=

⊥ ∧ Y u B 6

=

);

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

887

.

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

).