background image

15.3. POINTFREE FUNCOID AS CONTINUATION

202

Proposition

1078

.

(

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

g

)

f

)

1

=

f

1

(

h

g

)

1

=

f

1

g

1

h

1

=

(

g

f

)

1

h

1

=

(

h

(

g

f

))

1

.

15.3. Pointfree funcoid as continuation

Proposition

1079

.

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

(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

)

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

(Dst

f

;

Z

)

y

:

Y

6 h

f

i

x

⇔ ∀

Y

up

(Dst

f

;

Z

)

y

:

x

[

f

]

Y.

Corollary

1080

.

Let

f

be 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

1081

.

Let

f

be a pointfree funcoid. Let (Src

f

;

Z

0

) be a finitely

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

x

Src

f

: up

(Src

f

;

Z

0

)

x

6

=

and (Dst

f

;

Z

1

) is a primary filtrator over a boolean lattice.

h

f

i

x

=

Dst

f

l

hh

f

ii

up

(Src

f

;

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

(Src

f

;

Z

0

)

x

:

X

[

f

]

y

⇔ ∀

X

up

(Src

f

;

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

(Src

f

;

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

(Src

f

;

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

(Src

f

;

Z

0

)

x

;

A

u

Z

0

B

up

(Src

f

;

Z

0

)

x

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

311

and

R v P u

Dst

f

Q

for

R

=

h

f

i

(

A

u

Z

0

B

)

V

because Dst

f

is separable

by obvious

403

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

388

That is

X

up

(Src

f

;

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

(Src

f

;

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

(Src

f

;

Z

0

)

x

6

=

Dst

f

.