 15.10. ATOMIC POINTFREE FUNCOIDS

217

. Let

a

atoms

A

,

b

atoms

B

,

f

FCD

(

A

;

B

). If

b

B

h

f

i

a

then

¬

(

a

[

f

]

b

),

f

u

(

a

×

FCD

b

) =

FCD

(

A

;

B

)

(because

A

and

B

are bounded meet-

semilattices); if

b

v h

f

i

a

then

∀X ∈

A

: (

X 6

a

⇒ h

f

iX w

b

),

f

w

a

×

FCD

b

. Consequently

f

u

(

a

×

FCD

b

) =

FCD

(

A

;

B

)

f

w

a

×

FCD

b

; that

is

a

×

FCD

b

is an atomic pointfree funcoid.

Theorem

1133

.

Let

A

,

B

be sets of filters over boolean lattices. Then

FCD

(

A

;

B

) is atomic.

Proof.

Let

f

FCD

(

A

;

B

) and

f

6

=

FCD

(

A

;

B

)

. Then dom

f

6

=

A

, thus

exists

a

atoms dom

f

. So

h

f

i

a

6

=

B

thus exists

b

atoms

h

f

i

a

. Finally the

atomic pointfree funcoid

a

×

FCD

b

v

f

.

Theorem

1134

.

Let

A

,

B

be sets of filters over boolean lattices. Then the

poset

FCD

(

A

;

B

) is separable.

Proof.

Let

f, g

FCD

(

A

;

B

),

f

@

g

. Then taking into account the theorem

632

exists

a

atoms

A

such that

h

f

i

a

@

h

g

i

a

. By corollary

405

B

is atomically

separable. So exists

b

atoms

B

such that

h

f

i

a

u

b

=

B

and

b

v h

g

i

a

. For every

x

atoms

A

h

f

i

a

u

a

×

FCD

b

a

=

h

f

i

a

u

b

=

B

,

x

6

=

a

⇒ h

f

i

x

u

a

×

FCD

b

x

=

h

f

i

x

u ⊥

B

=

B

.

Thus

h

f

i

x

u

a

×

FCD

b

x

=

B

and consequently

f

u

(

a

×

FCD

b

) =

FCD

(

A

;

B

)

.

a

×

FCD

b

a

=

b

v h

g

i

a,

x

6

=

a

a

×

FCD

b

x

=

B

v h

g

i

x.

Thus

a

×

FCD

b

x

v h

g

i

x

and consequently

a

×

FCD

b

v

g

.

So the lattice of pointfree funcoids is separable by the theorem

173

.

Corollary

1135

.

FiXme

: Wrong theorem’s label.

Let

A

,

B

be sets of filters

over boolean lattices. The poset

FCD

(

A

;

B

) is:

1

. separable;

2

. atomically separable;

3

. conforming to Wallman’s disjunction property.

Proof.

By the theorem

180

.

Remark

1136

.

For more ways to characterize (atomic) separability of the

lattice of pointfree funcoids see subsections

Separation subsets and full stars

and

Atomically Separable Lattices

.

Corollary

1137

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices. The poset

FCD

(

A

;

B

) is an atomistic lattice.

Proof.

FiXme

: Is there a shorter proof just referring to a ready proposition?

By

the corollary

1090

FCD

(

A

;

B

) is a complete lattice. Let

f

FCD

(

A

;

B

). Suppose

contrary to the statement to be proved that

F

atoms

f

@

f

. Then there exists

a

atoms

f

such that

a

u

F

atoms

f

=

FCD

(

A

;

B

)

what is impossible.

Proposition

1138

.

Let

A

,

B

be sets of filters over boolean lattices.

atoms(

f

t

g

) = atoms

f

atoms

g

for every

f, g

FCD

(

A

;

B

).