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

- Transform(A,W)
- for ({transform (A|:W)}: Conjoin :),
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 - naTrans(F,G)
- for {transformation (A|T:W): G*T*F is a valid conjoint}
aka Hom(F,G) in Transform(A,W). Likewise, I'll write

- coTransform(A,W)
- for Transform(dual-A,W)
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:

- B([F,V]) = b
- = (naTrans(Y(V),F)| R-> R(V,V) :F(V))
- B([G,X])
- = (naTrans(Y(X),G)| S-> S(X,X) :G(X))
So compose b after M-> T*M*Y(f) to get

- B([T,f])
- = b&on;(: M-> T*M*Y(f) :)
- = (naTrans(Y(X),G)| M-> (T*M*Y(f))(V,V) :F(V))
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

- = (: M-> (T*M)(V,f) :)
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- = (naTrans(Y(f),T)| M-> (T*M)(V,f) :(T(f)|))

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 -

- (T*M)(f)
- = (T*M*Y(X))(u&on;v)
- = (T*M)(v)&on;Y(X,u)
with Y(X,u) mapping X to u, so

- (T*M)(v,u) = (T*M)(f,X)
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

- B([T,f])
- = (naTrans(Y(f),T)| M-> (T*M)(v,u) :(T(f)|))

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,

- Q([F,V]) = q
- = (F(V)| x->
- (C| g-> (C-Hom(g,V)| k-> F(k&on;g, x) :(F(g)|)) :Set) :naTrans(Y(V),F))

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

- Q([G,X])
- = (G(X)| x->
- (C| g-> (C-Set(g,X)| k-> G(k&on;g, x) :(G(g)|)) :Set) :naTrans(Y(X),G))

- Q([T,f])
- = ((|T(f))| x->
- (C| g-> (C-Hom(g,f)| k-> T(f&on;k&on;g, x) :(T(g)|)) :Set) :naTrans(Y(f),T))

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,

- (B*Q)([T,f])
- = B([F,V])&on;Q([T,f])
- = ((|T(f))| x-> (F*Q([T,f],x))(V,V) |(T(f)|))
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])

- = ((|T(f))| x-> T(f,x) |(T(f)|)) = T(f)
and B*Q = evaluate.

- (Q*B)([T,f])
- = Q([T,f])&on;B([G,X])
- = (naTrans(Y(X),G)| M->
- (C| g-> (C-Hom(g,f)| k-> T(f&on;k&on;g, (G*M)(X,X)) :(T(g)|)) :Set)
- :naTrans(Y(f),T))
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)

- = (naTrans(Y(X),G)| M-> (C| g-> (C-Hom(g,f)| k->
- T(f&on;k&on;g, M(X,X)),
- = (T(f&on;k&on;g)&on;M(X))(X)
with M conjoinable before T,

*via*G, and X&on;f = f, hence - = (T*M)(f&on;k&on;g, X) :G(X))

- = (| M-> (C| g-> (| k-> (T*M)(f&on;k&on;g, X) :) :Set) :)
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])- = (naTrans(Y(X),G)| M-> T*M*Y(f) :naTrans(Y(V),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.$Id: Yoneda.html,v 1.5 2001-10-17 17:11:30 eddy Exp $