Products by maps: a first universal property

MotivationH

A journey is two functions

A minibus leaves Kampala's old taxi park at 7:00 and heads for Entebbe. A phone on the dashboard records where it is every minute: a latitude and a longitude. So the journey is one function

\text{time} \;\longrightarrow\; \text{latitude} \times \text{longitude}, \qquad t \longmapsto \big(\text{lat}(t), \text{lon}(t)\big),

whose outputs are pairs. But the phone could equally store two separate columns in a spreadsheet: one function $t \mapsto \text{lat}(t)$ and another $t \mapsto \text{lon}(t)$ . Nothing is lost either way. One function into pairs is the same information as two functions.

That modest observation — true for every journey, every spreadsheet with two columns, every point moving in a plane — turns out to describe the set of pairs completely. Mathematicians call this kind of description a universal property, and it is one of the central ideas of modern mathematics. This lesson is your first meeting with one.

IntuitionH

Describing a set from the outside

Usually we describe a set by listing or characterising its elements: $A \times B$ is the set of ordered pairs $(a, b)$ with $a \in A$ and $b \in B$ .

A universal property describes it instead by how it connects to everything else through functions. For $A \times B$ the connections are:

Two functions out of it, the projections, which read off the first and second coordinates.
A rule for functions into it: whenever you have a function to $A$ and a function to $B$ from the same set $X$ , they combine into exactly one function from $X$ to $A \times B$ that "projects back" to them.

DefinitionsH

Projections, pairing and the universal property

Throughout, $A$ and $B$ are sets. Recall from Composition that $g \circ f$ means "first $f$ , then $g$ ".

Definition— projections

The projections of $A \times B$ are the functions

\pi_A : A \times B \to A, \quad \pi_A(a, b) = a, \qquad\qquad \pi_B : A \times B \to B, \quad \pi_B(a, b) = b.

Definition— pairing

Let $X$ be a set, and let $f : X \to A$ and $g : X \to B$ . Their pairing is the function

\langle f, g \rangle : X \to A \times B, \qquad \langle f, g \rangle(x) = \big(f(x), g(x)\big).

Feeding the pairing into a projection gives back the original functions: for every $x \in X$ ,

(\pi_A \circ \langle f, g \rangle)(x) = \pi_A\big(f(x), g(x)\big) = f(x), \qquad (\pi_B \circ \langle f, g \rangle)(x) = g(x).

So $\pi_A \circ \langle f, g \rangle = f$ and $\pi_B \circ \langle f, g \rangle = g$ . A function $h : X \to P$ that satisfies equations like these is called compatible with $f$ and $g$ .

Definition— product (universal property)

Let $P$ be a set with two functions $p : P \to A$ and $q : P \to B$ . We say that $(P, p, q)$ is a product of $A$ and $B$ , or has the universal property of the product, if:

for every set $X$ and every pair of functions $f : X \to A$ , $g : X \to B$ , there is exactly one function $h : X \to P$ with

p \circ h = f \qquad \text{and} \qquad q \circ h = g.

"Exactly one" packs in two demands. Existence: at least one such $h$ . Uniqueness: no more than one. Both matter, as the non-examples below show.

A universal property, in general, describes an object by how it relates, through maps, to all other objects of the same kind. The product is the first and simplest example; you will meet many more.

Explore

The picture, and two explorations

The universal property is usually drawn as a diagram. The dashed arrow is the one whose existence and uniqueness are claimed; the two triangles commute, meaning that following the arrows along either route gives the same function.

For every

X

,

f

and

g

there is exactly one dashed arrow making both triangles commute:

\pi_A \circ \langle f, g \rangle = f

and

\pi_B \circ \langle f, g \rangle = g

.

In the first exploration, $Z$ has three elements, $A$ is a set of two colours and $B = \{1, 2, 3\}$ . Choose $f$ and $g$ , then try to build a function $h : Z \to A \times B$ that projects back to them. Try hard to find a second one that works. Why can't you?

The product, by its maps

Choose maps f : Z → A and g : Z → B. Then try to build a map h : Z → A × B that projects back to f and g.

f : Z → A

f(p) =f(q) =f(r) =

g : Z → B

g(p) =g(q) =g(r) =

⟨f, g⟩ : Z → A × B

p ↦ (red, 2) q ↦ (blue, 2) r ↦ (red, 3)

Your turn: choose h(p), h(q), h(r) by clicking cells.

A × B	1	2	3
red
blue

In the second, a point moves in the plane. Its position at time $t$ is the pair $\big(\cos(at), \sin(bt)\big)$ : one function of $t$ into $\R \times \R$ , built by pairing two functions of $t$ into $\R$ . Change $a$ and $b$ and watch how the two coordinate functions together determine the whole curve — and how the curve determines them back.

One curve = two coordinate functions

A point moves along the curve as t changes: x and y are both functions of t.

t ↦ (cos at, sin bt)

aa = 1bb = 2

Move along tt = 0.79

(0.707, 1)

Worked examplesH

Examples and non-examples

Example— Computing a pairing

Let $X = \{1, 2, 3\}$ , $A = \{\text{red}, \text{blue}\}$ and $B = \Z$ . Define $f(1) = \text{red}$ , $f(2) = f(3) = \text{blue}$ , and $g(n) = n^2$ . Then

\langle f, g \rangle(1) = (\text{red}, 1), \qquad \langle f, g \rangle(2) = (\text{blue}, 4), \qquad \langle f, g \rangle(3) = (\text{blue}, 9).

