# nLab product

### Context

#### Limits and colimits

limits and colimits

# Contents

## 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 $|S|$ 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.

## 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^{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 theorycategory theory
syntaxsemantics
natural deductionuniversal construction
product typeproduct
type formation$\frac{\vdash \;A \colon Type \;\;\;\;\; \vdash \;B \colon Type}{\vdash A \times B \colon Type}$$A,B \in \mathcal{C} \Rightarrow A \times B \in \mathcal{C}$
term introduction$\frac{\vdash\; a \colon A\;\;\;\;\; \vdash\; b \colon B}{ \vdash \; (a,b) \colon A \times B}$$\array{ && Q\\ & {}^{\mathllap{a}}\swarrow &\downarrow_{\mathrlap{(a,b)}}& \searrow^{\mathrlap{b}}\\ A &&A \times B&& B }$
term elimination$\frac{\vdash\; t \colon A \times B}{\vdash\; p_1(t) \colon A} \;\;\;\;\;\frac{\vdash\; t \colon A \times B}{\vdash\; p_2(t) \colon B}$$\array{ && Q\\ &&\downarrow^{t} && \\ A &\stackrel{p_1}{\leftarrow}& A \times B &\stackrel{p_2}{\to}& B}$
computation rule$p_1(a,b) = a\;\;\; p_2(a,b) = b$$\array{ && Q \\ & {}^{\mathllap{a}}\swarrow &\downarrow_{(a,b)}& \searrow^{\mathrlap{b}} \\ A &\stackrel{p_1}{\leftarrow}& A \times B& \stackrel{p_2}{\to} & B}$

## 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

Revised on February 10, 2014 05:32:11 by Urs Schreiber (89.204.135.153)