Note: This was first posted as a mathstodon thread, and archived here. The thread has a critical typo in the main example (⊗ v.s. ×), which is fixed below.

I've just learned another weird fact about units in monoidal categories. 🌠 Or, more specifically, it's a weird fact about monoidal functors, F, and their unit constraints, F⁰.

The coherence theorems for strong or normal monoidal functors assert that every formal diagram commutes. But for general monoidal functors, there is a standard example of a formal diagram that doesn't commute. It's not even complicated!

For notation, suppose
F : A → A'
is a monoidal functor with unit constraint F⁰ and monoidal constraint F². I'll write the monoidal products of A and A' as a dot, like x·y, and I'll write I and I' for the monoidal units. I'll use λ/ρ for the left/right unit isomorphisms.

Now consider a square diagram, where the top-right composite is
F(I) —{λ⁻¹}⟶ I'·F(I) —{F⁰·1}⟶ F(I)·F(I)
and the left-bottom composite is
F(I) —{ρ⁻¹}⟶ F(I)·I' —{1·F⁰}⟶ F(I)·F(I).

This square doesn't commute in general!

This diagram, and the general coherence for monoidal functors, is given in the 1974 Ph.D. thesis of Geoffrey Lewis. There's also a more recent general treatment of coherence, with lots of applications, in "Coherence for bicategories, lax functors, and shadows" by Malkiewich-Ponto.

Lewis even gives a specific, simple example: Suppose A = (Ab, ⊗, ℤ) and A' = (Set, ×, *), with F being the forgetful functor from abelian groups to sets. Then the two ways around the diagram are the inclusions of ℤ into the two different factors of ℤ×ℤ.

So, how can coherence for strong monoidal functors be so much simpler? Lewis's diagram doesn't seem to have anything to do with the monoidal constraint, F².

The key observation is that you can compose Lewis's diagram with the monoidal constraint
F² : F(I)·F(I) ⟶ F(I·I).
Then, the unity axioms for (F,F⁰,F²) imply that the two total composites are F(λ⁻¹_I) and F(ρ⁻¹_I), where λ and ρ are the left/right unit isomorphisms. Since the components λ_I and ρ_I are always equal, this means that the two total composites are equal. So, if F² is an isomorphism, then the two composites around Lewis's diagram must be equal.

Actually, this argument doesn't require every component of F² to be an isomorphism, just the one at the pair of objects I,I. And if F⁰ is an isomorphism, then those same unity axioms for F imply that the components F²_x,y are isomorphisms whenever either x or y is the monoidal unit I. So, as long as F⁰ is an isomorphism, then Lewis's diagram always commutes. The coherence theorems for strong monoidal functors, or normal lax monoidal functors, basically say that Lewis's diagram is the only obstruction to having a simple coherence theorem.

Something about this still seems confusing to me. It seems like one of those "it just works" calculations that doesn't explain a deeper reason. Is there a deeper reason here? Or is the moral of this story just that units are weird and I should stop thinking they aren't?

tags: social