background image

15.11. COMPLETE POINTFREE FUNCOIDS

219

Corollary

1140

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices. Then

FCD

(

A

;

B

) is a co-brouwerian lattice.

Proposition

1141

.

Let

A

,

B

,

C

be sets of filters over some boolean lattices

and

f

FCD

(

A

;

B

),

g

FCD

(

B

;

C

). Let

B

be an atomic poset. 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

)

.

Proof.

(

x

×

FCD

z

)

u

(

g

f

)

6

=

FCD

(

A

;

C

)

x

[

g

f

]

z

y

atoms

B

: (

x

[

f

]

y

y

[

g

]

z

)

y

atoms

B

: ((

x

×

FCD

y

)

u

f

6

=

FCD

(

A

;

B

)

(

y

×

FCD

z

)

u

g

6

=

FCD

(

B

;

C

)

)

(were used corollary

1125

and theorem

1117

).

Theorem

1142

.

Let

f

be a pointfree funcoid between sets of filters on boolean

lattices.

1

.

X

[

f

]

Y ⇔ ∃

F

atoms

f

:

X

[

F

]

Y

for every

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

);

2

.

h

f

iX

=

F

F

atoms

f

h

F

iX

for every

X ∈

F

(Src

f

).

Proof.

1

.

F

atoms

f

:

X

[

F

]

Y ⇔

a

atoms

F

(Src

f

)

, b

atoms

F

(Dst

f

)

: (

a

×

FCD

b

6

f

∧ X

a

×

FCD

b

Y

)

a

atoms

F

(Src

f

)

, b

atoms

F

(Dst

f

)

: (

a

×

FCD

b

6

f

a

×

FCD

b

6 X ×

FCD

Y

)

F

atoms

f

: (

F

6

f

F

6 X ×

FCD

Y

)

f

6 X ×

FCD

Y ⇔

X

[

f

]

Y

.

2

Let

Y ∈

F

(Dst

f

). Suppose

Y 6 h

f

iX

. Then

X

[

f

]

Y

;

F

atoms

f

:

X

[

F

]

Y

;

F

atoms

f

:

Y 6 h

F

iX

;

Y 6

F

F

atoms

f

h

F

iX

. So

h

f

iX v

F

F

atoms

f

h

F

iX

. The contrary

h

f

iX w

F

F

atoms

f

h

F

iX

is obvious.

15.11. Complete pointfree funcoids

Definition

1143

.

Let

A

and

B

be posets. A pointfree funcoid

f

FCD

(

A

;

B

)

is

complete

, when for every

S

P

A

whenever both

F

S

and

F

hh

f

ii

S

are defined

we have

h

f

i

G

S

=

G

hh

f

ii

S.

Proposition

1144

.

Let

A

,

B

be sets of filters over boolean lattices. A pointfree

funcoid

f

FCD

(

A

;

B

) is complete iff

h

f

i

a

=

F

hh

f

ii

atoms

a

for every

a

A

.

Proof.

Direct implication is obvious. The reverse implication: