Products, coproducts, initial and terminal objects

Lens

MotivationH

The same construction, everywhere

The Cartesian product of sets, the direct product of groups, the product of topological spaces, the greatest common divisor of two numbers and the logical "and" of two statements look like five unrelated constructions. So do their partners: the disjoint union of sets, the free product of groups, the direct sum of abelian groups, the least common multiple and the logical "or".

They are not unrelated. Each of the first five is the answer to one question, asked in five different categories: what is the most economical object that maps to both $A$ and $B$ ? Each of the second five answers the mirror-image question: what is the most economical object that both $A$ and $B$ map to? The answers are called the product and the coproduct. When the pair is replaced by no objects at all, the same questions produce terminal and initial objects.

This lesson defines these notions by their universal properties, proves that the definitions pin the objects down up to a unique isomorphism, and then computes them — sometimes with surprising answers. The coproduct of two copies of $\Z$ in the category of groups is a non-abelian group whose geometry is a tree; the coproduct of $\Z/2$ and $\Z/3$ in commutative rings is the zero ring; and two fields usually have no product at all.

IntuitionH

Generalised elements and the best possible pair

In $\cat{Set}$ , an element of $A \times B$ is the same thing as a pair (an element of $A$ , an element of $B$ ). Category theory has no elements in general, but it has a replacement: a morphism $x : X \to A$ is a generalised element of $A$ "of shape $X$ " (in $\cat{Set}$ , a map $\{\ast\} \to A$ is an ordinary element). The product is then defined so that the slogan stays true for generalised elements:

\text{morphisms } X \to A \times B \quad \longleftrightarrow \quad \text{pairs of morphisms } (X \to A,\; X \to B).

The projections $\pi_1, \pi_2$ turn a morphism into a pair; the universal property says that this is a bijection, for every $X$ . Existence of the inverse says $A \times B$ is big enough to hold every pair; uniqueness says it has nothing superfluous. The experiment below shows both conditions failing for wrong candidates: $A \times B \times \{0, 1\}$ is too big (two morphisms for each pair), and $A$ alone is too small (some pairs have none).

The coproduct reverses every arrow: morphisms out of $A \sqcup B$ correspond to pairs of morphisms out of $A$ and out of $B$ — to define a map on $A \sqcup B$ , you define it on each piece separately. That is case analysis, and it is exactly how one defines a function on a disjoint union.

DefinitionsH

Definitions

Throughout, $\mathcal{C}$ is a category and composition is written $g \circ f$ .

Definition— terminal and initial objects

An object $T$ is terminal if for every object $X$ there is exactly one morphism $X \to T$ . An object $I$ is initial if for every object $X$ there is exactly one morphism $I \to X$ . An object that is both initial and terminal is a zero object.

Definition— product

A product of objects $A$ and $B$ is an object $P$ with morphisms $\pi_1 : P \to A$ and $\pi_2 : P \to B$ (the projections) such that for every object $X$ and every pair of morphisms $f : X \to A$ , $g : X \to B$ there is a unique morphism $h : X \to P$ with $\pi_1 \circ h = f$ and $\pi_2 \circ h = g$ . We write $P = A \times B$ and $h = \langle f, g \rangle$ .

The universal property of the product: every pair

f, g

factors through

A \times B

by exactly one dashed arrow.

More generally, a product of a family $(A_i)_{i \in I}$ is an object $\prod_i A_i$ with projections $\pi_i$ such that every family $f_i : X \to A_i$ factors as $f_i = \pi_i \circ h$ for a unique $h$ . For $I = \varnothing$ the condition says: for every $X$ there is a unique $h : X \to P$ . A terminal object is an empty product.

Definition— opposite category and coproduct

The opposite category $\mathcal{C}^{\mathrm{op}}$ has the same objects and a morphism $f^{\mathrm{op}} : B \to A$ for each $f : A \to B$ , with composition reversed. A coproduct of $A$ and $B$ in $\mathcal{C}$ is a product of $A$ and $B$ in $\mathcal{C}^{\mathrm{op}}$ . Unpacked: an object $S = A \sqcup B$ with morphisms $\iota_1 : A \to S$ , $\iota_2 : B \to S$ (the injections) such that for every pair $f : A \to Y$ , $g : B \to Y$ there is a unique $[f, g] : S \to Y$ with $[f, g] \circ \iota_1 = f$ and $[f, g] \circ \iota_2 = g$ . An initial object is an empty coproduct.

The coproduct: the same picture with every arrow reversed.

Definition— cones over a pair

