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: Resolving Equivalence and strictness

Alex Kreitzberg (Oct 11 2024 at 22:01):

I've realized I don't understand equivalences well.

There's a lot of moving parts, when you say two groups are isomorphic, then you know relationships between elements are preserved and reflected. And that feels like "the core of the story"

Equivalence of categories seem to do more. There are certain propositions about categories that are preserved, and certain structures that are preserved.

Further you can generalize "Equivalence" to an arbitrary n-category, like in HoTT. So equivalence involves dimension somehow. I feel like my foot was in the door, but then I fell down the stairs.

I want to focus on a couple examples that interact with strictness.

Any monoidal category is monoidally equivalent to a strict one.

And the category of Vector spaces is equivalent to the category of Matrices.

(This second example is a special case of the first one right?)

If I prove a relationship in Matrices(a strict category), like $(U' \times V') \times W' = V' \times (U' \times W')$, then the analogous dohicky in vector spaces is the associator $α : (U \times V) \times W \rightarrow U \times (V \times W)$ right? But isn't that structure?

Similarly I understand string diagrams to be strict versions of the structure maps in monoidal categories.

If I have a monoidal endofunctor on a strict category, it'll at best preserve the tensor product strictly $F(a \bigotimes b) = F(a) \bigotimes F(b)$, but under an equivalence presumably it should map to a weaker Functor intelligently right?

Right now the structure getting flattened into propositions, but everything being "the same", and vice versa, is confusing me about what "the same" means.

What do I need to do to get a handle on this, short of proving Mac Lane's strictification theorem?

John Baez (Oct 12 2024 at 00:33):

Equivalence between categories preserves everything that "really matters to a category theorist". You can think of this as a way to define what "really matters to a category theorist".

Alex Kreitzberg (Oct 12 2024 at 07:12):

How do you find the correct definition for "what really matters to a category theorists"?

I have a vague intuition that goes something like $F \circ G$ "is the same as" $\mathrm{id}$ and $G \circ F$ "is the same as" $\mathrm{id}$, where "is the same as" is from the category a step down, and so we recursively work our way up (from the base case of equality).

But I'm not sure that's quite right. So how do I verify this is the right choice? What really matters to a category theorist?

Another intuition I have for ordinary categories: if $x \cong x'$ and $y \cong y'$, then the hom sets $hom(x, y)$ and $hom(x',y')$ are essentially the same. So reducing a category to its skeleton, making isomorphic objects strictly equal, doesn't lose any data.

But Mac Lane's strictification theorem seems just a bit better in a way I'm struggling to put my finger on. It feels like a magic trick, but I'm not sure where the magic is.

Chris Grossack (they/them) (Oct 12 2024 at 15:25):

I can say more about this later if you want, but here's two perspectives that helped me which I can type quickly before I have to go:

1. A lot of this stuff should be thought of as data by default. Instead of thinking of a "strict" thing as being a version of that thing that happens to be a property, think of it as any other version of the thing, but the data happens to be supplied by identity arrows! For example, a strict monoidal category still has associators, etc. It just happens that the associator is given by the identity arrow on some object $A \otimes B \otimes C$.

2. Making sense of when this "data" you're carrying around still "acts" like a property is easier in the $\infty$-category perspetive. You always have a space of possible choices of data, and the data acts like a "property" whenever your space of choices is either empty or contractible. So for instance, there might be multiple choices of the limit of a diagram, but since they're all canonically isomorphic you can show the space of such choices is contractible.

Mike Shulman (Oct 12 2024 at 15:54):

Alex Kreitzberg said:

What really matters to a category theorist?

John already told you:
John Baez said:

Equivalence between categories preserves everything that "really matters to a category theorist". You can think of this as a way to define what "really matters to a category theorist".

That is, what matters to a category theorist is, by definition, those things that are invariant under equivalence of categories.

Mike Shulman (Oct 12 2024 at 15:56):

Although it's probably better to think of this as specifically defining the adverb "really" as a term of art, in the way of mathematicians, that doesn't necessarily align with its everyday meaning. Since in practice category theorists do care about various things that aren't invariant under equivalence, such as strict monoidal structures.

Alex Kreitzberg (Oct 12 2024 at 16:47):

Grossack's answer is in the spirit of what I was expecting as an answer, but Shulman's and Baez's answers have me worried I'm running past a profoundly simple insight :joy:

If I'm doing Euclidean geometry, and I care about angles and lengths, it's a clever jump to realize these can be indirectly defined by certain maps, and another jump to see distance preserving maps are good enough for everything.

