 19.7. MORE ON COMPOSITION OF POINTFREE FUNCOIDS

296

similarly

X δ

0

I

t

J

X δ

0

I

X δ

0

J

. Let’s continue

δ

0

till a funcoid

f

(by the

theorem

1513

):

X

[

f

]

Y ⇔ ∀

X

up

Z

0

X

, Y

up

Z

1

Y

:

X δ

0

Y.

The reverse of (

26

implication is trivial, so

X

up

Z

0

a, Y

up

Z

1

b

x

atoms

A

X, y

atoms

B

Y

:

x δ y

a δ b

;

X

up

Z

0

a, Y

up

Z

1

b

x

atoms

A

X, y

atoms

B

Y

:

x δ y

X

up

Z

0

a, Y

up

Z

1

b

:

X δ

0

Y

a

[

f

]

b.

So

a δ b

a

[

f

]

b

, that is [

f

] is a continuation of

δ

.

Theorem

1550

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices. If

R

P

pFCD

(

A

,

B

) and

x

atoms

A

,

y

atoms

B

, then

1

.

h

d

R

i

x

=

d

f

R

h

f

i

x

;

2

.

x

[

d

R

]

y

⇔ ∀

f

R

:

x

[

f

]

y

.

Proof.

2

Let denote

x δ y

⇔ ∀

f

R

:

x

[

f

]

y

.

X

up

Z

0

a, Y

up

Z

1

b

x

atoms

A

X, y

atoms

B

Y

:

x δ y

f

R, X

up

Z

0

a, Y

up

Z

1

b

x

atoms

A

X, y

atoms

B

Y

:

x

[

f

]

y

f

R, X

up

Z

0

a, Y

up

Z

1

b

:

X

[

f

]

Y

f

R

:

a

[

f

]

b

a δ b.

So by theorem

1549

,

δ

can be continued till [

p

] for some

p

pFCD

(

A

,

B

).

For every

q

pFCD

(

A

,

B

) such that

f

R

:

q

v

f

we have

x

[

q

]

y

⇒ ∀

f

R

:

x

[

f

]

y

x δ y

x

[

p

]

y

, so

q

v

p

. Consequently

p

=

d

R

.

From this

x

[

d

R

]

y

⇔ ∀

f

R

:

x

[

f

]

y

.

1

From the former

y

atoms

B

D

l

R

E

x

y

u

D

l

R

E

x

6

=

B

⇔ ∀

f

R

:

y

u h

f

i

x

6

=

B

y

\

atoms

B

h

f

i

x

f

R

y

atoms

l

h

f

i

x

f

R

for every

y

atoms

B

.

B

is atomically separable by the corollary

582

Thus

h

d

R

i

x

=

d

f

R

h

f

i

x

.

19.7. More on composition of pointfree funcoids

Proposition

1551

.

[

g

f

] = [

g

]

◦ h

f

i

=

g

1

1

[

f

] for every composable

pointfree funcoids

f

and

g

.

Proof.

For every

x

A

,

y

B

x

[

g

f

]

y

y

6 h

g

f

i

x

y

6 h

g

ih

f

i

x

⇔ h

f

i

x

[

g

]

y

x

([

g

]

◦ h

f

i

)

y.

Thus [

g

f

] = [

g

]

◦ h

f

i

.

[

g

f

] =

(

f

1

g

1

)

1

=

f

1

g

1

1

= (

f

1

g

1

)

1

=

g

1

1

[

f

]

.