background image

19.8. FUNCOIDAL PRODUCT OF ELEMENTS

298

19.8. Funcoidal product of elements

Definition

1552

.

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

1553

.

A ×

FCD

B

is really a pointfree funcoid and

X

A ×

FCD

B

Y ⇔ X 6 A ∧ Y 6 B

.

Proof.

Obvious.

Proposition

1554

.

Let

A

and

B

be posets with least elements,

f

pFCD

(

A

,

B

),

A ∈

A

,

B ∈

B

. Then

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

.

Theorem

1555

.

Let

A

and

B

be strongly separable bounded posets,

f

pFCD

(

A

,

B

),

A ∈

A

,

B ∈

B

. Then

f

v A ×

FCD

B ⇔

dom

f

v A ∧

im

f

v B

.

Proof.

One direction is the proposition above. The other:

If dom

f

v A ∧

im

f

v B

then

X

[

f

]

Y ⇒ Y 6 h

f

iX ⇒ Y 6

im

f

⇒ Y 6 B

(strong separability used) and similarly

X

[

f

]

Y ⇒ X 6 A

.

So [

f

]

A ×

FCD

B

and thus using separability

f

v A ×

FCD

B

.

Theorem

1556

.

Let

A

,

B

be bounded separable meet-semilattices. For every

f

pFCD

(

A

,

B

) and

A ∈

A

,

B ∈

B

f

u

(

A ×

FCD

B

) = id

pFCD

(

B

)

B

f

id

pFCD

(

A

)

A

.

Proof.

h

def

= id

pFCD

(

B

)

B

f

id

pFCD

(

A

)

A

. For every

X ∈

A

h

h

iX

=

D

id

pFCD

(

B

)

B

E

h

f

i

D

id

pFCD

(

A

)

A

E

X

=

B u h

f

i

(

A u X

)

and

h

1

X

=

D

id

pFCD

(

A

)

A

E

f

1

D

id

pFCD

(

B

)

B

E

X

=

A u

f

1

(

B 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

pFCD

(

A

,

B

) then dom

g

v A

.

A

and

B

are are strongly separable by

theorem

222

Thus by propositions

1537

we have:

h

g

iX

=

h

g

i

(

X u

dom

g

) =

h

g

i

(

X u A

) =

B u h

g

i

(

A u X

)

v

B u h

f

i

(

A u X

) =

D

id

pFCD

(

B

)

B

E

h

f

i

D

id

pFCD

(

A

)

A

E

X

=

h

h

iX

,

and similarly

g

1

Y v

h

1

Y

. Thus

g

v

h

.

So

h

=

f

u

(

A ×

FCD

B

).

Corollary

1557

.

Let

A

,

B

be bounded separable meet-semilattices. For

every

f

pFCD

(

A

,

B

) and

A ∈

A

we have

f

|

A

=

f

u

(

A ×

FCD

>

B

).

Proof.

f

u

(

A ×

FCD

>

B

) = id

pFCD

(

B

)

>

B

f

id

pFCD

(

A

)

A

=

f

id

pFCD

(

A

)

A

=

f

|

A

.