 19.3. POINTFREE FUNCOID AS CONTINUATION

288

K δ I

0

t

Z

1

J

0

(

I

0

t

Z

1

J

0

)

u

B

αK

6

=

B

(

I

0

t

B

J

0

)

u

αK

6

=

B

(

I

0

u

B

αK

)

t

(

J

0

u

B

αK

)

6

=

B

I

0

u

B

αK

6

=

B

J

0

u

B

αK

6

=

B

K δ I

0

K δ J

0

and

I

t

Z

0

J δ K

0

K

0

u

B

α

(

I

t

Z

0

J

)

6

=

B

K

0

u

B

(

αI

t

αJ

)

6

=

B

(

K

0

u

B

αI

)

t

(

K

0

u

B

αJ

)

6

=

B

K

0

u

B

αI

6

=

B

K

0

u

B

αJ

6

=

B

I δ K

0

J δ K

0

.

That is the formulas (

21

are true.

Accordingly the above

δ

can be continued to the relation [

f

] for some

f

pFCD

(

A

,

B

).

X

Z

0

, Y

Z

1

: (

Y

u

B

h

f

i

X

6

=

B

X

[

f

]

Y

Y

u

B

αX

6

=

B

),

consequently

X

Z

0

:

αX

=

h

f

i

X

because our filtrator is with separable core.

So

h

f

i

is a continuation of

α

.

Theorem

1514

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices. If

α

B

Z

0

,

β

A

Z

1

are functions such that

Y

6

αX

X

6

βY

for every

X

Z

0

,

Y

Z

1

, then there exists exactly one pointfree funcoid

f

:

A

B

such

that

h

f

i|

Z

0

=

α

,

f

1

|

Z

1

=

β

.

Proof.

Prove

α

(

I

t

J

) =

αI

t

αJ

. Really,

Y

6

α

(

I

t

J

)

I

t

J

6

βY

I

6

βY

J

6

βY

Y

6

αI

Y

6

αJ

Y

6

αI

t

αJ

. So

α

(

I

t

J

) =

αI

t

αJ

by star-separability. Similarly

β

(

I

t

J

) =

βI

t

βJ

.

Thus by the theorem above there exists a pointfree funcoid

f

such that

h

f

i|

Z

0

=

α

,

f

1

|

Z

1

=

β

.

That this pointfree funcoid is unique, follows from the above.

Proposition

1515

.

Let (Src

f,

Z

0

) be a primary filtrator over a bounded dis-

tributive lattice and (Dst

f,

Z

1

) be a primary filtrator over boolean lattice. If

S

is a

generalized filter base on Src

f

then

h

f

i

d

Src

f

S

=

d

Dst

f

hh

f

ii

S

for every pointfree

funcoid

f

.

Proof.

First the meets

d

Src

f

S

and

d

Dst

f

hh

f

ii

S

exist by corollary

518

.

(Src

f,

Z

0

) is a binarily meet-closed filtrator by corollary

536

and with separable

core by theorem

537

thus we can apply theorem

1512

(up

x

6

=

is obvious).

h

f

i

d

Src

f

S

v h

f

i

X

for every

X

S

because Dst

f

is strongly separable by

proposition

579

and thus

h

f

i

d

Src

f

S

v

d

Dst

f

hh

f

ii

S

.