Post #2516088

2026-04-17 16:05 UTC

The way we prove our main theorem uses some abstract 2-monad theory going back to Blackwell-Kelly-Power (flexibility of monads), and also Lack's model structure on 2-monads. I'll certainly leave those details to the paper, but they're not *that* hard. We've structured it so that you just need to understand the statements we've extracted, and then apply them as black boxes. This isn't the first time some wildly general 2-monadic algebra has been applied for concrete, computational applications; I think those applications are how people got into abstract 2-monad theory in the first place! But I do think ours is another neat one for those who are interested in such things. (8/9)

Replies (1)

@nilesjohnson@mathstodon.xyz 2026-04-17 16:08

We put a bunch of examples in the last section of our paper, starting with some of those figure morphisms and gradually building up to more complex examples. Here, I'll just give the final one, because it illustrates a diagram that *doesn't* (generally) commute, but looks at first like it ought to. To start, suppose a is an invertible object in a symmetric monoidal category A, with inverse a'. Then there is a conjugation functor Gₐ: A → A given by z ↦ zᵃ = a' + z + a You can show (using our coherence stuff) that this is a symmetric monoidal functor. Furthermore, you can show (again using coherence) that Gₐ is isomorphic to the identity on A. So, this is a categorification of the fact that conjugation in an abelian group is the identity homomorphism. Of course, conjugation by a' is also a symmetric monoidal functor, and also isomorphic to the identity. The example gets going when you realize that there is a natural isomorphism between these two, with components given by an isomorphism a' + z + a ≅ a + z + a' permuting the summands by a (1 3) permutation. So, is this a *monoidal* natural isomorphism? How could it not be??! (9/11; there are two bonus posts!)

Open ##2516089