background image

17.11. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

256

Remark

1330

.

We can carry definitions (such as below defined cross-

composition product) from categories with star-morphisms into plain dagger cat-

egories. This allows us to research properties of cross-composition product of in-

dexed families of morphisms for categories with star-morphisms without separately

considering the special case of dagger categories and just binary star-composition

product.

17.10.1. Abrupt of quasi-invertible categories with star-morphisms.

Definition

1331

.

The abrupt partially ordered precategory of a partially or-

dered precategory with star-morphisms is the abrupt precategory with the following

order of morphisms:

Indexed (by arity

m

for some

m

M

) families of morphisms of

C

are

ordered as function spaces of posets.

Star-morphisms (which are morphisms None

Obj

m

for some

m

M

)

are ordered in the same order as in the precategory with star-morphisms.

Morphisms None

None which are only the identity morphism ordered

by the unique order on this one-element set.

We need to prove it is a partially ordered precategory.

Proof.

It trivially follows from the definition of partially ordered precategory

with star-morphisms.

17.11. 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.

17.11.1. Mapping a morphism into a pointfree funcoid.

Definition

1332

.

Let’s define the pointfree funcoid

χf

for every morphism

f

or 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

1333

.

h

χf

i

= (

f

◦ −

) is the Mor-functor

1

Mor(

f,

) and we can apply

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

Obvious

1334

.

h

χ

(

g

f

)

i

a

=

g

f

a

for composable morphisms

f

and

g

or

a quasi-invertible category.

17.11.2. General cross-composition product.

Definition

1335

.

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 StarMor(

λi

dom

f

: Src

f

i

)

to StarMor(

λ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.

1

Also called Hom-functor.