nLab
product

Definition

In a category, a product (also called a cartesian product) of two objects $X$ and $Y$ is an object $X\times Y$ equipped with morphisms $p:X\times Y\to X$ and $q:X\times Y\to Y$, called projections, such that for any object $Z$ equipped with maps $f:Z\to X$ and $g:Z\to Y$ there exists a unique $h:Z\to X\times Y$ (called the pairing of $f$ and $g$) such that $p\circ h=f$ and $q\circ h=g$.

Such a categorical product is equivalently a limit over a diagram of the shape of the category $\{a,b\}$ with two objects and no non-trivial morphisms.

More generally, for $S\in$ Set $\hookrightarrow$ Cat any discrete category, an $S$-indexed limit is a product of $\mid S\mid$ factors. If $S$ is a finite set we speak of a finite product. Notice that this includes the case of the empty set, the product over which is, if it exists, the terminal object of the category in question.

• A product created by the forgetful functor of a concrete category, especially in algebra, is often called a direct product.

Properties

General

• When they exist, products are unique up to unique canonical isomorphism, so we often say “the product.”

• One can define in a similar way a product of any family of objects. A product of the empty family is a terminal object.

• A product is a special case of a limit in which the domain category is discrete.

• A product in $C$ is the same as a coproduct in its opposite category $C^{\mathrm{op}}$.

Relation to type theory

Under the relation between category theory and type theory products in a category correspond to product types in type theory.

	type theory	category theory
	syntax	semantics
	natural deduction	universal construction
	product type	product
type formation	$\frac{⊢A:\mathrm{Type}⊢B:\mathrm{Type}}{⊢A\times B:\mathrm{Type}}$	$A,B\in 𝒞\Rightarrow A\times B\in 𝒞$
term introduction	$\frac{⊢a:A⊢b:B}{⊢(a,b):A\times B}$	$\begin{array}{ccc}& & Q\\ & {}^a\swarrow & {\downarrow }_{(a,b)}& {\searrow }^b\\ A& & A\times B& & B\end{array}$
term elimination	$\frac{⊢t:A\times B}{⊢p_1(t):A}\frac{⊢t:A\times B}{⊢p_2(t):B}$	$\begin{array}{ccc}& & Q\\ & & {\downarrow }^t& & \\ A& \stackrel{p_1}{\leftarrow }& A\times B& \stackrel{p_2}{\to }& B\end{array}$
computation rule	$p_1(a,b)=a{p}_2(a,b)=b$	$\begin{array}{ccc}& & Q\\ & {}^a\swarrow & {\downarrow }_{(a,b)}& {\searrow }^b\\ A& \stackrel{p_1}{\leftarrow }& A\times B& \stackrel{p_2}{\to }& B\end{array}$

Examples

• This interactive demonstration in FinSet lets you type two sets and see a product, showing the unique map to it from a randomly chosen $Z$ equipped with $f$ and $g$. It also generates a second product, showing the unique canonical isomorphism between this and the first product.

• product of simplices

• product topological space

Related concepts

• product type

• base change

  • dependent sum, dependent product

  • dependent sum type, dependent product type