Yoneda (#9)

flake.lock

@@ -188,11 +188,11 @@
     },
     "nixpkgs_3": {
       "locked": {
-        "lastModified": 1711541258,
-        "narHash": "sha256-wB4TJZjeBImXC2DHXKHt5waRuxhp8hFYLNABHqXH/a8=",
+        "lastModified": 1713023617,
+        "narHash": "sha256-acok2VJ8nNqm2C5FmM727Kju6GMEJ5AmRAMUou20KBw=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "f0850972708cea377b39a03a52c8ae628868d191",
+        "rev": "7ea497abce1f2f64b5cac8be2047e024957dc96a",
         "type": "github"
       },
       "original": {

flake.nix

@@ -2,7 +2,7 @@
   description = "Static site builder for patrickstevens.co.uk";
 
   inputs = {
-    flake-utils.url = github:numtide/flake-utils;
+    flake-utils.url = "github:numtide/flake-utils";
     scripts.url = "github:Smaug123/flake-shell-script";
     nixpkgs.url = "github:NixOS/nixpkgs";
     extra-content = {
@@ -84,7 +84,7 @@
           mv output $out
         '';
       };
-    in rec {
+    in {
       packages = flake-utils.lib.flattenTree {
         gitAndTools = pkgs.gitAndTools;
         default = website;

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

@@ -0,0 +1,106 @@
+---
+lastmod: "2024-04-13T16:58:00.0000000+01:00"
+author: patrick
+date: "2024-04-13T16:58:00.0000000+01:00"
+title: The Yoneda lemma
+summary: "Another attempt to explain that the Yoneda lemma is actually intuitive."
+math: true
+---
+
+*Read this post with a pencil and paper! Draw pictures!*
+
+# What is a diagram?
+
+A functor \\(\mathcal{C} \to \mathcal{D}\\) is basically a way of identifying a copy of \\(\mathcal{C}\\) inside \\(\mathcal{D}\\).
+That is, it's a specification of an object of \\(\mathcal{D}\\) for every object of \\(\mathcal{C}\\), and corresponding morphisms inside \\(\mathcal{D}\\) which must go between the right objects for this to be a copy of \\(\mathcal{C}\\).
+
+If we specialise to the category of sets, a functor \\(\mathcal{C} \to \mathrm{\mathbf{Set}}\\) is a set for every object of \\(\mathcal{C}\\), and functions between those objects.
+
+Imagine \\(\mathcal{C}\\) as some kind of abstract template of a universe of types; then a functor \\(\mathcal{C} \to \mathrm{\mathbf{Set}}\\) is an *instantation* of that universe of types.
+For example, perhaps we decide that this particular object of \\(\mathcal{C}\\) will be instantiated to \\(\mathbb{N}\\), and that particular object will be instantiated to \\(\mathrm{Bool}\\), and this arrow between them will be instantiated to \\(n \mapsto \mathrm{isEven}(n)\\).
+
+Recall what the functor laws in this context are:
+
+* The functor respects endpoints of morphisms: if \\(f: A \to B\\) in \\(\mathcal{C}\\), then \\(Ff : FA \to FB\\) in \\(\mathrm{\mathbf{Set}}\\). That is, we really are identifying a copy of \\(\mathcal{C}\\) in \\(\mathrm{\mathbf{Set}}\\): we're not actively breaking the structure in translation. If the template \\(\mathcal{C}\\) tells us how to get from \\(A\\) to \\(B\\), then we can do that in our instantiation.
+* The identity morphism is always taken to the identity function. (This one's fairly self-explanatory.)
+* The functor respects compositions: \\(F(g \circ f) = F(g) \circ F(f)\\). That is, if the template tells us we can do \\(f\\) then \\(g\\), we can also do that in our instantiation; moreover, if our template tells us two paths are equal, then they're also equal in the instantiation.
+
+Note what we're *not* requiring of our instantiations: that they're somehow "fully preserving all the structure".
+If \\(\mathcal{C}\\) has two objects \\(A\\) and \\(B\\), we're perfectly happy to instantiate both of them to the same type, as long as all the arrows keep composing correctly.
+In particular, every category has a trivial instantiation to the universe where there's only one set \\(\emptyset\\), and only one arrow \\(\mathrm{id} : \emptyset \to \emptyset\\).
+
+# Homomorphisms between diagrams
+
+Thinking of a diagram as some kind of instantiation of an abstract template, we can define homomorphisms (that is, structure-preserving maps) between them.
+The concrete example of the "trivial instantiation" in the previous section may help you imagine how these homomorphisms should work.
+
+If we have two diagrams \\(F, G : \mathcal{C} \to \mathrm{\mathbf{Set}}\\), we can define some particular homomorphism \\(\alpha\\) from the \\(F\\)-instantiation to the \\(G\\)-instantiation by sending every concrete \\(F\\)-type to a corresponding concrete \\(G\\)-type.
+In order to deserve the name "homomorphism", it had better preserve the structure: that is, if \\(x : FA \to FB\\) is a function in our concrete instantiation of \\(\mathcal{C}\\), then it had better be the case that our homomorphism \\(\alpha\\) takes \\(x\\) to a suitable corresponding function \\(GA \to GB\\) in the \\(G\\)-instantiation.
+
+In fact, every function in the \\(F\\)-instantiation is an image of a morphism from \\(\mathcal{C}\\) (that is, we defined our instantiations so that we weren't considering any extraneous functions there might be between the sets), so instead of considering the set of all general \\(x : FA \to FB\\), we only need to consider the set of all \\(Ff : FA \to FB\\).
+Similarly, the functions \\(GA \to GB\\) are all of the form \\(Gg : GA \to GB\\) for some morphism \\(g\\) of \\(\mathcal{C}\\).
+
+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\\).
+
+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).
+
+We have a special name for these structure-preserving maps between diagrams: we call them *natural transformations*.
+They provide us with a way of mapping between instantiations of the abstract theory specified by \\(\mathcal{C}\\).
+
+# There are some very special examples of diagrams
+
+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)!
+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.
+
+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\\)".
+(If there weren't any such member of \\(FB\\), then our diagram has lost information: we might not be able to distinguish any more whether there was a morphism \\(f\\) in \\(\mathcal{C}\\) or not, just by looking at our instantiation \\(F\\).)
+
+So if we assume there's an element \\(a \in FA\\), then for every \\(B \in |\mathcal{C}|\\), we can deduce the existence of elements \\((Ff)(a) \in B\\) for every \\(f : A \to B\\) in \\(\mathcal{C}\\); and they'd better all be distinct if we couldn't prove them to be equal in \\(\mathcal{C}\\).
+
+Formally: for each object \\(A\\) of \\(\mathcal{C}\\), we can define a diagram \\(\mathrm{Rep}_A : \mathcal{C} \to \mathrm{\mathbf{Set}}\\) given by sending each \\(B\\) to the set of all morphisms in \\(\mathcal{C}\\) which go from \\(A\\) to \\(B\\).
+This somehow "captures exactly all the structure that \\(\mathcal{C}\\) said \\(A\\) has".
+(I've used the symbol \\(\mathrm{Rep}\\) to denote these diagrams, because the category-theoretic term for a diagram isomorphic to one of these is "*representable functor*".)
+
+Note that I haven't yet written down the functions in these concrete instantiations of \\(\mathcal{C}\\); there's only one thing it could plausibly be.
+Given \\(f : B \to C\\) a morphism of \\(\mathcal{C}\\), the corresponding function \\(\mathrm{Rep}_A(f) : \mathrm{Rep}_A(B) \to \mathrm{Rep}_A(C)\\) (that is, the function \\(\mathrm{Rep}_A(f) : \{\text{morphisms $A \to B$ in $\mathcal{C}$}\} \to \{\text{morphisms $A \to C$ in $\mathcal{C}$}\}\\) is defined to be given by composing with \\(f\\): we send \\(g : A \to B\\) to \\(f \circ g : A \to C\\).
+
+These particular diagrams, the *representable functors* (one for every object in \\(\mathcal{C}\\)), together tell you everything there is to know about the category.
+(That is kind of intuitive, by their definition as "the sets of morphisms": we can list out every morphism in the category, just by writing down every element of every object in each of these concrete instantiations.)
+What might be less intuitive and requires a bit more thinking is their characterisation as "define \\(F\\) by supposing there's some single member \\(a \in FA\\), and then seeing what else is forced to exist"; you might find it helps to write out a concrete example of performing this operation for some particular tiny categories.
+
+# Homomorphisms of the representable functors
+
+The representable functors contain so little structure that their homomorphisms are forced to be quite simple.
+
+Given any diagram \\(G : \mathcal{C} \to \mathrm{\mathbf{Set}}\\), and given any \\(A \in |\mathcal{C}|\\), we can precisely characterise the homomorphisms \\(\mathrm{Rep}_A \to G\\).
+Remember, \\(\mathrm{Rep}_A\\) was defined by supposing there's just one element \\(a \in \mathrm{Rep}_A\\), and then throwing in all the other elements that are forced to exist by morphisms of \\(\mathcal{C}\\).
+So intuitively speaking it should be the case that a homomorphism \\(\mathrm{Rep}_A \to G\\) is precisely defined by where that one element \\(a\\) is sent; once we've defined that, *everything* else in our instantiation \\(\mathrm{Rep}_A\\) should be forced by the "preserves morphism structure" property of homomorphisms.
+
+This reasoning is made formal in the *Yoneda lemma*:
+
+> Pick an arbitrary diagram \\(G : \mathcal{C} \to \mathrm{\mathbf{Set}}\\). Then for every object \\(A : |\mathcal{C}|\\), the homomorphisms from the diagram \\(\mathrm{Rep}_A\\) to \\(G\\) are precisely in correspondence with the elements of \\(G(A)\\). Moreover, this correspondence is natural in both \\(A\\) and \\(G\\).
+
+Intuition: the homomorphisms are precisely defined by what happens to the "free generator", and we can get such a homomorphism from any choice of where the "free generator" goes.
+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:
+
+* 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.