Projecting the three pairs onto their first coordinates gives back red, blue, blue — the values of $f$ — and onto their second coordinates gives $1, 4, 9$ — the values of $g$ .

Example— A curve in the plane

The unit circle traced at constant speed is $\gamma : \R \to \R \times \R$ , $\gamma(t) = (\cos t, \sin t)$ . In the language of this lesson, $\gamma = \langle \cos, \sin \rangle$ , and $\pi_1 \circ \gamma = \cos$ , $\pi_2 \circ \gamma = \sin$ . Every parametric curve in the plane is the pairing of its two coordinate functions — that is exactly what "parametric" means.

Example— A product that is not made of pairs

Let $A = \{\text{red}, \text{blue}\}$ and $B = \{1, 2, 3\}$ , and let $P = \{1, 2, 3, 4, 5, 6\}$ with

p(k) = \begin{cases} \text{red} & k \le 3 \\ \text{blue} & k \ge 4 \end{cases} \qquad\qquad q(k) = \text{the remainder of } k - 1 \text{ on division by } 3, \text{ plus } 1.

The table of $(p(k), q(k))$ is $1 \mapsto (\text{red}, 1)$ , $2 \mapsto (\text{red}, 2)$ , $3 \mapsto (\text{red}, 3)$ , $4 \mapsto (\text{blue}, 1)$ , $5 \mapsto (\text{blue}, 2)$ , $6 \mapsto (\text{blue}, 3)$ : every combination of a colour and a number occurs for exactly one $k$ . So, given $f : X \to A$ and $g : X \to B$ , the only compatible $h$ sends $x$ to the unique $k$ with $p(k) = f(x)$ and $q(k) = g(x)$ . Hence $(P, p, q)$ is a product of $A$ and $B$ — even though its elements are numbers, not pairs.

Example— Swapping the order

$B \times A$ , with $p(b, a) = a$ and $q(b, a) = b$ , is also a product of $A$ and $B$ : the unique compatible $h$ is $x \mapsto \big(g(x), f(x)\big)$ . A product is not "the set of pairs in a particular order"; it is any set with two maps that behave correctly.

Example— Non-example: existence fails

Take $P = A$ , with $p = \mathrm{id}_A$ and $q$ the constant function with value $1$ . If $g : X \to B$ ever takes a value other than $1$ , there is no compatible $h$ at all, because $q \circ h$ is always constant $1$ . Too few elements: some pairs of maps cannot be combined.

Example— Non-example: uniqueness fails

Take $P = A \times B \times \{0, 1\}$ , with $p$ and $q$ reading off the first and second coordinates and ignoring the extra bit. Now every pair $f, g$ has a compatible $h$ — but not just one: at each point $x$ we may choose the extra bit freely. If $X$ has $3$ elements, there are $2^3 = 8$ compatible maps. Too many elements: the combination is not determined.

ProofH

The theorems, with proofs

Theorem— Theorem 1 (the product of sets)

$A \times B$ , with the projections $\pi_A$ and $\pi_B$ , is a product of $A$ and $B$ . For $f : X \to A$ and $g : X \to B$ , the unique compatible function is $\langle f, g \rangle$ .

Proof

Existence. We computed above that $\pi_A \circ \langle f, g \rangle = f$ and $\pi_B \circ \langle f, g \rangle = g$ .

Uniqueness. Suppose $h : X \to A \times B$ also satisfies $\pi_A \circ h = f$ and $\pi_B \circ h = g$ . Fix $x \in X$ . The element $h(x)$ is some pair $(a, b)$ . Then $a = \pi_A(h(x)) = f(x)$ and $b = \pi_B(h(x)) = g(x)$ , so $h(x) = (f(x), g(x)) = \langle f, g \rangle(x)$ . As this holds for every $x$ , $h = \langle f, g \rangle$ .

∎

The uniqueness proof used one fact about pairs: a pair is determined by its two coordinates. That is the whole content of the universal property.

Theorem— Theorem 2 (maps into a product)

For every set $X$ , the rule $h \mapsto (\pi_A \circ h, \; \pi_B \circ h)$ is a bijection from the set of functions $X \to A \times B$ to the set of pairs of functions $(X \to A, \; X \to B)$ . Its inverse is $(f, g) \mapsto \langle f, g \rangle$ .

Proof

Starting from a pair $(f, g)$ , pairing and then projecting gives $(\pi_A \circ \langle f, g \rangle, \pi_B \circ \langle f, g \rangle) = (f, g)$ . Starting from $h$ , projecting and then pairing gives $\langle \pi_A \circ h, \pi_B \circ h \rangle$ , which is compatible with $\pi_A \circ h$ and $\pi_B \circ h$ — and so is $h$ itself. By the uniqueness in Theorem 1, $\langle \pi_A \circ h, \pi_B \circ h \rangle = h$ . Both round trips are the identity, so the two rules are inverse bijections.

∎

Theorem— Corollary (counting)

If $X$ , $A$ and $B$ are finite, then $|A \times B|^{|X|} = |A|^{|X|} \cdot |B|^{|X|}$ .

Proof

A function from a set with $n$ elements to a set with $m$ elements chooses one of $m$ outputs for each of the $n$ inputs, so there are $m^n$ of them. The left side counts functions $X \to A \times B$ ; the right side counts pairs of functions $X \to A$ and $X \to B$ . Theorem 2 matches them up one-to-one, so the two numbers are equal.

∎

