 21.10. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

338

We need to prove it is a partially ordered precategory.

Proof.

It trivially follows from the definition of partially ordered precategory

with star-morphisms.

21.10. Product of an arbitrary number of funcoids

In this section it will be defined a product of an arbitrary (possibly infinite)

indexed family of funcoids.

21.10.1. Mapping a morphism into a pointfree funcoid.

Definition

1722

.

Let’s define the pointfree funcoid

χf

for every morphism

f

of a quasi-invertible category:

h

χf

i

a

=

f

a

and

(

χf

)

1

b

=

f

b.

We need to prove it is really a pointfree funcoid.

Proof.

b

6 h

χf

i

a

b

6

f

a

a

6

f

b

a

6

(

χf

)

1

b

.

Remark

1723

.

h

χf

i

= (

f

◦−

) is the Hom-functor Hom(

f,

) and we can apply

Yoneda lemma to it. (See any category theory book for definitions of these terms.)

Obvious

1724

.

h

χ

(

g

f

)

i

a

=

g

f

a

for composable morphisms

f

and

g

or

a quasi-invertible category.

21.10.2. General cross-composition product.

Definition

1725

.

Let fix a quasi-invertible category with with star-morphisms.

If

f

is an indexed family of morphisms from its base category, then the pointfree

funcoid

Q

(

C

)

f

(

cross-composition product

of

f

) from StarHom(

λi

dom

f

: Src

f

i

)

to StarHom(

λi

dom

f

: Dst

f

i

) is defined by the formulas (for all star-morphisms

a

and

b

of these forms):

*

(

C

)

Y

f

+

a

= StarComp(

a, f

) and

*

(

C

)

Y

f

1

+

b

= StarComp(

b, f

)

.

It is really a pointfree funcoid by the definition of quasi-invertible category with

star-morphisms.

Theorem

1726

.

Q

(

C

)

g

Q

(

C

)

f

=

Q

(

C

)

i

n

(

g

i

f

i

) for every

n

-indexed

families

f

and

g

of composable morphisms of a quasi-invertible category with star-

morphisms.

Proof.

D

Q

(

C

)

i

n

(

g

i

f

i

)

E

a

=

StarComp(

a, λi

n

:

g

i

f

i

)

=

StarComp(StarComp(

a, f

)

, g

) and

*

(

C

)

Y

g

(

C

)

Y

f

+

a

=

*

(

C

)

Y

g

+*

(

C

)

Y

f

+

a

= StarComp(StarComp(

a, f

)

, g

)

.

The rest follows from symmetry.

Corollary

1727

.

Q

(

C

)

f

k

1

. . .

Q

(

C

)

f

0

=

Q

(

C

)

i

n

(

f

k

1

. . .

f

0

) for

every

n

-indexed families

f

0

, . . . , f

n

1

of composable morphisms of a quasi-invertible

category with star-morphisms.

Proof.

By math induction.