Let $K$ be a category with products $(X,Y)\mapsto X\sqcap Y$ and with a terminal object $T$. It seems obvious to me that $\sqcap$ and $T$ define a structure of a monoidal category on $K$, but I can't find a reference. When I try to prove this myself I come to amazingly bulky constructions. Is there a text where this is accurately proved, or at least formulated?
-
3$\begingroup$ I don't know a reference, but I do know this has a name: ncatlab.org/nlab/show/cartesian+monoidal+category . $\endgroup$– Eric PetersonCommented Nov 1, 2012 at 19:41
-
$\begingroup$ Eric, thank you, that's interesting. So this means that the accurate proof exists... It would be nice to look at it... $\endgroup$– Sergei AkbarovCommented Nov 1, 2012 at 20:00
-
$\begingroup$ Is easy (elements check) that $Set$ is cartesian (i.e. for finite products) monoidal, then for a general cartesian category you apply the (general) representable $(X, -)$ to the axioms diagrams (and use the result in $Set$), then the commutativity of each diagrams follow from Yoneda Lemma (need only the faithful part). $\endgroup$– Buschi SergioCommented Nov 1, 2012 at 20:03
-
$\begingroup$ Sergio, I don't understand this trick. Is it possible, for example, to prove the diagram of associativity (the pentagon) in this way? $\endgroup$– Sergei AkbarovCommented Nov 1, 2012 at 20:20
-
2$\begingroup$ @Sergei, using the Yoneda lemma it is, because that tells you the functor $X\mapsto Hom(-,X)$ is fully faithful. $\endgroup$– David Roberts ♦Commented Nov 1, 2012 at 23:15
3 Answers
Is very easy prove that $(Set, \times, 1)$ is monoidal (by elements checking). Now let $\mathcal{C}$ a category by finite product $\times$ and (then) with a final object $1$. Consider the axioms of monoidal category for $(\mathcal{C}, \times , 1)$ stated by diagrams (see for example p.462 of "Closed Categories" by Eilenberg & Kelly, LA Jolla 1967), now it remains to prove that these diagrams are commutative. COnsider a such diagram $\textbf{D}$ and a (general) object $X\in \mathcal{C}$ and the representable $(X, -): \mathcal{C}\to Set: A \mapsto (X, A)$, acting by $(X, -)$ on this diagram, we get a similar diagram in $Set$, say $X(\textbf{D})$, and $(X, -)$ preserve the product $\times$ and the final object $1$, now we just know that $(Set, \times, 1)$ is monoidal, then $X(\textbf{D})$ is commutative. Because this is true for each object $X$, by Yoneda lemma follow that $\textbf{D}$ is commutative (more easily observe that given $f, g: A \to B$, if $(X, f)=(X, g): (X, A)\to (X, B) $ for each $X$ then $f=g$ (consider $X=A$ and $1_A$)).
-
$\begingroup$ Interesting... OK, I need a time to verify the details. $\endgroup$ Commented Nov 2, 2012 at 7:54
-
$\begingroup$ It would amount to the same thing if we thought about this in terms of generalized elements. $\endgroup$ Commented Nov 2, 2012 at 17:03
-
$\begingroup$ Generalized elements? What's this? Anyway, I accept Sergio's answer. $\endgroup$ Commented Nov 2, 2012 at 17:36
-
$\begingroup$ Let $\mathcal{C}$ be a category and $X$ be an object. Then a generalized element of $X$ of shape $Y$ is a morphism, $f:Y\rightarrow X$. We may also write this as $f\in_{Y} X$, for $f$ is a $Y$ shaped element of $X$. See ncatlab.org/nlab/show/generalized+element and also see the book at the website patryshev.com/books/Sets%20for%20Mathematics.pdf. $\endgroup$ Commented Nov 3, 2012 at 2:30
You need to have chosen products for every pair of objects using the axiom of choice, otherwise you don't get a product functor, just a product anafunctor and I recommend you don't try to use those just yet. Then you can prove - and this is the key step - that any two bracketings of an iterated product are isomorphic in a unique way when you demand the isomorphism respects the all the projections. The unique such isomorphism for a triple product is then the associator, and the uniqueness of the isomorphism for the 4-fold product means that the pentagon commutes. Ditto with the other coherence conditions.
Note that you can choose the product of any object $X$ with the terminal object to be $X$. This makes the unit conditions automatic.
-
$\begingroup$ David, yes, I agree that the operation $(X,Y)\mapsto X\sqcap Y$ must be a mapping. Suppose this is so, then you say that the Yoneda lemma allows to simplify the proof? Can you recommend a text where this trick is used (not necessarily for proving what I am asking about, but just for something...), I would like to look how this trick works. $\endgroup$ Commented Nov 2, 2012 at 6:25
-
$\begingroup$ Could you explain precisely what is meant by when you demand the isomorphism respects the all the projections here? $\endgroup$ Commented Sep 26, 2019 at 16:52
-
$\begingroup$ I mean you have projections out of any iterated product to the various single factors, and you ask that that given two iterated products, the various triangles you write down (with one edge the isomorphism between the two iterated products, and the other edges projections) commute. At least, this is the only possible interpretation of what I wrote almost seven years ago :-) $\endgroup$– David Roberts ♦Commented Sep 26, 2019 at 21:17
You can find it as an example of a monoidal category in Tom Leinster's "Higher Operads, Higher Categories", which contains loads of coherence proofs for higher categories.
-
$\begingroup$ I didn't understand, is this proved there, or just formulated? $\endgroup$ Commented Nov 1, 2012 at 20:06
-
$\begingroup$ Just formulated, but the book gives a lot of information that will allow you to prove it yourself. $\endgroup$ Commented Nov 1, 2012 at 23:17