From eb2780622d28f97eadde2007189793191a4c0e29 Mon Sep 17 00:00:00 2001 From: Patrick Stevens <3138005+Smaug123@users.noreply.github.com> Date: Sat, 13 Apr 2024 17:39:45 +0100 Subject: [PATCH] Yoneda (#9) --- flake.lock | 6 +- flake.nix | 4 +- hugo/content/posts/2024-04-13-yoneda.md | 106 ++++++++++++++++++++++++ 3 files changed, 111 insertions(+), 5 deletions(-) create mode 100644 hugo/content/posts/2024-04-13-yoneda.md diff --git a/flake.lock b/flake.lock index c069f4d..5e10a67 100644 --- a/flake.lock +++ b/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": { diff --git a/flake.nix b/flake.nix index 3949164..f2a29d7 100644 --- a/flake.nix +++ b/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; diff --git a/hugo/content/posts/2024-04-13-yoneda.md b/hugo/content/posts/2024-04-13-yoneda.md new file mode 100644 index 0000000..971af5d --- /dev/null +++ b/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.