Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Efficiently checking naturality

Joshua Meyers (Nov 12 2020 at 19:26):

So I'm working through @fosco's coend calculus book and spending a lot of time checking naturality conditions.

For example, in the derivation on p.35,

$\text{Set}(\int^{C\in\mathcal{C}} KC \times \mathcal{C}(X,C),Y) \cong \int_{C\in\mathcal{C}} \text{Set}(KC\times\mathcal{C}(X,C),Y) \cong \int_{C\in\mathcal{C}} \text{Set}(\mathcal{C}(X,C),\text{Set}(KC,Y)) \cong \mathcal{C},\text{Set}\cong \text{Set}(KX,Y)$

it's necessary to check that each equivalence in the chain is natural in $Y$ --- then you can use the Yoneda lemma to get

$\int^{C\in\mathcal{C}} KC \times \mathcal{C}(X,C) \cong KX$

But then you have to check that each equivalence in the chain is also natural in $X$, to get the isomorphism of functors

$\int^{C\in\mathcal{C}} KC \times \mathcal{C}(-,C) \cong K$

So my question is, how do experienced category theorists efficiently check all these naturality conditions? Do they just get more obvious as you get more experienced? Do you stop caring about checking them because you get jaded with how often they are true? Does the feeling that "it couldn't be any other way" reach some level of rigor?

fosco (Nov 12 2020 at 20:06):

Joshua Meyers said:

So I'm working through fosco's coend calculus book and spending a lot of time checking naturality conditions.

For example, in the derivation on p.35,

$\text{Set}(\int^{C\in\mathcal{C}} KC \times \mathcal{C}(X,C),Y) \cong \int_{C\in\mathcal{C}} \text{Set}(KC\times\mathcal{C}(X,C),Y) \cong \int_{C\in\mathcal{C}} \text{Set}(\mathcal{C}(X,C),\text{Set}(KC,Y)) \cong \mathcal{C},\text{Set}\cong \text{Set}(KX,Y)$

it's necessary to check that each equivalence in the chain is natural in $Y$ --- then you can use the Yoneda lemma to get

$\int^{C\in\mathcal{C}} KC \times \mathcal{C}(X,C) \cong KX$

But then you have to check that each equivalence in the chain is also natural in $X$, to get the isomorphism of functors

$\int^{C\in\mathcal{C}} KC \times \mathcal{C}(-,C) \cong K$

So my question is, how do experienced category theorists efficiently check all these naturality conditions? Do they just get more obvious as you get more experienced? Do you stop caring about checking them because you get jaded with how often they are true? Does the feeling that "it couldn't be any other way" reach some level of rigor?

There are two kinds of proof in category theory:

1. "What else it could be?"
2. "This is just the Yoneda lemma in disguise"
3. "I was kidding, there are also times we have to do the computation for real"

fosco (Nov 12 2020 at 20:09):

This said, the particular argument you are looking for sounds like $\hom(widget, Y)$ is natural in $Y$, and the operation of co-ending is functorial, so $\int_C \hom(T(CC),Y) \to\int_C\hom(S(CC),Y)$ is the component (in Y) of a natural transformation, and...

fosco (Nov 12 2020 at 20:10):

...at some point you realise this is always the same argument, just with different icing

Dan Doel (Nov 12 2020 at 20:13):

Several of these are natural by definition in some presentations.

sarahzrf (Nov 12 2020 at 20:13):

i think one trick is learning to write a series of transformations as a chaining of some known natural ones

sarahzrf (Nov 12 2020 at 20:14):

and indeed, you could say that coend calculus is effective in part precisely because it lets you do that

sarahzrf (Nov 12 2020 at 20:15):

there are an awful lot of entirely formal equivalences that you can deduce by means of a fairly small number of [co]end manipulation rules, so if you can remember those and remember that they are natural, you're good

sarahzrf (Nov 12 2020 at 20:15):

i guess it's sort of like proving that things are continuous

sarahzrf (Nov 12 2020 at 20:18):

you eventually realize that most elementary functions are continuous, that most ways of plugging continuous things together result in something continuous, and that many/most "obviously" continuous functions are built in standard ways out of elementary functions

sarahzrf (Nov 12 2020 at 20:18):

also, personally, i just bullshit constantly

sarahzrf (Nov 12 2020 at 20:18):

but also im not a real category theorist (:

John Baez (Nov 12 2020 at 21:30):

Joshua Meyers said:

So my question is, how do experienced category theorists efficiently check all these naturality conditions? Do they just get more obvious as you get more experienced? Do you stop caring about checking them because you get jaded with how often they are true?

Usually if there's an isomorphism that's "systematic", not involving case-by-case arbitrary choices (as provided by the axiom of choice, for example), it tends to be natural in the technical sense. This heuristic is good if you're trying to focus on the big picture and not sink into boring calculations.

John Baez (Nov 12 2020 at 21:33):

So, if I were trying to learn the coend calculus and reading lots of calculations like this, I'd focus on making sure I knew what the isomorphisms are - what they do - and hardly ever bother checking a naturality square. Because life is short.

John Baez (Nov 12 2020 at 21:38):

It's probably good to check about 5 of them, which you've probably already done.

For any sort of routine calculation, it's good to do such calculations at first, before they actually feel routine. At that stage you're learning stuff. But after a while you probably start learning less. So ask yourself: do you feel that checking another natural isomorphism in this book is the best use of your time? Will make you a better person?

John Baez (Nov 12 2020 at 21:38):

When you're actually proving something new, which you plan to publish, you have more of a duty to check the details. But I don't see that you have a duty to check the details when you're reading a textbook.