I would expect that in any category $\mathcal{C}$ with finite products and a terminal object $1$, the isomorphism $X \times 1 \cong X$ should hold, but I have a rather hard time finding the proof of this.

In my attempt, I use the fact that there are arrows $1_X : X \rightarrow X$ and $\top_X : X \rightarrow 1$, from which the universal property of $X \times 1$ gives me a unique $u : X \rightarrow X \times 1$ such that $\pi_1 \circ u = 1_X$ (and $\pi_2 \circ u = \top_X$). This gets me halfway, but I still need to prove that $u \circ \pi_1 = 1_{X \times 1}$ to prove that $u$ is indeed an iso.

I can easily obtain that $\pi_1 \circ u \circ \pi_1 = \pi_1 = \pi_1 \circ 1_{X \times 1}$, so as far as I can see, the problem can be reduced to proving that $\pi_1$ is a mono.

However, how to get there? Is this even provable, or do I need extra assumptions about $\mathcal{C}$? If it is provable, would $X \times 0 \cong 0$ be provable as well (assuming initial objects)?


  • 1
    $\begingroup$ Your last statement is false: In the category of groups, $1$ is initial and terminal but $X\times 1\cong X$. $\endgroup$ – Dan Rust Oct 28 '13 at 15:21

To show that $u \circ \pi_1 = id$ consider that $u \circ \pi_1$ is a morphism from $X\times 1 \to X\times 1$ such that $\pi_1 \circ u \circ \pi_1 = \pi_1$ and $\top_{X\times 1} = \top_{X\times 1} \circ u \circ \pi_1$. Since these equations also hold if you replace $u \circ \pi_1$ by $1_{X\times 1}$, you get by uniqueness that $u \circ \pi_1 = 1_{X\times 1}$.

The property $X \times 0 = 0$ does not hold in general. Consider the category of groups, where $1 = 0$, so $X \times 1 = X$ and since there are nontrivial groups the property clearly doesn't hold.

The property does however hold if, for instance, the category is cartesian closed.

| cite | improve this answer | |
  • $\begingroup$ Oh, of course, I missed that! I somehow convinced myself that I couldn't use uniqueness of identity in this case. Thank you! $\endgroup$ – Ulrik Rasmussen Oct 28 '13 at 16:05

While I was writing, a proof was submitted. So I'll submit the following non-rigorous exposition, which will hopefully be good for some intuition.

Yes, this is true. we can see from quite general principles that it must be true, without working out any details: the identity is a limit, and the terminal object is a limit, and products are a limit. And limits commute; that is, it doesn't matter what order you compute them in, or whether you compute them in pieces or all at once.

(By the way, I'll use $\bullet$ instead of $1$ for now—$1$ is good notation but I don't want to get confused with the identity morphisms)

You are trying to calculate the limit of the diagram $X\to \bullet$ in two different ways. First, by simply taking $X$ itself as the limit diagram—then there is of course a unique way to add the map to $\bullet$. And second, by beginning with $\bullet$, then adding $X$ to your limit diagram. These must give the same answer, if category theory is to work right.

Getting a little more technical: Let's fix some $Y$ and look at the set $\operatorname{Hom}(Y,X\times \bullet)$. A map to a product is the same thing as a pair of maps, and so an element of this set is a map $Y\to X$, and map $Y\to\bullet$. But the latter is unique—so we have shown that $\operatorname{Hom}(Y,X\times \bullet)=\operatorname{Hom}(Y,X)$.

Actually, that's already a proof, if we are comfortable with the Yoneda embedding. But even if not, it gives us a few big hints on how to proceed, since it gives us a nice dictionary between the two objects.

Take the identity map $1_X : X\to X$. As we observed, this has a natural friend $\psi: X\to X\times \bullet$, which is $\psi = id_X \times u_X$, where $u_X : X\to \bullet$ is the unique map. It is reasonable to guess that it is an isomorphism. And it is also reasonable to guess that the inverse is the only map we can think of in the other direction, which is the projection $\pi: X\times \bullet \to X$.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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