nLab
ordered pair

Ordered pairs

Idea

Given any things aa and bb, the ordered pair of aa and bb is a thing, usually written (a,b)(a,b), sometimes [a,b][a,b] or a,b\langle{a,b}\rangle. The important property is

(1)(a,b)=(c,d)a=c,b=d. (a,b) = (c,d) \;\Leftrightarrow\; a = c,\; b = d .

The things aa and bb are called the components of the ordered pair (a,b)(a,b). Given any two sets XX and YY, their Cartesian product is a set X×YX \times Y whose elements are precisely the ordered pairs whose components are respectively elements of XX and elements of YY.

Note that nothing is ordered in an ordered pair other than how it is written out, so sometimes just the word pair is used for this concept. The concept of “pair” meaning a set containing just one or two members as in the axiom of pairing of Zermelo–Frankel Set Theory is now usually distinguished as an unordered pair. A pair in which the components are ordered is basically an arrow between the components, which is sometimes called or analyzed as an interval within a larger context.

Formalisations

One may wish to declare ordered pairs to exist by fiat, which was done, for example, by both Bourbaki and Bill Lawvere. In Bourbaki's foundational set theory, ,\langle{-,-}\rangle is a fundamental binary operation on mathematical objects satisfying two axioms: (1) and the existence (as a set) of the Cartesian product of any two sets. In Lawvere's foundational set theory, ETCS, one axiom is the existence of products in the category of sets; when applied to global elements, this gives their ordered pair (with the product itself being the Cartesian product), and (1) can be proved. Other structural set theories should contain an axiom similar to Lawvere's axiom of products.

I need to check that I remembered Bourbaki correctly; it varies with the edition. —Toby

Instead, one may construct ordered pairs out of some more basic operation. In a material set theory, one may use Kuratowski's definition

(a,b){{a},{a,b}}; (a,b) \coloneqq \big\{\,\{a\},\{a,b\}\,\big\} ;

it is straightforward (using the axiom of extensionality) to prove that (1) holds. Sometimes one sees the alternative

(a,b){a,{a,b}}; (a,b) \coloneqq \big\{a, \{a,b\}\,\big\} ;

but now the axiom of foundation is also needed to prove (1), so the first form is usually preferred. To prove that the cartesian product of two sets is a set, one may use the axiom of separation (bounded separation) is enough to construct X×YX \times Y as a subset of the power set of the power set of the union of XX and YY, or else use the axiom of replacement (restricted replacement? is enough) to construct it directly, since its elements are indexed by the sets XX and YY.

In a foundational type theory, ordered pairs are usually also given by fiat, but (1) may not hold, depending on the type theory used. Now Bourbaki's binary operation of pairing becomes a typed operation; given aa of type XX and bb of type YY, the ordered pair (x,y)(x,y) has type A×BA \times B. There are also two typed operations (either basic or definable, depending on the style of type theory used) π:X×YX\pi\colon X \times Y \to X and ρ:X×YY\rho\colon X \times Y \to Y, satisfying the beta-rules π(x,y)=x\pi(x,y) = x and ρ(x,y)=y\rho(x,y) = y. Then we can either add the eta-rule z=(πz,ρz)z = (\pi z,\rho z), which will allow (1) to be proved, or else take (1) as the definition of equality on the product type X×YX \times Y (which will then allow the eta-rule to be proved).

Generalisations

tuples …

families

pairings

dependent sums

Revised on September 5, 2011 16:25:30 by Toby Bartels (75.88.82.16)