background image

Theorem 21.

(

g

f

)

1

=

f

1

g

1

for every composable pointfree funcoids

f

and

g

.

Proof.

h

(

g

f

)

1

i

=

h

f

1

i ◦ h

g

1

i

=

h

f

1

g

1

i

;

h

((

g

f

)

1

)

1

i

=

h

g

f

i

=

h

(

f

1

g

1

)

1

i

.

Proposition 22.

(

h

g

)

f

=

h

(

g

f

)

for every composable pointfree funcoids

f

,

g

,

h

.

Proof.

h

(

h

g

)

f

i

=

h

h

g

i ◦ h

f

i

=

h

h

i ◦ h

g

i ◦ h

f

i

=

h

h

i ◦ h

g

f

i

=

h

h

(

g

f

)

i

.

h

((

h

g

)

f

)

1

i

=

h

f

1

(

h

g

)

1

i

=

h

f

1

g

1

h

1

i

=

h

(

g

f

)

1

h

1

i

=

h

(

h

(

g

f

))

1

i

.

3.3 Pointfree funcoid as continuation

Proposition 23.

Let

f

is 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

(

Src

f

;

Z

)

x

:

X

[

f

]

y

.

2. If

(

Dst

f

;

Z

)

is a filtrator with separable core then

x

[

f

]

y

⇔ ∀

Y

up

(

Dst

f

;

Z

)

x

:

x

[

f

]

Y

.

Proof.

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

x

[

f

]

y

y

Dst

f

h

f

i

x

⇔ ∀

Y

up

y

:

Y

Dst

f

h

f

i

x

⇔ ∀

Y

up

y

:

x

[

f

]

Y

.

Corollary 24.

Let

f

is a pointfree funcoid and

(

Src

f

;

Z

0

)

,

(

Dst

f

;

Z

1

)

are filtrators with separable

core. Then

x

[

f

]

y

⇔ ∀

X

up

(

Src

f

;

Z

0

)

x, Y

up

(

Dst

f

;

Z

1

)

y

:

X

[

f

]

Y .

Proof.

Apply the proposition twice.

Theorem 25.

Let

f

be a pointfree funcoid. Let

(

Src

f

;

Z

0

)

is a finitely meet-closed filtrator with

separable core and

(

Dst

f

;

Z

1

)

is a primary filtrator over a distributive lattice.

h

f

i

x

=

\

Dst

f

hh

f

ii

up

(

Src

f

;

Z

)

x.

Proof.

By the previous proposition for every

y

Dst

f

:

y

Dst

f

h

f

i

x

x

[

f

]

y

⇔ ∀

X

up

(

Src

f

;

Z

0

)

x

:

X

[

f

]

y

⇔ ∀

X

up

(

Src

f

;

Z

0

)

x

:

y

Dst

f

h

f

i

X.

Let’s denote

W

=

y

Dst

f

h

f

i

X

|

X

up

(

Src

f

;

Z

0

)

x

 

. We will prove that

W

is a generalized filter

base over

Z

1

. To prove this enough to show that

V

=

h

f

i

X

|

X

up

(

Src

f

;

Z

0

)

x

 

is a generalized

filter base.

Let

P

,

Q ∈

V

. Then

P

=

h

f

i

A

,

Q

=

h

f

i

B

where

A, B

up

(

Src

f

;

Z

0

)

x

;

A

Z

0

B

up

(

Src

f

;

Z

0

)

x

(used the fact that it is a finitely meet-closed and the theorem 29 in [3]) and

R ⊆ P ∩

Dst

f

Q

for

R

=

h

f

i

(

A

Z

0

B

)

V

. So

V

is a generalized filter base and thus

W

is a generalized filter base.

0

Dst

f

W

T

Dst

f

W

 

0

Dst

f

by the properties of generalized filter bases. That is

X

up

(

Src

f

;

Z

0

)

x

:

y

Dst

f

h

f

i

X

0

Dst

f

y

Dst

f

\

Dst

f

hh

f

ii

up

(

Src

f

;

Z

0

)

x

0

Dst

f

.

Comparing with the above,

y

Dst

f

h

f

i

x

0

Dst

f

y

Dst

f

T

Dst

f

hh

f

ii

up

(

Src

f

;

Z

0

)

x

0

Dst

f

. So

h

f

i

x

=

T

Dst

f

hh

f

ii

up

(

Src

f

;

Z

0

)

x

because Dst

f

is separable.

Theorem 26.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

are primary filtrators over boolean lattices.

1. A function

α

B

Z

0

conforming to the formulas (for every

I , J

Z

0

)

α

0

Z

0

= 0

B

,

α

(

I

Z

0

J

) =

αI

B

αJ

4

Section 3