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: Strict monoidal categories, concretely

Nathaniel Virgo (Sep 07 2023 at 03:09):

I've had this question since I started learning about monoidal categories, but didn't get around to asking it.

We know that every monoidal category is monoidally equivalent to a strict monoidal category. This means, for example, that there is a strict monoidal category that's monoidally equivalent to $(\mathbf{Set}, \times)$.

The question is, can we write down this category and its monoidal product explicitly? Schauenberg's Turning Monoidal Categories into Strict Ones says we can take the objects to be sets, but what does the monoidal product look like, if we write it down in elementary set-theoretic notation?

(Then I also have the same question for $(\mathbf{Set}, +)$, $(\mathbf{Vect},\otimes)$, $\mathbf{FinStoch}$ etc.)

Kevin Arlin (Sep 07 2023 at 05:40):

The existence of Schauenberg's product is interesting but the construction involves a lot of distinctions between things like $\{V\}\times S$ and $S$. Roughly speaking, he gets away with strictness by tagging iterated cartesian products with extra singletons indicating how deep their product is supposed to be. But it seems to me that this is just a clever way of squeezing the usual construction of the strictification into the actual category of sets, so I'd suggest just understanding the strictification itself. An explicit construction is outlined in decent detail here: https://ncatlab.org/nlab/show/clique#monoidal_strictifications. The heart of the idea is that you replace the original category $M$ with a category whose objects are lists of objects in $M$, and then you can define the tensor to be the strictly associative concatenation of lists. But the morphisms are a tad tricky.

Nathaniel Virgo (Sep 07 2023 at 06:39):

Thank you, that link looks really useful

Nathaniel Virgo (Sep 07 2023 at 06:41):

although the part about strictification isn't super clear - what does the notation $M^j$ mean?

James Deikun (Sep 07 2023 at 07:13):

Looks like it means the $j$-th Cartesian power of M.

John Baez (Sep 07 2023 at 08:16):

Yes, that's the usual meaning of a category to a natural number power, and that's what makes sense here.

John Baez (Sep 07 2023 at 08:19):

The claim $M^{j+k} \cong M^j \times M^k$ confirms it.

Cole Comfort (Sep 07 2023 at 09:12):

Nathaniel Virgo said:

I've had this question since I started learning about monoidal categories, but didn't get around to asking it.

We know that every monoidal category is monoidally equivalent to a strict monoidal category. This means, for example, that there is a strict monoidal category that's monoidally equivalent to $(\mathbf{Set}, \times)$.

The question is, can we write down this category and its monoidal product explicitly? Schauenberg's Turning Monoidal Categories into Strict Ones says we can take the objects to be sets, but what does the monoidal product look like, if we write it down in elementary set-theoretic notation?

(Then I also have the same question for $(\mathbf{Set}, +)$, $(\mathbf{Vect},\otimes)$, $\mathbf{FinStoch}$ etc.)

Paul Wilson, Dan Ghica and @Fabio Zanasi give a presentation for the strictification of monoidal categories in terms of generators and relations. They reprove the coherence theorem for monoidal categories by induction, which yields the result immediately. The strict monoidal category which is obtained is essentially the proof nets for degenerate linearly distributive categories (where both tensors are the same). Proof nets for monoidal categories are simpler than for linearly distributive categories since the lack of an extra tensorial dimension means that there are no thinning links.

This construction adds $2^{\sf Ob}$ (I think?) isomorphic generating objects, so for example, it won't reproduce the skeletons of $\mathsf{FinStoch}$, $\mathsf{FinVect} \cong \mathsf{Mat}$, $\mathsf{FinSet}\cong \mathsf{FinOrd}$ which are usually regarded as the monoidal strictifications. Of course this is obvious, but just to point it out because strictification is not unique.

I'm pretty sure the same thing works for the strictification of bicategories without any modification.

John Baez (Sep 07 2023 at 10:11):

Here's a cool fact I wish were proved or at least referenced on the nLab: $(\mathsf{FinSet},\times)$ is monoidally equivalent to a skeletal strict monoidal category, but $(\mathsf{Set},\times)$ is not.

Cole Comfort (Sep 07 2023 at 10:31):

John Baez said:

