COHERENCE AND NON-COMMUTATIVE DIAGRAMS IN CLOSED CATEGORIES 9
which is allowable. Then m is equal to the composite
A (b'^pu^
([XY]BI)BW
sSl
Ym
_L^B
which is of type , contrary to the hypothesis. So X is non-constant. D
THEOREM 5. Let h,hf :T - S be allowable natural transformations with [~ h =
ThT. If (h,h')^ , then h = h' .
Proof: Suppose (h,h')^^ . To show h = h', we do induction on r (h) = r(h'),
following the idea of the proof of Theorem 2.4 of [11] with appropriate
modifications and with references to the proof of Proposition C of [18]
for additional details. Suppose the theorem is true for all smaller values,
if any, of r(h). Using the cut elimination theorem for allowable natural
transformations, we consider the possible cases according to the form of
h and h'. The assumption (in the proof of Theorem 2.4 in [11] and in the
proof of Proposition C in [18]) that T and S have no constant prime fac-
tors is replaced here by the observation that, if [X,Y] is a constant
prime factor of T or S, then, via |~ h and the empty graph [X,Y]— I or
I —- [X,Y], Proposition B of [18] implies that h and hT are of type S;
so, in case no one of h and h' is of type ®, T and S have no constant
prime factors.
If both h and h* are central, then h = hf by the known facts about
centrals (p.xiii, or Theorem 4.9 of [11]); the hypothesis (h,h,)^)V is
trivial in this case.
If one of h and h', say h, is of the form yrr(f) with y central and
f allowable, then y_1h = ir(f) and y'V = 7r(f) for = 7r"1(y"1h') allow-
able; then Tf = rf1, and (f,f*)^^ by Y4. So, by induction, f = £f and
hence h = h'.
If one of h and h1, say h, is of the form y(fSg)x with x,y central
and f,g allowable non-trivial, we have y hx~ = f(Sg:AKB - CSD for some
shapes A,B,C,D. Then r(y_1hfx_1) = TCy^hx"1) = rfSSTg; so, by Proposition
B of [18],y h'x = f'Sg' for allowable natural transformations fT:A--C
and g':B-vD with Tf = Tf and Tg = Tg'. If (f,f')^W, then, by induction,
£ = £f; similarly, if (g,gT)^, then g = gr . So, if at least one of (f,ff)
and (g,g') is in K , then any one of (f,fT) and (g,g!) which is not in Itf
Previous Page Next Page