 19.3. POINTFREE FUNCOID AS CONTINUATION

286

19.3. Pointfree funcoid as continuation

Proposition

1510

.

Let

f

be a pointfree funcoid. Then for every

x

Src

f

,

y

Dst

f

we have

1

. If (Src

f,

Z

) is a filtrator with separable core then

x

[

f

]

y

⇔ ∀

X

up

Z

x

:

X

[

f

]

y

.

2

. If (Dst

f,

Z

) is a filtrator with separable core then

x

[

f

]

y

⇔ ∀

Y

up

Z

y

:

x

[

f

]

Y

.

Proof.

We will prove only the second because the first is similar.

x

[

f

]

y

y

6

Dst

f

h

f

i

x

⇔ ∀

Y

up

Z

y

:

Y

6 h

f

i

x

⇔ ∀

Y

up

Z

y

:

x

[

f

]

Y.

Corollary

1511

.

Let

f

be a pointfree funcoid and (Src

f,

Z

0

), (Dst

f,

Z

1

) be

filtrators with separable core. Then

x

[

f

]

y

⇔ ∀

X

up

Z

0

x, Y

up

Z

1

y

:

X

[

f

]

Y.

Proof.

Apply the proposition twice.

Theorem

1512

.

Let

f

be a pointfree funcoid. Let (Src

f,

Z

0

) be a binarily

meet-closed filtrator with separable core which is a meet-semilattice and

x

Src

f

: up

Z

0

x

6

=

and (Dst

f,

Z

1

) be a primary filtrator over a boolean lattice.

h

f

i

x

=

Dst

f

l

hh

f

ii

up

Z

0

x.

Proof.

By the previous proposition for every

y

Dst

f

:

y

6

Dst

f

h

f

i

x

x

[

f

]

y

⇔ ∀

X

up

Z

0

x

:

X

[

f

]

y

⇔ ∀

X

up

Z

0

x

:

y

6

Dst

f

h

f

i

X.

Let’s denote

W

=

n

y

u

Dst

f

h

f

i

X

X

up

Z

0

x

o

. We will prove that

W

is a generalized filter

base over

Z

1

. To prove this enough to show that

V

=

n

h

f

i

X

X

up

Z

0

x

o

is a generalized

filter base.

Let

P

,

Q ∈

V

. Then

P

=

h

f

i

A

,

Q

=

h

f

i

B

where

A, B

up

Z

0

x

;

A

u

Z

0

B

up

Z

0

x

(used the fact that it is a binarily meet-closed and theorem

535

and

R v P u

Dst

f

Q

for

R

=

h

f

i

(

A

u

Z

0

B

)

V

because Dst

f

is strongly separable by

proposition

579

So

V

is a generalized filter base and thus

W

is a generalized filter

base.

Dst

f

/

W

⇔ ⊥

Dst

f

/

d

Dst

f

W

by theorem

572

That is

X

up

Z

0

x

:

y

u

Dst

f

h

f

i

X

6

=

Dst

f

y

u

Dst

f

Dst

f

l

hh

f

ii

up

Z

0

x

6

=

Dst

f

.

Comparing with the above,

y

u

Dst

f

h

f

i

x

6

=

Dst

f

y

u

Dst

f

Dst

f

l

hh

f

ii

up

Z

0

x

6

=

Dst

f

.

So

h

f

i

x

=

d

Dst

f

hh

f

ii

up

Z

0

x

because Dst

f

is separable (proposition

579

and the

fact that

Z

1

is a boolean lattice).

Theorem

1513

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices.

1

. A function

α

B

Z

0

conforming to the formulas (for every

I, J

Z

0

)

α

Z

0

=

B

,

α

(

I

t

J

) =

αI

t

αJ