nLab
cartesian product

Context

Limits and colimits

Monoidal categories

Contents

Idea

In the strict sense of the word, a cartesian product is a product in Set, the category of sets. Hence for S 1S_1 and S 2S_2 two sets, their cartesian product is the set denoted S 1×S 2S_1\times S_2 whose elements are pairs of elements in S 1S_1 and S 2S_2, respectively.

The abstract concept of such products generalizes from Set to any other category (as a special case of a category-theoretic limit), only that in general products of any given objects may or may not actually exist in that category.

(If they all exists, then one one speaks of a cartesian monoidal category. Especially if the category is also a monoidal category with respect to some other tensor product, then one says “Cartesian product” to distinguish the two. For instance one speaks of the cartesian product on Cat and on 2Cat in contrast to the Gray tensor product.)

A product created by the forgetful functor of a concrete category, especially in algebra, is often called a direct product (for instance a direct product of groups).

Definition

In Sets

Given any family (A i) i:I(A_i)_{i:I} of sets, the cartesian product iA i\prod_i A_i of the family is the set of all functions ff from the index set II with f jf_j in A jA_j for each jj in II.

As stated, the target of such a function depends on the argument, which is natural in dependent type theory; but if you don’t like this, then define iA i\prod_i A_i to be the set of those functions ff from II to the disjoint union iA i\biguplus_i A_i such that f jA jf_j \in A_j (treating A jA_j as a subset of iA i\biguplus_i A_i as usual) for each jj in II.

In traditional forms of set theory, one can also take the target of ff to be the union iA i\bigcup_i A_i or even the class of all objects (equivalently, leave it unspecified).

In a general category

Given any category 𝒞\mathcal{C}, and any set {X i} iI\{X_i\}_{i \in I} of its objects, then the product of all these objects is, if it exists, an object denoted

iIX i𝒞 \underset{i \in I}{\prod} X_i \in \mathcal{C}

and equipped with morphisms

p i:(iIX i)X i p_i \;\colon\; \left(\underset{i \in I}{\prod} X_i\right) \longrightarrow X_i

(the projections), for each iIi \in I, such that it is universal with this property, i.e. such that given any other object Q𝒞Q \in \mathcal{C} with morphisms

Qf iX i Q \overset{f_i}{\longrightarrow} X_i

for iIi \in I, then there is a unique morphism

(f i) iI:QiIX i (f_i)_{i \in I} \;\colon\; Q \longrightarrow \underset{i \in I}{\prod} X_i

which factors the f if_i through the p ip_i, i.e. such that all these diagrams commute:

Q (f i) iI f i iIX i p i X i \array{ Q \\ {}^{\mathllap{(f_i)_{i \in I}}}\downarrow & \searrow^{\mathrlap{f_i}} \\ \underset{i \in I}{\prod} X_i &\underset{p_i}{\longrightarrow}& X_i }

for all iIi \in I.

The case of a binary products it is also denoted by “()×()(-)\times(-)”:

Q ! X 1 p 1 X 1×X 2 p 2 X 2. \array{ && Q \\ & \swarrow &\downarrow^{\mathrlap{\exists !}}& \searrow \\ X_1 &\overset{p_1}{\longleftarrow}& X_1 \times X_2 &\overset{p_2}{\longrightarrow}& X_2 } \,.

Examples

Products of sets

Given sets AA and BB, the cartesian product of the binary family (A,B)(A,B) is written A×BA \times B; its elements (a,b)(a,b) are called ordered pairs. (In set theory, one often makes a special definition for this case, defining

(a,b)={{a},{a,b}} (a,b) = \{\{a\},\{a,b\}\}

rather than as a function so that ordered pairs can then be used in the definition of function. From a structural perspective, however, this is unnecessary.)

Given sets A 1A_1 through A nA_n, the cartesian product of the nn-ary family (A 1,,A n)(A_1,\ldots,A_n) is written i=1 nA i\prod_{i=1}^n A_i; its elements (a 1,,a n)(a_1,\ldots,a_n) are called ordered nn-tuples.

Given sets A 1A_1, A 2A_2, etc, the cartesian product of the countably infinitary family (A 1,A 2,)(A_1,A_2,\ldots) is written i=1 A i\prod_{i=1}^\infty A_i; its elements (a 1,a 2,,)(a_1,a_2,\ldots,) are called infinite sequences.

Given a set AA, the cartesian product of the unary family (A)(A) may be identified with AA itself; that is, we identify the ordered singleton (a)(a) with aa.