Of course $|A \times B|^{|X|} = (|A|\,|B|)^{|X|} = |A|^{|X|} |B|^{|X|}$ also follows from the rule $(mn)^k = m^k n^k$ . The point is that the universal property explains this algebra: the familiar exponent law is a shadow of a bijection between sets of functions.

Now the main theorem: the universal property determines the product up to a unique compatible bijection. We first isolate the key trick.

Theorem— Lemma (the only compatible self-map)

Let $(P, p, q)$ be a product of $A$ and $B$ , and let $k : P \to P$ satisfy $p \circ k = p$ and $q \circ k = q$ . Then $k = \mathrm{id}_P$ .

Proof

Apply the universal property of $P$ with $X = P$ , $f = p$ and $g = q$ : there is exactly one $h : P \to P$ with $p \circ h = p$ and $q \circ h = q$ . Both $k$ and $\mathrm{id}_P$ have this property. Since there is only one such map, $k = \mathrm{id}_P$ .

∎

Theorem— Theorem 3 (uniqueness up to unique bijection)

Let $(P, p, q)$ be a product of $A$ and $B$ . Then $\varphi = \langle p, q \rangle : P \to A \times B$ is a bijection with $\pi_A \circ \varphi = p$ and $\pi_B \circ \varphi = q$ , and it is the only function $P \to A \times B$ compatible with $p$ and $q$ .

Proof

$\varphi$ is compatible with $p$ and $q$ by the definition of pairing, and by Theorem 1 (applied with $X = P$ ) it is the only compatible function $P \to A \times B$ . It remains to show that $\varphi$ is a bijection; we do this by finding an inverse.

Apply the universal property of $P$ to the set $X = A \times B$ and the projections $\pi_A$ , $\pi_B$ : there is a function $\psi : A \times B \to P$ with $p \circ \psi = \pi_A$ and $q \circ \psi = \pi_B$ .

$\psi \circ \varphi : P \to P$ is compatible with $p$ and $q$ : $\;p \circ (\psi \circ \varphi) = (p \circ \psi) \circ \varphi = \pi_A \circ \varphi = p$ , and likewise $q \circ (\psi \circ \varphi) = q$ . By the Lemma, $\psi \circ \varphi = \mathrm{id}_P$ .
$\varphi \circ \psi : A \times B \to A \times B$ is compatible with $\pi_A$ and $\pi_B$ : $\;\pi_A \circ (\varphi \circ \psi) = (\pi_A \circ \varphi) \circ \psi = p \circ \psi = \pi_A$ , and likewise for $\pi_B$ . The identity of $A \times B$ is also compatible, so by the uniqueness in Theorem 1 (with $X = A \times B$ ), $\varphi \circ \psi = \mathrm{id}_{A \times B}$ .

So $\psi$ is a two-sided inverse of $\varphi$ , and $\varphi$ is a bijection.

∎

Note

Testing one point at a time. Take $X = \{\star\}$ , a set with one element. A function $\{\star\} \to P$ is just a choice of an element of $P$ . So the universal property for this one $X$ says: for every $a \in A$ and $b \in B$ there is exactly one $u \in P$ with $p(u) = a$ and $q(u) = b$ — that is, $\langle p, q \rangle$ is a bijection. Conversely, if $\langle p, q \rangle$ is a bijection, the universal property holds for every $X$ (choose $h(x)$ point by point). So for sets, it is enough to test one-element sets. In other settings, such as groups, "points" do not see everything and the property must really be tested on every $X$ .

Formal mathematicsF

The universal property in Lean

In Lean we work with types and functions, the type-theoretic counterpart of sets and functions. The product type A × B comes with Prod.fst and Prod.snd, our $\pi_A$ and $\pi_B$ . Here is the pairing and the two equations, which hold by computation (rfl):

pairLean 4Formally verified

/-- The **pairing** `⟨f, g⟩ : X → A × B` of `f : X → A` and `g : X → B` sends `x` to the
ordered pair `(f x, g x)`. -/
def pair {X A B : Type u} (f : X → A) (g : X → B) : X → A × B :=
  fun x => (f x, g x)

Axioms used: No axiomsformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

fst_comp_pairLean 4Proved here from basic factsFormally verified

/-- First projection after pairing gives back `f`: `π₁ ∘ ⟨f, g⟩ = f`. Both sides send `x` to
`f x`, so Lean accepts `rfl` ("true by computation"). -/
theorem fst_comp_pair {X A B : Type u} (f : X → A) (g : X → B) :
    Prod.fst ∘ pair f g = f :=
  rfl

Axioms used: No axiomsformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

snd_comp_pairLean 4Proved here from basic factsFormally verified

/-- Second projection after pairing gives back `g`: `π₂ ∘ ⟨f, g⟩ = g`. -/
theorem snd_comp_pair {X A B : Type u} (f : X → A) (g : X → B) :
    Prod.snd ∘ pair f g = g :=
  rfl

Axioms used: No axiomsformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

Uniqueness follows the human proof line by line: compare at each x, and use that a pair is determined by its coordinates (Prod.ext).

pair_uniqueLean 4Proved here from basic factsFormally verified

