 19.4. THE ORDER OF POINTFREE FUNCOIDS

289

Taking into account properties of generalized filter bases:

h

f

i

Src

f

l

S

=

Dst

f

l

hh

f

ii

up

l

S

=

Dst

f

l

hh

f

ii

X

∃P ∈

S

:

X

up

P

=

Dst

f

l

h

f

i

X

∃P ∈

S

:

X

up

P

w

(because Dst

f

is a strongly separable poset)

Dst

f

l

h

f

iP

P ∈

S

=

Dst

f

l

hh

f

ii

S.

Proposition

1513

.

X

[

f

]

d

S

⇔ ∃Y ∈

S

:

X

[

f

]

Y

if

f

is a pointfree funcoid,

Dst

f

is a meet-semilattice with least element and

S

is a generalized filter base on

Dst

f

.

Proof.

X

[

f

]

l

S

l

S

u h

f

iX 6

=

⊥ ⇔

l

hh

f

iX ui

S

6

=

⊥ ⇔

(by properties of generalized filter bases)

∃Y ∈ hh

f

iX ui

S

:

Y 6

=

⊥ ⇔ ∃Y ∈

S

:

h

f

iX u Y 6

=

⊥ ⇔ ∃Y ∈

S

:

X

[

f

]

Y

.

Theorem

1514

.

A function

ϕ

:

A

B

, where (

A

,

Z

0

) and (

B

,

Z

1

) are primary

filtrators over boolean lattices, preserves finite joins (including nullary joins) and

filtered meets iff there exists a pointfree funcoid

f

such that

h

f

i

=

ϕ

.

Proof.

Backward implication follows from above.

Let

ψ

=

ϕ

|

Z

0

. Then

ψ

preserves bottom element and binary joins. Thus there

exists a funcoid

f

such that

h

f

i

=

ψ

.

It remains to prove that

h

f

i

=

ϕ

.

Really,

h

f

iX

=

d

hh

f

ii

up

X

=

d

h

ψ

i

up

X

=

d

h

ϕ

i

up

X

=

ϕ

d

up

X

=

ϕ

X

for every

X ∈

F

(Src

f

).

Corollary

1515

.

Pointfree funcoids

f

from a lattice

A

of fitlters on a boolean

lattice to a lattice

B

of fitlters on a boolean lattice bijectively correspond by the

formula

h

f

i

=

ϕ

to functions

ϕ

:

A

B

preserving finite joins and filtered meets.

Theorem

1516

.

The set of pointfree funcoids between sets of filters on boolean

lattices is a co-frame.

Proof.

Theorems

1510

and

530

.

19.4. The order of pointfree funcoids

Definition

1517

.

The order of pointfree funcoids

pFCD

(

A

,

B

) is defined by

the formula:

f

v

g

⇔ ∀

x

A

:

h

f

i

x

v h

g

i

x

∧ ∀

y

B

:

f

1

y

v

g

1

y.

Proposition

1518

.

It is really a partial order on the set

pFCD

(

A

,

B

).