17.1. PRODUCT OF TWO FUNCOIDS

232

Proposition

1201

.

a

f

×

(

C

)

g

b

a

f

6

g

b

.

Proof.

From the definition.

Proposition

1202

.

a

f

×

(

C

)

g

b

f

a

×

(

C

)

b

g

.

Proof.

f

a

×

(

C

)

b

g

f

a

6

b

g

a

f

6

g

b

a

f

×

(

C

)

g

b

.

Theorem

1203

.

(

f

×

(

C

)

g

)

1

=

f

×

(

C

)

g

.

Proof.

For every funcoids

a

Mor(Src

f

; Src

g

) and

b

Mor(Dst

f

; Dst

g

) we

have:

(

f

×

(

C

)

g

)

1

b

=

g

b

f

=

f

×

(

C

)

g

b

.

((

f

×

(

C

)

g

)

1

)

1

a

=

f

×

(

C

)

g

a

=

g

a

f

=

(

f

×

(

C

)

g

)

1

a

.

Theorem

1204

.

Let

f

,

g

be pointfree funcoids between filters on boolean

lattices. Then for every filters

A

0

F

(Src

f

),

B

0

F

(Src

g

)

D

f

×

(

C

)

g

E

(

A

0

×

FCD

B

0

) =

h

f

iA

0

×

FCD

h

g

iB

0

.

Proof.

FiXme

: No reason to restrict to atomic filters?

For every atom

a

1

×

FCD

b

1

(

a

1

atoms

Dst

f

,

b

1

atoms

Dstg

) (see theorem

1132

of the lattice of funcoids

we have:

a

1

×

FCD

b

1

6

D

f

×

(

C

)

g

E

(

A

0

×

FCD

B

0

)

A

0

×

FCD

B

0

h

f

×

(

C

)

g

i

a

1

×

FCD

b

1

(

A

0

×

FCD

B

0

)

f

1

6

g

1

(

a

1

×

FCD

b

1

)

h

f

iA

0

×

FCD

B

0

6

a

1

×

FCD

g

1

b

1

h

f

iA

0

6

a

1

g

1

b

1

6 B

0

h

f

iA

0

6

a

1

∧ h

g

iB

0

6

b

1

h

f

iA

0

×

FCD

h

g

iB

0

6

a

1

×

FCD

b

1

.

Thus

f

×

(

C

)

g

(

A

0

×

FCD

B

0

) =

h

f

iA

0

×

FCD

h

g

iB

0

because the lattice

FCD

(

F

(Dst

f

);

F

(Dst

g

)) is atomically separable (corollary

653

).

Corollary

1205

.

A

0

×

FCD

B

0

f

×

(

C

)

g

A

1

×

FCD

B

1

⇔ A

0

[

f

]

A

1

∧ B

0

[

g

]

B

1

for every

A

0

F

(Src

f

),

A

1

F

(Dst

f

),

B

0

F

(Src

g

),

B

1

F

(Dst

g

) where Src

f

,

Dst

f

, Src

g

, Dst

g

are boolean lattices.

Proof.

A

0

×

FCD

B

0

h

f

×

(

C

)

g

i

A

1

×

FCD

B

1

A

1

×

FCD

B

1

6

D

f

×

(

C

)

g

E

A

0

×

FCD

B

0

A

1

×

FCD

B

1

6 h

f

iA

0

×

FCD

h

g

iB

0

A

1

6 h

f

iA

0

∧ B

1

6 h

f

iB

0

A

0

[

f

]

A

1

∧ B

0

[

g

]

B

1

.