background image

19.10. ATOMIC POINTFREE FUNCOIDS

302

19.10. Atomic pointfree funcoids

Theorem

1569

.

Let

A

,

B

be atomic bounded separable meet-semilattices. An

f

pFCD

(

A

,

B

) is an atom of the poset

pFCD

(

A

,

B

) iff there exist

a

atoms

A

and

b

atoms

B

such that

f

=

a

×

FCD

b

.

Proof.

. Let

f

be an atom of the poset

pFCD

(

A

,

B

). Let’s get elements

a

atoms dom

f

and

b

atoms

h

f

i

a

. Then for every

X ∈

A

a

a

×

FCD

b

X

=

B

v h

f

iX

,

X 6

a

a

×

FCD

b

X

=

b

v h

f

iX

.

So

a

×

FCD

b

X v h

f

iX

and similarly

b

×

FCD

a

Y v

f

1

Y

for ev-

ery

Y ∈

B

thus

a

×

FCD

b

v

f

; because

f

is atomic we have

f

=

a

×

FCD

b

.

. Let

a

atoms

A

,

b

atoms

B

,

f

pFCD

(

A

,

B

). If

b

B

h

f

i

a

then

¬

(

a

[

f

]

b

),

f

u

(

a

×

FCD

b

) =

pFCD

(

A

,

B

)

(by corollary

1558

because

A

and

B

are

bounded meet-semilattices); if

b

v h

f

i

a

, then for every

X ∈

A

a

a

×

FCD

b

X

=

B

v h

f

iX

,

X 6

a

a

×

FCD

b

X

=

b

v h

f

iX

that is

a

×

FCD

b

X v h

f

iX

and likewise

b

×

FCD

a

Y v

f

1

Y

for every

Y ∈

B

, so

f

w

a

×

FCD

b

. Consequently

f

u

(

a

×

FCD

b

) =

pFCD

(

A

,

B

)

f

w

a

×

FCD

b

; that is

a

×

FCD

b

is an atomic pointfree funcoid.

Theorem

1570

.

Let

A

,

B

be atomic bounded separable meet-semilattices.

Then

pFCD

(

A

,

B

) is atomic.

Proof.

Let

f

pFCD

(

A

,

B

) and

f

6

=

pFCD

(

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

.

Proposition

1571

.

Let

A

,

B

be starrish bounded separable lattices.

atoms(

f

t

g

) = atoms

f

atoms

g

for every

f, g

pFCD

(

A

,

B

).

Proof.

(

a

×

FCD

b

)

u

(

f

t

g

)

6

=

pFCD

(

A

,

B

)

(corollary

1558

)

a

[

f

t

g

]

b

(theorem

1526

)

a

[

f

]

b

a

[

g

]

b

(corollary

1558

)

(

a

×

FCD

b

)

u

f

6

=

pFCD

(

A

,

B

)

(

a

×

FCD

b

)

u

g

6

=

pFCD

(

A

,

B

)

for every

a

atoms

A

and

b

atoms

B

.

Theorem

1572

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices. Then

pFCD

(

A

,

B

) is a co-frame.

Proof.

Theorems

1510

and

530

.

Corollary

1573

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices. Then

pFCD

(

A

,

B

) is a co-brouwerian lattice.

Proposition

1574

.

Let

A

,

B

,

C

be atomic bounded separable meet-

semilattices, and

f

pFCD

(

A

,

B

),

g

pFCD

(

B

,

C

). Then

atoms(

g

f

) =

x

×

FCD

z

x

atoms

A

, z

atoms

C

,

y

atoms

B

: (

x

×

FCD

y

atoms

f

y

×

FCD

z

atoms

g

)

.