By analogy, an example of what category theorists care about are universal properties. So whatever we mean by "equivalence" it better carry over universal properties. How can we use this to find the right definition for our notion of equivalence?

Although now that I've spelled that out, are what Baez and Shulman saying, is that there are multiple definitions of equivalence that category theorists move between depending on what they're paying attention to (like moving between different categories in math generally)?

And I guess the parallel question to this, if we don't "really care" about strictness, why doesn't it ruin our party? Grossack's answer helps with this.

If I do a calculation with angles in geometry, but can express the final result in terms of intersections, then the result is safe to use under a projective transformation even though I used angles. Don't I have to be similarly careful with strictness, even if I've established a category is equivalent to a strict one?

John Baez (Oct 12 2024 at 18:36):

Alex Kreitzberg said:

How do you find the correct definition for "what really matters to a category theorists"?

That sounds like a hard question, but luckily I answered it already:

Equivalence between categories preserves everything that "really matters to a category theorist". You can think of this as a way to define what "really matters to a category theorist".

What really matters is what's preserved by equivalence!

Alex Kreitzberg (Oct 12 2024 at 19:11):

If want to make up a new definition in a category, how do I make sure it's preserved by equivalence?

Alex Kreitzberg (Oct 12 2024 at 19:13):

Maybe that's a dumb question.

I'm reminded of a student asking "how do I make sure my function is continuously differentiable?"

Alex Kreitzberg (Oct 12 2024 at 19:14):

Because I guess the obvious answer to my question is "check that your definition is preserved under equivalence"

John Baez (Oct 12 2024 at 19:21):

Alex Kreitzberg said:

If want to make up a new definition in a category, how do I make sure it's preserved by equivalence?

Maybe that's a dumb question.

No, it's not a dumb question. One way is to randomly make up a definition and then check it's preserved by equivalence. But after you do that a few times, you'll see what's going on.

Most notably, your definition shouldn't include equations between objects: instead you should specify isomorphisms between objects! For example, compare the definitions of [[strict monoidal category]] , which has equations between objects, and [[monoidal category]], where those equations have been replaced by isomorphisms.

Chris Grossack (they/them) (Oct 12 2024 at 19:23):

There have also been purely syntactic conditions put forward for this. For instance there's a language (in the sense of logic) called [[FOLDS]] and if your statement can be expressed in this language then it's guaranteed to be invariant under equivalence.

Chris Grossack (they/them) (Oct 12 2024 at 19:25):

I believe homotopy type theory is a similar language, which can only express "things category theorists care about", provided one works with [[univalent categories]]

John Baez (Oct 12 2024 at 21:04):

Yes, if these 'automatically safe' languages for higher category theory and homotopy theory, ever catch on, us old-timers may talk to our grandchildren like "In the old days the wires for appliances had no insulation and you had to carefully learn how to deal with them without getting electrocuted! Nowadays you kids have it so easy!"

Alex Kreitzberg (Oct 12 2024 at 23:59):

I'm thinking about these answers, here's a (hopefully small) question

Chris Grossack's second example is a nice explanation of why universal properties, are properties, so thanks for that.

If, for a specific object $X$, an isomorphism going to $X$ implies the isomorphism is the identity on $X$, then is the natural notation to use here $=$?

This isn't preserved by equivalence, it's easy to add distinct isomorphic objects.

However, can we say a category is "essentially strict on $X$" if we can show it is equivalent to a category where $X$ does have the above strictness property?

I guess that was two questions, am I using $=$ correctly, and is a definition like "essentially strict" useful?

John Baez (Oct 13 2024 at 00:01):

I don't understand the definition: can you state it as a formal definition?

Alex Kreitzberg (Oct 13 2024 at 00:02):

Sorry I'll be more careful

Alex Kreitzberg (Oct 13 2024 at 00:18):

I'm calling an object $X$ in a category $\mathcal{C}$ strict, if for any object $A \in \mathcal{C}$ and any morphism $f \in hom(A, X)$

Whenever $f$ is an isomorphism, we have $f = id_C$ and we say $A = C$.

Something about that feels cursed. You shouldn't be allowed to compare morphisms until you've established the hom-sets they're from, I feel like I'm trying to get passed that somehow.

I'm trying to figure out what Grossack means by "It just happens that the associator is given by the identity arrow on some object $A \otimes B \otimes C$."

Alex Kreitzberg (Oct 13 2024 at 00:29):

How do you say $id_X$ is the only isomorphism to, or from, $X$?

Mike Shulman (Oct 13 2024 at 00:40):

