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.
Functors out of correspond to objects, and Functors out of correspond to isomorphisms.
But is equivalent to , does that mean that somehow objects are equivalent to isomorphisms?
The big question is, what's ? 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 is the walking isomorphism you've just given the proof! Congratulations!
Yes, 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
Say you first give me an object C. If you then give me an isomorphism , you might think this was an interesting extra structure. But any two ways of choosing this structure, say and , 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.)
Alex Kreitzberg said:
Yes, 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.
Let's see if I understand.
A morphism between isomorphisms , and , would be a pair of arrows , making the only square from the above commute.
But this pair is really one arrow, because .
Now an isomorphism of the isomorphisms , and , is determined by an arrow . Paired with the identity, this forms an isomorphism, but for to determine the identity we must have .
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.
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 which I don't consider relevant. I was claiming that all isomorphisms from to any other object are uniquely isomorphic. This of course only makes sense after we choose a category of "isomorphisms from 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 . 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 , where objects are morphisms from to an arbitrary other object, say for arbitrary . Then you could take the subcategory where 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.
I would have given a proof like this:
A morphism between isomorphisms and is an arrow with . But there's only one choice, namely , 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.
Anyway, this is very fun stuff to think about.
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.
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!
It might be related to the notion of path induction in HoTT, but I don’t know much about it…