Post #2516087

The shortest version of our main theorem is that there is an equivalence of symmetric monoidal categories K: Pₓ → Z, where Pₓ is the free symmetric monoidal category on one invertible object x. Moreover, this equivalence K does the following on generating morphisms: The de/cancel morphisms ηₓ and εₓ are sent to identities. The four braidings βₚ,ₛ (for p,s ∈ {x, x'}) are sent to *odd* morphisms in Z. This is the version we prove, and it's the one that isn't part of the previous literature. It's also the one with our favorite conceptual interpretation: in Pₓ you have a formally constructed object that, by design, has a free universal property. So, Pₓ is easy to work with in abstract or general terms. But—as often happens with universal constructions—Pₓ is a big complicated mess of objects and morphisms. So, it's hard to tell whether two morphisms (such as two ways around a diagram) are equal or not. On the other hand, Z is so simple it can be explained in a couple of paragraphs. Coherence in Z is so easy you don't even have to think about it. But—because Z is so simple—it's not something that appears "in nature". The examples that made people want to know about invertibility, like invertible modules over a ring or virtual vector spaces, almost never have *identities* for their de/cancel (i.e., unit/counit) morphisms. So, the equivalence K explains how to take interesting diagrams in Pₓ and convert them to easy diagrams in Z. Then you can use parity of morphisms there to determine whether the diagrams commute. (7/9)