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)?
Thanks!
Best Answer
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.