19.11. COMPLETE POINTFREE FUNCOIDS

304

1

.

f

1

is co-complete;

2

.

S

P

A

, J

Z

1

: (

d

A

S

[

f

]

J

⇒ ∃I ∈

S

:

I

[

f

]

J

);

3

.

S

P

Z

0

, J

Z

1

: (

d

Z

0

S

[

f

]

J

⇒ ∃

I

S

:

I

[

f

]

J

);

4

.

f

is complete;

5

.

S

P

Z

0

:

h

f

i

d

Z

0

S

=

d

B

hh

f

ii

S

.

Proof.

First note that the theorem

580

applies to the filtrator (

A

,

Z

0

).

3

1

For every

S

P

Z

0

,

J

Z

1

Z

0

l

S

u

A

f

1

J

6

=

A

⇒ ∃

I

S

:

I

u

A

f

1

J

6

=

A

,

(29)

consequently by the theorem

580

we have

f

1

J

Z

0

.

1

2

For every

S

P

A

,

J

Z

1

we have

f

1

J

Z

0

, consequently

S

P

A

, J

Z

1

:

A

l

S

6

f

1

J

⇒ ∃I ∈

S

:

I 6

f

1

J

!

.

From this follows

2

.

2

4

Let

h

f

i

d

Z

0

S

and

d

B

hh

f

ii

S

be defined. We have

h

f

i

d

A

S

=

h

f

i

d

Z

0

S

.

J

u

B

h

f

i

A

l

S

6

=

B

A

l

S

[

f

]

J

∃I ∈

S

:

I

[

f

]

J

∃I ∈

S

:

J

u

B

h

f

iI 6

=

B

J

u

B

B

l

hh

f

ii

S

6

=

B

(used theorem

580

). Thus

h

f

i

d

A

S

=

d

B

hh

f

ii

S

by star-separability of

(

B

,

Z

1

).

5

3

Let

h

f

i

d

Z

0

S

be defined.

Then

d

B

hh

f

ii

S

is also defined because

h

f

i

d

Z

0

S

=

d

B

hh

f

ii

S

. Then

Z

0

l

S

[

f

]

J

J

u

B

h

f

i

Z

0

l

S

6

=

B

J

u

B

B

l

hh

f

ii

S

6

=

B

what by theorem

580

is equivalent to

I

S

:

J

u

B

h

f

i

I

6

=

B

that is

I

S

:

I

[

f

]

J

.

2

3

,

4

5

By join-closedness of the core of (

A

,

Z

0

).

Theorem

1580

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices. If

R

is a set of co-complete pointfree funcoids in

pFCD

(

A

,

B

) then

d

R

is

a co-complete pointfree funcoid.

Proof.

Let

R

be a set of co-complete pointfree funcoids. Then for every

X

Z

0

D

l

R

E

X

=

B

l

f

R

h

f

i

X

=

Z

1

l

f

R

h

f

i

X

Z

1

(used the theorems

1524

and

531

).

Let

A

and

B

be posets with least elements. I will denote

ComplpFCD

(

A

,

B

) and

CoComplpFCD

(

A

,

B

) the sets of complete and co-complete funcoids correspondingly

from a poset

A

to a poset

B

.