background image

15.11. COMPLETE POINTFREE FUNCOIDS

220

Let

S

be a set of filters.

h

f

i

G

S

=

G

hh

f

ii

atoms

G

S

=

G

hh

f

ii

[

h

atoms

i

S

=

G [

hh

f

ii

h

atoms

i

S

=

GDGE

hh

f

ii

h

atoms

i

S

=

GDG

◦hh

f

ii

atoms

E

S

=

G

 F

hh

f

ii

atoms

a

a

S

=

G

h

f

i

a

a

S

=

G

hh

f

ii

S.

Definition

1145

.

Let

Z

0

and

Z

1

be join-semilattices with least elements. I will

call

pointfree generalized closure

such a function

α

(

Z

1

)

Z

0

that

FiXme

: It is just a

map preserving finite joins, no need to introduce a new term. It can be generalized

for arbitrary posets.

1

.

α

Z

0

=

Z

1

;

2

.

I, J

Z

0

:

α

(

I

t

J

) =

αI

t

αJ

.

Definition

1146

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices. I will call a

co-complete pointfree funcoid

a pointfree funcoid

f

FCD

(

A

;

B

) such that

h

f

i|

Z

0

is a pointfree generalized closure.

Proposition

1147

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices. Co-complete pointfree funcoids

FCD

(

A

;

B

) bijectively correspond to point-

free generalized closures

Z

Z

0

1

, where the bijection is

f

7→ h

f

i|

Z

0

.

Proof.

It follows from the theorem

1082

.

Theorem

1148

.

Let (

A

;

Z

0

) be semifiltered, star-separable, down-aligned filtra-

tor with finitely meet closed, join-closed, and separable core, where

Z

0

is a complete

boolean lattice and both

Z

0

and

A

are atomistic lattices.

Let (

B

;

Z

1

) be a star-separable filtrator.

The following conditions are equivalent for every pointfree funcoid

f

FCD

(

A

;

B

):

1

.

f

1

is co-complete;

2

.

S

P

A

, J

Z

1

: (

F

A

S

[

f

]

J

⇒ ∃I ∈

S

:

I

[

f

]

J

);

3

.

S

P

Z

0

, J

Z

1

: (

F

Z

0

S

[

f

]

J

⇒ ∃

I

S

:

I

[

f

]

J

);

4

.

f

is complete;

5

.

S

P

Z

0

:

h

f

i

F

Z

0

S

=

F

B

hh

f

ii

S

.

Proof.

First note that the theorem

320

applies to the filtrator (

A

;

Z

0

).

3

1

For every

S

P

Z

0

,

J

Z

1

Z

0

G

S

u

A

f

1

J

6

=

A

⇒ ∃

I

S

:

I

u

A

f

1

J

6

=

A

,

(22)

consequently by the theorem

320

we have

f

1

J

Z

0

.