A category in which every isomorphism is an identity is called a [[gaunt category]]; you seem to be trying to relativize this to a single object. Gauntness is not a category-theoretic property, since in particular it includes being a [[skeletal category]]; but there is an up-to-equivalence version where you ask instead that any two parallel isomorphisms are equal, and in that case one can also argue that writing $=$ for isomorphisms is more justified.

However, none of that is relevant to Chris's statement, because it said nothing about the identity being the only isomorphism, only that the specific associator isomorphism happens to be an identity morphism (which entails, therefore, that its domain and codomain must be equal).

Alex Kreitzberg (Oct 13 2024 at 01:09):

I tried to use Chris's comment on "contractible groupoids", to make my definition of equality "like a property". I probably messed the moral up.

Thinking about it more any nontrivial set has lots of automorphisms.

And often strictly distinct sets have exactly one "important" isomorphism between them.

I'm going to think about this more before asking another question.

Mike Shulman (Oct 13 2024 at 01:15):

Ah, yes, I can see how that could have been confusing. What Chris meant is that there is a contractible groupoid of isomorphisms with some specific property. So, for instance, given two objects $A$ and $B$, the groupoid whose objects are spans $A \leftarrow P \to B$ with the universal property of the product, and whose morphisms are isomorphisms that commute with the projections, is contractible (as long as it's nonempty).

Alex Kreitzberg (Oct 14 2024 at 16:55):

From [[coherence and strictification for monoidal categories]]:

Most people, when they first hear about strictifications, imagine that strictifying a monoidal category is like taking a quotient, in order to identify associativities with identities. That’s actually the wrong picture, and it leads to a lot of confusion...

I think the error described here is essentially what I was mentally doing (albeit poorly). I'm going to keep thinking about your answers and maybe try to read Mac Lane's proof.

John Baez (Oct 14 2024 at 16:59):

At the very least it's good to understand the basic idea of the proof sketched out in the rest of that short nLab article.

John Baez (Oct 14 2024 at 17:00):

Maybe you can pay @Todd Trimble to finish writing the article. I forget what his rates are. :wink:

Todd Trimble (Oct 14 2024 at 17:05):

Heh! Actually, I might recommend the article [[clique]], where the connection between Mac Lane's theorem and strictification is explained.

Alex Kreitzberg (Oct 21 2024 at 21:58):

Okay, after a lot of thought, here's my understanding of Strictification in Set.

In $\mathrm{Set}$, there is a unique natural isomorphism between $A \otimes (B \otimes C)$ and $(A \otimes B) \otimes C$, that I'll call $\alpha$.
Its components are $\alpha_{A,B,C}(a, (b, c)) = ((a, b), c)$.
There's even a unique natural isomorphism from $X$ to $X$ whose components are just the identity morphisms $\mathrm{id}_X$. We also have unitor natural transformations.

These natural transformations satisfy the coherency conditions, so no matter where we add units and parenthesis when combining units and objects with tensors (provided we don't change their order), there exists a unique natural isomorphism between them. So for example, there is a unique natural isomorphism between $1\otimes (A \otimes (B \otimes (C \otimes D)))$ and $(((1 \otimes A)\otimes B) \otimes C ) \otimes D$.

All these ways of combining unitors and associators form a contractible groupoid called a clique, which can be represented as a functor embedding into $\mathrm{Set}$. I'll label it as $F_{A,B,C,D}: C_{A \otimes B \otimes C \otimes D} \rightarrow \mathrm{Set}$.

These cliques are the objects of a certain category that I'll call $Set^{st}$. There's a bit of machinery I think I could type out without making a mistake, but the upshot is if you consider any morphism between two objects of separate cliques, like $f : A \otimes ( B \otimes C) \rightarrow C$, and you replace the ends with isomorphic members of the respective cliques, a unique morphism is determined that commutes with our original $f$, say $f' : (A \otimes B) \otimes C \rightarrow C$.

So I'm saying $f \in hom(A \otimes (B \otimes C), C)$ gets mapped to $f' \in hom((A \otimes B) \otimes C, C)$ under the natural isomorphism, precomposition by $\alpha^{-1}$.

So the collection of such arrows from one clique to another clique, mutually determine each other, so their composition is well defined (but I haven't proven this).

In particular, the associator commutes with the identity morphism of any object in the clique to itself.

We define an embedding from $\mathrm{Set}$ into $\mathrm{Set^{st}}$, by sending objects to their cliques, and morphisms to the morphism of cliques I alluded to above. So identity arrows of objects in a clique go to identity arrows of the clique, which is where the associator and the unitors get mapped to as well. Because the corresponding associator and unitor in $\mathrm{Set^{st}}$ are natural identities, $\mathrm{Set^{st}}$ is strict.

Because our functor is an embedding, the commutative diagrams in $\mathrm{Set^{st}}$ get reflected, so equations we prove in $\mathrm{Set^{st}}$, get reflected back to $\mathrm{Set}$ when we put all the parenthesis, associators, and unitors back. In any case, it's safe to write both $(A\otimes B) \otimes C$ and $A \otimes (B \otimes C)$ as $A \otimes B \otimes C$.

If all of that is essentially correct, I have two follow up questions. In [[monoidal category]] I don't see it required anywhere that the associator be a unique natural isomorphism, do I not have to show an associator is unique when specifying a monoidal category? Is it being unique a theorem?

And maybe the answer to the following question will become clearer as what I've written above starts to sink in more, but is there a way to relate all the above to naive intuitions involving equality of sets? Or is it a sort of accident that $A \times B \times C = \{(a, b, c) : a \in A, b \in B, c \in C\}$ works?

John Baez (Oct 21 2024 at 22:00):

Alex Kreitzberg said:

Okay, after a lot of thought, here's my understanding of Strictification in Set.

In $\mathrm{Set}$, there is a unique natural isomorphism between $A \otimes (B \otimes C)$ and $(A \otimes B) \otimes C$, that I'll call $\alpha$.

Just for the benefit of newbies, $\otimes$ here is what people usually denote by $\times$. (I would use $\times$ myself.)

John Baez (Oct 21 2024 at 22:15):

I don't see it required anywhere that the associator be a unique natural isomorphism,

Good!

do I not have to show an associator is unique when specifying a monoidal category?

No.

Is it being unique a theorem?

No, it's not.

The associator is part of the data you have to give when you specify a monoidal category. You can have two different monoidal categories that differ only in that they have different associators!

Alex Kreitzberg (Oct 21 2024 at 22:26):

Okay, if I give an associator and a unitor that satisfy the coherency conditions, there'll be at most one way to use them to rearrange parenthesis then?

Or in other words, if I have two morphisms that involve complicated combinations of the given associator and unitor, provided the ends match (which must be true for equality to be meaningful), the morphisms must be equal. That's what it means to say "every 'formal' diagram in a monoidal category made up of associators and unitors commutes" right?

Alex Kreitzberg (Oct 21 2024 at 22:29):

Yeah I believe that's right, I think I get all the key points.

If there's anything anybody feels is worth commenting on, I definitely appreciate any feedback given. The above was very hard to paraphrase.

John Baez (Oct 21 2024 at 23:10):

Alex Kreitzberg said:

Okay, if I give an associator and a unitor that satisfy the coherence conditions, there'll be at most one way to use them to rearrange parenthesis then?

Yes, that's the idea. It took Mac Lane to make it precise.

Or in other words, if I have two morphisms that involve complicated combinations of the given associator and unitor, provided the ends match (which must be true for equality to be meaningful), the morphisms must be equal. That's what it means to say "every 'formal' diagram in a monoidal category made up of associators and unitors commutes" right?

One key word here is "formal". We might be in a monoidal category where some parenthesized expression just happens to equal some very different-looking parenthesized expression. There's nothing to stop that from happening! Then we could use associators and unitors in tricky ways to get diagrams that don't commute. You can see an example provided by @Mike Shulman on the top of page 6 of this paper.

John Baez (Oct 21 2024 at 23:11):

The "formal" business is designed to rule out such dirty tricks.

Alex Kreitzberg (Oct 21 2024 at 23:20):

Man this stuff is hard, thanks for the warning.

John Baez (Oct 21 2024 at 23:30):

Indeed, you'll see if you read a little of the paper I pointed you to that the famous category theorist Jean Benabou gave a plausible but wrong definition of 'monoidal category' where he just said "all diagrams built from associators and unitors must commute" - which turns out to be incorrect.

You might like this section of the paper.

Alex Kreitzberg (Oct 22 2024 at 01:17):

Both sections 1 and 2 of that paper were very nice, thank you for sharing it.

Alex Kreitzberg (Oct 22 2024 at 19:57):

One big takeaway from all this, two objects being in the same contractible groupoid is an important categorical analog of being "the same", perhaps the most important one. This makes sense because any particular contractible groupoid is equivalent to a category with one object and one morphism.

So, the point behind Grossack's answer and Shulman's clarification - is that although constructing a product in $Set$, can be done in various ways, the various ways form a contractible groupoid, which is just one object with one morphism up to equivalence. So the product construction returns one object with one morphism, up to equivalence.

Okay, cool. I think I'm getting it, I'll put this thread down. Thanks everyone for the answers.