Cartesian Category Definition

Question

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 $⟨−,−⟩$?

Answer 1

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.

Answer 2

A pairing is the composite of a product and a diagonal morphism:

$$G\xrightarrow{\Delta_G} G\times G \xrightarrow{a\times b} A\times B$$

where $a:G\to A$ and $b:G\to B$ are morphisms in $\mathscr{C}$.