/-- **Uniqueness.** If `h : X → A × B` satisfies `π₁ ∘ h = f` and `π₂ ∘ h = g`, then
`h = ⟨f, g⟩`. Proof, as in the lesson: for each `x`, the pair `h x` has first coordinate
`f x` and second coordinate `g x`, and a pair is determined by its two coordinates
(`Prod.ext`). -/
theorem pair_unique {X A B : Type u} {f : X → A} {g : X → B} (h : X → A × B)
    (h₁ : Prod.fst ∘ h = f) (h₂ : Prod.snd ∘ h = g) : h = pair f g := by
  funext x
  apply Prod.ext
  · -- first coordinates: `(h x).1 = f x`
    exact congrFun h₁ x
  · -- second coordinates: `(h x).2 = g x`
    exact congrFun h₂ x

Axioms used: Quot.soundformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

Theorem 2 becomes an equivalence — Lean's word for a bijection packaged with its inverse and the two round-trip proofs. Mathlib already contains it, and the counting corollary follows by comparing cardinalities:

mapsIntoProdEquivLean 4Formally verified

/-- Functions `X → A × B` correspond one-to-one with pairs of functions `(X → A, X → B)`.
Forward: compose with the two projections. Backward: pair. The two round trips are the
identity: one by `fst_comp_pair`/`snd_comp_pair`, the other by `pair_unique`. -/
def mapsIntoProdEquiv (X A B : Type u) : (X → A × B) ≃ (X → A) × (X → B) where
  toFun h := (Prod.fst ∘ h, Prod.snd ∘ h)
  invFun fg := pair fg.1 fg.2
  left_inv h := (pair_unique h rfl rfl).symm
  right_inv _ := rfl

Axioms used: Quot.soundformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

mapsIntoProdEquivLibraryLean 4Applies a library theoremFormally verified

/-- Mathlib already has this correspondence, for dependent functions too:
`Equiv.arrowProdEquivProdArrow`. Here we just specialise it to ordinary functions. -/
def mapsIntoProdEquivLibrary (X A B : Type u) : (X → A × B) ≃ (X → A) × (X → B) :=
  Equiv.arrowProdEquivProdArrow X (fun _ => A) (fun _ => B)

Axioms used: No axiomsformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

card_maps_into_prodLean 4Proved here from basic factsFormally verified

/-- **Counting.** For finite types, `|A × B|^|X| = |A|^|X| · |B|^|X|`. The left side counts
functions `X → A × B`, the right side counts pairs of functions, and `mapsIntoProdEquiv`
matches them up one-to-one. -/
theorem card_maps_into_prod (X A B : Type u) [Fintype X] [DecidableEq X] [Fintype A]
    [Fintype B] :
    Fintype.card (A × B) ^ Fintype.card X =
      Fintype.card A ^ Fintype.card X * Fintype.card B ^ Fintype.card X := by
  calc Fintype.card (A × B) ^ Fintype.card X
      = Fintype.card (X → A × B) := Fintype.card_fun.symm
    _ = Fintype.card ((X → A) × (X → B)) := Fintype.card_congr (mapsIntoProdEquiv X A B)
    _ = Fintype.card (X → A) * Fintype.card (X → B) := Fintype.card_prod _ _
    _ = Fintype.card A ^ Fintype.card X * Fintype.card B ^ Fintype.card X := by
        rw [Fintype.card_fun, Fintype.card_fun]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

Now the universal property itself, as a definition. ∃! is Lean's "there exists exactly one".

IsProductLean 4Formally verified

