This is about natural transformations in category theory.
Almost always, I somewhat know why some defined maps or homomorphisms behave naturally, but I am almost never entirely sure (if things get sufficiently complicated). For quite some time now, I was wondering if there is some sort of magic trick (other than saying “it’s natural because we could define the transformation for all objects at the same time”) which automatically gives naturality of a transformation when defined only as a family of maps.
For example, Yoneda is beautifully natural in everything it can be natural in. It can be stated as:
If $\mathcal C$ is a small category, then there is a natural isomorphism of functors $\mathrm{Set}^{\mathcal C} × \mathcal C → \mathrm{Set}$ $$\mathrm{Ar}_{\mathrm{Set}^{\mathcal C}}(\mathrm{Ar}_{\mathcal C}(r,–),F) \cong Fr,$$ which is “natural in both $F$ and $r$” for $F ∈ \operatorname{Ob} \mathrm{Set}^{\mathcal C}$ and $r ∈ \operatorname{Ob} \mathcal C$, given by $$\mathrm{Ar}_{\mathrm{Set}^{\mathcal C}}(\mathrm{Ar}_{\mathcal C}(r,–),F) → Fr,~τ ↦ τ_r(\mathrm{1}_r).$$
Often only the bijection for fixed $F$ and $r$ is proved and nothing is said about the naturality. This is not only the case for Yoneda. Whenever I see something like this, I am trying to prove the naturality on my own, but very often I get tired and confused doing so and I give up.
- Are we just supposed to “see” the naturality or is it really tedious work left to the reader?
- Are there some principles behind showing naturality in such cases? What are these?
- How can I express arguments like “since all maps are defined in the same way” in precise mathematical language? Is it even possible?
- More generally, how should I think of naturality to just accept it whenever it’s stated and reasonable?
I am asking this question because after one semester of Linear Algebra, I have been able to “see” linearity of maps, after two semesters of Analysis, I have been able to “see” continuity and differentiability (at least in the trivial cases), and so on. After struggling with category theory for about five years now, I still can’t “see” naturality. What am I missing?
I don't know how much this helps, but in computer science the concept of parametric polymorphic function is quite useful.
What the polymorphic function principle basically says is this:
The base language wrt which these functions need to be defined is usually any reasonable type-theoretic language, but the most well-known example is system F, from which the above principle follows from the parametricity theorem (the wikipedia article is quite poor, but it links the 2 main relevant papers by Reynolds and Wadler respectively).
Note that the formal connection is a bit complicated, see this cstheory question: https://cstheory.stackexchange.com/questions/21516/natural-transformations-and-parametricity