15.10. ATOMIC POINTFREE FUNCOIDS

216

Thus

F

FCD

S

=

A ×

FCD

F

S

by theorem

1081

.

D

l

FCD

S

E

x

=

l

A ×

FCD

B

x

B ∈

S

)

=

(

d

S

if

X

u

A

A 6

=

A

B

if

X

u

A

A

=

A

=

D

A ×

FCD

l

S

E

x.

Thus

d

FCD

S

=

A ×

FCD

d

S

by theorem

1110

.

If

A 6

=

A

then obviously the function

FCD

is injective.

Proposition

1130

.

Let

A

be a meet-semilattice with least element and

B

be a poset with least element. If

a

is an atom of

A

,

f

FCD

(

A

;

B

) then

f

|

a

=

a

×

FCD

h

f

i

a

.

Proof.

Let

X ∈

A

.

X u

a

6

=

A

⇒ h

f

|

a

iX

=

h

f

i

a,

X u

a

=

A

⇒ h

f

|

a

iX

=

B

.

Proposition

1131

.

f

(

A ×

FCD

B

) =

A ×

FCD

h

f

iB

for elements

A ∈

A

and

B

B

of some posets

A

,

B

,

C

with least elements and

f

FCD

(

B

;

C

).

Proof.

Let

X ∈

A

,

Y ∈

B

.

f

(

A ×

FCD

B

)

X

=

(

h

f

iB

if

X 6 A

if

X  A

!

=

A ×

FCD

h

f

iB

X

;

(

f

(

A ×

FCD

B

))

1

Y

=

(

B ×

FCD

A

)

f

1

Y

=

(

A

if

f

1

Y 6 B

if

f

1

Y  B

!

=

(

A

if

Y 6 h

f

iB

if

Y  h

f

iB

!

=

h

f

iB ×

FCD

A

Y

=

(

A ×

FCD

h

f

iB

)

1

Y

.

15.10. Atomic pointfree funcoids

Theorem

1132

.

Let

A

,

B

be sets of filters over boolean lattices. A

f

FCD

(

A

;

B

) is an atom of the poset

FCD

(

A

;

B

) iff there exist

a

atoms

A

and

b

atoms

B

such that

f

=

a

×

FCD

b

.

Proof.

A

and

B

are atomic by the theorem

402

.

. Let

f

be an atom of the poset

FCD

(

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

v

f

; because

f

is atomic we have

f

=

a

×

FCD

b

.