More Yoneda

hugo/content/posts/2024-04-13-yoneda.md

@@ -44,7 +44,8 @@ That is, a homomorphism from diagram \\(F\\) to diagram \\(G\\) is:
 
 * an assignment, for each \\(A : |\mathcal{C}|\\), of some \\(GX\\) corresponding to \\(FA\\);
 * an assignment, for each \\(\mathcal{C}\\)-morphism \\(f : A \to B\\), of some \\(Gg\\) corresponding to \\(Ff\\);
-* proofs that this all respects the structure: if \\(f : A \to B\\) in \\(\mathcal{C}\\), then the map \\(Ff : FA \to FB\\) gets taken to the map \\(Gf : GA \to GB\\).
+* proofs that the homomorphism respects the basic structure of the category: if \\(f : A \to B\\) in \\(\mathcal{C}\\), then the map \\(Ff : FA \to FB\\) gets taken to the map \\(Gf : GA \to GB\\);
+* proofs that the homomorphism "respects moving around within the diagram": "moving around in \\(F\\) and then taking the homomorphism over to \\(G\\)" should be the same as "taking the homomorphism to \\(G\\) and then making the same movement in \\(G\\)".
 
 So actually the homomorphism \\(\alpha\\) is pretty constrained: it must map \\(FA \mapsto GA\\) for each \\(A \in |\mathcal{C}|\\) (so there's no freedom about where the objects go).
 
@@ -56,13 +57,16 @@ They provide us with a way of mapping between instantiations of the abstract the
 We saw already that there are some pretty degenerate diagrams: the one which has every object going to the empty set, for instance.
 That diagram has somehow "thrown away all the information" from the category.
 
-Diagrams can also be pretty complex: for example, if we imagine the diagrams for the very simple category that contains just one element and one arrow, literally every set in the universe is a diagram for this category (together with the identity function on that set)!
+Diagrams can also be pretty complex.
+For example, take the diagrams for the very simple category that contains just one object and one arrow.
+Literally every set in the universe (together with the corresponding identity function on that set) is a diagram for this category!
 Most of those diagrams involve us ignoring tons of structure.
+
 For example, there are \\(\mathbb{R}\\)-many functions \\(\mathbb{N} \to \mathbb{N}\\), so we're having to ignore uncountably many functions in the category of sets if we take the diagram consisting of "\\(\mathbb{N}\\) and its sole identity function".
 This diagram wants to have way more structure than there was in \\(\mathcal{C}\\), and it's only by shutting our eyes and ignoring the set-structure we don't care about that we recover anything that looks remotely like \\(\mathcal{C}\\)!
 
 It turns out there's a sweet spot of diagrams with "exactly the amount of structure \\(\mathcal{C}\\) specified, and no more".
-The construction is: assume there's only one element in \\(FA\\) (for some \\(A\\)), and then chase through everything else that \\(\mathcal{C}\\) says should exist (which may involve adding in more elements of \((FA\)) if there are morphisms telling us there should be more).
+The construction is: start with only one element in \\(FA\\) (for some \\(A\\)), and then chase through everything else that \\(\mathcal{C}\\) says should exist (which may involve adding in more elements of \\(FA\\) if there are morphisms telling us there should be more).
 
 What does \\(\mathcal{C}\\) say should exist?
 If \\(f : A \to B\\) is a morphism of \\(\mathcal{C}\\), and if \\(a \in FA\\) is an element of our concrete instantiation of the object \\(A\\), we really want there to be a distinct object \\((Ff)(a) \in FB\\) so that we've preserved the information "\\(f\\) was a morphism \\(A \to B\\)".
@@ -98,11 +102,46 @@ Moreover,
 * this construction is respected by homomorphisms out of \\(G\\) (that's "naturality in \\(G\\)": if we have a homomorphism \\(h : G \to H\\), and we perform the construction on both \\(G\\) and \\(H\\), we find that every homomorphism \\(\mathrm{Rep}_A \xrightarrow{\text{Yoneda corresponding to $x \in GA$}} G \xrightarrow{h} H\\) is equal to \\(\mathrm{Rep}_A \xrightarrow{\text{Yoneda corresponding to $h(x) \in HA$}} H\\));
 * this construction is respected by morphisms \\(A \to B\\) (that's "naturality in \\(A\\)"): this is currently entirely an exercise because I've ground to a halt.
 
-The precise construction is as follows:
+The precise construction is like so:
 
 * Given an element \\(a \in G(A)\\), define a homomorphism \\(\mathrm{Rep}_A\\) to \\(G\\) by sending \\(f : A \to B\\) to \\((Gf)(a)\\).
 * Given a homomorphism \\(\alpha : \mathrm{Rep}_A\\) to \\(G\\), define an element of \\(G(A)\\) by \\(\alpha(\mathrm{id}_A : A \to A)\\).
 * Show that these are inverse to each other.
 * Prove the naturality conditions.
 
-Exercise: do those formally!
+Exercise: do those formally, as follows!
+
+1. Prove that the homomorphism \\((f : A \to B) \mapsto (Gf)(a)\\) is indeed a homomorphism (that is, a natural transformation), by writing out the necessary properties which define a natural transformation and showing that they each hold.
+1. Prove (by writing out the equations) that the two Yoneda maps are inverse to each other.
+1. Write out the equations for both naturality conditions (that is, in \\(A\\) and in \\(F\\)) in full, and prove them.
+
+# The Yoneda embedding
+
+Given any (locally-small) category \\(\mathcal{C}\\) and an object \\(A : |\mathcal{C}|\\), we've seen a way to construct an instantiation of \\(\mathcal{C}\\) in \\(\mathrm{\mathbf{Set}}\\) in a canonical way, representing exactly the structure of \\(\mathcal{C}\\) that was available at \\(A\\).
+
+## Definition of "fully faithful"
+
+Recall the definitions of "full" and "faithful" for a functor \\(F : \mathcal{C} \to \mathcal{D}\\):
+* The functor is *faithful* if it is injective on parallel arrows: for all \\(A, B : |\mathcal{C}|\\), no two morphisms \\(A \to B\\) get mapped to the same target arrow.
+* The functor is *full* if it is surjective on objects which came from the functor: for all \\(A, B : |\mathcal{C}|\\), and for all \\(g : FA \to FB\\), there is \\(f : A \to B\\) with \\(Ff = g\\).
+
+A functor \\(\mathcal{C} \to \mathcal{D}\\) is *fully faithful* if it is both full and faithful.
+While it may collapse away some of \\(\mathcal{C}\\)'s structure, and while it might not hit all of \\(\mathcal{D}\\), it does "locally" preserve all of \\(\mathcal{C}\\)'s structure and introduces no new structure locally: if we fix two objects \\(A, B\\) in \\(\mathcal{C}\\) and restrict ourselves to only looking at \\(A, B\\) and \\(FA, FB\\), the restricted \\(F\\) is a bijection.
+
+## The Yoneda embedding is fully faithful
+
+Notice that the collection of representable functors (that is, the "sweet spot" instantiations of \\(\mathcal{C}\\)) has got the right number of objects to try and be a copy of \\(\mathcal{C}\\): there's a representable functor for each object of \\(\mathcal{C}\\) already (because that's how we defined the representable functors).
+So what happens if we try and complete this into a copy of \\(\mathcal{C}\\) with all its categorical structure, inside the much larger space of instantiations of \\(\mathcal{C}\\)?
+This would be a nice thing to have, because the space of instantiations of \\(\mathcal{C}\\) is very well-behaved (they're all just sets!).
+
+So to view it as a copy of \\(\mathcal{C}\\), we need for any \\(A, B : |\mathcal{C}|\\) and any morphism \\(f : A \to B\\) to find a homomorphism from \\(\mathrm{Rep}_A\\) to \\(\mathrm{Rep}_B\\).
+Take the Yoneda lemma and specialise it by setting \\(G := \mathrm{Rep}_B\\); then we have that the homomorphisms \\(\mathrm{Rep}_A \to \mathrm{Rep}_B\\) are naturally in bijection with the elements of \\(\mathrm{Rep}_B(A) = \mathrm{Hom}_{\mathcal{C}}(B, A)\\).
+
+That's… not actually what we wanted!
+It's very close, but the arrows are going the wrong way: we have morphisms \\(\mathrm{Rep}_A \to \mathrm{Rep}_B\\) corresponding naturally to \\(\mathrm{Hom}_{\mathcal{C}}(B, A)\\).
+
+What we've actually done is built a canonical copy of the *opposite* category of \\(\mathcal{C}\\) inside the space of instantiations of \\(\mathcal{C}\\).
+This canonical copy is called the *Yoneda embedding*, and you can prove that it is full and faithful.
+
+That was the *contravariant Yoneda embedding*, which takes \\(\mathcal{C}^{\mathrm{op}}\\) and embeds it fully faithfully in \\(\mathrm{Nat}(\mathcal{C} \to \mathrm{\mathbf{Set}})\\), the space of all \\(\mathrm{\mathbf{Set}}\\)-instantiations of \\(\mathcal{C}\\).
+By flipping all the arrows around, we also get the *covariant Yoneda embedding*, which takes \\(\mathcal{C}\\) and embeds it fully faithfully in \\(\mathrm{Nat}(\mathcal{C}^{\mathrm{op}} \to \mathrm{\mathbf{Set}})\\), the space of all \\(\mathrm{\mathbf{Set}}\\)-instantiations of \\(\mathcal{C}^{\mathrm{op}}\\) (also known as the space of all *presheaves* over \\(\mathcal{C}\\)).