21.13. ON PRODUCTS AND PROJECTIONS

355

Proof.

Pr

k

GR

Strd

Y

x

=

Pr

k

L

form

x

i

dom

x

:

x

i

6

L

i

=

(used the fact that

x

i

are proper filters)

l

(form

x

)

k

x

k

6

l

=

?x

k

.

Proposition

1793

.

Pr

Strd

k

Q

Strd

x

=

x

k

if

x

is an indexed family of proper

filters, and

k

dom

x

.

Proof.

Strd

Pr

k

Strd

Y

x

=

val

Strd

Y

x

!

k

(

λi

(dom

x

)

\ {

k

}

:

>

(form

x

)

i

) =

X

form

Q

Strd

x

k

(

λi

(dom

x

)

\ {

k

}

:

>

(form

x

)

i

)

∪ {

(

k, X

)

} ∈

GR

Q

Strd

x

=

X

Base

x

k

(

i

(dom

x

)

\ {

k

}

:

>

(form

x

)

i

6

x

i

)

X

6

x

k

=

X

Base

x

k

X

6

x

k

=

∂x

k

.

Consequently Pr

Strd

k

Q

Strd

x

=

x

k

.

21.13.2. Cross-composition product of pointfree funcoids.

Definition

1794

.

Zero

pointfree funcoid

pFCD

(

A

,

B

)

from a poset

A

to to a

poset

B

is the least pointfree funcoid in the set

pFCD

(

A

,

B

).

Proposition

1795

.

A pointfree funcoid

f

is zero iff [

f

]=

.

Proof.

Direct implication is obvious.

Let now [

f

]=

. Then

h

f

i

x

y

for every

x

Src

f

,

y

Dst

f

and thus

h

f

i

x

h

f

i

x

. It is possible only when

h

f

i

x

=

Dst

f

.

Corollary

1796

.

A pointfree funcoid is zero iff its reverse is zero.

Proposition

1797

.

Values

x

i

(for every

i

dom

x

) can be restored from the

value of

Q

(

C

)

x

provided that

x

is an indexed family of non-zero pointfree funcoids,

Src

f

i

(for every

i

n

) is an atomic lattice and every Dst

f

i

is an atomic poset with

greatest element.

Proof.

D

Q

(

C

)

x

E

Q

Strd

p

=

Q

Strd

i

n

h

x

i

i

p

i

by theorem

1749

.

Since

x

i

is non-zero there exist

p

such that

h

x

i

i

p

i

is non-least. Take

k

n

,

p

0

i

=

p

i

for

i

6

=

k

and

p

0

k

=

q

for an arbitrary value

q

; then (using the staroidal

projections from the previous subsection)

h

x

k

i

q

=

Strd

Pr

k

Strd

Y

i

n

h

x

i

i

p

0

i

=

Strd

Pr

k

*

(

C

)

Y

x

+

Strd

Y

p

0

.