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: mathematics

Topic: Unnatural isomorphisms of hom-functors

Todd Trimble (Apr 24 2025 at 11:50):

I bumped into an amusing thing yesterday that some of you might enjoy. Say that two functors $F, G: C \to D$ are unnaturally isomorphic if for every object $c \in C$ there is an isomorphism $F(c) \cong G(c)$.

Problem: find two non-isomorphic abelian groups $A, B$ that induce unnaturally isomorphic hom-functors $\hom(A, -), \hom(B, -): \mathsf{Ab} \to \mathsf{Ab}$.

If you'd like to come up with an example on your own, then shield your eyes after this sentence I guess, but fair warning: it could be challenging!

If you want to see an answer, then I invite you to have fun checking that the following works. Let $F$ be a free abelian group on an infinite set (say $\mathbb{N}$ to be definite), and then take $A = F \oplus \mathbb{Q}$ and $B = F \oplus \mathbb{Q} \oplus \mathbb{Q}$. If you like homological algebra, this might be up your alley.

Morgan Rogers (he/him) (Apr 24 2025 at 12:31):

There is spoiler formatting! :)

Todd Trimble (Apr 24 2025 at 12:33):

Yes, but I don't know what the syntax is or where to find it.

Tom de Jong (Apr 24 2025 at 12:36):

https://categorytheory.zulipchat.com/help/format-your-message-using-markdown#spoilers
It's ```spoiler

Todd Trimble (Apr 24 2025 at 12:42):

Thanks, Tom.

John Baez (Apr 24 2025 at 20:43):

As a counterpoint to @Todd Trimble's excellent puzzle, I'll pose this one. Some of you may have seen it before:

Problem: Let $\mathsf{C}$ be the category of algebras of some Lawvere theory, and let $A,B \in \mathsf{C}$ be two algebras whose underlying sets are finite. Show that if the functors $\text{hom}(−,A)$ and $\text{hom}(−,B)$ are unnaturally isomorphic, then $A \cong B$.

Of course if those functors were naturally isomorphic we could simply use the Yoneda lemma.

Patrick Nicodemus (Apr 25 2025 at 02:39):

Just on the topic of these unnatural isomorphisms, I am always blown away when I think of the result that there are no unnatural transformations between definable functors $\mathsf{Type}\to\mathsf{Type}$ in System F, or in related type theories satisfying a similar parametricity theorem. It just shows that somehow the abstraction offered by typing is somehow more abstract than the usual universal quantifier of classical mathematics.

Patrick Nicodemus (Apr 25 2025 at 02:41):

I found a thread on some Haskell forums a while back that in the presence of parametericity, for $F: \mathsf{Type}\to\mathsf{Type}$, equipped with $\mathsf{map} : \forall \alpha,\beta.(\alpha\to\beta)\to(F\alpha\to F\beta)$, one can derive the composition law $F(g\circ f)=F(g)\circ F(f)$ from the identity law $F(1)=1$

Mike Shulman (Apr 25 2025 at 04:17):

That's interesting; I don't actually find that especially mind-blowing. To me it basically says that "natural" means what it sounds like: anything you can actually write down a definition of, in a way that doesn't do silly special-casing or depend on making arbitrary choices, must be "natural".

Mike Shulman (Apr 25 2025 at 04:20):

What I do find incredibly mind-blowing is that in a dependent type theory with internal parametricity (such as the topos of semicartesian cubical sets), the naive System-F-style impredicative definition of an inductive type like the natural numbers is actually correct.

Which is interesting, now that I come to think of it, because that's also basically a naturality statement, since the naive definition can always be rectified by adding naturality assumptions. But somehow it's more "hidden" in that result and that makes it blow my mind more.

Patrick Nicodemus (Apr 25 2025 at 17:14):

To me it basically says that "natural" means what it sounds like: anything you can actually write down a definition of, in a way that doesn't do silly special-casing or depend on making arbitrary choices, must be "natural".

Yes, but this common-sense intuition about the meaning of the word "natural" was not validated for something like 40 years after natural transformations were first invented. I guess what's mind-blowing is not the statement itself, but the fact that we can create a logical system that allows us to constrain "silly special casing and arbitrary choices" in a precise way. Any classical first-order set theory with equality would allow case analysis on equality between two sets, so a fundamentally different set theory than ZFC or ETCS is necessary.