background image

15.9. FUNCOIDAL PRODUCT OF ELEMENTS

213

Proof.

I will prove only the first equality because the other is analogous.

We can apply theorem

1091

.

For every

X ∈

A

,

Y ∈

C

X

[

f

(

g

t

h

)]

Z ⇔

y

atoms

B

: (

X

[

g

t

h

]

y

y

[

f

]

Z

)

y

atoms

B

: ((

X

[

g

]

y

∨ X

[

h

]

y

)

y

[

f

]

Z

)

y

atoms

B

: ((

X

[

g

]

y

y

[

f

]

Z

)

(

X

[

h

]

y

y

[

f

]

Z

))

y

atoms

B

: (

X

[

g

]

y

y

[

f

]

Z

)

∨ ∃

y

atoms

B

: (

X

[

h

]

y

y

[

f

]

Z

)

X

[

f

g

]

Z ∨ X

[

f

h

]

Z ⇔

X

[

f

g

t

f

h

]

Z

.

Thus

f

(

g

t

h

) =

f

g

t

f

h

by theorem

1068

.

Theorem

1119

.

Let

A

,

B

,

C

be posets of filters over some boolean lattices,

f

FCD

(

A

;

B

),

g

FCD

(

B

;

C

),

h

FCD

(

A

;

C

). Then

g

f

6

h

g

6

h

f

1

.

Proof.

g

f

6

h

a

atoms

A

, c

atoms

C

:

a

[(

g

f

)

u

h

]

c

a

atoms

A

, c

atoms

C

: (

a

[

g

f

]

c

a

[

h

]

c

)

a

atoms

A

, b

atoms

B

, c

atoms

C

: (

a

[

f

]

b

b

[

g

]

c

a

[

h

]

c

)

a

atoms

A

, c

atoms

C

: (

b

[

g

]

c

b

h

f

1

c

)

a

atoms

A

, c

atoms

C

:

b

g

u

(

h

f

1

)

c

g

6

h

f

1

.

15.9. Funcoidal product of elements

Definition

1120

.

Funcoidal product

FCD

B

where

A ∈

A

,

B ∈

B

and

A

and

B

are posets with least elements is a pointfree funcoid such that for every

X ∈

A

,

Y ∈

B

A ×

FCD

B

X

=

B

if

X 6 A

;

B

if

X  A

;

and

(

A ×

FCD

B

)

1

Y

=

A

if

Y 6 B

;

A

if

Y  B

.

Proposition

1121

.

A ×

FCD

B

is really a pointfree funcoid and

X

A ×

FCD

B

Y ⇔ X 6 A ∧ Y 6 B

.

Proof.

Obvious.

Proposition

1122

.

Let

A

and

B

be separable bounded posets

FiXme

: Switch

to correct conditions for existence and due properties of image and domain.

,

f

FCD

(

A

;

B

),

A ∈

A

,

B ∈

B

. Then

FiXme

: Should add proposition with one-direction

implication, without separability requirement.

f

v A ×

FCD

B ⇔

dom

f

v A ∧

im

f

v 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

]

Y ⇒ Y 6 h

f

iX ⇒ Y 6 B

and similarly

X

[

f

]

Y ⇒ X 6 A

.

So [

f

]

A ×

FCD

B

and thus using separability

f

v A ×

FCD

B

.