I am working with the following definition of a cartesian category, found in the appendix of https://arxiv.org/abs/2103.01931.
A category $\mathscr{C}$ is said to be Cartesian when there are chosen binary products $×$, with projection maps $𝜋_𝑖$ and pairing operation $⟨−,−⟩$, and a chosen terminal object 𝑇, with unique maps ! to the terminal object.
Can someone explain the definition and function of the pairing operation $⟨−,−⟩$?
Best Answer
The ‘pairing operation’ is redundant if seen as an axiom (that it exists) since it must exist by definition of product. The source is surely only mentioning this to establish a notation for it.
If $f:Z\to X$ and $g:Z\to Y$ then $\langle f,g\rangle$ is notation for he unique morphism $h$ (which exists uniquely by very definition of product) $Z\to X\times Y$ such that $\pi_1 h=f$ and $\pi_2h=g$. The diagonal is a special case of this, $\Delta_Z=\langle1,1\rangle:Z\to Z\times Z$. This ‘operation’ enjoys some nice interactions with composition such as $\langle f,g\rangle h=\langle fh,gh\rangle$ and $(u\times v)\langle f,g\rangle=\langle uf,vg\rangle$. These are proven using the all-important uniqueness given by the universal property.