background image

Proposition 17.5.

a

f

(

C

)

g

b

,

a

f

y

/

g

y

b

.

Proof.

From the denition.

Proposition 17.6.

a

f

(

C

)

g

b

,

f

a

(

C

)

b

g

.

Proof.

f

a

(

C

)

b

g

,

f

a

y

/

b

y

g

,

a

f

y

/

g

y

b

,

a

f

(

C

)

g

b

.

Theorem 17.7.

¡

f

(

C

)

g

¡

1

=

f

y

(

C

)

g

y

.

Proof.

For every funcoids

a

2

Mor

(

Src

f

;

Src

g

)

and

b

2

Mor

(

Dst

f

;

Dst

g

)

we have:

¡

f

(

C

)

g

¡

1

b

=

g

y

b

f

=

f

y

(

C

)

g

y

b

.

¡¡

f

(

C

)

g

¡

1

¡

1

a

=

f

(

C

)

g

a

=

g

a

f

y

=

¡

f

y

(

C

)

g

y

¡

1

a

.

Theorem 17.8.

Let

f

,

g

be pointfree funcoids between lters on boolean lattices. Then for every

lters

A

0

2

F

(

Src

f

)

,

B

0

2

F

(

Src

g

)

f

(

C

)

g

(

A

0

FCD

B

0

) =

h

f

iA

0

FCD

h

g

iB

0

:

Proof.

[TODO: No reason to restrict to atomic lters?]

For every atom

a

1

FCD

b

1

(

a

1

2

atoms

Dst

f

,

b

1

2

atoms

Dst

g

) (see theorem

15.76

of the lattice of funcoids we have:

a

1

FCD

b

1

/

f

(

C

)

g

(

A

0

FCD

B

0

)

, A

0

FCD

B

0

f

(

C

)

g

a

1

FCD

b

1

,

(

A

0

FCD

B

0

)

f

¡

1

/

g

¡

1

(

a

1

FCD

b

1

)

, h

f

iA

0

FCD

B

0

/

a

1

FCD

h

g

¡

1

i

b

1

, h

f

iA

0

/

a

1

^ h

g

¡

1

i

b

1

/

B

0

, h

f

iA

0

/

a

1

^

h

g

iB

0

/

b

1

, h

f

iA

0

FCD

h

g

iB

0

/

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

15.79

).

Corollary 17.9.

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

2

F

(

Src

f

)

,

A

1

2

F

(

Dst

f

)

,

B

0

2

F

(

Src

g

)

,

B

1

2

F

(

Dst

g

)

where Src

f

, Dst

f

, Src

g

, Dst

g

are boolean lattices.

Proof.

A

0

FCD

B

0

f

(

C

)

g

A

1

FCD

B

1

, A

1

FCD

B

1

/

f

(

C

)

g

(

A

0

FCD

B

0

)

,

A

1

FCD

B

1

/

h

f

iA

0

FCD

h

g

iB

0

, A

1

/

h

f

iA

0

^ B

1

/

h

g

iB

0

, A

0

[

f

]

A

1

^ B

0

[

g

]

B

1

.

17.2 Function spaces of posets

Denition 17.10.

Let

A

i

be a family of posets indexed by some set dom

A

. We will dene order

of families of posets by the formula

a

v

b

, 8

i

2

dom

A

:

a

i

v

b

i

:

I will call this new poset

A

=

Q

A

the function space

of posets and the above order

product order

.

Proposition 17.11.

The function space for posets is also a poset.

Proof.

Reexivity.

Obvious.

Antisymmetry.

Obvious.

Transitivity.

Obvious.

Obvious 17.12.

A

has least element i each

A

i

has a least element. In this case

min

A

=

Y

i

2

dom

A

min

A

i

:

Proposition 17.13.

a

/

b

, 9

i

2

dom

A

:

a

i

/

b

i

for every

a; b

2

Q

A

if every

A

i

has least element.

204

Multifuncoids and staroids