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: strictification theorems


view this post on Zulip Daniel Teixeira (Jan 20 2022 at 13:37):

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

view this post on Zulip John Baez (Jan 20 2022 at 18:05):

Of course the stricter structures don't transport along equivalences: e.g. given a strict monoidal category CC and an equivalence F:CDF: C \to D, you don't get a way to make DD into a strict monoidal category. What you get is a way to make DD into a monoidal category.

view this post on Zulip John Baez (Jan 20 2022 at 18:11):

I've been using this idea to motivate the concept of "resolution" in homological algebra in this thread.

view this post on Zulip Antonin Delpeuch (Jan 21 2022 at 08:50):

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.

view this post on Zulip Morgan Rogers (he/him) (Jan 21 2022 at 08:58):

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.

view this post on Zulip Mike Shulman (Jan 21 2022 at 19:48):

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.

view this post on Zulip Nathaniel Virgo (Jan 22 2022 at 03:15):

John Baez said:

Of course the stricter structures don't transport along equivalences: e.g. given a strict monoidal category CC and an equivalence F:CDF: C \to D, you don't get a way to make DD into a strict monoidal category. What you get is a way to make DD 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.

view this post on Zulip Mike Shulman (Jan 22 2022 at 04:00):

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 TT on some 2-category, then a weakened notion of that structure is given by the pseudo-TT-algebras. Similar things can be done with other formalizations of structure, such as operads or Lawvere theroies.

view this post on Zulip Mike Shulman (Jan 22 2022 at 04:03):

These methods can often be related to this "transport of structure" property that was mentioned. For a general 2-monad TT, a (strict) TT-structure can't in general be transported across an equivalence. But this is true if TT is "flexible" or "cofibrant". And the pseudo TT-algebras are in fact the strict TT'-algebras for some other 2-monad TT', which is flexible/cofibrant and "weakly equivalent" to TT, and these properties determine TT'. So in a sense, one can say that the notion of pseudo-TT-algebra is the canonical modification of strict TT-algebras that can be transported across equivalences (although flexibility says rather more than this).

view this post on Zulip John Baez (Jan 22 2022 at 17:44):

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 BB when you have a structure on AA and an equivalence f:ABf: A \to B. 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.)

view this post on Zulip Jules Hedges (Jan 23 2022 at 12:50):

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?

view this post on Zulip Nathanael Arkor (Jan 23 2022 at 13:48):

Gould's Coherence for Categorified Operadic Theories is probably a good starting point.

view this post on Zulip Mike Shulman (Jan 23 2022 at 16:45):

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.

view this post on Zulip Matteo Capucci (he/him) (Jan 24 2022 at 10:27):

Also Kelly's An abstract approach to coherence

view this post on Zulip Matteo Capucci (he/him) (Jan 24 2022 at 10:28):

and On clubs and doctrines

view this post on Zulip Jules Hedges (Jan 24 2022 at 12:55):

Thanks!