The cartesian product of the empty family ()() is the point, a set whose only element is the empty list ()(); we often call this set 11 (or pt\pt, when we're Urs) and write its element as **.

Further examples

For algebraic categories like Grp, where the objects are sets equipped with (globally defined) specified operations that satisfy specified universally quantified identities, products are always constructed in the way you’d expect, viz. by taking products at the level of the underlying sets and endowing them with operations defined in the evident pointwise fashion, just like the way it works in GrpGrp. More commentary on this in more general contexts will be given below.

  • For a non-example: the category of fields does not admit products, even though some might consider that an algebraic example (in some loose or informal sense).

  • In categories of topological type, products are again constructed in a common sense manner; see for instance product topological space for a prototype.

For topological categories, which include examples like Top and Preord, products (e.g. product topological spaces) are always constructed in the way one expects, by taking products at the level of the underlying sets and endowing them with an initial lift structure; e.g., in the case of TopTop, the smallest or initial topology for which the projection maps are continuous.

This principle continues to hold even for infinitary products, where the correct structure might not be obvious without guidance from categorical considerations. For example, for topological spaces, for an infinite product iIX i\prod_{i \in I} X_i, we use the product topology, and not say the box topology? which might be the first thing one would try.

  • In any presheaf category, i.e., a category of type Set CSet^C where CC is a small category, products are calculated in obvious pointwise fashion, where (F×G)(c)=F(c)×G(c)(F \times G)(c) = F(c) \times G(c) with the pointwise product projection maps. This even works if CC is large (making Set CSet^C ‘very large’).

  • If DD has products and CDC \hookrightarrow D is a reflective subcategory, products in CC exist and are calculated as they are in DD. For example, this applies to any Grothendieck topos, as a category of sheaves on a site forming a reflective subcategory of a category of presheaves (on the underlying category of the site).

    • For instance, the category Pos of posets is a reflective subcategory of Preord.
    • Any locally presentable category can be exhibited as a reflective subcategory of a presheaf topos; as such we know how to calculate products there.
  • Generalizing the last example still further, if U:AXU: A \to X is a monadic functor, then products and more generally limits in AA are created (or reflected) from products/limits in XX. In other words, products of algebras over a monad T:XXT: X \to X are given by products in XX, equipped with the evident “pointwise” TT-algebra structure.

  • If DD has products and i:CDi: C \hookrightarrow D is a coreflective subcategory, where ii has a right adjoint (co-reflector) rr, then products in CC can be formed by taking products in DD and then applying rr.

    • For example, the category CGCG of compactly generated spaces is coreflective in Top. The product in CGCG does not coincide in general with the topological product: one may have to add to the product topology still more sets, just enough to ensure that the topology is compactly generated.
  • Products in C opC^{op} are given by coproducts in CC.

    • In some cases, this formal tautology gives the only sensible way to construct products. For example, to form products X×YX \times Y in the category Loc of locales, one must take the formal dual of the coproduct (denoted 𝒪(X)𝒪(Y)\mathcal{O}(X) \otimes \mathcal{O}(Y)) in the category of frames.

    • Similarly, the product of two affine schemes is the formal dual of the coproduct of their corresponding coordinate rings, again given by a tensor product.

  • Relative to a symmetric monoidal category CC with monoidal product \otimes, products in the category of cocommutative comonoids are given by the tensor product XYX \otimes Y in the underlying smc category.

    • For instance, this is how products of cocommutative coalgebras are formed. This applies for instance to cocommutative Hopf algebras.
    • In a cartesian bicategory such as RelRel, the accompanying category of objects and maps (= left adjoint 1-cells) coincides with the category of cocommutative comonoids and comonoid maps between them (which is SetSet in the case of RelRel). Thus, at the level of objects, the usual tensor product in RelRel coincides with the cartesian product in SetSet.
  • For categories CC enriched in the category of commutative monoids, finite products are biproducts and hence coincide with coproducts in a controlled fashion (via matrices). However, this is usually not the case for infinite products. For such examples, finite products are absolute limits.

  • In the category SupLat of sup-lattices, arbitrary products coincide with coproducts (and in fact the functor XX opX \mapsto X^{op} that takes a sup-lattice to its posetal opposite is part of a perfect duality SupLat opSupLatSupLat^{op} \to SupLat, taking a sup-lattice map f:XYf: X \to Y to g op:Y opX opg^{op}: Y^{op} \to X^{op} where fgf \dashv g). This example descends to RelRel itself, so we conclude that products in RelRel are actually given by coproducts in RelRel which in turn are given by coproducts in SetSet.

See also

Properties

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}

Foundational status

In material set theory, the existence of binary cartesian products follows from the axiom of pairing and the axiom of weak replacement? (which is very weak). In structural set theory, their existence generally must be stated as an axiom: the axiom of products. See ordered pair for more details.

Revised on May 3, 2016 12:04:25 by Todd Trimble (67.81.95.215)