background image

Proposition 176.

Pr

k

GR

Q

Strd

x

=

⋆x

k

.

Proof.

Pr

k

GR

Q

Strd

x

=

Pr

k

{

L

dom

x

| ∀

i

dom

x

:

x

i

L

i

}

= ?? =

{

l

|

x

k

l

}

=

⋆x

k

.

Proposition 177.

Pr

k

Strd

Q

Strd

x

=

x

k

if

x

is an indexed family of proper filters, and

k

dom

x

.

Proof.

Pr

k

Strd

Q

Strd

x

=

 Q

Strd

x

k

λi

(

dom

x

)

\ {

k

}

: 1

(

form

x

)

i

.

Thus

Pr

k

Strd

Q

Strd

x

=

val

Q

Strd

x

k

λ i

(

dom

x

)

\ {

k

}

: 1

(

form

x

)

i

=

X

form

Q

Strd

x

k

|

λi

(

dom

x

)

\ {

k

}

: 1

(

form

x

)

i

∪ {

(

k

;

X

)

} ∈

GR

Q

Strd

x

 

=

X

Base

x

k

| ∀

i

(

dom

x

)

\ {

k

}

: 1

(

form

x

)

i

x

i

X

x

k

 

=

{

X

Base

x

k

|

X

x

k

}

=

∂ x

k

.

Consequently Pr

k

Strd

Q

Strd

x

=

x

k

.

15.2 Cross-composition product of pointfree funcoids

Zero morphisms of the category of pointfree funcoids are ??.

Proposition 178.

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 if Src

f

i

(for every

i

n

) is an

atomic lattice and every Dst

f

i

has greatest element.

Proof.

D

Q

(

C

)

x

E

Q

Strd

p

=

Q

i

n

FCD

h

x

i

i

p

i

by the theorem 145.

Since

x

i

0

there exist

p

such that

h

x

i

i

p

i

0

. Take

k

n

,

p

i

=

p

i

for

i

k

and

p

k

=

q

for an

arbitrary value

q

; then (using the staroidal projections from the previous subsection)

h

x

k

i

q

=

Pr

k

Strd

Y

i

n

FCD

h

x

i

i

p

i

=

Pr

k

Strd

*

Y

(

C

)

x

+

Y

Strd

p

.

So the value of

x

can be restored from

Q

(

C

)

x

by this formula.

15.3 Subatomic product

Proposition 179.

Values

x

i

(for every

i

dom

x

) can be restored from the value of

Q

(

A

)

x

provided that

x

is an indexed family of non-zero funcoids.

Proof.

Fix

k

dom

f

. Let for some filters

x

and

y

a

=

(

1

F

(

Base

(

x

))

if

i

k

;

x

if

i

=

k

and

b

=

(

1

F

(

Base

(

y

))

if

i

k

;

y

if

i

=

k.

Then

a

k

[

x

k

]

b

k

⇔ ∀

i

dom

f

:

a

i

[

x

i

]

b

i

Q

RLD

a

h

Q

(

A

)

x

i

Q

RLD

b

. So we have restored

x

k

from

Q

(

A

)

x

.

Conjecture 180.

For every funcoid

f

:

Q

A

Q

B

(where

A

and

B

are indexed families of sets)

there exists a funcoid Pr

k

(

A

)

f

defined by the formula

x

h

Pr

k

(

A

)

f

i

y

Y

RLD

  (

1

F

(

Base

(

x

))

if

i

k

;

x

if

i

=

k

!

[

f

]

Y

RLD

  (

1

F

(

Base

(

y

))

if

i

k

;

y

if

i

=

k.

!

for:

1. every filters

x

and

y

;

2. every principal filters

x

and

y

;

3. every atomic filters

x

and

y

.

On products and projections

29