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.
Strictification theorems exist for monoidal categories, bicategories, pseudo double categories and all sorts of (bidimensional?) weak structures, but I guess I never figured how to think about these. On one hand, they would mean "oh, you know this complicated coherent new structure you have? Up to equivalence it's just the same as the older strict structure", but then it would sound like the weak structures aren't important, which usually is quite not the case. Thanks!
PS I'm currently thinking mostly about pseudo and strict double categories
Of course the stricter structures don't transport along equivalences: e.g. given a strict monoidal category and an equivalence , you don't get a way to make into a strict monoidal category. What you get is a way to make into a monoidal category.
I've been using this idea to motivate the concept of "resolution" in homological algebra in this thread.
I think this is a great question, with which I have been struggling for some time. For me, it really helped when I discovered the notion of [[rig category]], where you only have partial strictification available. Basically, if you ask for all structural isos to be equalities, you end up with a monoidal symmetry which is an equality, which is undesirable. But you can still get most of the isomorphisms involved in the definition to be equalities. So that example shows what strictification does: cut through the bureaucracy as much as possible, but stop before it gives you nonsense.
It's like how you can consider a skeleton of a category to make some calculations/notation simpler, but you might actually be interested in non-skeletal categories. The category of quotients of a monoid (with all homomorphisms between them rather than just those that commute with the quotient maps) is my personal favourite example of this, where the objects have a nice indexing in terms of congruences on the monoid; this indexing gets thrown away when one takes a skeleton but none of the categorical structure does, and it can be easier to see some of the structure that way.
Another important point is that even when complete strictifications exist, the naturally arising structures are not generally strict. So even if you like to pass across strictifications and work with strict structures, you still need the notion of weak structure because it's what you see in practice and have to apply strictification to.
John Baez said:
Of course the stricter structures don't transport along equivalences: e.g. given a strict monoidal category and an equivalence , you don't get a way to make into a strict monoidal category. What you get is a way to make into a monoidal category.
Does that suggest a general definition of "weakening" of a structure? It often strikes me as odd that weak structures often have rather complicated definitions and I'm wondering if there's some systematic way of seeing where they all come from.
There are systematic ways of weakening structures, once you have a general context to say what you mean by "structure". For instance, if your structures are the algebras for some 2-monad on some 2-category, then a weakened notion of that structure is given by the pseudo--algebras. Similar things can be done with other formalizations of structure, such as operads or Lawvere theroies.
These methods can often be related to this "transport of structure" property that was mentioned. For a general 2-monad , a (strict) -structure can't in general be transported across an equivalence. But this is true if is "flexible" or "cofibrant". And the pseudo -algebras are in fact the strict -algebras for some other 2-monad , which is flexible/cofibrant and "weakly equivalent" to , and these properties determine . So in a sense, one can say that the notion of pseudo--algebra is the canonical modification of strict -algebras that can be transported across equivalences (although flexibility says rather more than this).
So yeah: I was trying to suggest that for any sort of structure and any sort of equivalence, there's a concept of "weak structure" that's what you get on when you have a structure on and an equivalence . But apparently most work has been on slightly more specific cases, where you can prove more things - like the case Mike explained where you have structures on objects of a 2-category, described by a 2-monad on that 2-category. In this case you can systematically work out the syntactic description of your "weak structure" given the description of your structure.
(I'm using "syntactic description" a bit controversially here to mean "description in terms of a 2-monad"; at least in some cases you can make this very syntactic.)
Is there a "theory of strictification"? I mean things like, is there an "explanation" of why certain structures can be fully strictified but for others (eg. symmetric monoidal categories, rig categories, higher categories) it's more subtle?
Gould's Coherence for Categorified Operadic Theories is probably a good starting point.
Another good pair of references is Power's A general coherence result, and Lack's Codescent objects and coherence which puts it in a more abstract context.
Also Kelly's An abstract approach to coherence
Thanks!