 19.11. COMPLETE POINTFREE FUNCOIDS

303

Proof.

(

x

×

FCD

z

)

u

(

g

f

)

6

=

pFCD

(

A

,

C

)

x

[

g

f

]

z

y

atoms

B

: (

x

[

f

]

y

y

[

g

]

z

)

y

atoms

B

: ((

x

×

FCD

y

)

u

f

6

=

pFCD

(

A

,

B

)

(

y

×

FCD

z

)

u

g

6

=

pFCD

(

B

,

C

)

)

(were used corollary

1558

and theorem

1549

).

Theorem

1575

.

Let

f

be a pointfree funcoid between atomic bounded sepa-

rable meet-semilattices

A

and

B

.

1

.

X

[

f

]

Y ⇔ ∃

F

atoms

f

:

X

[

F

]

Y

for every

X ∈

A

,

Y ∈

B

;

2

.

h

f

iX

=

d

F

atoms

f

h

F

iX

for every

X ∈

A

provided that

B

is a complete

lattice.

Proof.

1

.

F

atoms

f

:

X

[

F

]

Y ⇔

a

atoms

A

, b

atoms

B

: (

a

×

FCD

b

6

f

∧ X

a

×

FCD

b

Y

)

a

atoms

A

, b

atoms

B

: (

a

×

FCD

b

6

f

a

×

FCD

b

6 X ×

FCD

Y

)

F

atoms

f

: (

F

6

f

F

6 X ×

FCD

Y

)

(by theorem

1570

)

f

6 X ×

FCD

Y ⇔

X

[

f

]

Y

.

2

Let

Y ∈

B

. Suppose

Y 6 h

f

iX

. Then

X

[

f

]

Y

;

F

atoms

f

:

X

[

F

]

Y

;

F

atoms

f

:

Y 6 h

F

iX

; and (taking into account that

B

is strongly separable

by theorem

222

)

Y 6

d

F

atoms

f

h

F

iX

. So

h

f

iX v

d

F

atoms

f

h

F

iX

by strong

separability. The contrary

h

f

iX w

d

F

atoms

f

h

F

iX

is obvious.

19.11. Complete pointfree funcoids

Definition

1576

.

Let

A

and

B

be posets. A pointfree funcoid

f

pFCD

(

A

,

B

)

is

complete

, when for every

S

P

A

whenever both

d

S

and

d

hh

f

ii

S

are defined

we have

h

f

i

l

S

=

l

hh

f

ii

S.

Definition

1577

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be filtrators. I will call a

co-complete

pointfree funcoid

a pointfree funcoid

f

pFCD

(

A

,

B

) such that

h

f

i

X

Z

1

for every

X

Z

0

.

Proposition

1578

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices. Co-complete pointfree funcoids

pFCD

(

A

,

B

) bijectively correspond to func-

tions

Z

Z

0

1

preserving finite joins, where the bijection is

f

7→ h

f

i|

Z

0

.

Proof.

It follows from the theorem

1510

.

Theorem

1579

.

Let (

A

,

Z

0

) be a down-aligned, with join-closed, binarily meet-

closed and separable core which is a complete boolean lattice.

Let (

B

,

Z

1

) be a star-separable filtrator.

The following conditions are equivalent for every pointfree funcoid

f

pFCD

(

A

,

B

):