Are the projection morphisms of a categorical product unique? We say that an object $X$ is the categorical product of $X_1$ and $X_2$ if there exist morphisms $\pi_1$ and $\pi_2$, called projection morphisms, such that for every object $Y$ with morphisms $f_1 : Y \rightarrow X_1$ and $f_2 : Y \rightarrow X_2$ such that there is a unique $f : Y \rightarrow X$ making the relevant diagrams commute. Are these $\pi_1$ and $\pi_2$ maps unique?
This has come up in a proof I am working on, where I have a category $C$ in which the categorical product exists. In my proof of proposition $P$, I am trying to arrive at a contradiction by assuming the negation of $P$, and showing that this implies the existence of two distinct morphisms $f$ and $f'$ that makes the diagrams commute. But this does not seem sufficient, since I am using specific projection maps $\pi_1$ and $\pi_2$, and instead the contradiction would seem to imply that those specific maps don't work. I suppose I could amend my proof to avoid the use of specific projection morphisms, though knowing if projection maps are unique would suffice.
Does this question make sense?
 A: Let $X$ and $Y$ be objects in a category $\mathscr C$. A product of $X$ and $Y$ is the data $(P,\pi_X,\pi_Y)$ where $P$ is a $\mathscr C$-object and $\pi_X:P\to X$ and $\pi_Y:P\to Y$ are morphisms such that for every $f_X:U\to X$ and $f_Y:U\to Y$ there exists a unique $f:U\to P$ satisfying $\pi_X\circ f=f_X$ and $\pi_Y\circ f=f_Y$.
Now, suppose $u:Q\to P$ is an isomorphism.  Let $\pi^\prime_X=\pi_X\circ u$ and $\pi^\prime_Y=\pi_Y\circ u$ and let $f^\prime=u^{-1}\circ f$. Then clearly $\pi^\prime_X\circ f^\prime=f_X$ and $\pi^\prime_Y\circ f^\prime=f_Y$. That is, $(Q,\pi_x^\prime,\pi_Y^\prime)$ is also a product of $X$ and $Y$.
This shows that if $P$ admits a nontrivial automorphism, then the projection maps are not unique.
One may also show that the only other projection maps are of the form $\pi_X\circ u$ for an isomorphism $u$. This is pretty straightforward to prove. It's also a consequence of the fact that limits are "unique up to isomorphism" in category theory.
As a somewhat trivial example, consider the category ${}_{\Bbb R}\mathsf{Vect}$ and take $P=\Bbb R\times\Bbb R$. We can define our projection maps by $\pi_1,\pi_2:\Bbb R\times\Bbb R\to\Bbb R$ by $\pi_1(x,y)=x$ and $\pi_2(x,y)=y$. However, it's also possible, though somewhat inconvenient, to define $\pi_1(x,y)=y$ and $\pi_2(x,y)=x$.
