nLab
product

Contents

Definition

In a category, a product (also called a cartesian product) of two objects XX and YY is an object X×YX\times Y equipped with morphisms p:X×YXp:X\times Y \to X and q:X×YYq:X\times Y \to Y, called projections, such that for any object ZZ equipped with maps f:ZXf:Z\to X and g:ZYg:Z\to Y there exists a unique h:ZX×Yh:Z\to X\times Y (called the pairing of ff and gg) such that ph=fp \circ h=f and qh=gq \circ h=g.

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

More generally, for SS \in Set \hookrightarrow Cat any discrete category, an SS-indexed limit is a product of |S||S| factors. If SS 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 CC is the same as a coproduct in its opposite category C opC^{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 formationA:TypeB:TypeA×B:Type\frac{\vdash \;A \colon Type \;\;\;\;\; \vdash \;B \colon Type}{\vdash A \times B \colon Type}A,B𝒞A×B𝒞A,B \in \mathcal{C} \Rightarrow A \times B \in \mathcal{C}
term introductiona:Ab:B(a,b):A×B\frac{\vdash\; a \colon A\;\;\;\;\; \vdash\; b \colon B}{ \vdash \; (a,b) \colon A \times B} Q a (a,b) b A A×B B\array{ && Q\\ & {}^{\mathllap{a}}\swarrow &\downarrow_{\mathrlap{(a,b)}}& \searrow^{\mathrlap{b}}\\ A &&A \times B&& B }
term eliminationt:A×Bp 1(t):At:A×Bp 2(t):B\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} Q t A p 1 A×B p 2 B\array{ && Q\\ &&\downarrow^{t} && \\ A &\stackrel{p_1}{\leftarrow}& A \times B &\stackrel{p_2}{\to}& B}
computation rulep 1(a,b)=ap 2(a,b)=bp_1(a,b) = a\;\;\; p_2(a,b) = b Q a (a,b) b A p 1 A×B p 2 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

Revised on July 19, 2014 07:31:02 by Urs Schreiber (82.113.121.244)