 19.6. SPECIFYING FUNCOIDS BY FUNCTIONS OR RELATIONS ON ATOMIC FILTERS294

19.6. Specifying funcoids by functions or relations on atomic filters

Theorem

1545

.

Let

A

be an atomic poset and (

B

,

Z

1

) is a primary filtrator

over a boolean lattice. Then for every

f

pFCD

(

A

,

B

) and

X ∈

A

we have

h

f

iX

=

B

l

hh

f

ii

atoms

A

X

.

Proof.

For every

Y

Z

1

we have

Y

6

B

h

f

iX ⇔ X 6

A

f

1

Y

x

atoms

A

X

:

x

6

A

f

1

Y

⇔ ∃

x

atoms

A

X

:

Y

6

B

h

f

i

x.

Thus

h

f

iX

=

S

h

i

hh

f

ii

atoms

A

X

=

d

B

hh

f

ii

atoms

A

X

(used corol-

lary

569

). Consequently

h

f

iX

=

d

B

hh

f

ii

atoms

A

X

by the corollary

568

.

Proposition

1546

.

Let

f

be a pointfree funcoid. Then for every

X ∈

Src

f

and

Y ∈

Dst

f

1

.

X

[

f

]

Y ⇔ ∃

x

atoms

X

:

x

[

f

]

Y

if Src

f

is an atomic poset.

2

.

X

[

f

]

Y ⇔ ∃

y

atoms

Y

:

X

[

f

]

y

if Dst

f

is an atomic poset.

Proof.

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

If

X

[

f

]

Y

, then

Y 6 h

f

iX

, consequently exists

y

atoms

Y

such that

y

6

h

f

iX

,

X

[

f

]

y

. The reverse is obvious.

Corollary

1547

.

If

f

is a pointfree funcoid with both source and destination

being atomic posets, then for every

X ∈

Src

f

and

Y ∈

Dst

f

X

[

f

]

Y ⇔ ∃

x

atoms

X

, y

atoms

Y

:

x

[

f

]

y.

Proof.

Apply the theorem twice.

Corollary

1548

.

If

A

is a separable atomic poset and

B

is a separable poset

then

f

pFCD

(

A

,

B

) is determined by the values of

h

f

i

X

for

X

atoms

A

.

Proof.

y

6 h

f

i

x

x

6

f

1

y

⇔ ∃

X

atoms

x

:

X

6

f

1

y

⇔ ∃

X

atoms

x

:

y

6 h

f

i

X.

Thus by separability of

B

we have

h

f

i

is determined by

h

f

i

X

for

X

atoms

x

.

By separability of

A

we infer that

f

can be restored from

h

f

i

(theorem

1498

).

Theorem

1549

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices.

1

. A function

α

B

atoms

A

such that (for every

a

atoms

A

)

αa

v

l

D

l

◦h

α

i

atoms

A

E

up

Z

0

a

(24)

can be continued to the function

h

f

i

for a unique

f

pFCD

(

A

,

B

);

h

f

iX

=

l

h

α

i

atoms

A

X

(25)

for every

X ∈

A

.

2

. A relation

δ

P

(atoms

A

×

atoms

B

) such that (for every

a

atoms

A

,

b

atoms

B

)

X

up

Z

0

a, Y

up

Z

1

b

x

atoms

A

X, y

atoms

B

Y

:

x δ y

a δ b

(26)

can be continued to the relation [

f

] for a unique

f

pFCD

(

A

,

B

);

X

[

f

]

Y ⇔ ∃

x

atoms

X

, y

atoms

Y

:

x δ y

(27)

for every

X ∈

A

,

Y ∈

B

.