background image

Thus

f

(

g

t

h

) =

f

g

t

f

h

by theorem

15.12

.

Theorem 15.63.

Let

A

,

B

,

C

be posets of lters over some boolean lattices,

f

2

FCD

(

A

;

B

)

,

g

2

FCD

(

B

;

C

)

,

h

2

FCD

(

A

;

C

)

. Then

g

f

/

h

,

g

/

h

f

¡

1

:

Proof.

g

f

/

h

,

9

a

2

atoms

A

; c

2

atoms

C

:

a

[(

g

f

)

u

h

]

c

,

9

a

2

atoms

A

; c

2

atoms

C

: (

a

[

g

f

]

c

^

a

[

h

]

c

)

,

9

a

2

atoms

A

; b

2

atoms

B

; c

2

atoms

C

: (

a

[

f

]

b

^

b

[

g

]

c

^

a

[

h

]

c

)

,

9

b

2

atoms

B

; c

2

atoms

C

: (

b

[

g

]

c

^

b

[

h

f

¡

1

]

c

)

,

9

b

2

atoms

B

; c

2

atoms

C

:

b

[

g

u

(

h

f

¡

1

)]

c

,

g

/

h

f

¡

1

:

15.9 Direct product of elements

Denition 15.64.

Funcoidal product

FCD

B

where

A 2

A

,

B 2

B

and

A

and

B

are posets with

least elements is a pointfree funcoid such that for every

X 2

A

,

Y 2

B

hA 

FCD

BiX

=

(

B

if

/

A

;

0

B

if

X  A

;

and

h

(

FCD

B

)

¡

1

iY

=

(

A

if

/

B

;

0

A

if

Y  B

:

Proposition 15.65.

FCD

B

is really a pointfree funcoid and

X

[

FCD

B

]

Y , X 

/

A ^ Y 

/

B

:

Proof.

Obvious.

Proposition 15.66.

Let

A

and

B

be separable bounded posets,

f

2

FCD

(

A

;

B

)

,

A 2

A

,

B 2

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

. If

dom

f

v A ^

im

f

v B

then

X

[

f

]

Y ) Y 

/

h

f

iX ) Y 

/

B

and similarly

X

[

f

]

Y ) X 

/

A

.

So

[

f

]

[

FCD

B

]

and thus using separability

f

v A 

FCD

B

.

Theorem 15.67.

Let

A

,

B

be sets of lters over boolean lattices. For every

f

2

FCD

(

A

;

B

)

and

A 2

A

,

B 2

B

f

u

(

FCD

B

) =

id

B

FCD

(

B

)

f

id

A

FCD

(

A

)

:

Proof.

From above

FCD

(

A

;

B

)

is a (complete) lattice.

h

=

def

id

B

FCD

(

B

)

f

id

A

FCD

(

A

)

. For every

X 2

A

h

h

iX

=

D

id

B

FCD

(

B

)

E

h

f

i

D

id

A

FCD

(

A

)

E

X

=

B u h

f

i

(

A u X

)

and

h

h

¡

1

iX

=

D

id

A

FCD

(

A

)

E

h

f

¡

1

i

D

id

B

FCD

(

B

)

E

X

=

A u h

f

¡

1

i

(

B u X

)

:

188

Pointfree funcoids