patrick/static-site-pipeline
1
0
Fork 0
mirror of https://github.com/Smaug123/static-site-pipeline synced 2025-10-05 00:08:40 +00:00
Code Issues Packages Projects Releases Wiki Activity

Clarify some out-of-order bits

Browse Source
This commit is contained in:
Smaug123
2024-04-14 20:54:56 +01:00
parent 2ce132a914
commit 4caf4ee1e6
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
hugo/content/posts/2024-04-13-yoneda.md
View File

@@ -42,12 +42,12 @@ Similarly, the functions \\(GA \to GB\\) are all of the form \\(Gg : GA \to GB\\
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\\);
* an assignment, for each \\(A : |\mathcal{C}|\\), of some \\(GX\\) corresponding to \\(FA\\) (but note that in fact this \\(GX\\) must be \\(GA\\) to meet the later requirements, so there was no choice of target here);
* an assignment, for each \\(\mathcal{C}\\)-morphism \\(f : A \to B\\), of some \\(Gg\\) corresponding to \\(Ff\\) (but note that this must be \\(Gf\\) to meet the later requirements, so similarly there's no choice of target here);
* 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).
The homomorphism \\(\alpha\\) is pretty constrained: the only freedom is to decide exactly *how* \\(\alpha\\) sends \\(FA\\) to \\(GA\\) for each \\(A : |\mathcal{C}|\\).
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}\\).