Michael Shulman
closed category

In the definition of closed category, the hom-sets C(X,Y)C(X,Y) for XIX\neq I are redundant information, being isomorphic to C(I,[X,Y])C(I,[X,Y]). If we remove them, we obtain an axiomatization of a closed category that doesn’t assume from the outset that we are given a category at all.

I will use the Eilenberg-Kelly notion of closed category, with a given “underlying-set functor” U:CSetU:C\to Set such that U([X,Y])=C(X,Y)U([X,Y]) = C(X,Y) (and another axiom); this enables us to simply replace C(X,Y)C(X,Y) everywhere that it appears by U([X,Y])U([X,Y]). I will also make two notational changes, writing XYX\Rightarrow Y instead of [X,Y][X,Y], and writing xXx \Vdash X instead of xU(X)x\in U(X).

The data we are given is now the following. We start with the following stuff:

  • A set of objects X,Y,Z,X,Y,Z,\dots.
  • For any two objects X,YX,Y, an object XYX\Rightarrow Y.
  • An object II.
  • For any object XX, a set of “realizers” denoted xXx\Vdash X.

Add the following structure:

  • For any fXYf\Vdash X\Rightarrow Y and g:YZg:Y\Rightarrow Z a composite gfXZg\circ f \Vdash X\Rightarrow Z (composition in the category CC).
  • For any XX a realizer 1 XXX1_X \Vdash X\Rightarrow X (identities in the category CC).
  • For any fXXf\Vdash X' \Rightarrow X and gYYg\Vdash Y \Rightarrow Y', a realizer (fg)(XY)(XY)(f\Rightarrow g) \Vdash (X\Rightarrow Y) \Rightarrow (X' \Rightarrow Y') (functoriality of [,][-,-]).
  • For any fXYf\Vdash X\Rightarrow Y and xXx\Vdash X, a realizer fxYf\cdot x \Vdash Y (functoriality of UU).
  • For any XX, realizers i XX(IX)i_X \Vdash X \Rightarrow (I \Rightarrow X) and i X(IX)Xi'_X \Vdash (I\Rightarrow X) \Rightarrow X.
  • For any XX, a realizer j XI(XX)j_X \Vdash I \Rightarrow (X\Rightarrow X).
  • For any X,Y,ZX,Y,Z, a realizer L YZ X(YZ)((XY)(XZ))L^X_{Y Z} \Vdash (Y\Rightarrow Z) \Rightarrow ((X\Rightarrow Y) \Rightarrow (X \Rightarrow Z)).