Here's a cool fact I wish were proved or at least referenced on the nLab: $(\mathsf{FinSet},\times)$ is monoidally equivalent to a skeletal strict monoidal category, but $(\mathsf{Set},\times)$ is not.

This is also true for the coproduct as well, I believe. I think this fact causes lots of confusion because people get the intuition that the strictification has fewer objects (when in general it adds objects)

John Baez (Sep 07 2023 at 11:35):

Yes! Almost everyone starts out by thinking you can strictify by skeletalizing. But in fact every monoidal category is monoidally equivalent to a strict one and to a skeletal one, but often not to a strict and skeletal one.

Mike Shulman (Sep 07 2023 at 15:49):

Fortunately, the nLab is a wiki, so anyone can add to it... (-:O

Kevin Arlin (Sep 07 2023 at 17:06):

I was writing up Mac Lane's argument for the nlab and realized I didn't understand why a strict monoidal category equivalent to $(\mathbf{Set},\times)$ would have its associator equal to the canonical isomorphism $A(BC)\to (AB)C$. So I checked, and Mac Lane doesn't prove this, either–he just shows there's no cartesian skeletal strict monoidal guy equivalent to $\mathbf{Set}$. But I think the linked ncafe discussion shows that the associator for a semicartesian monoidal structure on $\mathbf{Set}$ is determined by the $\otimes$ bifunctor, so probably the stronger result is actually true?

Mike Shulman (Sep 07 2023 at 17:08):

Yes, being cartesian is a mere property of a monoidal category, so any monoidal category that's monoidally equivalent to a cartesian one is also cartesian.

Kevin Arlin (Sep 07 2023 at 17:57):

Oh, that's different than what I was thinking...Ah, I guess Fox's theorem is at least one way of formalizing your claim, right?

Patrick Nicodemus (Sep 07 2023 at 18:50):

Something really fun about this is that some of the same strictification tricks in category theory also occur in type theory to try and replace propositional equality with definitional equality, because the compiler can automatically validate the latter.

For example, in Coq, it's a theorem that for all natural numbers $n, m, k$, $n+(m+k) = (n+m)+k$, where $=$ refers to the Martin-Lof dependent equality type, but it's not true that the compiler will let you swap out $n+(m+k)$ for $(n+m)+k$ anywhere; if you have a family of sets $\left\{ A_n\right\}_n$ indexed by natural numbers, and you have some variable $x:A_{n+(m+k)}$, the type-checker will reject it if you try to write $x: A_{(n+m)+k}$.

However, it is possible to "strictify" the natural numbers by introducing a new data type where the natural number $n$ is coded as the function $\lambda k. k+n: \mathbb{N}\to\mathbb{N}$. Then addition is coded as composition of functions, and the compiler is capable of verifying that $(f \circ g) \circ h = f\circ (g \circ h)$ because unfolding the definition of composition reduces both to $\lambda x. f(g(h(x)))$.

This trick is very useful. For example if Vec A n is the data type of vectors of elements of A of length n, we would like to prove that vector concatenation is associative, i.e. if $\ell_1: \mathsf{Vec} \; A\; n, \ell_2: \mathsf{Vec} \; A\; m, \ell_3: \mathsf{Vec} \; A\; k$, then we can prove that $\ell_1 ++(\ell_2++\ell_3)=(\ell_1++\ell_2)++\ell_3$. But equality of these expressions is only well defined if both of them are inhabitants of the same data type, i.e. if Vec A (n+m)+k is the same data type as Vec A n+(m+k); and the compiler will only accept this as valid if n+(m+k) is definitionally equal to (n+m)+k, which motivates this kind of clever encoding of the natural numbers as functions.

Now, this is the exact same technique as the strictification of a monoidal category by means of the embedding into the strict monoidal category of endofunctors, i.e., associating to each object $M$ the tensor functor $M\otimes -$.

I find this quite a beautiful correspondence!

Tom Hirschowitz (Sep 08 2023 at 06:19):

Nice, I didn't know about this!

How do you define, e.g., vectors exactly then? As a type depending on... all maps $\mathbb{N} \to \mathbb{N}$?
Or on a sum type like $\sum_{f\colon \mathbb{N} \to \mathbb{N}} \sum_n \ldots$?

Also, is it merely a correspondence or a plain instance?