background image

Denition 15.89.

Let

Z

0

and

Z

1

be join-semilattices with least elements. I will call

pointfree

generalized closure

such a function

2

(

Z

1

)

Z

0

that

[TODO: It is just a map preserving nite joins,

no need to introduce a new term. It can be generalized for arbitrary posets.]

1.

0

Z

0

= 0

Z

1

;

2.

8

I ; J

2

Z

0

:

(

I

t

J

) =

I

t

J

.

Denition 15.90.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over boolean lattices. I will call

a

co-complete pointfree funcoid

a pointfree funcoid

f

2

FCD

(

A

;

B

)

such that

h

f

ij

Z

0

is a pointfree

generalized closure.

Proposition 15.91.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over boolean lattices. Co-

complete pointfree funcoids

FCD

(

A

;

B

)

bijectively correspond to pointfree generalized closures

Z

1

Z

0

,

where the bijection is

f

7! h

f

ij

Z

0

.

Proof.

It follows from the theorem

15.26

.

Theorem 15.92.

Let

(

A

;

Z

0

)

be semiltered, star-separable, down-aligned ltrator with nitely

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

The following conditions are equivalent for every pointfree funcoid

f

2

FCD

(

A

;

B

)

:

1.

f

¡

1

is co-complete;

2.

8

S

2

P

A

; J

2

Z

1

: (

F

A

S

[

f

]

J

) 9I 2

S

:

I

[

f

]

J

)

;

3.

8

S

2

P

Z

0

; J

2

Z

1

: (

F

Z

0

S

[

f

]

J

) 9

I

2

S

:

I

[

f

]

J

)

;

4.

f

is complete;

5.

8

S

2

P

Z

0

:

h

f

i

F

Z

0

S

=

F

B

hh

f

ii

S

.

Proof.

First note that the theorem

4.53

applies to the ltrator

(

A

;

Z

0

)

.

(

3

)

)

(

1

).

For every

S

2

P

Z

0

,

J

2

Z

1

G

Z

0

S

u

A

h

f

¡

1

i

J

=

/ 0

A

) 9

I

2

S

:

I

u

A

h

f

¡

1

i

J

=

/ 0

A

;

(15.9)

consequently by the theorem

4.53

we have

h

f

¡

1

i

J

2

Z

0

.

(

1

)

)

(

2

).

For every

S

2

P

A

,

J

2

Z

1

we have

h

f

¡

1

i

J

2

Z

0

, consequently

8

S

2

P

A

; J

2

Z

1

:

 

G

A

S

/

h

f

¡

1

i

J

) 9I 2

S

:

/

h

f

¡

1

i

J

!

:

From this follows (

2

).

(

2

)

)

(

4

).

Let

h

f

i

F

Z

0

S

and

F

B

hh

f

ii

S

be dened. We have

h

f

i

F

A

S

=

h

f

i

F

Z

0

S

.

J

u

B

h

f

i

F

A

S

=

/ 0

B

,

F

A

S

[

f

]

J

, 9I 2

S

:

I

[

f

]

J

, 9I 2

S

:

J

u

B

h

f

iI

=

/

0

B

,

J

u

B

F

B

hh

f

ii

S

=

/ 0

B

(used theorem

4.53

). Thus

h

f

i

F

A

S

=

F

B

hh

f

ii

S

by

star-separability of

(

B

;

Z

1

)

.

(

5

)

)

(

3

).

Let

h

f

i

F

Z

0

S

be dened. Then

F

B

hh

f

ii

S

is also dened because

h

f

i

F

Z

0

S

=

F

B

hh

f

ii

S

. Then

F

Z

0

S

[

f

]

J

,

J

u

B

h

f

i

F

Z

0

S

=

/ 0

B

,

J

u

B

F

B

hh

f

ii

S

=

/ 0

B

what by

theorem

4.53

is equivalent to

9

I

2

S

:

J

u

B

h

f

i

I

=

/ 0

B

that is

9

I

2

S

:

I

[

f

]

J

.

(

2

)

)

(

3

), (

4

)

)

(

5

).

By join-closedness of the core of

(

A

;

Z

0

)

.

Theorem 15.93.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over boolean lattices. If

R

is a set

of co-complete pointfree funcoids in

FCD

(

A

;

B

)

then

F

R

is a co-complete pointfree funcoid.

15.11 Complete pointfree funcoids

193