A cone over the pair $(A, B)$ is an object $X$ with morphisms $f : X \to A$ , $g : X \to B$ . A morphism of cones $(X, f, g) \to (X', f', g')$ is a morphism $h : X \to X'$ with $f' \circ h = f$ and $g' \circ h = g$ . Cones and their morphisms form a category $\mathrm{Cone}(A, B)$ .

Worked examplesH

A tour of products and coproducts

Category	terminal	initial	$A \times B$	$A \sqcup B$
$\cat{Set}$	any one-point set	$\varnothing$	pairs $(a, b)$	disjoint union $A \times \{1\} \cup B \times \{2\}$
$\cat{Grp}$	trivial group	trivial group	direct product	free product $A * B$
$\cat{Ab}$ , $\cat{Vect}_k$	$0$	$0$	direct sum $A \oplus B$	the same $A \oplus B$
$\cat{Ring}$ (unital)	zero ring	$\Z$	$R \times S$	free product of rings
$\cat{CRing}$	zero ring	$\Z$	$R \times S$	tensor product $R \otimes_{\Z} S$
$\cat{Top}$	one-point space	$\varnothing$	product topology	disjoint union topology
poset $(P, \le)$	greatest element	least element	meet $a \wedge b$	join $a \vee b$
$\cat{Field}$	none	none	usually none	usually none

Example— Sets

$A \times B$ with the coordinate projections is a product: given $f, g$ , the map $h(x) = (f(x), g(x))$ works, and any $h$ with $\pi_1 h = f$ , $\pi_2 h = g$ has both coordinates determined. The disjoint union $A \sqcup B = (A \times \{1\}) \cup (B \times \{2\})$ is a coproduct: $[f, g](a, 1) = f(a)$ , $[f, g](b, 2) = g(b)$ , and this is forced. (The plain union $A \cup B$ is not a coproduct when $A \cap B \neq \varnothing$ : for $A = B = \{\ast\}$ , the maps $f = \mathrm{id}$ and $g$ constant at a different point cannot both be extended.) The empty set is initial (the empty function is the unique map $\varnothing \to X$ ) and every one-point set is terminal. The empty set is not terminal: there is no map $\{\ast\} \to \varnothing$ .

Example— Groups: the free product

The direct product $G \times H$ with componentwise multiplication is a product in $\cat{Grp}$ , as in $\cat{Set}$ — the induced map $x \mapsto (f(x), g(x))$ is a homomorphism. The coproduct is the free product $G * H$ : its elements are reduced words $x_1 x_2 \cdots x_n$ with letters alternately from $G \setminus \{e\}$ and $H \setminus \{e\}$ , multiplied by concatenation followed by cancellation. Given $f : G \to K$ and $g : H \to K$ , the map $[f, g]$ sends a word to the product of the images of its letters in $K$ ; it is the only homomorphism extending $f$ and $g$ , because the letters generate $G * H$ . (That reduced words multiply associatively is the normal form theorem for free products; see the reading list.) For example $\Z * \Z$ is the free group on two generators, and $\Z/2 * \Z/2$ is the infinite dihedral group.

Example— Abelian groups: product and coproduct coincide

In $\cat{Ab}$ the direct sum $A \oplus B$ is a product (as in $\cat{Grp}$ ) and a coproduct with injections $a \mapsto (a, 0)$ , $b \mapsto (0, b)$ : given $f : A \to C$ and $g : B \to C$ , the map $[f, g](a, b) = f(a) + g(b)$ is a homomorphism because $C$ is abelian, and it is the only one extending $f$ and $g$ since $(a, b) = (a, 0) + (0, b)$ . The same holds in $\cat{Vect}_k$ and $R\text{-}\cat{Mod}$ . For infinitely many factors the two notions separate: $\prod_{i \in \N} \Z$ is the product, while the coproduct $\bigoplus_{i \in \N} \Z$ is the subgroup of sequences with finitely many non-zero terms.

Example— Rings

In the category of rings with identity (and homomorphisms preserving $1$ ), $\Z$ is initial: the only homomorphism $\Z \to R$ is $n \mapsto n \cdot 1_R$ . The zero ring $\{0\}$ is terminal. They differ, so there is no zero object. In commutative rings the coproduct of $R$ and $S$ is $R \otimes_{\Z} S$ , with $\iota_1(r) = r \otimes 1$ and $\iota_2(s) = 1 \otimes s$ ; for instance $\Z[x] \otimes \Z[y] \cong \Z[x, y]$ , while $\Z/2 \otimes \Z/3 = 0$ , because $1 \otimes 1 = 3(1 \otimes 1) - 2(1 \otimes 1) = 1 \otimes 3 - 2 \otimes 1 = 0$ .

Example— Posets: meets and joins

A poset $(P, \le)$ is a category with exactly one morphism $x \to y$ when $x \le y$ and none otherwise. All equations between morphisms hold automatically, so a product of $a$ and $b$ is just an element $p$ with $p \le a$ , $p \le b$ , and such that $x \le a$ , $x \le b$ imply $x \le p$ : a greatest lower bound (meet). Dually the coproduct is the least upper bound (join). In $(\N_{>0}, \mid)$ , ordered by divisibility, the product of $12$ and $18$ is $\gcd = 6$ and the coproduct is $\operatorname{lcm} = 36$ . In the power set $\mathcal{P}(X)$ they are intersection and union. In the four-element poset $\{2, 3, 12, 18\}$ under divisibility, $2$ and $3$ have two minimal upper bounds and no least one, so they have no coproduct:

The divisibility poset $\{2, 3, 12, 18\}$: each of $2, 3$ divides each of $12, 18$, but $12 \nmid 18$ and $18 \nmid 12$. The pair $2, 3$ has no join and the pair $12, 18$ has no meet.

Example— Topological spaces

The product of spaces $X$ and $Y$ is $X \times Y$ with the product topology, generated by the boxes $U \times V$ : it is the coarsest topology making $\pi_1, \pi_2$ continuous, and a map $h = \langle f, g \rangle : Z \to X \times Y$ is continuous exactly when $f$ and $g$ are, since $h^{-1}(U \times V) = f^{-1}(U) \cap g^{-1}(V)$ . The coproduct is the disjoint union with the topology in which a set is open when its intersection with each piece is open. The one-point space is terminal, the empty space is initial.

Example— Non-existence: fields

In the category of fields (with ring homomorphisms, which are automatically injective), $\mathbb{F}_2$ and $\mathbb{F}_3$ have no product: a product $P$ would come with homomorphisms $P \to \mathbb{F}_2$ and $P \to \mathbb{F}_3$ , forcing $P$ to have characteristic $2$ and characteristic $3$ at once. They have no coproduct either (a field receiving maps from both would again have two characteristics), and the category of fields has neither an initial nor a terminal object (a terminal field would receive a map from fields of every characteristic). Universal properties characterise objects; whether such an object exists is a separate question.

ProofH

Theorems and proofs

Theorem— Theorem 1 (products are unique up to unique isomorphism)

Let $(P, \pi_1, \pi_2)$ and $(Q, \rho_1, \rho_2)$ both be products of $A$ and $B$ . Then there is exactly one morphism $\varphi : P \to Q$ with $\rho_1 \circ \varphi = \pi_1$ and $\rho_2 \circ \varphi = \pi_2$ , and it is an isomorphism.

Proof

First a lemma: if $h, k : X \to P$ satisfy $\pi_1 h = \pi_1 k$ and $\pi_2 h = \pi_2 k$ , then $h = k$ . Indeed both are morphisms whose composites with the projections are the pair $(\pi_1 h, \pi_2 h)$ , and by the uniqueness clause there is only one such morphism.

By the universal property of $Q$ applied to the pair $(\pi_1, \pi_2)$ there is a unique $\varphi = \langle \pi_1, \pi_2 \rangle_Q : P \to Q$ with $\rho_i \circ \varphi = \pi_i$ ; this is the uniqueness claim. Symmetrically there is $\psi : Q \to P$ with $\pi_i \circ \psi = \rho_i$ . Then

\pi_i \circ (\psi \circ \varphi) = \rho_i \circ \varphi = \pi_i = \pi_i \circ \mathrm{id}_P \qquad (i = 1, 2),

so $\psi \circ \varphi = \mathrm{id}_P$ by the lemma, and likewise $\varphi \circ \psi = \mathrm{id}_Q$ .

∎

The proof never looked inside $P$ or $Q$ — no elements, no construction. That is why it applies verbatim in every category, and why we may speak of the product $A \times B$ : any two choices are related by one canonical isomorphism, compatible with all the structure we care about. The same argument shows that terminal (and initial) objects are unique up to unique isomorphism: if $T, T'$ are terminal, the unique maps $T \to T' \to T$ compose to an endomorphism of $T$ , which must be $\mathrm{id}_T$ since $T$ has only one.

Theorem— Theorem 2 (a product is a terminal cone)

A cone $(P, \pi_1, \pi_2)$ over $(A, B)$ is a product of $A$ and $B$ if and only if it is a terminal object of the category $\mathrm{Cone}(A, B)$ .

Proof

A morphism of cones $(X, f, g) \to (P, \pi_1, \pi_2)$ is precisely a morphism $h : X \to P$ with $\pi_1 h = f$ and $\pi_2 h = g$ . "Exactly one such $h$ for every cone $(X, f, g)$ " is the universal property of the product on the one hand and the definition of a terminal object of $\mathrm{Cone}(A, B)$ on the other.

∎

So Theorem 1 is a special case of the uniqueness of terminal objects. This pattern — a universal object is a terminal (or initial) object in a cleverly chosen category — is the backbone of limits and colimits.

Theorem— Theorem 3 (duality)

A coproduct in $\mathcal{C}$ is a product in $\mathcal{C}^{\mathrm{op}}$ , and an initial object of $\mathcal{C}$ is a terminal object of $\mathcal{C}^{\mathrm{op}}$ . Consequently every theorem about products and terminal objects that holds in all categories yields a theorem about coproducts and initial objects: in particular, coproducts and initial objects are unique up to unique isomorphism.

Proof

A morphism $Y \to A$ in $\mathcal{C}^{\mathrm{op}}$ is a morphism $A \to Y$ in $\mathcal{C}$ , and composition is reversed. Translating the universal property of a product of $A$ and $B$ in $\mathcal{C}^{\mathrm{op}}$ , with projections $\iota_1^{\mathrm{op}}, \iota_2^{\mathrm{op}}$ , word for word gives the universal property of a coproduct in $\mathcal{C}$ with injections $\iota_1, \iota_2$ . Theorem 1, applied in the category $\mathcal{C}^{\mathrm{op}}$ , then gives uniqueness of coproducts in $\mathcal{C}$ .

∎

Theorem— Theorem 4 (the coproduct of groups is not the product)

The free product $\Z * \Z$ is not abelian; in particular it is not isomorphic to $\Z \times \Z$ .

Proof

Let $x$ and $y$ be the generators of the two copies of $\Z$ , i.e. $x = \iota_1(1)$ , $y = \iota_2(1)$ . In the symmetric group $S_3$ take the transpositions $\sigma = (1\,2)$ and $\tau = (2\,3)$ ; there are homomorphisms $\Z \to S_3$ with $1 \mapsto \sigma$ and $1 \mapsto \tau$ . By the universal property of the coproduct there is a homomorphism $\varphi : \Z * \Z \to S_3$ with $\varphi(x) = \sigma$ and $\varphi(y) = \tau$ . If $xy = yx$ , then $\sigma\tau = \varphi(xy) = \varphi(yx) = \tau\sigma$ . But $\sigma\tau = (1\,2\,3)$ and $\tau\sigma = (1\,3\,2)$ . Hence $xy \neq yx$ .

∎

The proof used nothing about reduced words — only the universal property and one non-abelian group to map into. In $\cat{Ab}$ , by contrast, the coproduct of $\Z$ and $\Z$ is $\Z \oplus \Z = \Z \times \Z$ : the same two objects have different coproducts in different categories. Coproducts depend on the ambient category, which is the content of the misconception "coproducts look like products".

Theorem— Theorem 5 (products and coproducts in posets)

In a poset regarded as a category, $a$ and $b$ have a product if and only if they have a greatest lower bound, and then the product is $a \wedge b$ ; dually for coproducts and least upper bounds. A least element is an initial object and a greatest element is a terminal object.

Proof

As in the example: all diagrams commute in a poset, so the universal property of a product reduces to " $p \le a$ , $p \le b$ , and every common lower bound is $\le p$ ", which is the definition of a greatest lower bound. Conversely, a product $p$ is a lower bound, and applying the universal property to the cone $a \wedge b$ gives $a \wedge b \le p$ , so $p = a \wedge b$ by antisymmetry. Least and greatest elements are empty joins and meets.

∎

Theorem— Theorem 6 (the product topology is forced)

Let $(X_i)_{i \in I}$ be topological spaces. The product topology on $\prod_i X_i$ — generated by the sets $\pi_i^{-1}(U)$ , $U \subseteq X_i$ open — makes it a product in $\cat{Top}$ . The box topology (generated by all $\prod_i U_i$ , $U_i$ open) in general does not: for $X_i = \R$ , $i \in \N$ , the diagonal map $\Delta : \R \to \R^{\N}$ , $t \mapsto (t, t, t, \dots)$ , has continuous components but is not continuous for the box topology.

Proof

A map $h : Z \to \prod X_i$ is continuous for the product topology iff the preimages of the generating sets are open, i.e. iff every $\pi_i \circ h$ is continuous. So the continuous maps $Z \to \prod X_i$ correspond exactly to families of continuous maps $Z \to X_i$ , which is the universal property (the underlying function is forced, as in $\cat{Set}$ ). For the box topology, $B = \prod_{n \ge 1} (-\tfrac1n, \tfrac1n)$ is open and $\Delta^{-1}(B) = \bigcap_n (-\tfrac1n, \tfrac1n) = \{0\}$ is not open in $\R$ . Since $\Delta$ is continuous for the product topology (each $\pi_n \circ \Delta = \mathrm{id}$ ), the box topology on $\R^{\N}$ is strictly finer and fails the existence half of the universal property.

∎

Formal mathematicsF

Products and coproducts in Lean

We state the universal property by hand, in an arbitrary Mathlib category. Mathlib composes in diagrammatic order, so $\pi_1 \circ h$ is written h ≫ π₁.

IsBinaryProductLean 4Formally verified

/-- **The universal property of a product.** Projections `π₁ : P ⟶ A` and `π₂ : P ⟶ B` make `P`
a product of `A` and `B` when every pair `f : X ⟶ A`, `g : X ⟶ B` factors through `P` by exactly
one morphism `lift f g : X ⟶ P`. Mathlib composes in diagrammatic order: `h ≫ π₁` means
"first `h`, then `π₁`", i.e. `π₁ ∘ h`. -/
structure IsBinaryProduct {A B P : C} (π₁ : P ⟶ A) (π₂ : P ⟶ B) where
  /-- The induced morphism `⟨f, g⟩ : X ⟶ P`. -/
  lift : ∀ {X : C}, (X ⟶ A) → (X ⟶ B) → (X ⟶ P)
  /-- `π₁ ∘ ⟨f, g⟩ = f`. -/
  lift_fst : ∀ {X : C} (f : X ⟶ A) (g : X ⟶ B), lift f g ≫ π₁ = f
  /-- `π₂ ∘ ⟨f, g⟩ = g`. -/
  lift_snd : ∀ {X : C} (f : X ⟶ A) (g : X ⟶ B), lift f g ≫ π₂ = g
  /-- Uniqueness: any `h` with `π₁ ∘ h = f` and `π₂ ∘ h = g` is `⟨f, g⟩`. -/
  uniq : ∀ {X : C} (f : X ⟶ A) (g : X ⟶ B) (h : X ⟶ P), h ≫ π₁ = f → h ≫ π₂ = g → h = lift f g

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

Theorem 1, exactly as proved above: the lemma (hom_ext), the comparison isomorphism, and its uniqueness.

hom_extLean 4Proved here from basic factsFormally verified

/-- **Morphisms into a product are determined by their components.** If `h` and `k` agree after
both projections, both equal `lift (h ≫ π₁) (h ≫ π₂)` by the uniqueness clause. -/
theorem hom_ext (hP : IsBinaryProduct π₁ π₂) {X : C} {h k : X ⟶ P} (h₁ : h ≫ π₁ = k ≫ π₁)
    (h₂ : h ≫ π₂ = k ≫ π₂) : h = k := by
  rw [hP.uniq _ _ h rfl rfl, hP.uniq _ _ k h₁.symm h₂.symm]

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

isoLean 4Formally verified

/-- **Two products are isomorphic.** The comparison maps are `⟨π₁, π₂⟩ : P ⟶ Q` and
`⟨ρ₁, ρ₂⟩ : Q ⟶ P`. Each composite commutes with the projections, so by `hom_ext` it is the
identity — the proof in the lesson, verbatim. -/
def iso (hP : IsBinaryProduct π₁ π₂) (hQ : IsBinaryProduct ρ₁ ρ₂) : P ≅ Q where
  hom := hQ.lift π₁ π₂
  inv := hP.lift ρ₁ ρ₂
  hom_inv_id := hP.hom_ext (by rw [Category.assoc, hP.lift_fst, hQ.lift_fst, Category.id_comp])
    (by rw [Category.assoc, hP.lift_snd, hQ.lift_snd, Category.id_comp])
  inv_hom_id := hQ.hom_ext (by rw [Category.assoc, hQ.lift_fst, hP.lift_fst, Category.id_comp])
    (by rw [Category.assoc, hQ.lift_snd, hP.lift_snd, Category.id_comp])

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

iso_uniqueLean 4Proved here from basic factsFormally verified

/-- **…by a unique isomorphism compatible with the projections.** Any isomorphism `i : P ≅ Q`
with `ρ₁ ∘ i = π₁` and `ρ₂ ∘ i = π₂` is the comparison isomorphism `iso hP hQ`: its forward map
satisfies the defining equations of `lift π₁ π₂`, so uniqueness in `Q`'s universal property
identifies them (and an isomorphism is determined by its forward map). -/
theorem iso_unique (hP : IsBinaryProduct π₁ π₂) (hQ : IsBinaryProduct ρ₁ ρ₂) (i : P ≅ Q)
    (h₁ : i.hom ≫ ρ₁ = π₁) (h₂ : i.hom ≫ ρ₂ = π₂) : i = iso hP hQ := by
  ext
  exact hQ.uniq π₁ π₂ i.hom h₁ h₂

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

Mathlib's own products (A ⨯ B, prod.lift) satisfy our definition, and Mathlib proves Theorem 2 for all limits:

ofHasBinaryProductLean 4Formally verified

/-- **Mathlib's products satisfy our universal property.** When `A` and `B` have a (chosen)
product `A ⨯ B` in Mathlib, its projections `prod.fst`, `prod.snd` form an `IsBinaryProduct`;
the induced map is Mathlib's `prod.lift`, and uniqueness is `prod.hom_ext`. -/
noncomputable def ofHasBinaryProduct (A B : C) [HasBinaryProduct A B] :
    IsBinaryProduct (prod.fst : A ⨯ B ⟶ A) prod.snd where
  lift f g := prod.lift f g
  lift_fst f g := prod.lift_fst f g
  lift_snd f g := prod.lift_snd f g
  uniq f g h h₁ h₂ := prod.hom_ext (by rw [h₁, prod.lift_fst]) (by rw [h₂, prod.lift_snd])

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

product_is_terminal_coneLean 4Applies a library theoremFormally verified

/-- **A product is a terminal cone.** A cone over the pair `(A, B)` is an object with two maps to
`A` and `B` (a `BinaryFan`); cones and their morphisms form a category, and a cone is a limit —
here, a product — exactly when it is a terminal object of that category. This applies Mathlib's
`Cone.isLimitEquivIsTerminal`. -/
theorem product_is_terminal_cone {A B : C} (c : BinaryFan A B) :
    Nonempty (IsLimit c) ↔ Nonempty (IsTerminal c) :=
  ⟨fun ⟨h⟩ => ⟨Cone.isLimitEquivIsTerminal c h⟩,
    fun ⟨h⟩ => ⟨(Cone.isLimitEquivIsTerminal c).symm h⟩⟩

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

Coproducts are defined as products in the opposite category (Theorem 3 becomes a definition), and then unpacked:

IsBinaryCoproductLean 4Formally verified

/-- **A coproduct in `C` is a product in `Cᵒᵖ`.** Injections `ι₁ : A ⟶ S`, `ι₂ : B ⟶ S` make
`S` a coproduct of `A` and `B` when the reversed arrows `ι₁.op : op S ⟶ op A`,
`ι₂.op : op S ⟶ op B` make `op S` a product of `op A` and `op B` in the opposite category.
This *is* the definition — duality is built in. -/
abbrev IsBinaryCoproduct {A B S : C} (ι₁ : A ⟶ S) (ι₂ : B ⟶ S) : Type _ :=
  IsBinaryProduct ι₁.op ι₂.op

Axioms used: propextformal/Lumenary/ProductsCoproducts.leanTry it in the Lean web editor

descLean 4Formally verified

/-- **Unpacking the dual definition: copairing.** Maps `f : A ⟶ Y` and `g : B ⟶ Y` in `C` are
maps `op Y ⟶ op A` and `op Y ⟶ op B` in `Cᵒᵖ`; the product property gives `op Y ⟶ op S`, i.e. a
map `[f, g] : S ⟶ Y` in `C`. -/
def desc (hS : IsBinaryCoproduct ι₁ ι₂) {Y : C} (f : A ⟶ Y) (g : B ⟶ Y) : S ⟶ Y :=
  (hS.lift f.op g.op).unop

Axioms used: propextformal/Lumenary/ProductsCoproducts.leanTry it in the Lean web editor

inl_descLean 4Proved here from basic factsFormally verified

/-- **The copairing restricts correctly:** `[f, g] ∘ ι₁ = f` and `[f, g] ∘ ι₂ = g`. These are the
product equations in `Cᵒᵖ`, read backwards (`unop` of `lift f.op g.op ≫ ι₁.op = f.op`). -/
theorem inl_desc (hS : IsBinaryCoproduct ι₁ ι₂) {Y : C} (f : A ⟶ Y) (g : B ⟶ Y) :
    ι₁ ≫ hS.desc f g = f ∧ ι₂ ≫ hS.desc f g = g :=
  ⟨congrArg Quiver.Hom.unop (hS.lift_fst f.op g.op),
    congrArg Quiver.Hom.unop (hS.lift_snd f.op g.op)⟩

Axioms used: propextformal/Lumenary/ProductsCoproducts.leanTry it in the Lean web editor

desc_uniqueLean 4Proved here from basic factsFormally verified

/-- **…and uniquely:** any `h : S ⟶ Y` with `h ∘ ι₁ = f` and `h ∘ ι₂ = g` is `[f, g]`. This is
the uniqueness clause in `Cᵒᵖ`, applied to `h.op`. -/
theorem desc_unique (hS : IsBinaryCoproduct ι₁ ι₂) {Y : C} (f : A ⟶ Y) (g : B ⟶ Y) (h : S ⟶ Y)
    (h₁ : ι₁ ≫ h = f) (h₂ : ι₂ ≫ h = g) : h = hS.desc f g :=
  congrArg Quiver.Hom.unop
    (hS.uniq f.op g.op h.op (congrArg Quiver.Hom.op h₁) (congrArg Quiver.Hom.op h₂))

Axioms used: propextformal/Lumenary/ProductsCoproducts.leanTry it in the Lean web editor

terminal_uniqueLean 4Proved here from basic factsFormally verified

/-- **Terminal objects are unique up to unique isomorphism.** If `T` and `T'` are terminal, the
unique maps `T ⟶ T'` and `T' ⟶ T` compose to endomorphisms of a terminal object, which must be
identities because a terminal object has only one endomorphism. (Mathlib: `IsTerminal.uniqueUpToIso`.)
Dually for initial objects. -/
theorem terminal_unique {T T' : C} (hT : IsTerminal T) (hT' : IsTerminal T') :
    ∃ i : T ≅ T', ∀ j : T ≅ T', j = i :=
  ⟨⟨hT'.from T, hT.from T', hT.hom_ext _ _, hT'.hom_ext _ _⟩,
    fun _ => Iso.ext (hT'.hom_ext _ _)⟩

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

In the category of types — Lean's counterpart of $\cat{Set}$ — pairs form a product and the sum type A ⊕ B a coproduct; one-element and empty types are terminal and initial.

typesProductLean 4Formally verified

/-- **In the category of types, the product is the type of pairs.** Given `f : X → A` and
`g : X → B`, the unique map `X → A × B` compatible with the projections is
`x ↦ (f x, g x)`: any compatible `h` has first and second coordinates `f x` and `g x`. -/
def typesProduct (A B : Type u) :
    IsBinaryProduct (C := Type u) (↾(Prod.fst : A × B → A)) (↾(Prod.snd : A × B → B)) where
  lift f g := ↾fun x => (f x, g x)
  lift_fst _ _ := rfl
  lift_snd _ _ := rfl
  uniq f g h h₁ h₂ := by
    -- `ext` reduces to the two coordinates of `h x`.
    ext x
    · simpa using ConcreteCategory.congr_hom h₁ x
    · simpa using ConcreteCategory.congr_hom h₂ x

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

typesCoproductLean 4Formally verified

/-- **In the category of types, the coproduct is the disjoint union** `A ⊕ B`, with the
injections `Sum.inl`, `Sum.inr`. Following the definition, we exhibit a product in `(Type u)ᵒᵖ`:
the induced map is "case analysis" `Sum.elim f g`, and it is unique because a function on
`A ⊕ B` is determined by its values on the two summands. -/
def typesCoproduct (A B : Type u) :
    IsBinaryCoproduct (C := Type u) (↾(Sum.inl : A → A ⊕ B)) (↾(Sum.inr : B → A ⊕ B)) where
  lift f g := (↾(Sum.elim f.unop g.unop)).op
  lift_fst _ _ := rfl
  lift_snd _ _ := rfl
  uniq f g h h₁ h₂ := by
    apply Quiver.Hom.unop_inj
    ext x
    rcases x with a | b
    · exact ConcreteCategory.congr_hom (congrArg Quiver.Hom.unop h₁) a
    · exact ConcreteCategory.congr_hom (congrArg Quiver.Hom.unop h₂) b

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

types_terminal_initialLean 4Applies a library theoremFormally verified

/-- **In the category of types, a one-element type is terminal and the empty type is initial.**
Every type has exactly one map to `PUnit` and exactly one map from `PEmpty`. These are Mathlib's
`Types.isTerminalPUnit` and `Types.isInitialPEmpty`. -/
theorem types_terminal_initial :
    Nonempty (IsTerminal (PUnit : Type u)) ∧ Nonempty (IsInitial (PEmpty : Type u)) :=
  ⟨⟨Types.isTerminalPUnit⟩, ⟨Types.isInitialPEmpty⟩⟩

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

Theorem 5, for posets with meets and joins:

infIsProductLean 4Formally verified

/-- **In a poset regarded as a category, the product is the meet.** There is a morphism `x ⟶ y`
exactly when `x ≤ y`, and then only one, so the equations in the universal property are
automatic; what remains is existence: `x ≤ a` and `x ≤ b` imply `x ≤ a ⊓ b`. -/
def infIsProduct [SemilatticeInf α] (a b : α) :
    IsBinaryProduct (homOfLE (inf_le_left : a ⊓ b ≤ a)) (homOfLE inf_le_right) where
  lift f g := homOfLE (le_inf (leOfHom f) (leOfHom g))
  lift_fst _ _ := Subsingleton.elim _ _
  lift_snd _ _ := Subsingleton.elim _ _
  uniq _ _ _ _ _ := Subsingleton.elim _ _

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

product_eq_infLean 4Proved here from basic factsFormally verified

/-- **Conversely, every product in a poset is the meet.** If `p` (with `p ≤ a`, `p ≤ b`) is a
product of `a` and `b`, then `p ≤ a ⊓ b` because `a ⊓ b` is a lower bound, and `a ⊓ b ≤ p` by
the universal property applied to the cone `a ⊓ b`. Antisymmetry gives `p = a ⊓ b`. So a pair
with no greatest lower bound has no product. -/
theorem product_eq_inf [SemilatticeInf α] {a b p : α} {π₁ : p ⟶ a} {π₂ : p ⟶ b}
    (hp : IsBinaryProduct π₁ π₂) : p = a ⊓ b :=
  le_antisymm (le_inf (leOfHom π₁) (leOfHom π₂))
    (leOfHom (hp.lift (homOfLE inf_le_left) (homOfLE inf_le_right)))

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

supIsCoproductLean 4Formally verified

/-- **Dually, the coproduct in a poset is the join** `a ⊔ b`: in the opposite poset, `a ⊔ b` is
the meet. -/
def supIsCoproduct [SemilatticeSup α] (a b : α) :
    IsBinaryCoproduct (homOfLE (le_sup_left : a ≤ a ⊔ b)) (homOfLE le_sup_right) where
  lift f g := (homOfLE (sup_le (leOfHom f.unop) (leOfHom g.unop))).op
  lift_fst _ _ := Subsingleton.elim _ _
  lift_snd _ _ := Subsingleton.elim _ _
  uniq _ _ _ _ _ := Subsingleton.elim _ _

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

Initial and terminal objects in algebra, from Mathlib:

int_initialLean 4Applies a library theoremFormally verified

/-- **`ℤ` is initial among commutative rings**: for every commutative ring `R` there is exactly one
ring homomorphism `ℤ → R`, namely `n ↦ n · 1`. This is Mathlib's `CommRingCat.zIsInitial`
(uniqueness is `RingHom.ext_int`). -/
theorem int_initial : Nonempty (IsInitial (CommRingCat.of ℤ)) :=
  ⟨CommRingCat.zIsInitial⟩

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

trivial_group_zeroLean 4Applies a library theoremFormally verified

/-- **The trivial group is both initial and terminal in `Grp`** (a *zero object*): from any group
there is one homomorphism to it, and to any group there is one homomorphism from it (sending the
identity to the identity). This applies Mathlib's `GrpCat.isZero_of_subsingleton`. -/
theorem trivial_group_zero : IsZero (GrpCat.of PUnit) :=
  GrpCat.isZero_of_subsingleton _

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

And Theorem 4. Lean finds the contradiction $\sigma\tau = \tau\sigma$ in $S_3$ by evaluating both permutations (decide), after the universal property (Monoid.Coprod.lift) has transported the hypothetical equation $xy = yx$ to $S_3$ .

free_product_not_commLean 4Proved here from basic factsFormally verified

/-- **`ℤ ∗ ℤ` is not commutative.** In `Grp`, the coproduct of `ℤ` with itself is the free product
`ℤ ∗ ℤ` (Mathlib's `Monoid.Coprod`, written multiplicatively). Let `x` and `y` be the generators of
the two copies. By the universal property there is a homomorphism `φ : ℤ ∗ ℤ → S₃` sending `x` to
the transposition `(0 1)` and `y` to `(1 2)`. If `x y = y x`, then `φ` would make these two
transpositions commute, and they do not (checked by `decide`). Contrast `prod_comm`. -/
theorem free_product_not_comm :
    ∃ x y : Multiplicative ℤ ∗ Multiplicative ℤ, x * y ≠ y * x := by
  refine ⟨Monoid.Coprod.inl (Multiplicative.ofAdd 1), Monoid.Coprod.inr (Multiplicative.ofAdd 1),
    fun h => ?_⟩
  -- The homomorphism given by the universal property of the coproduct.
  let φ := Monoid.Coprod.lift (zpowersHom (Equiv.Perm (Fin 3)) (Equiv.swap 0 1))
    (zpowersHom (Equiv.Perm (Fin 3)) (Equiv.swap 1 2))
  have hφ := congrArg φ h
  simp only [φ, map_mul, Monoid.Coprod.lift_apply_inl, Monoid.Coprod.lift_apply_inr,
    zpowersHom_apply, toAdd_ofAdd, zpow_one] at hφ
  exact absurd hφ (by decide)

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

prod_commLean 4Proved here from basic factsFormally verified

/-- **`ℤ × ℤ` is commutative**: the product of two abelian groups is abelian, componentwise. So the
product and the coproduct of `ℤ` with itself in `Grp` are genuinely different groups. -/
theorem prod_comm (x y : Multiplicative ℤ × Multiplicative ℤ) : x * y = y * x :=
  Prod.ext (mul_comm x.1 y.1) (mul_comm x.2 y.2)

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

Not formalised here: the description of free products by reduced words (Mathlib has it as Monoid.CoprodI.Word), coproducts of commutative rings as tensor products, and Theorem 6.

ComputationC

Experiment: testing universal properties by brute force

For finite sets the universal property is a finite statement, so a computer can check it: for every pair $f : X \to A$ , $g : X \to B$ it counts the morphisms $h : X \to P$ with $\pi_1 h = f$ and $\pi_2 h = g$ . The count must be exactly $1$ every time. In a finite poset, products and coproducts can be found by searching for greatest lower and least upper bounds — or found not to exist.

Universal properties by brute force: finite sets and divisibility posetsPythonExhaustive finite checkCounterexampleComputationally tested

"""Testing universal properties by brute force, in finite sets and finite posets.

Part 1 counts, for every pair of maps f : X -> A and g : X -> B between small
finite sets, the maps h : X -> P with p1 o h = f and p2 o h = g, for three
candidate products P. Only the cartesian product gives exactly one h every
time: a bigger set breaks uniqueness, a smaller one breaks existence.
Part 2 searches finite posets (ordered by divisibility) for greatest lower
bounds and least upper bounds - the products and coproducts of the poset
regarded as a category - and finds pairs that have none.
"""

from itertools import product
from math import gcd

def maps(dom, cod):
    """All functions dom -> cod, as dicts."""
    return [dict(zip(dom, values)) for values in product(cod, repeat=len(dom))]

def factorisations(X, P, p1, p2, f, g):
    """Number of h : X -> P with p1(h(x)) = f(x) and p2(h(x)) = g(x) for all x."""
    return sum(1 for h in maps(X, P)
               if all(p1[h[x]] == f[x] and p2[h[x]] == g[x] for x in X))

def candidates(A, B):
    """Three would-be products of A and B: (name, P, p1, p2)."""
    pairs = list(product(A, B))
    triples = list(product(A, B, (0, 1)))
    return [
        ("A x B", pairs, {p: p[0] for p in pairs}, {p: p[1] for p in pairs}),
        ("A x B x {0,1}", triples, {t: t[0] for t in triples},
         {t: t[1] for t in triples}),
        ("A, p2 constant", list(A), {a: a for a in A}, {a: B[0] for a in A}),
    ]

def count_profile(A, B, X, cand):
    """The set of factorisation counts over all pairs (f, g) for one candidate."""
    _, P, p1, p2 = cand
    return {factorisations(X, P, p1, p2, f, g)
            for f in maps(X, A) for g in maps(X, B)}

def divides(a, b):
    """The divisibility order: a <= b iff a divides b."""
    return b % a == 0

def glb(elements, leq, a, b):
    """Greatest lower bound of a and b in a finite poset, or None."""
    lower = [x for x in elements if leq(x, a) and leq(x, b)]
    best = [x for x in lower if all(leq(y, x) for y in lower)]
    return best[0] if best else None

def lub(elements, leq, a, b):
    """Least upper bound (the dual notion), or None."""
    return glb(elements, lambda x, y: leq(y, x), a, b)

def main():
    A, B = (0, 1), ("a", "b", "c")
    print("Part 1: number of h : X -> P with p1 o h = f, p2 o h = g")
    print("        (all pairs f : X -> A, g : X -> B; |A| = 2, |B| = 3)")
    for cand in candidates(A, B):
        row = []
        for n in range(3):
            row.append(sorted(count_profile(A, B, tuple(range(n)), cand)))
        print(f"  P = {cand[0]:<15} |X| = 0, 1, 2: {row}")
    print("  Exactly one h every time only for A x B.")
    divs = [d for d in range(1, 61) if 60 % d == 0]
    ok = all(glb(divs, divides, a, b) == gcd(a, b)
             and lub(divs, divides, a, b) == a * b // gcd(a, b)
             for a in divs for b in divs)
    print()
    print(f"Part 2: divisors of 60 ({len(divs)} elements) under divisibility:")
    print(f"  product = gcd and coproduct = lcm for all {len(divs) ** 2} pairs: "
          f"{ok}")
    small = [2, 3, 12, 18]
    for a, b in [(2, 3), (12, 18), (2, 12)]:
        print(f"  in {small}: product of {a}, {b} = "
              f"{glb(small, divides, a, b)}, coproduct = "
              f"{lub(small, divides, a, b)}")
    print("  2, 3: no lower bound, two minimal upper bounds 12, 18; 12, 18 dually.")
    print()
    print("Epistemic status: exhaustive checks of finitely many maps and pairs.")
    print("They illustrate the definitions; that A x B is a product of any two")
    print("sets, and that products in a poset are meets, are proved in the lesson.")

if __name__ == "__main__":
    main()

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

Explore

Explore: one pair, one map

Choose maps $f : Z \to A$ and $g : Z \to B$ between small finite sets, then try to build $h : Z \to A \times B$ with $\pi_1 \circ h = f$ and $\pi_2 \circ h = g$ . Notice that at each point $z$ you have no freedom at all: $h(z)$ must be the pair $(f(z), g(z))$ . That absence of choice is the uniqueness clause.

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

Exercises

1. Products, coproducts, initial and terminal objects

Warm-upHuman

In $\cat{Set}$ , which statement is correct?

Choose one

\varnothing

is initial and every one-point set is terminal

\varnothing

is terminal and

\{\ast\}

is initial

\varnothing

is a zero object

\cat{Set}

has no terminal object, since there are many one-point sets

2. Products, coproducts, initial and terminal objects

CoreHuman

Which of these categories have a zero object (an object that is both initial and terminal)? Select all that apply.

Choose all that apply

3. Products, coproducts, initial and terminal objects

Warm-upHuman

Regard the positive integers, ordered by divisibility ( $a \le b$ iff $a \mid b$ ), as a category. What is the coproduct of $12$ and $18$ ?

4. Products, coproducts, initial and terminal objects

CoreHuman

In $\cat{Set}$ , let $|X| = 2$ , $|A| = 2$ and $|B| = 3$ . How many morphisms $X \to A \times B$ are there? (Use the universal property rather than listing them.)

5. Products, coproducts, initial and terminal objects

CoreHuman

In the proof that two products $(P, \pi_i)$ and $(Q, \rho_i)$ of $A$ and $B$ are isomorphic, we have $\varphi : P \to Q$ and $\psi : Q \to P$ with $\rho_i \varphi = \pi_i$ and $\pi_i \psi = \rho_i$ . Why is $\psi \circ \varphi = \mathrm{id}_P$ ?

Choose one

Both

\psi \circ \varphi

and

\mathrm{id}_P

satisfy

\pi_i \circ h = \pi_i

for

i = 1, 2

, and by the uniqueness clause for

P

(applied to the pair

(\pi_1, \pi_2)

) there is only one such

h

Because

\varphi

is injective and

\psi

is surjectiveBecause

P

and

Q

have the same number of elementsBy the existence clause of the universal property of

Q

6. Products, coproducts, initial and terminal objects

StretchHuman

What is the coproduct of $\Z/2$ and $\Z/3$ in the category of commutative rings with identity?

Choose one

the zero ring

\Z/6 \cong \Z/2 \times \Z/3

it does not exist

\Z

7. Products, coproducts, initial and terminal objects

StretchHuman

Which statements are true? Select all that apply.

Choose all that apply

The coproduct of

\Z

and

\Z

\cat{Grp}

is non-abelian.The coproduct of

\Z

and

\Z

\cat{Ab}

\Z \oplus \Z

.Since

\cat{Ab}

is a full subcategory of

\cat{Grp}

, the two coproducts above must agree.The product of

\Z

and

\Z

\Z \times \Z

in both

\cat{Grp}

and

\cat{Ab}

8. Products, coproducts, initial and terminal objects

CoreFormal

Mathlib writes h ≫ π₁ for $\pi_1 \circ h$ (first h, then π₁). Which Lean field correctly expresses the uniqueness clause of the universal property of a product with projections π₁ : P ⟶ A, π₂ : P ⟶ B?

Choose one

uniq : ∀ {X} (f : X ⟶ A) (g : X ⟶ B) (h : X ⟶ P), h ≫ π₁ = f → h ≫ π₂ = g → h = lift f guniq : ∀ {X} (f : X ⟶ A) (g : X ⟶ B) (h : X ⟶ P), π₁ ≫ h = f → π₂ ≫ h = g → h = lift f guniq : ∀ {X} (f : X ⟶ A) (g : X ⟶ B), ∃ h : X ⟶ P, h ≫ π₁ = f ∧ h ≫ π₂ = guniq : ∀ {X} (h k : X ⟶ P), h = k

9. Products, coproducts, initial and terminal objects

CoreComputational

Write glb(elements, leq, a, b) returning the product of a and b in a finite poset — the greatest lower bound — or None if it does not exist. Here elements is a list and leq(x, y) decides $x \le y$ .

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

Common misconceptionsH

Common misconceptions

Misconception

"Coproducts look like products." In $\cat{Set}$ the two look different but at least familiar; in $\cat{Grp}$ the coproduct $\Z * \Z$ is a non-abelian group, utterly unlike $\Z \times \Z$ (Theorem 4). In $\cat{CRing}$ the coproduct is a tensor product, and $\Z/2 \sqcup \Z/3$ is the zero ring. In $\cat{Ab}$ the finite products and coproducts coincide. There is no general recipe "coproduct = something like a sum": you must compute it from the universal property in the category at hand.

Misconception

"Every category has products." Many do not. A poset has a product of $a$ and $b$ only when $a \wedge b$ exists ( $\{2, 3, 12, 18\}$ under divisibility lacks several); the category of fields has no product of $\mathbb{F}_2$ and $\mathbb{F}_3$ ; the category of finite sets has all finite products but not, for example, a product of countably many copies of $\{0, 1\}$ (its points would correspond to the uncountably many sequences). A universal property characterises an object — existence must be proved separately.

Misconception

"The union is the coproduct of sets." Only for disjoint sets. In general the coproduct needs the two sets to be made disjoint first ( $A \times \{1\} \cup B \times \{2\}$ ), otherwise a map on $A \cup B$ cannot be defined independently on $A$ and on $B$ .

Misconception

"The product is defined as the set of pairs." In $\cat{Set}$ the set of pairs is a product, but so is any set in bijection with it with the matching projections, and in other categories there may be no "pairs" at all (posets, $\cat{Set}^{\mathrm{op}}$ ). The definition is the universal property; the set of pairs is one construction satisfying it.

ViewpointsH

Viewpoints

Topology— Tychonoff, wedges and van Kampen

The universal property forces the product topology (Theorem 6), and with it a deep theorem: Tychonoff's theorem says that any product of compact spaces is compact — a statement about the categorical product that is equivalent to the axiom of choice (Kelley, 1950). The box topology, which looks more natural to beginners, fails the universal property and is not compact even for $\{0, 1\}^{\N}$ (where it is discrete and infinite).

In pointed spaces the coproduct is the wedge $X \vee Y$ (the disjoint union with base points identified), and the fundamental group turns it into the coproduct of groups: by the Seifert–van Kampen theorem, for path-connected spaces whose base points are deformation retracts of open neighbourhoods (for example CW complexes with a vertex as base point), $\pi_1(X \vee Y) \cong \pi_1(X) * \pi_1(Y)$ . So the figure eight $S^1 \vee S^1$ has fundamental group $\Z * \Z$ , while the torus $S^1 \times S^1$ has $\Z \times \Z$ — and indeed $\pi_1(X \times Y) \cong \pi_1(X) \times \pi_1(Y)$ always. Products go to products and (nice) coproducts to coproducts. See the fundamental group.

Geometry— A grid and a tree

Draw the Cayley graph of a group with respect to generators $x, y$ : a vertex for each element, an edge from $g$ to $gx$ and to $gy$ . For $\Z \times \Z$ it is the square grid in the plane — flat geometry, where $xy = yx$ closes every unit square. For $\Z * \Z$ it is the infinite 4-valent tree: since no non-trivial reduced word equals the identity, there are no cycles at all, and the number of elements at distance $n$ from the identity is $4 \cdot 3^{n-1}$ , growing exponentially, like the area of a disc in the hyperbolic plane. Geometric group theory takes such pictures seriously: free groups are the basic examples of hyperbolic groups, and a group acting freely on a tree is free (Serre's theory of groups acting on trees). The product and the coproduct of the same two groups live in different geometries.

Algebra— Biproducts, tensor products and the infinite

In $\cat{Ab}$ , $\cat{Vect}_k$ and $R\text{-}\cat{Mod}$ , finite products and coproducts coincide: $A \oplus B$ carries both structures, and $\pi_1 \iota_1 = \mathrm{id}$ , $\pi_2 \iota_2 = \mathrm{id}$ , $\iota_1 \pi_1 + \iota_2 \pi_2 = \mathrm{id}$ . Such an object is a biproduct, and categories where all finite biproducts exist and hom-sets are abelian groups are the additive categories underlying homological algebra (see abelian categories). Infinite products and coproducts differ: $\Hom(\bigoplus_i A_i, B) \cong \prod_i \Hom(A_i, B)$ , and for a vector space this is why the dual of a space with a countably infinite basis is so much larger than the space. In commutative rings, the coproduct $R \otimes_{\Z} S$ explains why tensor products are inevitable: the polynomial ring $\Z[x, y]$ is the coproduct $\Z[x] \sqcup \Z[y]$ , and a pair of ring maps out of $R$ and $S$ is a ring map out of $R \otimes S$ .

Logic— And, or, true, false

Order propositions by entailment: $\varphi \le \psi$ when $\varphi \vdash \psi$ . In this preorder the product of $\varphi$ and $\psi$ is $\varphi \wedge \psi$ (it entails both, and anything entailing both entails it), the coproduct is $\varphi \vee \psi$ , the terminal object is $\top$ and the initial object is $\bot$ ("ex falso quodlibet" is the statement that $\bot$ is initial). Remembering which proof witnesses an entailment upgrades the preorder to a category whose morphisms are proofs; then the universal properties are the introduction and elimination rules of natural deduction: a proof of $\varphi \wedge \psi$ from $\chi$ is a pair of proofs, and $\vee$ -elimination is the copairing $[f, g]$ — proof by cases. This is one face of the Curry–Howard correspondence (see categorical logic).

Computation— Algebraic data types

In a typed programming language, the product of types $A$ and $B$ is the type of pairs or records, with projections fst and snd; the coproduct is the sum type (tagged union, Either A B, or Lean's A ⊕ B), whose universal property is pattern matching: to define a function on A ⊕ B, give one branch for inl a and one for inr b. The unit type is terminal and the empty type initial. Counting confirms the names: for finite types $|A \times B| = |A|\,|B|$ and $|A + B| = |A| + |B|$ , and type isomorphisms such as $A \times (B + C) \cong A \times B + A \times C$ are laws of arithmetic one level up. See the λ-calculus.

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

History & global context

History and global context

Products of sets are named after René Descartes, whose coordinates (1637) identify points of the plane with pairs of numbers. A purely set-theoretic definition of the ordered pair came much later: Norbert Wiener (1914) and Kazimierz Kuratowski (1921), whose $\{\{a\}, \{a, b\}\}$ is the one in use today.
Andrey Tychonoff introduced the product topology around 1930 and proved the compactness theorem that bears his name; John Kelley showed in 1950 that Tychonoff's theorem is equivalent to the axiom of choice.
Free products of groups grew out of combinatorial group theory: Otto Schreier studied amalgamated free products (1927), and Alexander Kurosh proved his subgroup theorem for free products (1934).
Pierre Samuel (1948) formulated "universal mapping problems", and Saunders Mac Lane's "Duality for groups" (1950) characterised direct and free products by arrows alone and observed that the two are dual — the first appearance of products and coproducts as categorical notions. The modern names and the general theory of limits followed in the 1950s.

The same construction, everywhere

Generalised elements and the best possible pair

Definitions

A tour of products and coproducts

Theorems and proofs

Products and coproducts in Lean

Experiment: testing universal properties by brute force

Explore: one pair, one map

Exercises

Common misconceptions

Viewpoints

Wonder Trails

History and global context

Further reading