/-- `IsProduct p q` says that the type `P` with maps `p : P → A` and `q : P → B` has the
**universal property of the product**: for every type `X` and every pair of maps
`f : X → A`, `g : X → B` there is **exactly one** `h : X → P` with `p ∘ h = f` and
`q ∘ h = g`. (`∃!` is Lean's "there exists exactly one".) -/
def IsProduct {A B P : Type u} (p : P → A) (q : P → B) : Prop :=
  ∀ (X : Type u) (f : X → A) (g : X → B), ∃! h : X → P, p ∘ h = f ∧ q ∘ h = g

Axioms used: No axiomsformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

prod_isProductLean 4Proved here from basic factsFormally verified

/-- The set of ordered pairs `A × B`, with its two projections, has the universal property:
existence is the pairing `⟨f, g⟩`, uniqueness is `pair_unique`. -/
theorem prod_isProduct (A B : Type u) : IsProduct (Prod.fst : A × B → A) Prod.snd := by
  intro X f g
  refine ⟨pair f g, ⟨fst_comp_pair f g, snd_comp_pair f g⟩, ?_⟩
  rintro h ⟨h₁, h₂⟩
  exact pair_unique h h₁ h₂

Axioms used: Quot.soundformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

swap_isProductLean 4Proved here from basic factsFormally verified

/-- A *different* type can be a product of `A` and `B`: `B × A`, with the first map reading
off the **second** coordinate and the second map the **first**. Given `f` and `g`, the unique
compatible map is `x ↦ (g x, f x)`. -/
theorem swap_isProduct (A B : Type u) : IsProduct (Prod.snd : B × A → A) Prod.fst := by
  intro X f g
  refine ⟨fun x => (g x, f x), ⟨rfl, rfl⟩, ?_⟩
  rintro h ⟨h₁, h₂⟩
  funext x
  exact Prod.ext (congrFun h₂ x) (congrFun h₁ x)

Axioms used: Quot.soundformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

And the main theorem, in two steps exactly as in the proof above:

eq_id_of_isProductLean 4Proved here from basic factsFormally verified

/-- **The key trick.** If `(P, p, q)` is a product and `k : P → P` is compatible with the maps
(`p ∘ k = p` and `q ∘ k = q`), then `k` is the identity. Reason: apply the universal property
with `X = P`, `f = p`, `g = q`. Both `k` and `id` are compatible maps, and there is only one. -/
theorem eq_id_of_isProduct {A B P : Type u} {p : P → A} {q : P → B} (hP : IsProduct p q)
    (k : P → P) (hk₁ : p ∘ k = p) (hk₂ : q ∘ k = q) : k = id := by
  obtain ⟨_, _, huniq⟩ := hP P p q
  have hk : k = _ := huniq k ⟨hk₁, hk₂⟩
  have hid : id = _ := huniq id ⟨rfl, rfl⟩
  exact hk.trans hid.symm

Axioms used: No axiomsformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

isProduct_bijectiveLean 4Proved here from basic factsFormally verified

/-- **A product is determined up to a unique compatible bijection.** If `(P, p, q)` has the
universal property, then `⟨p, q⟩ : P → A × B` is a bijection. (It is compatible with the maps
by `fst_comp_pair`/`snd_comp_pair`, and it is the *only* compatible map by `pair_unique`.)

Proof, as in the lesson. The universal property of `P`, applied to the projections of `A × B`,
gives `ψ : A × B → P` with `p ∘ ψ = π₁` and `q ∘ ψ = π₂`. Then `ψ ∘ ⟨p, q⟩ : P → P` is
compatible with `p` and `q`, so it is the identity by `eq_id_of_isProduct`; and
`⟨p, q⟩ ∘ ψ : A × B → A × B` is compatible with the projections, so it is the identity by
`pair_unique`. A map with a two-sided inverse is a bijection. -/
theorem isProduct_bijective {A B P : Type u} {p : P → A} {q : P → B} (hP : IsProduct p q) :
    Function.Bijective (pair p q) := by
  obtain ⟨ψ, ⟨hψ₁, hψ₂⟩, _⟩ := hP (A × B) (Prod.fst : A × B → A) (Prod.snd : A × B → B)
  rw [Function.bijective_iff_has_inverse]
  refine ⟨ψ, ?_, ?_⟩
  · -- `ψ ∘ ⟨p, q⟩ = id` on `P`
    have h : ψ ∘ pair p q = id := by
      apply eq_id_of_isProduct hP
      · calc p ∘ (ψ ∘ pair p q) = (p ∘ ψ) ∘ pair p q := rfl
          _ = Prod.fst ∘ pair p q := by rw [hψ₁]
          _ = p := fst_comp_pair p q
      · calc q ∘ (ψ ∘ pair p q) = (q ∘ ψ) ∘ pair p q := rfl
          _ = Prod.snd ∘ pair p q := by rw [hψ₂]
          _ = q := snd_comp_pair p q
    exact congrFun h
  · -- `⟨p, q⟩ ∘ ψ = id` on `A × B`
    have h : pair p q ∘ ψ = id := by
      have hu : pair p q ∘ ψ = pair (Prod.fst : A × B → A) (Prod.snd : A × B → B) :=
        pair_unique (pair p q ∘ ψ) hψ₁ hψ₂
      rw [hu]
      rfl
    exact congrFun h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

Finally, the two fake products. Each one fails one half of "exactly one":

not_isProduct_emptyLean 4Proved here from basic factsFormally verified

/-- **Existence can fail.** Take `A = B = Unit` (one element each) and `P = Empty`. There is no
map at all from `Unit` to `Empty`, so the pair of maps `Unit → Unit` cannot factor through `P`. -/
theorem not_isProduct_empty :
    ¬ IsProduct (fun e : Empty => (Empty.elim e : Unit)) (fun e : Empty => (Empty.elim e : Unit)) := by
  intro hP
  obtain ⟨h, _, _⟩ := hP Unit id id
  exact (h ()).elim

Axioms used: No axiomsformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

not_isProduct_boolLean 4Proved here from basic factsFormally verified

/-- **Uniqueness can fail.** Take `A = B = Unit` and `P = Bool` (two elements), with the only
possible maps `P → Unit`. Then *both* constant maps `Unit → Bool` are compatible, so there is
not exactly one. The universal property needs its "exactly". -/
theorem not_isProduct_bool : ¬ IsProduct (fun _ : Bool => ()) (fun _ : Bool => ()) := by
  intro hP
  obtain ⟨_, _, huniq⟩ := hP Unit id id
  have ht : (fun _ : Unit => true) = _ := huniq (fun _ => true) ⟨rfl, rfl⟩
  have hf : (fun _ : Unit => false) = _ := huniq (fun _ => false) ⟨rfl, rfl⟩
  have h : (fun _ : Unit => true) = (fun _ : Unit => false) := ht.trans hf.symm
  exact Bool.noConfusion (congrFun h ())

Axioms used: No axiomsformal/Lumenary/IntroUniversalProperties.leanTry it in the Lean web editor

ComputationC

Counting compatible maps

Counting compatible maps into a candidate productPythonExhaustive finite checkCounterexampleComputationally tested

"""Testing the universal property of the product on small finite sets.

A candidate product is a set P with two maps p : P -> A and q : P -> B.
For every pair of functions f : X -> A and g : X -> B we count the maps
h : X -> P with p(h(x)) = f(x) and q(h(x)) = g(x) for all x, by listing all
maps X -> P. The universal property says the count is always exactly 1.
We test the set of ordered pairs, a 6-element product that is not made of
pairs, and two fakes: one where some counts are 0 (existence fails) and one
where counts are 4 (uniqueness fails). This is exhaustive-finite evidence
for the small sets X used here; the lesson's proof covers every X.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from collections import Counter
from itertools import product
import textwrap

A = ("red", "blue")
B = (1, 2, 3)

def all_functions(domain, codomain):
    """Every function domain -> codomain, as a tuple of values in domain order."""
    return list(product(codomain, repeat=len(domain)))

def count_compatible(domain, P, p, q, f, g):
    """Number of h : domain -> P with p(h(x)) = f(x) and q(h(x)) = g(x).

    ``f``, ``g`` are tuples of values (one per element of ``domain``); ``p``,
    ``q`` are dicts on P. Every map h : domain -> P is listed and tested.
    """
    count = 0
    for h in product(P, repeat=len(domain)):
        if all(p[h[i]] == f[i] and q[h[i]] == g[i] for i in range(len(domain))):
            count += 1
    return count

def profile(domain, P, p, q):
    """Counter {number of compatible h: how many pairs (f, g) have it}."""
    fs = all_functions(domain, A)
    gs = all_functions(domain, B)
    return Counter(count_compatible(domain, P, p, q, f, g) for f in fs for g in gs)

def is_product_on(domain, P, p, q):
    """True if every pair (f, g) on ``domain`` has exactly one compatible h."""
    return set(profile(domain, P, p, q)) == {1}

def candidates():
    """The four candidate products (name, P, p, q) studied in the lesson."""
    pairs = list(product(A, B))
    six = list(range(1, 7))
    triples = [(a, b, c) for a, b in pairs for c in (0, 1)]
    return [
        ("ordered pairs A x B", pairs,
         {u: u[0] for u in pairs}, {u: u[1] for u in pairs}),
        ("numbers 1..6", six,
         {k: "red" if k <= 3 else "blue" for k in six},
         {k: (k - 1) % 3 + 1 for k in six}),
        ("A with q constant 1", list(A),
         {a: a for a in A}, {a: 1 for a in A}),
        ("A x B x {0, 1}", triples,
         {u: u[0] for u in triples}, {u: u[1] for u in triples}),
    ]

def main():
    X = ("x", "y")
    print(f"A = {{red, blue}}, B = {{1, 2, 3}}, X = {{x, y}}")
    n_pairs = len(all_functions(X, A)) * len(all_functions(X, B))
    print(f"pairs of functions (f, g): {n_pairs}")
    print("candidate P               |P|  compatible h per (f, g)   product?")
    for name, P, p, q in candidates():
        prof = profile(X, P, p, q)
        if len(prof) == 1:
            counts = "{} for all {}".format(*next(iter(prof.items())))
        else:
            counts = ", ".join(f"{k} for {v}" for k, v in sorted(prof.items()))
        verdict = "yes" if set(prof) == {1} else "no"
        print(f"{name:<25} {len(P):>3}  {counts:<24}  {verdict}")
    print()
    print("Listing maps: |A x B|^|X| = |A|^|X| * |B|^|X|")
    pairs = candidates()[0][1]
    for n in range(5):
        dom = tuple(range(n))
        lhs = len(all_functions(dom, pairs))
        rhs = len(all_functions(dom, A)) * len(all_functions(dom, B))
        print(f"  |X| = {n}: {lhs:>5} maps X -> A x B, {rhs:>5} pairs (f, g)")
    X3 = ("x", "y", "z")
    name, P, p, q = candidates()[1]
    print(f"With |X| = 3, '{name}' still gives one h each time: "
          f"{is_product_on(X3, P, p, q)}")
    print()
    print(textwrap.fill(
        "Epistemic status: exhaustive-finite. Every pair (f, g) and every map "
        "h was checked, but only for X with 2 or 3 elements and these "
        "particular A and B. The universal property is about every set X; "
        "the lesson proves it for ordered pairs, and proves that any two "
        "products are matched by exactly one compatible bijection.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The two genuine products give $1$ for all $36$ pairs. The candidate with too few elements gives $0$ for most pairs (existence fails); the one with an extra bit gives $4 = 2^2$ for every pair (uniqueness fails; with $|X| = 2$ there are two free bits). This is exhaustive-finite evidence: complete for these particular small sets, silent about all others. The proofs above are what cover every $X$ .

Exercises

1. Products by maps: a first universal property

Warm-upHuman

Let $X = \{1, 2, 3\}$ , $f : X \to \{\text{red}, \text{blue}\}$ with $f(1) = \text{red}$ and $f(2) = f(3) = \text{blue}$ , and $g : X \to \Z$ with $g(n) = n^2$ . What is $\langle f, g \rangle(2)$ ?

Choose one

(\text{blue}, 4)

(4, \text{blue})

(\text{blue}, 2)

(\text{red}, 4)

2. Products by maps: a first universal property

Warm-upHuman

Let $|X| = 2$ , $|A| = 2$ and $|B| = 3$ . How many functions $X \to A \times B$ are there?

3. Products by maps: a first universal property

CoreHuman

Let $A = B = \{0, 1\}$ . Which of these $(P, p, q)$ are products of $A$ and $B$ ? (Choose all that apply.)

Choose all that apply

P = \{0, 1, 2, 3\}

,

p(n) = n \bmod 2

,

q(n) = \lfloor n/2 \rfloor

P = A \times B

with

p(a, b) = b

and

q(a, b) = a

P = \{0, 1, 2\}

,

p(n) = \min(n, 1)

,

q(n) = \lfloor n/2 \rfloor

P = \{0, 1, \dots, 7\}

,

p(n) = n \bmod 2

,

q(n) = \lfloor n/2 \rfloor \bmod 2

4. Products by maps: a first universal property

CoreHuman

In the proof of Theorem 3 we showed that $\psi \circ \varphi = \mathrm{id}_P$ . Which fact justifies that final equality?

Choose one

Both

\psi \circ \varphi

and

\mathrm{id}_P

are compatible with

p

and

q

, and the universal property of

P

(with

X = P

) allows only one such map.

\psi

was defined to be the inverse of

\varphi

.

\varphi

is injective.The universal property of

A \times B

.

5. Products by maps: a first universal property

CoreHuman

Let $P = A \times B \times \{0, 1\}$ , with $p(a, b, c) = a$ and $q(a, b, c) = b$ . Let $X$ have $3$ elements and fix $f : X \to A$ and $g : X \to B$ . How many functions $h : X \to P$ satisfy $p \circ h = f$ and $q \circ h = g$ ?

6. Products by maps: a first universal property

CoreFormal

Given p : P → A, q : P → B, f : X → A and g : X → B, which Lean proposition says "there is exactly one $h$ compatible with $f$ and $g$ "?

Choose one

∃! h : X → P, p ∘ h = f ∧ q ∘ h = g∃ h : X → P, p ∘ h = f ∧ q ∘ h = g∀ h : X → P, p ∘ h = f ∧ q ∘ h = g∃! h : X → P, p ∘ h = f ∨ q ∘ h = g

7. Products by maps: a first universal property

CoreComputational

Represent a finite function as a Python dict. Write pairing(f, g), which takes two dicts with the same keys and returns the dict $x \mapsto (f(x), g(x))$ , and components(h), which takes a dict whose values are pairs and returns the two dicts $(\pi_A \circ h, \pi_B \circ h)$ . Check that the two are inverse to each other (Theorem 2).

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

8. Products by maps: a first universal property

StretchHuman

Let $|A| = 3$ and $|B| = 4$ , and suppose a set $P$ with maps $p : P \to A$ and $q : P \to B$ has the universal property of the product. How many elements must $P$ have?

9. Products by maps: a first universal property

StretchHuman

Make the positive integers into a category: there is one arrow $x \to y$ exactly when $x$ divides $y$ (and no arrow otherwise). A product of $12$ and $18$ is a number $P$ with arrows $P \to 12$ and $P \to 18$ such that every $X$ with arrows $X \to 12$ and $X \to 18$ has an arrow $X \to P$ (uniqueness is automatic, as there is at most one arrow between two numbers). What is $P$ ?

Choose one

6

36

216

3

Common misconceptionsH

Common misconceptions

Misconception

"The universal property defines some new object, different from $A \times B$ ." It describes $A \times B$ by its behaviour. The set of ordered pairs has the property (Theorem 1), and anything else with the property is matched with it by exactly one compatible bijection (Theorem 3).

Misconception

Forgetting the uniqueness part. "There is a compatible $h$ " is not enough: $A \times B \times \{0, 1\}$ has compatible maps for every $f, g$ but is not a product. Uniqueness is what makes the proof of Theorem 3 work — the Lemma is nothing but uniqueness.

Misconception

"Only the set of ordered pairs is really a product." Any set with two maps having the property serves equally well, like $\{1, \dots, 6\}$ in the examples, or $B \times A$ with swapped maps. Even "ordered pair" itself is defined in more than one way in set theory (see below); the universal property is what all the definitions agree on.

Misconception

Confusing $\langle f, g \rangle$ with $f \times g$ . For $f : X \to A$ and $g : Y \to B$ , the map $f \times g : X \times Y \to A \times B$ sends $(x, y)$ to $(f(x), g(y))$ : two inputs, processed separately. The pairing $\langle f, g \rangle : X \to A \times B$ takes one input and feeds it to both. They are related by $\langle f, g \rangle = (f \times g) \circ \Delta$ , where $\Delta(x) = (x, x)$ (when $Y = X$ ).

Misconception

"Unique up to bijection" means "equal". $\{1, \dots, 6\}$ and $A \times B$ are different sets. What is unique is the compatible bijection between them — so we may treat them as interchangeable, as long as we use that bijection to translate.

ViewpointsH

The same idea, seen by others

Geometry— Coordinates are projections

When Descartes and Fermat put coordinates on the plane, they identified it with $\R \times \R$ : a point is its pair of coordinates, and the two coordinate functions are the projections. A curve $\gamma : I \to \R^2$ is the pairing of its coordinate functions, and every statement about the curve can be translated into two statements about real functions. In three dimensions $\R^3 = \R \times \R \times \R$ has three projections, and a path in space is three functions of time — exactly what a GPS receiver records (adding altitude).

Topology— Continuity, one coordinate at a time

A map $\gamma : \R \to \R^2$ is continuous if and only if both coordinate functions $\pi_1 \circ \gamma$ and $\pi_2 \circ \gamma$ are continuous. So $t \mapsto (\cos t, \sin t)$ is continuous because $\cos$ and $\sin$ are. This is the universal property again, now for continuous maps: for spaces $A$ and $B$ , the product topology on $A \times B$ is chosen precisely so that continuous maps $X \to A \times B$ correspond to pairs of continuous maps $X \to A$ , $X \to B$ . (It is the coarsest topology making both projections continuous.) See point-set topology.

Algebra— Direct products of groups

For groups $G$ and $H$ , the set $G \times H$ with componentwise operation $(g, h)(g', h') = (gg', hh')$ is again a group, and a homomorphism $K \to G \times H$ is the same as a pair of homomorphisms $K \to G$ and $K \to H$ . For example, $n \mapsto (n \bmod 2, \, n \bmod 3)$ pairs two homomorphisms $\Z \to \Z/2$ and $\Z \to \Z/3$ ; it sends exactly the multiples of $6$ to $(0, 0)$ , and this leads to the Chinese remainder theorem $\Z/6 \cong \Z/2 \times \Z/3$ , an isomorphism you can check in structure-preserving maps.

Probability— Random vectors, and a warning

Two random variables $X, Y : \Omega \to \R$ on the same sample space pair up into one random vector $(X, Y) : \Omega \to \R^2$ , and every random vector arises this way. But the distributions of $X$ and $Y$ do not determine the distribution of $(X, Y)$ . Toss a fair coin: let $X = 1$ for heads and $0$ for tails, and compare $Y = X$ with $Y = 1 - X$ . In both cases $Y$ is a fair $0/1$ variable, yet $(X, Y)$ takes the values $(0,0), (1,1)$ in the first case and $(0,1), (1,0)$ in the second. The universal property is about functions on the same $\Omega$ , not about distributions — which is exactly why independence and correlation are interesting (conditional probability and independence).

Logic— 'And' has the same property

Order propositions by implication. Then $P \wedge Q$ behaves exactly like a product: $R \Rightarrow P \wedge Q$ holds if and only if both $R \Rightarrow P$ and $R \Rightarrow Q$ hold, and $P \wedge Q$ implies each of $P$ and $Q$ (the "projections"). In a proof assistant such as Lean this is literal: a proof of $P \wedge Q$ is a pair of proofs, written ⟨hp, hq⟩. See First steps in Lean.

Wonder Trails

Wonder Trail · Optional · never gradedThe product, by its mapsCan you describe the set of pairs

A \times B

without ever looking inside it — only by how functions go into it?Follow the trail Wonder Trail · Optional · never gradedArrows that composeWhat do functions between sets, maps between groups and continuous maps between shapes have in common? What if we studied only the arrows?Follow the trail

Set-theoretic connectionH

Set-theoretic connection: what is an ordered pair?

In set theory everything is a set, so an ordered pair must be one too. The standard choice, due to Kazimierz Kuratowski (1921), is

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

One proves that $(a, b) = (a', b')$ exactly when $a = a'$ and $b = b'$ — the one fact our uniqueness proof used. But this is not the only choice: Norbert Wiener proposed a different encoding in 1914, and others work too. Each encoding produces a different set " $A \times B$ ", but every one of them satisfies the universal property, so by Theorem 3 they are all matched by unique compatible bijections. The encoding is an implementation; the universal property is the specification.

Category-theoretic connectionH

Products in any category

In a category (see Composition), a product of objects $A$ and $B$ is an object $P$ with arrows $p : P \to A$ , $q : P \to B$ such that for every object $X$ and arrows $f : X \to A$ , $g : X \to B$ there is exactly one arrow $h : X \to P$ with $p \circ h = f$ and $q \circ h = g$ . Our definition is the case of the category of sets, and the proof of Theorem 3 works word for word in every category: any two products of $A$ and $B$ are isomorphic by a unique isomorphism compatible with the projections.

The same words describe very different things:

In sets: the Cartesian product. In groups: the direct product. In spaces: the product space.
In the positive integers ordered by divisibility (an arrow $x \to y$ means $x$ divides $y$ ), a product of $12$ and $18$ is a number that divides both, and is divisible by every number dividing both: $\gcd(12, 18) = 6$ .
In the subsets of a set ordered by $\subseteq$ , the product of $A$ and $B$ is $A \cap B$ .

Turning all the arrows around gives the coproduct: in sets, the disjoint union; for divisibility, the least common multiple. These ideas continue in universal properties, products and coproducts and, eventually, the Yoneda lemma, which says that every object is determined up to isomorphism by the maps into it.

History & global context

History and global context

Coordinates. Describing a position by two numbers is ancient. Ptolemy's Geography (2nd century, Alexandria) listed places by longitude and latitude; in 9th-century Baghdad, al-Khwārizmī's Book of the Description of the Earth tabulated coordinates for thousands of places; in 3rd-century China, the cartographer Pei Xiu set out principles of mapmaking that included a scale and a rectangular grid. In 17th-century France, René Descartes (La Géométrie, 1637) and Pierre de Fermat turned coordinates into a method for geometry.
Ordered pairs as sets. Norbert Wiener (1914) and Kazimierz Kuratowski (1921) showed how to define ordered pairs inside set theory.
Universal properties. In the late 1940s, mathematicians began describing constructions by their maps rather than their elements. Pierre Samuel's 1948 paper On universal mappings and free topological groups used "universal mappings"; Saunders Mac Lane's papers on duality for groups (1948–1950) characterised products and free products by such properties, building on the theory of categories that he and Samuel Eilenberg had introduced in 1945. The style was taken up by the Bourbaki group and by Daniel Kan's adjoint functors (1958), and is now everywhere.

A journey is two functions

Describing a set from the outside

Projections, pairing and the universal property

The picture, and two explorations

Examples and non-examples

The theorems, with proofs

The universal property in Lean

Counting compatible maps

Exercises

Common misconceptions

The same idea, seen by others

Wonder Trails

Set-theoretic connection: what is an ordered pair?

Products in any category

History and global context

Further reading