 17.10. STAR CATEGORIES

255

Compositions of morphisms are defined by the formulas:

g

f

=

λi

dom

f

:

g

i

f

i

for our indexed families

f

and

g

of

morphisms;

f

m

= StarComp(

m

;

f

) for

m

M

and a composable indexed family

f

;

m

id

None

=

m

for

m

M

;

id

None

id

None

= id

None

.

Identity morphisms for an object

X

are:

λi

X

: id

X

i

if

X

6

= None;

id

None

if

X

= None.

Proof.

We need to prove it is really a category.

We need to prove:

1

. Composition is associative.

2

. Composition with identities complies with the identity law.

Really:

1

(

h

g

)

f

=

λi

dom

f

: (

h

i

g

i

)

f

i

=

λi

dom

f

:

h

i

(

g

i

f

i

) =

h

(

g

f

);

g

(

f

m

) = StarComp(StarComp(

m

;

f

);

g

) =

StarComp(

m

;

λi

arity

m

:

g

i

f

i

) = StarComp(

m

;

g

f

) = (

g

f

)

m

;

f

(

m

id

None

) =

f

m

= (

f

m

)

id

None

.

2

.

m

id

None

=

m

; id

Dst

m

m

= StarComp(

m

;

λi

arity

m

: id

Obj

m

i

) =

m

.

Remark

1327

.

I call the above defined category

abrupt category

because (ex-

cluding identity morphisms) it allows composition with an

m

M

only on the left

(not on the right) so that the morphism

m

is “abrupt” on the right.

FiXme

: Need to be defined easier. Is it defined earlier?

By

J

x

0

;

. . .

;

x

n

1

K

I denote

an

n

-tuple.

Definition

1328

.

Precategory with star morphisms

induced

by a dagger pre-

category

C

is:

The base category is

C

.

Star-morphisms are morphisms of

C

.

arity

f

=

{

0

,

1

}

.

Obj

m

=

J

Src

m

; Dst

m

K

.

StarComp(

m

;

J

f

;

g

K

) =

g

m

f

.

Let prove it is really a precategory with star-morphisms.

Proof.

We need to prove the associativity law:

StarComp(StarComp(

m

;

J

f

;

g

K

);

J

p

;

q

K

) = StarComp(

m

;

J

p

f

;

q

g

K

)

.

Really,

StarComp(StarComp(

m

;

J

f

;

g

K

);

J

p

;

q

K

) = StarComp(

g

m

f

;

J

p

;

q

K

) =

q

g

m

f

p

=

q

g

m

(

p

f

)

= StarComp(

m

;

J

p

f

;

q

g

K

)

.

Definition

1329

.

Category with star morphisms

induced

by a dagger category

C

is the above defined precategory with star-morphisms.

That it is a category (the law of composition with identity) is trivial.