Somewhen in the mid-1980's, Dr. Rossolini gave lectures on Category theory. I didn't give them the attention they deserved but I got the impression they were talking about something significant. I took careful notes but knew I didn't understand it all. One part stuck out as significant (if only because the folk who seemed to understand what was going on seemed to think it so): Yoneda's lemma. That has quietly spurred me on, several times over, to revisit my notes and see whether I can make sense of it yet. It is has become a beacon in the terrain I've been exploring.
The Yoneda lemma relates to natural transformations between functors; and it involves representing homsets using sets. That's why I've taken the time to sort out my understanding of those: so that I can refer to them here.
An arrow land, L, is described as locally small precisely if, for every a in (|L) and w in (L|), Hom(a,w) is a set (which is a kind of collection with good `exactness' properties, designed to avoid undecidabilities). Thus any functor from a locally small arrow world with factorising composition may be expressed in terms of the functions (ie mappings between sets) it induces on homsets.
Consider a factorising composition, &on;, on a locally small arrow world and two arrows, a and w, of that arrow world. We have Hom(a,w) as the set of arrows, f, for which w&on;f&on;a is a valid composition. This induces a function y(a,w) = (Hom(a,w): f-> w&on;f&on;a :Parallel([w,f,a])): from two arrows in our arrow world, our composition generates an arrow in the category, Set, of functions. Now examine (: p-> y(p,w) :), for fixed w, and (: p-> y(a,p) :), for fixed a: they turn out to be transformations.
Proof: I first show that y(a) = ((|&on;)| p->y(a,p) :Set) respects containment relations on:
- Prior
Suppose Prior(p) subsumes Prior(q) and examine Prior(y(a,p)) and Prior(y(a,q)). Now, Prior(y(a,p)) is {functions (: :Hom(a,p))} and Hom(a,p) is Post(a)&intersect;Prior(p), which thus subsumes Hom(a,q). Consequently, an function (: :Hom(a,q)) is trivially (a restriction of) a function (: :Hom(a,p)), so Prior(y(a,p)) subsumes Prior(y(a,q)).
- Post
Suppose Post(p) subsumes Post(q). Post(y(a,p)) is {function m: (m|) subsumes Parallel[a,.,p]} with Parallel[a,.,p] standing for unite( Hom(a,p): f-> Parallel([p,f,a]) |), the collection of arrows parallel to some composable list with a as start and p as end. Thus Parallel[p,.,a] is just {f in (|&on;): Post(f) subsumes Post(p) and Prior(f) subsumes Prior(a)}: and if Post(f) subsumes Post(p), it necessarily subsumes Post(q) also; so f in Parallel[p,.,a] implies f in Parallel[q,.,a]. Thus, for a function m, if (m|) subsumes Parallel[q,.,a] then it also subsumes Parallel[p,.,a]: so m in Post(y(a,q)) implies m in Post(y(a,p)) and Post(y(a,p)) subsumes Post(y(a,q)), just as Post(p) subsumed Post(q).
Thus y(a) is a transform from &on; to Set.
[Aside: If a is an identity, we have y(a,p)&on;y(a,q) = (Hom(a,q): f-> p&on;q&on;f&on;a :) = y(a, p&on;q). Thus y(a,p) is composable (in Set) after y(a,q) precisely if p is composable (in our arrow world) after q: and (: p-> y(a,p) :) respects composition. Thus any identity, a, in (|&on;) gives a functor ((|&on;): p-> y(a,p) :Set).]
Whenever b&on;a and x&on;w are valid compositions, we have y(b&on;a, x&on;w) = (: f-> x&on;w&on;f&on;b&on;a :) = y(a,x)&on;y(b,w). We thus find that y(a) is conjoinable after y(b), whereas a was composable before b: and y(a)*y(b) = y(b&on;a). This makes y a co-functor from &on; to ({transform ((|&on;)| :Set)}: Conjoin :). Conversely, it makes transpose(y) a functor from &on; to ({coTransform ((|&on;)| :Set)}: Contrajoin :) - and `contrajoin' is a synonym for `conjoin'. Thus (: p-> w&on;p :) = transpose(y,w) is a coTransform from &on; to Set.
Thus y is a co-functor from &on; to Transform(&on;, Set) and its transpose, Yoneda = transpose(y), is a functor from &on; to coTransform(&on;, Set). The latter is known as the Yoneda Functor for our given arrow world, &on;. In the following section I abbreviate Yoneda to Y. From the definition of y, we obtain Y(w,a,f) = w&on;f&on;a.
In what follows, `category' means `identified arrow world with factorising associative composition'. For small categories A, W: I'll write
the arrow world of transformations from A to W, with `composition' conjoin, ie *. For any two arrows F, G of Transform(A,W) I'll write
aka Hom(F,G) in Transform(A,W). Likewise, I'll write
in which, for any F, G, naTrans(F,G) retains the meaning Transform(dual-A,W) gives it.
In a locally small category, C, consider any coFunctor, (C|F:Set), and identity, X, in C: Y(X) and F are identities in coTransform(C,Set) and naTrans(Y(X), F) is a homset in coTransform(C,Set); F(X) is an identity in Set, ie a set; (C|T:Set) in naTrans(Y(X),F) maps any identity U in C to a function; T(U) is composable (in Set) between the identities Y(X,U)=y(U,X) and F(U); so T(U) accepts, as input, any mapping (U|:X) and produces, as outputs, members of F(U). In particular, when U=X, X is in (X|:X) and T(X) accepts X as input, with T(X,X) in F(X).
Lemma: in such a case, the mapping b = (naTrans(Y(X),F)| T-> T(X,X) :F(X)) is invertible. This makes naTrans(Y(X),F) isomorphic to F(X) and, in particular, a set.
Proof: define (F(X)| q :coTransform(C,Set)) by x-> (C| g-> (C-Hom(g,X)| f-> F(f&on;g, x) :(F(g)|)) :Set), so q(x,g,f) = F(f&on;g, x) is an output of F(g) - note that (F(g)|) = (F(f&on;g)|) as F(f&on;g) is F(g)&on;F(f). Now, given r&on;s in C, examine q(x,s)&on;Y(X,r) = q(x,s)&on;y(r,X) and F(s)&on;q(x,r).
- q(x,s)&on;y(r,X)
- = (C-Hom(r,X)| f-> q(x,s,f&on;r) = F(f&on;r&on;s, x) :)
- = q(x,r&on;s)
- F(s)&on;q(x,r)
- = (C-Hom(r,X)| f->
- F(s, q(x,r,f))
- = F(s, F(f&on;r, x))
- = (F(s)&on;F(f&on;r))(x)
- = F(f&on;r&on;s, x)
:)- = q(x,r&on;s)
Thus each q(x) is a transformation in naTrans(Y(X),F), so we have (F(X)| q :naTrans(Y(X),F)) antiparallel to b. Next, consider q&on;b and b&on;q.
- for x in F(X)
- (b&on;q)(x) = b(q(x))
- = q(x,X,X)
- = F(X&on;X, x)
- = F(X,x)
- = x, as F(X) is an identity.
- for T in naTrans(Y(X),F)
- (q&on;b)(T) = q(T(X,X))
- = (C| g->
:Set)
- (C-Hom(g,X)| f->
- F(f&on;g, T(X,X))
- = (F(f&on;g)&on;T(X))(X)
but X&on;f = f and F*T = T, so
- = (F(g)&on;T(f))(X) = T(f&on;g, X)
and T = T*Y(X)
- = (T(g)&on;Y(X,f))(X)
:)Now, for f in C-Hom(g,X), Y(X,f)=y(f,X) = (C-Hom(X,X)| u-> u&on;f :) maps X to X&on;f = f, as X is an identity; so T(g)(Y(X,f)(X)) = T(g,f), whence
- = (C| g-> T(g) :) = T
Thus b and q are inverse to one another: QED.
Notice that this at least gives us some homsets of coTransform(C,Set) which are sets, namely those starting at Y(X) for some identity X in C. We don't immediately know that coTransform(C,Set) is even locally small, but this does give us a locally small, full, faithful sub-category, namely Y's image of C.
Proof, that Y is full and faithful (C| :coTransform(C,Set)). We need C to be identified: then we have identities X, U in C with f= X&on;f&on;U and Parallel(Y(f)) is naTrans(Y(X),Y(U)), which is isomorphic to F(X) = Y(U,X) = y(X,U) = C-Hom(X,U). in which context, for any arrow f of C,
- full
- means that, for any coTransform conjoin-parallel (in coTransform(C,Set)) to Y(f), there is an arrow parallel to f which Y maps to the given coTransform.
As q(f,g,k) = Y(U,k&on;g,f) = Y(f,g,k), we have q(f) = Y(f) and q is just Y's restriction to C-Hom(U,X) = C-Parallel(f). Since q is an isomorphism, in Set and hence injective, every natural transformation in Parallel(Y(f)) is Y(h) for some h in Parallel(f), so Y is full.
- faithful
- means that, when f and g are parallel, in C, `Y(f) = Y(g)' implies `f=g'.
Likewise, b(T) = T(X,X), with Y(g)=T=Y(f) and g in Parallel(f). But Y(f,X,X) = f, and b is a function: hence Y(g)=Y(f) gives b(Y(g))=b(Y(f)) which is just g=f. So Y is faithful.
Thus every transformation natural between Y(X) and Y(U) is Y(f) for some (unique) f in C-Hom(X,U). The Yoneda Functor is also known as the Yoneda Embedding: it embeds C fully and faithfully in coTransform(C,Set).
This gives us, for each coFunctor (C|F:Set) and identity X in C, a function, b, in Set. Can we extend this mapping [F,X]->b to accept arbitrary coTransforms, (C|:Set) in place of F, and arrows of C, in place of X ? If so, call the extension B: it's (coTransform(C,Set)×dual-C| B :Set) and we can ask whether it, in turn, is a transform or coTransform: for which we might want to drop the `dual-'. (Recap: an arrow of coTransform(C,Set)×dual-C is a pair, [T,f], with (C|T:Set) a coTransform and f an arrow of C (hence, equally, of dual-C); [T,f]&on;[R,g] is then [T*R, g&on;f]. If we drop `dual-' as noted, the final g&on;f becomes f&on;g. Either way, [T,f]&on;[R,g] is thus valid composition precisely when T*R and g&on;f (or f&on;g) are both valid.)
For F*T*G conjoinable in coTransform(C,Set) with F, G functors; for X&on;f&on;V composable in C with X, V identities: an arrow M of naTrans(Y(X),G) gives us F*T*G*M*Y(X) conjoinable: whence T*G*M = T*M is in naTrans(Y(X),F). Y is a functor, so Y(X)*Y(f)*Y(V) is conjoinable, with Y(X) a functor, so T*M*Y(f) is in naTrans(Y(V),F). To be a (co)transform, B([T,f]) must begin where one of the following starts and end where the other ends:
So compose b after M-> T*M*Y(f) to get
Now, (T*M*Y(f))(V), exploiting V=V&on;V, is (T*M)(V)&on;Y(f,V) and V is indeed in C-Hom(V,f) = (|Y(f,V)), with Y(f,V,V)= f&on;V&on;V = f; so B([T,f]) reduces to
Observing that M is conjoinable before T, via G, and M is conjoinable after Y(f), via Y(X), we can write naTrans(Y(X),G) as naTrans(Y(f),T) to remove reference to G and X. Likewise, F(V) is (T(f)|), giving
This leaves (T*M)(V,f) containing the only remaining reference to (F,G,X or) V. NB: (T*M)(V) = T(V)&on;M(V) which accepts the same inputs as Y(X,V), one of which is f, and both T(V) and M(V) are functions in Set. For any factorisation of f, u&on;v =f - eg f&on;V = f = X&on;f -
with Y(X,u) mapping X to u, so
with (T*M)(V,f) as a particular example. Thus the appearance of V in the definition of B([T,f]) is entirely natural and, for any factorisation u&on;v of f, we have
We had [F,V]&on;[T,f]&on;[G,X] valid in coTransform(C,Set)×dual-C, with [F,V] and [G,X] identities: we obtain B([F,V]) ending where B([T,f]) ends and B([G,X]) starting where B([T,f]) starts: so B is a transform. From its construction, we have the coTransform [T,f]-> (naTrans(Y(f),T)| M-> T*M*Y(f) :naTrans(Y(|f),(T|))) conjoinable before it: and this is just coTransform(C,Set)'s Yoneda(T,Y(f)). So B is conjoinable after K = (coTransform(C,Set)×dual-C| [T,f]-> Yoneda(T,Y(f)) :Set), in which Y is C-Yoneda and the other use of Yoneda is in coTransform(C,Set). B is also conjoinable before [T,f]-> T(f), the evaluation functor on coTransform(C,Set)×dual-C. [In general, evaluation is just (Transform(A,W)×A| [T,f]-> T(f) :W) and we have A= dual-C and W=Set.]
Thus Yoneda's lemma gives us a transformation, B, conjoinable between K and evaluation in coTransform(C,Set)×dual-C: and B's images of identities are all isomorphisms in Set, which makes B an isomorphism in naTrans(K, evaluate), within Transform(coTransform(C,Set)×dual-C, Set). Both K and evaluate are functors.
Now to make explicit B's `inverse' (as to conjoining, that is: B*Q and Q*B will be functors), Q. This turned [F,X] into q in the proof. As before, with [F,V]&on;[T,f]&on;[G,X] in coTransform(C,Set)×dual-C,
so, for each x in F(V), Q([F,V], x) is a coTransformation (C|:Set) and is natural between Y(V) and F. We can compose Q([F,V]) after (F(X)|F(f)|F(V)) &on; (G(X)|T(X)|F(X)) = (G(X)|T(f)|F(V)) = (G(V)|T(V)|F(V)) &on; (G(X)|G(f)|G(V)) to get a mapping (G(X)| :naTrans(Y(V),F)). The crucial term then turns into F(k&on;g, T(f,x)) = (F(k&on;g)&on;T(f))(x) = T(f&on;k&on;g, x).
and we can use the constructions (|T(f)), (T(g)|) because T(f), T(g) are functions, hence mappings, hence relations - on which these denotations stand. [By contrast, C-Prior(f) and C-Post(g) are the closest notions in C.]
By construction, Q([F,V])&on;T(f) = Q([T,f]) = Q([F,V]&on;[T,f]). Consequently, Q is conjoinable after the evaluation functor, consequently after B. The lemma gives us Q([F,V])&on;B([F,V]) and B([F,V])&on;Q([F,V]) as identities, so Q*B and B*Q respect identities. We can then use (Q*B*Q)([F,V]&on;[F,V]&on;[T,f]) = Q([F,V])&on;B([F,V])&on;Q([T,f]) = Q([T,f]) to show that Q*B*Q=Q; likewise, B*Q*B=B. Indeed,
is parallel to T(f)= evaluate([T,f]) and F*Q([T,f],x) = Q([T,f],x) maps V=V&on;V in C to Q([T,f],x,V) = (C-Hom(V,f)| k-> T(f&on;k&on;V, x) :(T(V)|)) = (C-Hom(V,V)| k-> T(f&on;k, x) :(T(f)|)), which maps V to T(f,x). Thus (B*Q)([T,f])
and B*Q = evaluate.
but G is a functor, so G*M = M. Note that (|M(f)) = (|M(X)) = (|(M*Y(X))(X)) = Y(X,X), of which X is a member, and (M(X)|) = G(X), so M(X,X) is in G(X)
with M conjoinable before T, via G, and X&on;f = f, hence
As before, (T*M)(u,v) depends only on u, v only via v&on;u, so (T*M)(f&on;k&on;g, X) = (T*M)(g, f&on;k) = (T*M)(k&on;g, f). Indeed, as T*M = T*M*Y(X), we get (T*M)(f&on;k&on;g, X) = (T(g)&on;M(k)&on;Y(X,f))(X), with Y(X,f,X) = f = Y(f,V,V) and V&on;k = k, to give (T(g)&on;M(k)&on;Y(f,V))(V) = (T*M*Y(f))(k&on;g, V)) = (T*M*Y(f))(g, k). Thus (Q*B)([T,f])
so Q*B = (| [T,f]-> Yoneda(T,Y(f)) :Set), which is our functor K.
Thus Q and B are mutually `inverse' (under conjoining) transformations natural between K and evaluation, one each way.
Written by Eddy.