And impose the following axioms:

  • h(gf)=(hg)fh\circ (g\circ f) = (h\circ g)\circ f
  • f1 X=f=1 Yff \circ 1_X = f = 1_Y \circ f
  • (1 X1 Y)=1 XY(1_X \Rightarrow 1_Y) = 1_{X\Rightarrow Y}
  • (hk)(fg)=(hf)(gk)(h \Rightarrow k) \circ (f\Rightarrow g) = (h \circ f) \Rightarrow (g\circ k)
  • 1 Xx=x1_X \cdot x = x
  • (gf)x=g(fx)(g\circ f) \cdot x = g \cdot (f\cdot x)
  • (hf)g=fgh(h \Rightarrow f) \cdot g = f\circ g\circ h
  • i Xi X=1 Xi'_X \circ i_X = 1_X and i Xi X=1 IXi'_X \circ i_X = 1_{I\Rightarrow X}
  • i Yf=(1 If)i Xi_Y \circ f = (1_I \Rightarrow f) \circ i_X and (redundantly) i Y(1 If)=fi Xi'_Y \circ (1_I \Rightarrow f) = f \circ i'_X
  • (1 Xf)j X=(f1 Y)j Y(1_X \Rightarrow f) \circ j_X = (f\Rightarrow 1_Y) \circ j_Y
  • (1 YZ((1 Xf)(1 Xg)))L YZ X=L YZ X(fg)(1_{Y\Rightarrow Z} \Rightarrow ((1_X \Rightarrow f) \Rightarrow (1_X \Rightarrow g))) \circ L^X_{Y Z} = L^X_{Y' Z'} \circ (f\Rightarrow g)
  • ((h1 Y)1 XZ)L YZ X=(1 XY(h1 Z))L YZ X((h \Rightarrow 1_Y) \Rightarrow 1_{X\Rightarrow Z}) \circ L^X_{Y Z} = (1_{X'\Rightarrow Y} \Rightarrow (h \Rightarrow 1_Z)) \circ L^{X'}_{Y Z}
  • L YY Xj Y=j XYL^X_{Y Y} \circ j_Y = j_{X\Rightarrow Y}
  • (j X1 XY)L XY X=i XY(j_X \Rightarrow 1_{X\Rightarrow Y}) \circ L^X_{X Y} = i_{X\Rightarrow Y}
  • (i Y1 IZ)L YZ I=(1 Yi Z)(i_Y \Rightarrow 1_{I\Rightarrow Z}) \circ L^I_{Y Z} = (1_{Y} \Rightarrow i_Z)
  • (1 YUL YV X)L UV Y=(L YU X1 (XY)(XV))L (XU),(XV) XYL UV X(1_{Y\Rightarrow U} \Rightarrow L^X_{Y V}) \circ L^Y_{U V} = (L^X_{Y U} \Rightarrow 1_{(X\Rightarrow Y)\Rightarrow (X \Rightarrow V)}) \circ L^{X\Rightarrow Y}_{(X\Rightarrow U),(X\Rightarrow V)} \circ L^X_{U V}
  • i XX1 X=j Xi_{X\Rightarrow X} \cdot 1_X = j_X.

However, this definition still contains redundant data. The most obvious is j Xj_X, which by the last axiom could be simply defined to be i XX1 Xi_{X\Rightarrow X} \cdot 1_X. This was already noted by Eilenberg-Kelly, who also asserted that jj thusly defined is automatically natural (i.e. the axiom (1 Xf)j X=(f1 Y)j Y(1_X \Rightarrow f) \circ j_X = (f\Rightarrow 1_Y) \circ j_Y is redundant). To see this, first note that Lemma 2.2 of EK says that for f(AA)Xf \Vdash (A\Rightarrow A)\Rightarrow X we have (using naturality of ii):

i A(f1 A)=(i Af)1 A=((1 If)i AA)1 A=(1 If)(i AA1 A)=(1 If)j A=fj A.i_A \cdot (f\cdot 1_A) = (i_A \circ f) \cdot 1_A = ((1_I \Rightarrow f) \circ i_{A\Rightarrow A}) \cdot 1_A = (1_I \Rightarrow f) \cdot (i_{A\Rightarrow A} \cdot 1_A) = (1_I \Rightarrow f) \cdot j_A = f\circ j_A.

Now Proposition 2.4 says for any gABg\Vdash A\Rightarrow B we have (applying 2.2 with f=(1 Ag)f = (1_A \Rightarrow g) and (g1 B)(g \Rightarrow 1_B) respectively, and using the axiom (hf)g=fgh(h \Rightarrow f) \cdot g = f\circ g\circ h):

(1 Ag)j A=i A((1 Ag)1 A)=i Ag (1_A \Rightarrow g) \circ j_A = i_A \cdot ((1_A \Rightarrow g)\cdot 1_A) = i_A \cdot g
(g1 B)j A=i A((g1 B)1 A)=i Ag (g \Rightarrow 1_B) \circ j_A = i_A \cdot ((g \Rightarrow 1_B) \cdot 1_A) = i_A \circ g

so that (1 Ag)j A=(g1 B)j A(1_A \Rightarrow g) \circ j_A = (g \Rightarrow 1_B) \circ j_A, i.e. jj is natural (which we did not use in this proof).

We note the other basic propositions of EK in our notation. Prop 2.5 says i IA=(1 Ii A)i_{I\Rightarrow A} = (1_I \Rightarrow i_A), since when precomposed with the isomorphism i Ai_A they are equal by naturality. Prop 2.6 says for fIAf\Vdash I\Rightarrow A we have i Af=i IAfi_A \circ f = i_{I\Rightarrow A} \cdot f, by acting on ff with Prop 2.5. Taking A=IA=I and f=1f=1 then gives Prop 2.7: j I=i Ij_I = i_I. In particular, j Ij_I is an isomorphism, so putting X=YX=Y in its naturality we get Prop 2.8: (1 If)=(f1 I)(1_I \Rightarrow f) = (f\Rightarrow 1_I) for any fIIf\Vdash I \Rightarrow I. By acting on gIIg\Vdash I\Rightarrow I this gives Prop 2.9: fg=gff\circ g = g\circ f, i.e. the monoid of endomorphisms of II is commutative.

The next most obvious redundancy is that the axiom (hf)g=fgh(h \Rightarrow f) \cdot g = f\circ g\circ h says that composition can be defined in terms of the “functorial” action of \Rightarrow and the “action” \cdot. However, using this axiom to define binary composition would involve a seemingly-arbitrary choice of which of f,g,hf,g,h to take as an identity. A better option is to note that by Proposition 2.3 in Eilenberg-Kelly, the axiom L YY Xj Y=j XYL^X_{Y Y} \circ j_Y = j_{X\Rightarrow Y} is equivalent to

  • L YZ Xf=(1 Xf)L^X_{Y Z} \cdot f = (1_X \Rightarrow f) for any fYZf\Vdash Y\Rightarrow Z.

and therefore we also have

(L YZ Xf)g=(1 Xf)g=fg1 X=fg (L^X_{Y Z} \cdot f) \cdot g = (1_X \Rightarrow f) \cdot g = f\circ g \circ 1_X = f\circ g

for any fYZf\Vdash Y\Rightarrow Z and gXYg\Vdash X \Rightarrow Y. Thus, the natural definition of fgf\circ g is as (L YZ Xf)g(L^X_{Y Z} \cdot f) \cdot g.

I expect, with this definition, that it should be possible to prove associativity and unitality of composition, and naturality of ii, from the corresponding “internalized” properties for L YZ XL^X_{Y Z}.

We may be able to define (fg)(f\Rightarrow g) in terms of the other data; we have already noted that (1f)(1\Rightarrow f) is definable, so all that remains to define is (f1)(f\Rightarrow 1). In the symmetric case, there is no problem; in the non-symmetric case we argue that (f1)=L YZ Xev f=(L (YZ),(XZ) (XY)(XZ)ev f)L YZ X(f\Rightarrow 1) = L^X_{Y Z} \circ ev_f = (L^{(X\to Y)\to (X\to Z)}_{(Y\to Z),(X\to Z)} \cdot ev_f) \cdot L^X_{Y Z}.

Last revised on May 31, 2018 at 18:30:48. See the history of this page for a list of all contributions to it.