21.15. CROSS-INNER AND CROSS-OUTER PRODUCT

360

Proof.

a

0

×

RLD

b

0

h

f

×

(

A

)

g

i

a

1

×

RLD

b

1

A

0

a

0

, B

0

b

0

, A

1

a

1

, B

1

b

1

:

A

0

×

B

0

h

f

×

(

A

)

g

i

A

1

×

B

1

.

A

0

×

B

0

h

f

×

(

A

)

g

i

A

1

×

B

1

A

0

×

B

0

h

f

×

(

C

)

g

i

A

1

×

B

1

A

0

[

f

]

A

1

B

0

[

g

]

B

1

.

(Here by

A

0

×

B

0

f

×

(

C

)

g

A

1

×

B

1

I mean

FCD

(Base

a,

Base

b

)

(

A

0

×

B

0

)

f

×

(

C

)

g

FCD

(Base

a,

Base

b

)

(

A

1

×

B

1

).)

Thus it is equivalent to

a

0

[

f

]

a

1

b

0

[

g

]

b

1

that is

a

0

×

FCD

b

0

f

×

(

C

)

g

a

1

×

FCD

b

1

.

(It was used the corollary

1629

.)

Can the above theorem be generalized for the infinitary case?

21.15. Cross-inner and cross-outer product

Let

f

be an indexed family of funcoids.

Definition

1821

.

Q

in

i

dom

f

f

=

Q

(

C

)

i

dom

f

(

RLD

)

in

f

i

(

cross-inner product

).

Definition

1822

.

Q

out

i

dom

f

f

=

Q

(

C

)

i

dom

f

(

RLD

)

out

f

i

(

cross-outer product

).

Proposition

1823

.

Q

in

i

dom

f

f

and

Q

out

i

dom

f

f

are funcoids (not just pointfree

funcoids).

Proof.

They are both morphisms StarHom(

λi

dom

f

: Src

f

i

)

StarHom(

λi

dom

f

: Src

f

i

) for the category of multireloids with star-morphisms,

that is StarHom(

λi

dom

f

: Src

f

i

) is the set of filters on the cartesian product

Q

i

dom

f

Src

f

i

and likewise for StarHom(

λi

dom

f

: Src

f

i

).

Obvious

1824

.

For every funcoids

f

and

g

1

.

f

×

in

g

= (

RLD

)

in

f

×

(

C

)

(

RLD

)

in

g

;

2

.

f

×

out

g

= (

RLD

)

out

f

×

(

C

)

(

RLD

)

out

g

.

Corollary

1825

.

1

.

h

f

×

in

g

i

a

= (

RLD

)

in

g

a

(

RLD

)

in

f

1

;

2

.

h

f

×

out

g

i

a

= (

RLD

)

out

g

a

(

RLD

)

out

f

1

Corollary

1826

.

For every funcoids

f

and

g

and filters

a

and

b

on suitable

sets:

1

.

a

[

f

×

in

g

]

b

b

6

(

RLD

)

in

g

a

(

RLD

)

in

f

1

b

(

RLD

)

in

f

6

(

RLD

)

in

g

a

;

2

.

a

[

f

×

out

g

]

b

b

6

(

RLD

)

out

g

a

(

RLD

)

out

f

1

b

(

RLD

)

out

f

6

(

RLD

)

out

g

a

.

Proposition

1827

.

Knowing that every

f

i

is nonzero, we can restore the values

of

f

i

from the value of

Q

in

i

dom

f

f

.

Proof.

It follows that every (

RLD

)

in

f

i

is nonzero, thus we can restore

each (

RLD

)

in

f

i

from

Q

(

C

)

i

dom

f

(

RLD

)

in

f

i

=

Q

in

i

dom

f

f

and then we know

f

i

=

(

FCD

)(

RLD

)

in

f

i

.

Example

1828

.

The values of

f

and

g

cannot be restored from

f

×

out

g

for

some nonzero funcoids

f

and

g

.