16
$\begingroup$

If $\mathcal C$ is a category with products and a terminal object, then $\mathcal C$ is monoidal.

This seems obvious, but wherever I look for a proof or a reference it simply states that the proof is "pretty involved".
I found this 8 years old question on MathOverflow:
Monoidal structure on a category with products and with terminal object

The answer given there uses the fact that Set is monoidal, along with the Yoneda lemma. Is there any other reference that proves it more "generally" (i.e without resorting to Set), or a standard reference?

$\endgroup$
3
  • 2
    $\begingroup$ In Higher Algebra Lurie proves it for an ∞-category with finite products, but I suspect the language and technology might be a bit far afield. The general approach though is easy to describe. If you buy that a symmetric monoidal category is the same thing as a $\Gamma$-category (i.e. a functor from finite pointed sets to categories such that $F(I_+)→\prod_{i\in I} F(\{i\}_+)$ is an equivalence), then the idea is to send the finite pointed set $I_+$ to the category of totally cartesian $I$-cubes sending the "bottom right" corner to the terminal object. $\endgroup$ Jan 26, 2021 at 18:04
  • 2
    $\begingroup$ I’m shocked that anyone would describe this proof as “involved”. I can just about imagine someone describing it as “tedious” or “lengthy” (although it really isn’t), but there’s really no further difficulty besides what comes in inevitably from the definition of “monoidal category”. $\endgroup$ Jan 27, 2021 at 15:40
  • 2
    $\begingroup$ @PeterLeFanuLumsdaine Maybe it's a linguistic matter, but for me "involved" and "tedious" are pretty much synonyms. Note that the proof was not referred to as "difficult" (and indeed you don't need ideas, just a lot more patience than I have for big commutative diagrams) $\endgroup$ Jan 27, 2021 at 16:52

3 Answers 3

31
$\begingroup$

There is a complete proof formalised by Scott Morrison in the Lean proof assistant here:

monoidal/of_has_finite_products.lean

[UPDATE] Here is some commentary. In the above file, we see

variables (C : Type u) [category.{v} C] {X Y : C}

In ordinary mathematical language, this means roughly as follows:

Let $C$ be a set in the Grothendieck universe $u$. Suppose we have a category structure on $C$, i.e. a category with object set $C$; the hom sets are in the Grothendieck universe $v$. Let $X$ and $Y$ be objects of $C$.

This is slightly inaccurate because Lean is based on type theory rather than set theory, and $u$ and $v$ are not really Grothendieck universes but they play the same sort of role in avoiding Russell-type paradoxes.

Later we see

def monoidal_of_has_finite_products [has_terminal C] [has_binary_products C] : monoidal_category C :=
{ tensor_unit  := ⊤_ C,
  tensor_obj   := λ X Y, X ⨯ Y,
  tensor_hom   := λ _ _ _ _ f g, limits.prod.map f g,
  associator   := prod.associator,
  left_unitor  := λ P, prod.left_unitor P,
  right_unitor := λ P, prod.right_unitor P,
  pentagon'    := prod.pentagon,
  triangle'    := prod.triangle,
  associator_naturality' := @prod.associator_naturality _ _ _, }
end

This can be translated as follows:

Suppose that $C$ also has a terminal object and binary products. Then we define a monoidal category structure on $C$, which we call monoidal_of_has_finite_products C, as follows: the tensor unit is the terminal object, the tensor product of two objects X and Y is X ⨯ Y, the tensor product of morphisms is given by the function limits.prod.map that was defined elsewhere, ...

Most of the ingredients used here are actually defined in the file binary_products.lean. For example, in that file we see

lemma prod.pentagon [has_binary_products C] (W X Y Z : C) :
  prod.map ((prod.associator W X Y).hom) (𝟙 Z) ≫
      (prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) ((prod.associator X Y Z).hom) =
    (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom :=
by simp

The symbol used here is just backwards composition, i.e. f ≫ g = g o f. Everything before the := is the statement of the pentagon lemma, and after the := we have the proof, which is just by simp. Earlier in this file, and in other files, there are many lemmas marked with @[simp]. The directive by simp just tells Lean to try to apply any such lemmas that are applicable, and in this case, that is enough to complete the proof.

$\endgroup$
4
  • 6
    $\begingroup$ link to docs: leanprover-community.github.io/mathlib_docs/category_theory/… . $\endgroup$ Jan 27, 2021 at 10:01
  • 3
    $\begingroup$ The fact that the automatic simp tactic suffices for all these lemmas supports the claim that this is a matter of “straightforward verification from the definitions”. $\endgroup$ Jan 27, 2021 at 15:42
  • 1
    $\begingroup$ In Lean, when a tactic like "simp" is used, is there a way to "expand out" the resulting proof, and "see what simp actually did"? After all, in non-formal mathematics, when we say "Proof: straightforward application of the definitions", we view this as just a shorthand for the "actual proof". $\endgroup$
    – Tim Campion
    Jan 27, 2021 at 16:59
  • 2
    $\begingroup$ @TimCampion You can use the squeeze_simp tactic instead of simp, and then you will get a list of the lemmas that were used, but without details of exactly how they were applied. Alternatively, you can print out the fully elaborated proof term, although that is typically very large and indigestible. $\endgroup$ Jan 27, 2021 at 17:04
17
$\begingroup$

In Categories for the Working Mathematician, the first thing that Mac Lane does after defining a monoidal category in Ch. VII.1 is to verify that a category with finite products is monoidal. The associator and unitors were constructed and verified to be natural earlier in the book, in Prop III.5.1, so all that remains for Mac Lane to do is to verify that the coherence diagrams commute. He does this in sketch form only, indicating that one should check on product projections. But this is probably as explicit a verification as you'll find in the literature.

You may find more explicit verification of stronger claims. For instance, Selinger discusses in his Survey of graphical languages for monoidal categories, Sec 6.1 the fact that a cartesian monoidal category may be defined as a symmetric monoidal category where every object has a commutative comonoid structure and every morphism is a comonoid homomorphism and $\otimes$ preserves counits and comultiplications. He doesn't explicitly prove this, but perhaps somebody has worked this out in detail somewhere else.

$\endgroup$
1
  • 7
    $\begingroup$ The annoyance involved in explicitly checking that associators are natural and that associativity pentagons commute are, I think, as good a reason as any to be interested in formalisms like multicategories or $\Gamma$-categories which replace this data-and-equations with a universal property. $\endgroup$
    – Tim Campion
    Jan 26, 2021 at 19:36
3
$\begingroup$

One can find a completely explicit, constructive proof of this in the agda-categories library too, with explicit equational proofs for all pieces. There's an html version for easy web readability too (go to the almost bottom of that file). The symmetric monoidal category is worked out too.

The advantage of doing it this way is that, if you ever wonder why some specific detail is true, it's all here to be seen. No details omitted.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.