background image

15.3. POINTFREE FUNCOID AS CONTINUATION

204

Combining the equivalencies we get

Y u

α

0

X 6

=

B

⇔ X

δ

0

Y

. Analogously

X u

β

0

Y 6

=

A

⇔ X

δ

0

Y

. So

Y u

α

0

X 6

=

B

⇔ X u

β

0

Y 6

=

A

, that is (

A

;

B

;

α

0

;

β

0

)

is a pointfree funcoid. From the formula

Y u

α

0

X 6

=

B

⇔ X

δ

0

Y

it follows that

[(

A

;

B

;

α

0

;

β

0

)] is a continuation of

δ

.

1

Let define the relation

δ

P

(

Z

0

×

Z

1

) by the formula

X δ Y

Y

u

B

αX

6

=

B

.

That

¬

(

Z

0

δ I

0

) and

¬

(

I δ

Z

1

) is obvious. We have

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

= 0

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

= 0

B

K

0

u

B

αJ

6

=

B

I δ K

0

J δ K

0

.

That is the formulas (

15

are true.

Accordingly the above

δ

can be continued to the relation [

f

] for some

f

FCD

(

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

α

.

Proposition

1083

.

Let (Src

f

;

Z

0

) be a primary filtrator over a bounded dis-

tributive lattice and (Dst

f

;

Z

1

) is a primary filtrator over a 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

374

.

(Src

f

;

Z

0

) is a finitely meet-closed filtrator by proposition

364

and with sepa-

rable core by theorem

379

thus we can apply theorem

1081

(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 separable by obvious

403

and thus

h

f

i

d

Src

f

S

v

d

Dst

f

hh

f

ii

S

.