background image

15.7 Specifying funcoids by functions or relations on atomic

lters

Theorem 15.54.

Let

A

be an atomic poset and

(

B

;

Z

1

)

is a primary ltrator over a boolean

lattice. Then for every

f

2

FCD

(

A

;

B

)

and

X 2

A

we have

h

f

iX

=

G

B

hh

f

ii

atoms

A

X

:

Proof.

For every

Y

2

Z

1

we have

Y

/

B

h

f

iX , X 

/

A

h

f

¡

1

i

Y

, 9

x

2

atoms

A

X

:

x

/

A

h

f

¡

1

i

Y

, 9

x

2

atoms

A

X

:

Y

/

B

h

f

i

x:

Thus

@

h

f

iX

=

S

h

@

i hh

f

ii

atoms

A

X

=

@

F

B

hh

f

ii

atoms

A

X

(used theorem

4.132

). Consequently

h

f

iX

=

F

B

hh

f

ii

atoms

A

X

by the corollary

4.128

.

Proposition 15.55.

Let

f

be a pointfree funcoid. Then for every

X 2

Src

f

and

Y 2

Dst

f

1.

X

[

f

]

Y , 9

x

2

atoms

X

:

x

[

f

]

Y

if Src

f

is an atomic poset.

2.

X

[

f

]

Y , 9

y

2

atoms

Y

:

X

[

f

]

y

if Dst

f

is an atomic poset.

Proof.

I will prove only the second as the rst is similar.

If

X

[

f

]

Y

, then

/

h

f

iX

, consequently exists

y

2

atoms

Y

such that

y

/

h

f

iX

,

X

[

f

]

y

. The

reverse is obvious.

Corollary 15.56.

If

f

is a pointfree funcoid with both source and destination being atomic posets,

then for every

X 2

Src

f

and

Y 2

Dst

f

X

[

f

]

Y , 9

x

2

atoms

X

; y

2

atoms

Y

:

x

[

f

]

y:

Proof.

Apply the theorem twice.

Corollary 15.57.

If

A

is a separable atomic poset and

B

is a separable poset then

f

2

FCD

(

A

;

B

)

is determined by the values of

h

f

i

X

for

X

2

atoms

A

.

Proof.

y

/

h

f

i

x

,

x

/

h

f

¡

1

i

y

, 9

X

2

atoms

x

:

X

/

h

f

¡

1

i

y

, 9

X

2

atoms

x

:

y

/

h

f

i

X

.

Thus by separability of

B

we have

h

f

i

is determined by

h

f

i

X

for

X

2

atoms

x

.

By separability of

A

we infer that

f

can be restored from

h

f

i

(theorem

15.12

).

Theorem 15.58.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over boolean lattices.

1. A function

2

B

atoms

A

such that (for every

a

2

atoms

A

)

a

v

l

G

h

atoms

A

up

(

A

;

Z

0

)

a

(15.5)

can be continued to the function

h

f

i

for a unique

f

2

FCD

(

A

;

B

)

;

h

f

iX

=

G

h

i

atoms

A

X

(15.6)

for every

X 2

A

.

2. A relation

2

P

(

atoms

A

atoms

B

)

such that (for every

a

2

atoms

A

,

b

2

atoms

B

)

8

X

2

up

(

A

;

Z

0

)

a; Y

2

up

(

B

;

Z

1

)

b

9

x

2

atoms

A

X ; y

2

atoms

B

Y

:

x  y

)

a  b

(15.7)

can be continued to the relation

[

f

]

for a unique

f

2

FCD

(

A

;

B

)

;

X

[

f

]

Y , 9

x

2

atoms

X

; y

2

atoms

Y

:

x  y

(15.8)

for every

X 2

A

,

Y 2

B

.

15.7 Specifying funcoids by functions or relations on atomic filters

185