background image

y

/

Q

i

2

dom

f

RLD

h

f

i

i

Pr

i

RLD

x

, 8

i

2

dom

f

:

Pr

i

RLD

y

/

h

f

i

i

Pr

i

RLD

x

, 8

i

2

dom

f

:

Pr

i

RLD

x

[

f

i

]

Pr

i

RLD

y

,

x

h Q

(

A

)

f

i

y

,

y

/

DQ

(

A

)

f

E

x

.

Thus

DQ

(

A

)

f

E

x

=

Q

i

2

dom

f

RLD

h

f

i

i

Pr

i

RLD

x

.

Corollary 17.194.

f

(

A

)

g

x

=

h

f

i

(

dom

x

)

RLD

h

g

i

(

im

x

)

.

17.14 On products and projections

Conjecture 17.195.

For principal funcoids

Q

(

C

)

and

Q

(

A

)

coincide with the conventional

product of binary relations.

17.14.1 Staroidal product

Let

f

be a staroid, whose form components are boolean lattices.

Denition 17.196.

Staroidal projection

of a staroid

f

is the lter Pr

k

Strd

f

corresponding to the

free star

(

val

f

)

k

¡

i

2

(

arity

f

)

n f

k

g

: 1

(

form

f

)

i

:

Proposition 17.197.

Pr

k

GR

Q

Strd

x

=

?x

k

if

x

is an indexed family of proper lters, and

k

2

dom

x

.

Proof.

Pr

k

GR

Q

Strd

x

=

Pr

k

L

2

`

i

2

dom

x

form

x

i

j 8

i

2

dom

x

:

x

i

/

L

i

 

=

(used the fact that

x

i

are proper lters)

=

f

l

2

form

x

k

j

x

k

/

l

g

=

?x

k

.

Proposition 17.198.

Pr

k

Strd

Q

Strd

x

=

x

k

if

x

is an indexed family of proper lters, and

k

2

dom

x

.

Proof.

@

Pr

k

Strd

Q

Strd

x

=

¡

val

Q

Strd

x

k

¡

 i

2

(

dom

x

)

n f

k

g

: 1

(

form

x

)

i

=

X

2

¡

form

Q

Strd

x

k

j

¡

i

2

(

dom

x

)

n f

k

g

: 1

(

form

x

)

i

[ f

(

k

;

X

)

g 2

GR

Q

Strd

x

 

=

X

2

Base

x

k

j

¡

8

i

2

(

dom

x

)

n f

k

g

: 1

(

form

x

)

i

/

x

i

^

X

/

x

k

 

=

f

X

2

Base

x

k

j

X

/

x

k

g

=

@ x

k

.

Consequently Pr

k

Strd

Q

Strd

x

=

x

k

.

17.14.2 Cross-composition product of pointfree funcoids

Denition 17.199.

Zero

pointfree funcoid from a poset

A

to to a poset

B

is such a pointfree

funcoid

A

!

B

that

h

f

i

x

is a least element of

B

for every

x

2

A

.

Proposition 17.200.

A pointfree funcoid

f

is zero i

[

f

]=

;

.

Proof.

Direct implication is obvious.

Let now

[

f

]=

;

. Then

h

f

i

x

y

for every

x

2

Src

f

,

y

2

Dst

f

and thus

h

f

i

x

 h

f

i

x

. It is possible

only when

h

f

i

x

= 0

Dst

f

.

Corollary 17.201.

A pointfree funcoid is zero i its reverse is zero.

Proposition 17.202.

Values

x

i

(for every

i

2

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

2

n

) is an

atomic lattice and every Dst

f

i

is an atomic poset with greatest element.

Proof.

DQ

(

C

)

x

EQ

Strd

p

=

Q

i

2

n

Strd

h

x

i

i

p

i

by theorem

17.154

.

232

Multifuncoids and staroids