background image

19.11. COMPLETE POINTFREE FUNCOIDS

304

Proposition

1581

.

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

1513

.

Theorem

1582

.

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

):

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

583

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

583

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

583

). 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

583

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

).