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: learning: questions

Topic: Is it risky to distinguish between 1 and I?

Alex Kreitzberg (Mar 15 2025 at 21:44):

Functors out of $\mathbb{1}$ correspond to objects, and Functors out of $\mathbb{I}$ correspond to isomorphisms.

But $\mathbb{1}$ is equivalent to $\mathbb{I}$, does that mean that somehow objects are equivalent to isomorphisms?

John Baez (Mar 15 2025 at 23:46):

The big question is, what's $\mathbb{I}$? I can guess, but is this really a standard symbol? It seem clearer to use words.

Anyway, the category of objects in a category C is equivalent to the category of objects in C equipped with an isomorphism to some other object (possibly itself). This is an important realization and if $\mathbb{I}$ is the walking isomorphism you've just given the proof! Congratulations!

Alex Kreitzberg (Mar 15 2025 at 23:50):

Yes, $\mathbb{I}$ is the walking isomorphism, I'm following Reihl's usage here, but I'll use more words in the future, thank you!

ecc4185d-1a3e-454c-90fb-c6f1dfae26bd.jpg

John Baez (Mar 15 2025 at 23:52):

Say you first give me an object $x \in$ C. If you then give me an isomorphism $f: x \to y$, you might think this was an interesting extra structure. But any two ways of choosing this structure, say $f: x \to y$ and $f': x \to y'$, are isomorphic in a unique way. So we category theorists consider it to be uninteresting, or 'fluff'.

(That's not a standard term, but I sometimes use 'fluff' to mean structure with the property that any two ways of choosing this structure are isomorphic in a unique way.)

John Baez (Mar 15 2025 at 23:53):

Alex Kreitzberg said:

Yes, $\mathbb{I}$ is the walking isomorphism, I'm following R[ie]hl's usage here, but I'll use more words in the future, thank you!

Thanks! You can't assume that the terminology found in one textbook is standard terminology that all experts know. If you see the same terminology in several textbooks, then it's more safe to assume that.

Alex Kreitzberg (Mar 16 2025 at 01:03):

Let's see if I understand.

A morphism between isomorphisms $i_1 : x \rightarrow y$, and $i_2 : x' \rightarrow y'$, would be a pair of arrows $f : x \rightarrow x'$, $g : y \rightarrow y'$ making the only square from the above commute.

But this pair is really one arrow, because $f := i_2^{-1} \circ g \circ i_1$.

Now an isomorphism of the isomorphisms $i : x \rightarrow y$, and $i' : x \rightarrow y'$, is determined by an arrow $h : y \rightarrow y'$. Paired with the identity, this forms an isomorphism, but for $h$ to determine the identity we must have $h = i' \circ i^{-1}$.

So there exists exactly one isomorphism between two isomorphisms based on an object.

I think that argument works, but it feels clumsy.

In any case, your point is this fact is proved by my observation, in my question. Maybe I can figure out why that is.

John Baez (Mar 16 2025 at 01:17):

Your argument is only four sentences long so I don't see how it could be called "clumsy" - there's no way to be clumsy that quickly. :smile:

You do bring in an object $x'$ which I don't consider relevant. I was claiming that all isomorphisms from $x$ to any other object are uniquely isomorphic. This of course only makes sense after we choose a category of "isomorphisms from $x$ to another object in C". You do this by first considering the category of "isomorphisms from one object to another in C", which is a subcategory of the [[arrow category]] of C. Morphisms in the arrow category are commutative squares. Then you look at at subcategory where the first object is $x$. You correctly want morphisms in this category to be commutative triangles - that is, commutative squares where one side is the identity. (That happens where you say "Paired with the identity...") So it was a bit of a digression to bring in the arrow category. You could have started with the under category of $x$, where objects are morphisms from $x$ to an arbitrary other object, say $f: x \to y$ for arbitrary $y$. Then you could take the subcategory where $f$ is an isomorphism.

But notice that my explanation of how your proof could have been shorter is much longer than your actual proof!

Still, it's good to understand the relation between the concepts of arrow category and under category.

John Baez (Mar 16 2025 at 01:21):

I would have given a proof like this:

A morphism between isomorphisms $i_1 : x \rightarrow y$ and $i_2 : x \rightarrow y'$ is an arrow $g : y \rightarrow y'$ with $i_2 = g \circ i_1$. But there's only one choice, namely $g = i_2 \circ i_1^{-1}$, and it's an isomorphism.

This is a bit shorter than yours.

In any case, your point is this fact is proved by my observation, in my question.

I wasn't claiming that, actually.

Your original observation shows something else: the category C is equivalent to the category of "objects in C equipped with an isomorphism out of that object". This is another, slightly different sense in which equipping an object with an isomorphism out of it ain't worth much.

John Baez (Mar 16 2025 at 01:26):

Anyway, this is very fun stuff to think about.

Alex Kreitzberg (Mar 16 2025 at 02:25):

Is this a fair way to summarize the situation then?

In any category, you might think it'd be interesting to equip an object with an isomorphism, but there's only a contractible groupoid of ways to do this, so you don't actually gain anything.

Similarly, if you consider a category of object with isomorphism pairs, this category ends up being equivalent to the category of just the underlying objects.

The latter observation seems slightly stronger, because you have to show two pairs are in the same contractible groupoid iff their objects are isomorphic.

While proving the former claim, I think I used the arrow category, because that seemed more symmetrical for understanding the arrows from the walking isomorphism.

But it's clear the under category is the more natural choice for showing isomorphisms from an object are the same as that object.

And I guess my argument used that they were related, and you explained in what way they were related.

Okay, I think that all makes sense.

John Baez (Mar 16 2025 at 04:16):

All this is very nice!

The latter observation seems slightly stronger, because you have to show two pairs are in the same contractible groupoid iff their objects are isomorphic.

Ah, so you've figured out a way to derive one observation from the other. Great!

Ryo Suzuki (Mar 16 2025 at 05:35):

It might be related to the notion of path induction in HoTT, but I don’t know much about it…