Universal properties · The Lumenary

Lens

MotivationH

What is an ordered pair, really?

In set theory an ordered pair is often defined as $(a, b) = \{\{a\}, \{a, b\}\}$ (Kuratowski, 1921). Norbert Wiener had proposed a different definition in 1914, and one could invent many more. No working mathematician cares which is used. What matters is one property: from a pair you can recover its first and second entries, and any two entries make exactly one pair.

The same happens across mathematics. The integers can be built from pairs of natural numbers, the rationals from pairs of integers, the real numbers from Dedekind cuts or from Cauchy sequences. The constructions differ; the objects behave identically. A universal property says precisely what behaviour we care about, in terms of maps to or from the object — and then proves that this behaviour determines the object up to a unique isomorphism. You met the first example in products by maps; this lesson develops the idea across categories.

IntuitionH

The best solution to a problem

A universal property usually describes the most efficient solution to some problem, measured against all other solutions.

Problem: an object with a map to $A$ and a map to $B$ . Best solution: the product $A \times B$ — every other solution $X$ (with $f : X \to A$ , $g : X \to B$ ) maps to it in exactly one compatible way.
Problem: a monoid containing the letters of an alphabet $S$ . Best solution: the monoid of words in $S$ — it satisfies no equations except those forced by the monoid axioms, so it maps to every other solution in exactly one compatible way.
Problem: a map out of a set $X$ that makes equivalent elements equal. Best solution: the quotient $X \to X/{\sim}$ , through which every other solution factors uniquely.

"Exactly one" packs two demands: existence (there is a compatible map) and uniqueness (there is only one). The second is easy to forget and is what makes the theory work.

DefinitionsH

Definitions

Definition— product

Let $A, B$ be objects of a category $\cat{C}$ . A product of $A$ and $B$ is an object $P$ with morphisms $\pi_A : P \to A$ and $\pi_B : P \to B$ (the projections) such that for every object $X$ and every pair $f : X \to A$ , $g : X \to B$ there is exactly one $h : X \to P$ with $\pi_A \circ h = f$ and $\pi_B \circ h = g$ . We write $h = \langle f, g \rangle$ .

Every pair

f, g

factors through

P

by exactly one dashed arrow.

Reversing all arrows gives a coproduct: an object $Q$ with $\iota_A : A \to Q$ , $\iota_B : B \to Q$ such that every pair $f : A \to Y$ , $g : B \to Y$ factors as $f = h \circ \iota_A$ , $g = h \circ \iota_B$ for exactly one $h : Q \to Y$ . In $\cat{Set}$ the coproduct is the disjoint union.

Definition— initial and terminal objects

An object $I$ is initial if for every object $Y$ there is exactly one morphism $I \to Y$ , and terminal if for every $Y$ there is exactly one morphism $Y \to I$ .

In $\cat{Set}$ the empty set is initial and every one-element set is terminal; in $\cat{Grp}$ the trivial group is both; in $\cat{Ring}$ the ring $\Z$ is initial (there is exactly one ring homomorphism $\Z \to R$ , determined by $1 \mapsto 1$ ).

The general shape covering free objects, quotients and many others is the following, where $U : \cat{D} \to \cat{C}$ is a functor (often a forgetful functor).

Definition— universal arrow

A universal arrow from an object $X$ of $\cat{C}$ to a functor $U : \cat{D} \to \cat{C}$ is an object $F$ of $\cat{D}$ together with a morphism $\eta : X \to U(F)$ of $\cat{C}$ such that for every object $E$ of $\cat{D}$ and every morphism $f : X \to U(E)$ there is exactly one morphism $g : F \to E$ of $\cat{D}$ with $U(g) \circ \eta = f$ .

\mathcal{C}

(left):

f = U(g) \circ \eta

. In

\mathcal{D}

(right): the unique

g

Definition— free monoid

Let $U : \cat{Mon} \to \cat{Set}$ be the forgetful functor. A free monoid on a set $S$ is a universal arrow from $S$ to $U$ : a monoid $F(S)$ with a function $\eta : S \to F(S)$ such that every function $f : S \to M$ into a monoid factors as $f = \bar f \circ \eta$ for exactly one monoid homomorphism $\bar f : F(S) \to M$ .

Note

A universal arrow $(F, \eta)$ is the same as an initial object of the category whose objects are pairs $(E, f)$ with $f : X \to U(E)$ , and whose morphisms $(E, f) \to (E', f')$ are the $g : E \to E'$ with $U(g) \circ f = f'$ . (This is a comma category, written $X \downarrow U$ .) Products are likewise terminal objects of a category of "cones" over $A$ and $B$ . So every universal property in this lesson says that some object is initial or terminal in a suitable category.

Worked examplesH

Examples

Example— Products

In $\cat{Set}$ : the cartesian product $A \times B$ with the coordinate projections; $\langle f, g \rangle(x) = (f(x), g(x))$ .
In $\cat{Grp}$ : the direct product $G \times H$ with coordinatewise multiplication.
In $\cat{Top}$ : $X \times Y$ with the product topology (generated by the sets $U \times V$ with $U, V$ open).
In $\cat{Vect}_k$ : $V \times W = V \oplus W$ ; in this category it is also the coproduct.
In a poset regarded as a category, a product of $x$ and $y$ is an element $p \le x, y$ such that every $z \le x, y$ has $z \le p$ : the greatest lower bound (meet) $x \wedge y$ . In the subsets of a set it is $x \cap y$ ; for the positive integers ordered by divisibility it is $\gcd(x, y)$ ; in the poset of propositions ordered by entailment it is " $x$ and $y$ ".
Products need not exist. In the poset with two incomparable elements $a, b$ (and nothing else), $a$ and $b$ have no lower bound at all, hence no product. In the category of fields the product of $\mathbb{F}_2$ and $\mathbb{F}_3$ does not exist (Theorem 5).

Example— Quotients

If $\sim$ is an equivalence relation on a set $X$ , the quotient set $X/{\sim}$ of equivalence classes comes with $q : X \to X/{\sim}$ , $q(x) = [x]$ . For a normal subgroup $N$ of a group $G$ , the quotient group $G/N$ comes with the homomorphism $q(g) = gN$ . Both are universal among maps that "kill" the relation (Theorem 3). For instance $\Z \to \Z/n$ is universal among homomorphisms out of $\Z$ that vanish on $n\Z$ — the Remainder families trail explores these classes.

Example— Free objects

Free monoid: words in $S$ under concatenation (Theorem 4). On one letter $\{a\}$ it is $\{\varepsilon, a, aa, aaa, \dots\} \cong (\N, +)$ .
Free group: reduced words in the letters $s$ and their formal inverses $s^{-1}$ (no $s s^{-1}$ or $s^{-1} s$ adjacent), multiplied by concatenating and cancelling. Every map from $S$ to a group extends uniquely to a homomorphism. That the reduced words form a group needs a careful argument (associativity is the subtle point); see Aluffi, Algebra: Chapter 0, §II.5. On one letter it is $\Z$ .
Free vector space: $k[S]$ , with basis $S$ . "Every function $S \to W$ extends uniquely to a linear map $k[S] \to W$ " is exactly what it means for $S$ to be a basis. So a basis is a universal property.

Example— Field of fractions

$\Q$ with the inclusion $\Z \to \Q$ is universal among injective ring homomorphisms from $\Z$ into fields: if $\varphi : \Z \to K$ is injective and $K$ is a field, there is exactly one ring homomorphism $\bar\varphi : \Q \to K$ extending it, namely $\bar\varphi(a/b) = \varphi(a)\varphi(b)^{-1}$ . The same holds for every integral domain $R$ and its field of fractions $\mathrm{Frac}(R)$ ; for example the field of rational functions $k(x) = \mathrm{Frac}(k[x])$ .

Example— Tensor products

For vector spaces $V, W$ over $k$ , a tensor product is a vector space $V \otimes W$ with a bilinear map $\beta : V \times W \to V \otimes W$ such that every bilinear map $V \times W \to U$ equals $\ell \circ \beta$ for exactly one linear map $\ell : V \otimes W \to U$ . The universal property turns bilinear algebra into linear algebra. Constructions exist (a quotient of the free vector space on $V \times W$ ; or, in finite dimensions, a space with basis $e_i \otimes f_j$ ), but almost every proof about tensor products uses only the universal property. This is the textbook case of a construction "best defined by its universal property".

ProofH

Uniqueness, existence and non-existence

Theorem— Theorem 1 (uniqueness up to unique isomorphism)

Let $(F, \eta)$ and $(F', \eta')$ be universal arrows from $X$ to $U : \cat{D} \to \cat{C}$ . Then there is exactly one morphism $\varphi : F \to F'$ with $U(\varphi) \circ \eta = \eta'$ , and it is an isomorphism.

Proof

Existence and uniqueness of $\varphi$ . Apply the universal property of $(F, \eta)$ to $f = \eta' : X \to U(F')$ : there is exactly one $\varphi : F \to F'$ with $U(\varphi) \circ \eta = \eta'$ . Likewise there is exactly one $\psi : F' \to F$ with $U(\psi) \circ \eta' = \eta$ .

$\psi \circ \varphi = \id_F$ . Both $\psi \circ \varphi$ and $\id_F$ are morphisms $F \to F$ that carry $\eta$ to $\eta$ :

U(\psi \circ \varphi) \circ \eta = U(\psi) \circ U(\varphi) \circ \eta = U(\psi) \circ \eta' = \eta, \qquad U(\id_F) \circ \eta = \eta.

By the uniqueness clause of the universal property of $(F, \eta)$ , applied to $f = \eta$ , they are equal. By symmetry $\varphi \circ \psi = \id_{F'}$ .

∎

The same argument, word for word, shows that two initial objects are isomorphic by a unique isomorphism, that two products of $A$ and $B$ are isomorphic by a unique isomorphism commuting with the projections, and so on. This is why we may say the product, the free monoid, the quotient: any two choices are identified in exactly one sensible way. Notice where uniqueness was used — without it, $\psi \circ \varphi$ need not be the identity.

Theorem— Theorem 2 (products exist in Set, Grp and Top)

The cartesian product, the direct product of groups and the product of spaces with the product topology satisfy the universal property of the product.

Proof

In $\cat{Set}$ . Given $f, g$ , the map $h(x) = (f(x), g(x))$ satisfies $\pi_A \circ h = f$ , $\pi_B \circ h = g$ . If $h'$ also does, then $h'(x)$ is a pair with first entry $f(x)$ and second entry $g(x)$ , so $h'(x) = h(x)$ .

In $\cat{Grp}$ . The same $h$ is the only candidate, since a homomorphism is in particular a function. It is a homomorphism: $h(xy) = (f(xy), g(xy)) = (f(x)f(y), g(x)g(y)) = (f(x), g(x))(f(y), g(y)) = h(x)h(y)$ , because multiplication in $G \times H$ is coordinatewise. The projections are homomorphisms for the same reason.

In $\cat{Top}$ . Again $h$ is the only candidate. It is continuous: for open $U \subseteq A$ and $V \subseteq B$ , $h^{-1}(U \times V) = f^{-1}(U) \cap g^{-1}(V)$ is open, and these sets $U \times V$ generate the topology. The projections are continuous since $\pi_A^{-1}(U) = U \times B$ .

∎

The product topology is not an arbitrary choice: it is the coarsest topology making both projections continuous, and that is exactly what the universal property demands. (For infinite products, the "box topology" generated by all products of open sets is finer, and it fails the universal property — see the topologist's viewpoint below.)

Theorem— Theorem 3 (the universal property of quotients)

(a) Let $\sim$ be an equivalence relation on $X$ . If $f : X \to Y$ satisfies $x \sim x' \Rightarrow f(x) = f(x')$ , there is exactly one $\bar f : X/{\sim} \to Y$ with $\bar f \circ q = f$ . (b) Let $N$ be a normal subgroup of $G$ . If $f : G \to H$ is a homomorphism with $N \subseteq \ker f$ , there is exactly one homomorphism $\bar f : G/N \to H$ with $\bar f \circ q = f$ .

Proof

(a) Define $\bar f([x]) = f(x)$ . This is well defined: if $[x] = [x']$ then $x \sim x'$ , so $f(x) = f(x')$ . Clearly $\bar f \circ q = f$ . If also $g \circ q = f$ , then $g([x]) = f(x) = \bar f([x])$ for every class, since every class is $[x]$ for some $x$ ( $q$ is surjective).

(b) The cosets of $N$ are the classes of the relation $x \sim x' \iff x^{-1}x' \in N$ , and $N \subseteq \ker f$ gives $f(x) = f(x')$ whenever $x \sim x'$ . So (a) gives a unique function $\bar f(gN) = f(g)$ . It is a homomorphism: $\bar f(gN \cdot g'N) = \bar f(gg'N) = f(gg') = f(g)f(g') = \bar f(gN)\,\bar f(g'N)$ .

∎

Theorem— Corollary (first isomorphism theorem)

If $f : G \to H$ is a surjective homomorphism, then $\bar f : G/\ker f \to H$ is an isomorphism.

Proof

By Theorem 3(b) with $N = \ker f$ we get $\bar f$ with $\bar f(gN) = f(g)$ . It is surjective because $f$ is. It is injective: if $\bar f(gN) = e$ then $f(g) = e$ , so $g \in N$ and $gN = N$ , the identity of $G/N$ ; a homomorphism with trivial kernel is injective. A bijective homomorphism is an isomorphism of groups.

∎

Theorem— Theorem 4 (the free monoid is the monoid of words)

Let $S^\ast$ be the set of finite words in $S$ with concatenation and the empty word $\varepsilon$ , and $\eta(s) = s$ the one-letter word. For every function $f : S \to M$ into a monoid there is exactly one monoid homomorphism $\bar f : S^\ast \to M$ with $\bar f(s) = f(s)$ for all $s \in S$ , namely

\bar f(s_1 s_2 \cdots s_k) = f(s_1)\, f(s_2) \cdots f(s_k), \qquad \bar f(\varepsilon) = 1.

Proof

Existence. The formula sends $\varepsilon$ to $1$ and one-letter words $s$ to $f(s)$ ; and $\bar f(vw) = \bar f(v)\,\bar f(w)$ because the product of the values of the letters of $vw$ is the product for $v$ followed by the product for $w$ (associativity in $M$ lets us regroup).

Uniqueness. Let $h : S^\ast \to M$ be a homomorphism with $h(s) = f(s)$ . We show $h(w) = \bar f(w)$ by induction on the length of $w$ . For $w = \varepsilon$ : $h(\varepsilon) = 1 = \bar f(\varepsilon)$ , since homomorphisms preserve the unit. For $w = s\,v$ with $s \in S$ : $h(sv) = h(s)\,h(v) = f(s)\,\bar f(v) = \bar f(sv)$ .

∎

With Theorem 1, Theorem 4 says: any free monoid on $S$ is isomorphic to $S^\ast$ , by a unique isomorphism fixing the letters. For example $\{a\}^\ast \cong (\N, +)$ via $a^n \mapsto n$ .

Theorem— Theorem 5 (a universal property that nothing satisfies)

In the category of fields (with ring homomorphisms), $\mathbb{F}_2$ and $\mathbb{F}_3$ have no product.

Proof

A product would in particular be a field $K$ with ring homomorphisms $p : K \to \mathbb{F}_2$ and $q : K \to \mathbb{F}_3$ . A ring homomorphism out of a field is injective (its kernel is an ideal not containing $1$ , and the only such ideal of a field is $0$ ). Since $p(2) = 2 = 0$ in $\mathbb{F}_2$ , injectivity gives $2 = 0$ in $K$ ; since $q(3) = 3 = 0$ in $\mathbb{F}_3$ , also $3 = 0$ in $K$ . Then $1 = 3 - 2 = 0$ in $K$ , which is impossible in a field. So no field even has maps to both, let alone a universal one.

∎

So a universal property is a specification. Theorem 1 says at most one object (up to unique isomorphism) meets it; whether any object does is a separate question, answered by a construction — or, as here, by a proof that none exists.

Theorem— Theorem 6 (Q is the field of fractions of Z)

Let $K$ be a field and $\varphi : \Z \to K$ an injective ring homomorphism. There is exactly one ring homomorphism $\bar\varphi : \Q \to K$ with $\bar\varphi(n) = \varphi(n)$ for all $n \in \Z$ .

Proof

Uniqueness. If $\bar\varphi$ extends $\varphi$ and $b \neq 0$ , then $\bar\varphi(1/b)$ is an inverse of $\bar\varphi(b) = \varphi(b)$ , and inverses are unique; so $\bar\varphi(a/b) = \varphi(a)\varphi(b)^{-1}$ is forced. (This is the argument that showed $\Z \to \Q$ is an epimorphism of rings in the lesson on categories.)

Existence. Define $\bar\varphi(a/b) = \varphi(a)\varphi(b)^{-1}$ ; here $\varphi(b) \neq 0$ because $\varphi$ is injective. It is well defined: if $a/b = c/d$ then $ad = bc$ , so $\varphi(a)\varphi(d) = \varphi(b)\varphi(c)$ and $\varphi(a)\varphi(b)^{-1} = \varphi(c)\varphi(d)^{-1}$ . Checking that it preserves sums and products is routine algebra with fractions.

∎

Formal mathematicsF

Universal properties in Lean and Mathlib

We package the definition of a universal arrow as a Lean structure, with lift f the unique factorisation, fac its existence and uniq its uniqueness (Mathlib composes diagrammatically: unit ≫ U.map g is our $U(g) \circ \eta$ ):

UniversalArrowLean 4Formally verified

/-- A **universal arrow** from an object `X` of `C` to a functor `U : D ⥤ C`: an object `obj`
of `D` with a morphism `unit : X ⟶ U(obj)` such that every morphism `f : X ⟶ U(E)` factors as
`U(g) ∘ unit` for exactly one `g : obj ⟶ E`. Here `lift f` is that `g`, `fac` says it works and
`uniq` says it is the only one. (Free monoids: `X` a set, `U` the forgetful functor from monoids
to sets, `obj` the free monoid, `unit` the inclusion of one-letter words.) -/
structure UniversalArrow {C : Type u} [Category.{v} C] {D : Type u₂} [Category.{v₂} D]
    (X : C) (U : D ⥤ C) where
  /-- The universal object. -/
  obj : D
  /-- The universal morphism `X ⟶ U(obj)`. -/
  unit : X ⟶ U.obj obj
  /-- The factorisation of a morphism `X ⟶ U(E)` through `unit`. -/
  lift : {E : D} → (X ⟶ U.obj E) → (obj ⟶ E)
  /-- Existence: `U(lift f) ∘ unit = f`. -/
  fac : ∀ {E : D} (f : X ⟶ U.obj E), unit ≫ U.map (lift f) = f
  /-- Uniqueness: any `g` with `U(g) ∘ unit = f` is `lift f`. -/
  uniq : ∀ {E : D} (f : X ⟶ U.obj E) (g : obj ⟶ E), unit ≫ U.map g = f → g = lift f

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

Theorem 1 then follows the human proof exactly. First, the uniqueness clause as a cancellation principle, and the fact that the factorisation of $\eta$ itself is the identity:

hom_extLean 4Proved here from basic factsFormally verified

/-- **Maps out of a universal object are determined by what they do to the unit.** If
`U(g) ∘ unit = U(g') ∘ unit` then `g = g'`: both are the unique factorisation of the same
morphism. This is the "uniqueness clause" doing its work. -/
theorem hom_ext (A : UniversalArrow X U) {E : D} {g g' : A.obj ⟶ E}
    (h : A.unit ≫ U.map g = A.unit ≫ U.map g') : g = g' :=
  (A.uniq _ g h).trans (A.uniq _ g' rfl).symm

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

lift_unitLean 4Proved here from basic factsFormally verified

/-- The factorisation of `unit` itself is the identity: `lift unit = id`, because `id` also
factors `unit` (`U(id) ∘ unit = unit`) and factorisations are unique. -/
theorem lift_unit (A : UniversalArrow X U) : A.lift A.unit = 𝟙 A.obj :=
  (A.uniq A.unit (𝟙 A.obj) (by rw [U.map_id, Category.comp_id])).symm

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

Then the comparison isomorphism, its compatibility with the structure maps, and its uniqueness:

isoLean 4Formally verified

/-- **Two universal arrows have isomorphic objects.** The comparison maps are `A.lift B.unit`
and `B.lift A.unit`; each composite factors the unit through itself, so by `hom_ext` (the
uniqueness clause) it is the identity. This is the proof of the lesson, verbatim. -/
def iso (A B : UniversalArrow X U) : A.obj ≅ B.obj where
  hom := A.lift B.unit
  inv := B.lift A.unit
  hom_inv_id := by
    apply A.hom_ext
    rw [U.map_comp, ← Category.assoc, A.fac, B.fac, U.map_id, Category.comp_id]
  inv_hom_id := by
    apply B.hom_ext
    rw [U.map_comp, ← Category.assoc, B.fac, A.fac, U.map_id, Category.comp_id]

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

iso_compatibleLean 4Proved here from basic factsFormally verified

/-- The isomorphism `iso A B` is **compatible with the structure maps**: it carries `A.unit` to
`B.unit`, i.e. `U(φ) ∘ A.unit = B.unit`. -/
theorem iso_compatible (A B : UniversalArrow X U) : A.unit ≫ U.map (A.iso B).hom = B.unit :=
  A.fac B.unit

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

iso_uniqueLean 4Proved here from basic factsFormally verified

/-- **…and it is the only compatible isomorphism** (indeed the only compatible morphism): any
`φ : A.obj ⟶ B.obj` with `U(φ) ∘ A.unit = B.unit` equals `(iso A B).hom`. So an object with a
universal property is unique *up to a unique isomorphism compatible with the structure maps*. -/
theorem iso_unique (A B : UniversalArrow X U) (φ : A.obj ⟶ B.obj)
    (hφ : A.unit ≫ U.map φ = B.unit) : φ = (A.iso B).hom :=
  A.uniq B.unit φ hφ

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

Our structure connects to Mathlib's general machinery through the Note above: a universal arrow is an initial object of the comma category, which Mathlib calls StructuredArrow X U, and Mathlib proves that initial objects are unique up to unique isomorphism:

isInitialLean 4Formally verified

/-- **A universal arrow is an initial object.** Objects of Mathlib's comma category
`StructuredArrow X U` are pairs `(E, f : X ⟶ U(E))`, and morphisms `(E, f) ⟶ (E', f')` are maps
`g : E ⟶ E'` with `U(g) ∘ f = f'`. The universal arrow `(obj, unit)` has exactly one morphism to
every other object — `lift` gives one (`fac`), and `uniq` says there are no others — so it is
initial. This connects our structure to Mathlib's library of initial objects and limits. -/
def isInitial (A : UniversalArrow X U) : Limits.IsInitial (StructuredArrow.mk A.unit) :=
  Limits.IsInitial.ofUniqueHom
    (fun E => StructuredArrow.homMk (A.lift E.hom) (A.fac E.hom))
    (fun E m => by
      ext
      exact A.uniq E.hom m.right (StructuredArrow.w m))

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

initial_unique_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's form of the same principle: **initial objects are unique up to unique
isomorphism.** A universal arrow from `X` to `U` is exactly an initial object of the comma
category `StructuredArrow X U`, so this covers every universal property of the lesson. This
applies `IsInitial.uniqueUpToIso` and `IsInitial.hom_ext`. -/
theorem initial_unique_library {C : Type u} [Category.{v} C] {I J : C}
    (hI : Limits.IsInitial I) (hJ : Limits.IsInitial J) :
    Nonempty (I ≅ J) ∧ ∀ φ ψ : I ⟶ J, φ = ψ :=
  ⟨⟨hI.uniqueUpToIso hJ⟩, fun φ ψ => hI.hom_ext φ ψ⟩

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

Products (Theorem 2). For spaces, Mathlib's lemma says precisely that a map into a product is continuous iff its components are:

prod_universalLean 4Proved here from basic factsFormally verified

/-- **The product of sets.** For maps `f : X → A` and `g : X → B` there is exactly one
`h : X → A × B` with `π₁ ∘ h = f` and `π₂ ∘ h = g`, namely `h(x) = (f(x), g(x))`. Uniqueness: a
point of `A × B` is determined by its two coordinates. -/
theorem prod_universal {X A B : Type u} (f : X → A) (g : X → B) :
    ∃! h : X → A × B, Prod.fst ∘ h = f ∧ Prod.snd ∘ h = g := by
  refine ⟨fun x => (f x, g x), ⟨rfl, rfl⟩, ?_⟩
  rintro h ⟨h₁, h₂⟩
  funext x
  exact Prod.ext (congrFun h₁ x) (congrFun h₂ x)

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

group_prod_universalLean 4Proved here from basic factsFormally verified

/-- **The product of groups.** For homomorphisms `f : G → H` and `g : G → K` there is exactly
one homomorphism `h : G → H × K` with `π₁ ∘ h = f` and `π₂ ∘ h = g`. The map is the same as for
sets (`x ↦ (f x, g x)`, Mathlib's `MonoidHom.prod`); the new point is that it is a homomorphism
because the operation on `H × K` is defined coordinatewise. -/
theorem group_prod_universal {G H K : Type u} [Group G] [Group H] [Group K] (f : G →* H)
    (g : G →* K) :
    ∃! h : G →* H × K, (MonoidHom.fst H K).comp h = f ∧ (MonoidHom.snd H K).comp h = g := by
  refine ⟨f.prod g, ⟨MonoidHom.fst_comp_prod f g, MonoidHom.snd_comp_prod f g⟩, ?_⟩
  rintro h ⟨h₁, h₂⟩
  ext x
  · exact DFunLike.congr_fun h₁ x
  · exact DFunLike.congr_fun h₂ x

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

continuous_prod_libraryLean 4Applies a library theoremFormally verified

/-- **The product of spaces.** With the product topology, a map into `Y × Z` is continuous
exactly when both coordinates are: the product topology is the coarsest topology making the
projections continuous, which is precisely what makes `X × Y` the product in **Top**. This
applies `continuous_prodMk`. -/
theorem continuous_prod_library {X Y Z : Type u} [TopologicalSpace X] [TopologicalSpace Y]
    [TopologicalSpace Z] (f : X → Y) (g : X → Z) :
    Continuous (fun x => (f x, g x)) ↔ Continuous f ∧ Continuous g :=
  continuous_prodMk

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

Quotients (Theorem 3). Lean has quotient types built in; Quotient.lift is the existence half of the universal property, and Quotient.ind (every class is the class of some element) gives uniqueness:

quotient_universalLean 4Proved here from basic factsFormally verified

/-- **The quotient set.** If `f : X → Y` is constant on equivalence classes (`a ~ b` implies
`f a = f b`), there is exactly one `g : X/~ → Y` with `g ∘ q = f`, where `q : X → X/~` sends an
element to its class. Existence is `Quotient.lift`: define `g [a] = f a`, well defined by the
hypothesis. Uniqueness: every class is `[a]` for some `a` (`Quotient.ind`). -/
theorem quotient_universal {X Y : Type u} (s : Setoid X) (f : X → Y)
    (hf : ∀ a b, s a b → f a = f b) :
    ∃! g : Quotient s → Y, g ∘ Quotient.mk s = f := by
  refine ⟨Quotient.lift f hf, rfl, ?_⟩
  intro g hg
  funext c
  induction c using Quotient.ind with
  | _ a => exact congrFun hg a

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

quotient_group_libraryLean 4Applies a library theoremFormally verified

/-- **The quotient group.** If `N` is a normal subgroup of `G` and `f : G → H` is a homomorphism
killing `N` (`N ⊆ ker f`), there is exactly one homomorphism `g : G/N → H` with `g ∘ q = f`.
This applies `QuotientGroup.lift`, `QuotientGroup.lift_mk` and `QuotientGroup.monoidHom_ext`. -/
theorem quotient_group_library {G H : Type u} [Group G] [Group H] (N : Subgroup G) [N.Normal]
    (f : G →* H) (hN : N ≤ f.ker) :
    ∃! g : G ⧸ N →* H, g.comp (QuotientGroup.mk' N) = f :=
  ⟨QuotientGroup.lift N f hN, MonoidHom.ext fun x => QuotientGroup.lift_mk N hN x,
    fun _ hg => QuotientGroup.monoidHom_ext N (hg.trans
      (MonoidHom.ext fun x => (QuotientGroup.lift_mk N hN x).symm))⟩

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

The free monoid (Theorem 4), with words as Lean lists; the uniqueness proof is the induction on the length of a word. Mathlib's FreeMonoid is a type of lists with its own universal property:

evalWordLean 4Formally verified

/-- Evaluate a word `[s₁, s₂, …, sₖ]` in a monoid `M`, given a value `f(s)` for each letter:
the product `f(s₁) · f(s₂) ⋯ f(sₖ)` (the empty word gives `1`). -/
def evalWord {S M : Type u} [Monoid M] (f : S → M) (w : List S) : M :=
  (w.map f).prod

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

evalWord_appendLean 4Proved here from basic factsFormally verified

/-- `evalWord f` is a **monoid homomorphism** from words under concatenation: it sends the empty
word to `1` and `v ++ w` to the product of the values. -/
theorem evalWord_append {S M : Type u} [Monoid M] (f : S → M) (v w : List S) :
    evalWord f [] = 1 ∧ evalWord f (v ++ w) = evalWord f v * evalWord f w := by
  constructor
  · rfl
  · simp [evalWord, List.map_append, List.prod_append]

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

free_monoid_uniqueLean 4Proved here from basic factsFormally verified

/-- **Uniqueness in the universal property of the free monoid.** Any map `h` from words to a
monoid that preserves `1` and concatenation and agrees with `f` on one-letter words is
`evalWord f`. Proof by induction on the word: `s :: w` is the concatenation `[s] ++ w`, so
`h(s :: w) = h[s] · h(w) = f(s) · evalWord f w = evalWord f (s :: w)`. -/
theorem free_monoid_unique {S M : Type u} [Monoid M] (f : S → M) (h : List S → M)
    (h_nil : h [] = 1) (h_append : ∀ v w, h (v ++ w) = h v * h w) (h_single : ∀ s, h [s] = f s) :
    h = evalWord f := by
  funext w
  induction w with
  | nil => exact h_nil
  | cons s w ih =>
    calc h (s :: w) = h ([s] ++ w) := rfl
      _ = h [s] * h w := h_append [s] w
      _ = f s * evalWord f w := by rw [h_single, ih]
      _ = evalWord f (s :: w) := by simp [evalWord]

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

free_monoid_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's `FreeMonoid S` (words in `S`, with concatenation) and its universal property:
for every map `f : S → M` into a monoid there is exactly one monoid homomorphism
`FreeMonoid S → M` sending each letter `of s` to `f s`. This applies `FreeMonoid.lift`,
`FreeMonoid.lift_eval_of` and `FreeMonoid.hom_eq`. -/
theorem free_monoid_library {S M : Type u} [Monoid M] (f : S → M) :
    ∃! g : FreeMonoid S →* M, ∀ s, g (FreeMonoid.of s) = f s :=
  ⟨FreeMonoid.lift f, FreeMonoid.lift_eval_of f, fun _ hg =>
    FreeMonoid.hom_eq fun s => (hg s).trans (FreeMonoid.lift_eval_of f s).symm⟩

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

Fields: the universal property of $\Q$ (Theorem 6, for fields of characteristic zero, which is the same as $\Z \to K$ being injective), and the non-existence of a product of $\mathbb{F}_2$ and $\mathbb{F}_3$ (Theorem 5), where ZMod p is $\mathbb{F}_p$ :

rat_universal_libraryLean 4Applies a library theoremFormally verified

/-- **`ℚ` is the field of fractions of `ℤ`.** For every field `K` of characteristic zero (so that
`ℤ → K` is injective) there is exactly one ring homomorphism `ℚ → K` extending `ℤ → K`. This
applies `Rat.castHom` (existence) and `RingHom.ext_rat` (uniqueness); the general construction
for any integral domain is Mathlib's `IsFractionRing.lift`. -/
theorem rat_universal_library (K : Type u) [Field K] [CharZero K] :
    ∃! φ : ℚ →+* K, φ.comp (Int.castRingHom ℚ) = Int.castRingHom K :=
  ⟨Rat.castHom K, RingHom.ext_int _ _, fun φ _ => RingHom.ext_rat φ (Rat.castHom K)⟩

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

no_field_maps_to_f2_f3Lean 4Proved here from basic factsFormally verified

/-- **`𝔽₂` and `𝔽₃` have no product in the category of fields.** A product would be a field `K`
with homomorphisms `K → 𝔽₂` and `K → 𝔽₃`. But a ring homomorphism out of a field is injective;
`2 ↦ 0` in `𝔽₂` forces `2 = 0` in `K`, and `3 ↦ 0` in `𝔽₃` forces `3 = 0` in `K`; then
`1 = 3 - 2 = 0` in `K`, which no field allows. So no such `K` exists at all — the universal
property *characterises* products but does not *construct* them. -/
theorem no_field_maps_to_f2_f3 (K : Type u) [Field K] (f : K →+* ZMod 2) (g : K →+* ZMod 3) :
    False := by
  have h2 : (2 : K) = 0 := by
    apply f.injective
    rw [map_ofNat, map_zero]
    decide
  have h3 : (3 : K) = 0 := by
    apply g.injective
    rw [map_ofNat, map_zero]
    decide
  have h1 : (1 : K) = 0 := by
    calc (1 : K) = 3 - 2 := by norm_num
      _ = 0 := by rw [h2, h3, sub_zero]
  exact one_ne_zero h1

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

Not formalised here: the free group (Mathlib has FreeGroup with FreeGroup.lift), the tensor product (Mathlib's TensorProduct.lift), and the existence half of the general field-of-fractions construction (Mathlib's IsFractionRing.lift).

ComputationC

Existence and uniqueness, counted

For finite sets the universal property of the product can be checked by counting. The first experiment confirms that maps $X \to A \times B$ correspond exactly to pairs of maps, then tests three candidate "products": for each pair $(f, g)$ it counts the maps $u : X \to P$ with $p \circ u = f$ and $q \circ u = g$ . A genuine product gives the count $1$ every time; a count of $0$ is a failure of existence, a count above $1$ a failure of uniqueness.

Products of finite sets: existence and uniquenessPythonExact computationExhaustive finite checkComputationally tested

"""The universal property of the product, checked on finite sets.

For finite sets X, A, B, maps X -> A x B correspond exactly to pairs of maps
(X -> A, X -> B). We check this bijection exhaustively for small sizes. Then
we test three candidate "products" P with maps p : P -> A and q : P -> B by
counting, for every pair (f, g) of maps from a test set X, how many maps
u : X -> P satisfy p . u = f and q . u = g. A product needs exactly one every
time. The numbers model k = a*|B| + b passes; a set with a spare coordinate
fails uniqueness; the disjoint union fails existence whatever maps we choose
(it has 5 elements but there are 6 pairs to hit), and with the maps chosen
here it also fails uniqueness. Exhaustive and exact for these small sets.
"""

from itertools import product

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

def pairing(f, g):
    """The map x -> (f(x), g(x)) into the product."""
    return {x: (f[x], g[x]) for x in f}

def factorisations(xs, P, p, q, f, g):
    """Number of u : X -> P with p(u(x)) = f(x) and q(u(x)) = g(x) for all x."""
    count = 1
    for x in xs:
        count *= sum(1 for z in P if p(z) == f[x] and q(z) == g[x])
    return count

def candidates(A, B):
    """Three candidate products: (name, P, p, q)."""
    nb = len(B)
    numbers = list(range(len(A) * nb))
    spare = list(product(A, B, [0, 1]))
    union = [("A", a) for a in A] + [("B", b) for b in B]
    return [
        ("numbers k = a*|B| + b", numbers,
         lambda k: A[k // nb], lambda k: B[k % nb]),
        ("A x B x {0, 1}", spare, lambda z: z[0], lambda z: z[1]),
        ("disjoint union A + B", union,
         lambda z: z[1] if z[0] == "A" else A[0],
         lambda z: z[1] if z[0] == "B" else B[0]),
    ]

def factorisation_counts(X, A, B, P, p, q):
    """The set of factorisation counts over all pairs (f, g)."""
    return {factorisations(X, P, p, q, f, g)
            for f in maps(X, A) for g in maps(X, B)}

def main():
    print("1. Maps X -> A x B versus pairs of maps (X -> A, X -> B)")
    for nx, na, nb in [(1, 2, 3), (2, 2, 2), (2, 3, 2), (3, 2, 2)]:
        X, A, B = range(nx), range(na), range(nb)
        n_pairs = len(maps(X, A)) * len(maps(X, B))
        images = {tuple(sorted(pairing(f, g).items()))
                  for f in maps(X, A) for g in maps(X, B)}
        total = len(maps(X, list(product(A, B))))
        ok = n_pairs == len(images) == total
        print(f"   |X|={nx} |A|={na} |B|={nb}: {n_pairs:>3} pairs, "
              f"{total:>3} maps, pairing is a bijection: {ok}")
    print()
    print("2. Factorisations through candidate products, |A| = 2, |B| = 3")
    A, B = ["a0", "a1"], ["b0", "b1", "b2"]
    for nx in (1, 2):
        X = range(nx)
        print(f"   test set X with {nx} element(s):")
        for name, P, p, q in candidates(A, B):
            counts = sorted(factorisation_counts(X, A, B, P, p, q))
            verdict = "product" if counts == [1] else "not a product"
            print(f"     {name:<22} counts {str(counts):<13} {verdict}")
    print()
    print("Epistemic status: exhaustive and exact for these small sets. Part 1")
    print("illustrates |A x B|^|X| = |A|^|X| |B|^|X|; part 2 shows how")
    print("existence (count >= 1) and uniqueness (count <= 1) can each fail.")
    print("The lesson proves the universal property for all sets.")

if __name__ == "__main__":
    main()

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

The second experiment takes the free monoid on two letters $L, R$ and the unique homomorphism to $2 \times 2$ integer matrices sending $L \mapsto \left(\begin{smallmatrix} 1 & 0 \\ 1 & 1 \end{smallmatrix}\right)$ and $R \mapsto \left(\begin{smallmatrix} 1 & 1 \\ 0 & 1 \end{smallmatrix}\right)$ . Different words turn out to give different matrices, and a subtraction algorithm — Euclid's algorithm in disguise — reads the word back off the matrix. Homomorphisms to $(\N, +)$ or $(\Z, +)$ , by contrast, forget almost everything.

Words in L and R, evaluated in three monoidsPythonExact computationExhaustive finite checkComputationally tested

"""The free monoid on {L, R}, evaluated in three monoids.

The universal property of the free monoid says: choosing a value for each
letter in a monoid M determines exactly one monoid homomorphism from words
to M, namely "multiply the values of the letters". We take M to be the 2x2
integer matrices with L = [[1,0],[1,1]] and R = [[1,1],[0,1]], check the
homomorphism property, and find that different words give different
matrices; a subtraction algorithm (Euclid's algorithm in disguise) reads the
word back off the matrix, which is why this homomorphism is injective. Other
choices of target, (N, +) and (Z, +), give homomorphisms that are far from
injective. Finally each word gives a fraction, listing positive rationals as
in the Stern-Brocot tree. Exact, exhaustive for words of bounded length.
"""

from fractions import Fraction
from itertools import product

IDENTITY = ((1, 0), (0, 1))
GENERATORS = {"L": ((1, 0), (1, 1)), "R": ((1, 1), (0, 1))}

def matmul(x, y):
    """Product of 2x2 matrices given as nested tuples."""
    return tuple(
        tuple(sum(x[i][k] * y[k][j] for k in range(2)) for j in range(2))
        for i in range(2)
    )

def evaluate(word, values, op, unit):
    """The unique homomorphism from words: multiply the letters' values."""
    result = unit
    for letter in word:
        result = op(result, values[letter])
    return result

def words(max_length, alphabet="LR"):
    """All words of length 0..max_length, shortest first."""
    out = []
    for n in range(max_length + 1):
        out.extend("".join(w) for w in product(alphabet, repeat=n))
    return out

def decode(m):
    """Recover the word of a matrix in the monoid generated by L and R.

    If the top row dominates the bottom row the word starts with R
    (strip it: subtract the bottom row from the top), otherwise with L.
    Returns None if m is not reached by any word.
    """
    word = []
    (a, b), (c, d) = m
    if min(a, b, c, d) < 0:
        return None
    # Each step subtracts a non-zero row of non-negative entries, so the
    # entries stay non-negative and their sum strictly decreases: it stops.
    while ((a, b), (c, d)) != IDENTITY:
        if a >= c and b >= d and (c, d) != (0, 0):
            word.append("R")
            a, b = a - c, b - d
        elif c >= a and d >= b and (a, b) != (0, 0):
            word.append("L")
            c, d = c - a, d - b
        else:
            return None
    return "".join(word)

def fraction_of(m):
    """The Stern-Brocot fraction (a + b) / (c + d) of a matrix."""
    (a, b), (c, d) = m
    return Fraction(a + b, c + d)

def main():
    def mat(w):
        return evaluate(w, GENERATORS, matmul, IDENTITY)

    short = words(4)
    hom = all(mat(v + w) == matmul(mat(v), mat(w)) for v in short for w in short)
    print("Target 1: 2x2 matrices, L = [[1,0],[1,1]], R = [[1,1],[0,1]]")
    print(f"  eval(vw) = eval(v) eval(w) for all {len(short)}^2 pairs of words"
          f" of length <= 4: {hom}")
    long = words(10)
    images = {mat(w) for w in long}
    print(f"  {len(long)} words of length <= 10 give {len(images)} distinct"
          " matrices")
    back = all(decode(mat(w)) == w for w in long)
    print(f"  decoding by subtraction recovers every one of these words: {back}")
    print(f"  LR = {mat('LR')} but RL = {mat('RL')}")
    print()
    length = {"L": 1, "R": 1}
    signed = {"L": 1, "R": -1}
    plus = (lambda x, y: x + y)
    for name, values in [("(N, +), L, R -> 1", length),
                         ("(Z, +), L -> 1, R -> -1", signed)]:
        image = {evaluate(w, values, plus, 0) for w in long}
        print(f"Target: {name:<24} {len(long)} words -> {len(image)} values")
    print()
    fracs = [fraction_of(mat(w)) for w in words(3)]
    print(f"Stern-Brocot: the {len(fracs)} words of length <= 3 give"
          f" {len(set(fracs))} distinct")
    print("fractions (a + b)/(c + d), where [[a, b], [c, d]] is the matrix:")
    print("  " + " ".join(str(f) for f in sorted(set(fracs))))
    print()
    print("Epistemic status: exact and exhaustive for words of length at most")
    print("10. That no two words share a matrix for all lengths is a theorem")
    print("(the decoding always works, by the argument of Euclid's algorithm);")
    print("this run is evidence for it, not a proof.")

if __name__ == "__main__":
    main()

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

Both experiments are exhaustive for bounded sizes. They illustrate the theorems; they do not prove them. (That the $L, R$ homomorphism is injective for words of every length is a theorem: the decoding step always succeeds because exactly one of the two rows of a matrix of non-negative integers with determinant $1$ , other than the identity, dominates the other.)

Explore

Explore: maps into a product, maps out of a quotient

Choose maps $f : Z \to A$ and $g : Z \to B$ between small finite sets, then try to build a map $h : Z \to A \times B$ that is compatible with the projections. You will find that each choice of $h(z)$ is forced: its first coordinate must be $f(z)$ and its second $g(z)$ . That is existence and uniqueness, one element at a time.

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

The quotient that makes a torus. Gluing opposite sides of a square is a quotient: points on opposite edges are declared equivalent. By the universal property of the quotient (topology), a continuous function on the torus is exactly a continuous function on the square taking equal values at glued points. Walk the flatlander off one edge and watch it re-enter through the partner edge; the tiling view shows the same functions as doubly periodic functions on the plane.

A quotient of the square

Opposite sides are identified; maps out of the torus are maps out of the square that respect the gluing.

Keys: ↑ forward, ↓ back, ← and → turn, Space walks or stops. You can also drag it.

Torusa b a⁻¹ b⁻¹

Orientable: Yes
Euler characteristic: χ = 0

Gluing turns the 4 corners into V = 1, the 4 sides into E = 2 and the square into F = 1: V − E + F = 1 − 2 + 1 = 0

Same way round as at the start.

Sides crossed so far: 0

Opposite sides are glued with arrows pointing the same way. Walk off the right side and you come back on the left, the same way round. However it walks, the flatlander is never mirrored: the torus is orientable.

Copies of the square tile the plane, and the trail runs on smoothly from copy to copy. This plane is the universal cover of the torus.

Exercises

1. Universal properties

Warm-upHuman

Let $|X| = 2$ , $|A| = 2$ and $|B| = 3$ . How many functions $X \to A \times B$ are there? (Use the universal property: such a function is the same as a pair of functions $X \to A$ , $X \to B$ .)

2. Universal properties

Warm-upHuman

The free monoid on a one-element set $\{a\}$ is isomorphic to which monoid?

Choose one

(\mathbb{N}, +, 0)

(\mathbb{Z}, +, 0)

(\mathbb{Z}/2, +, 0)

The trivial monoid

\{1\}

3. Universal properties

CoreHuman

Let $\bar f$ be the unique monoid homomorphism from the free monoid on $\{a, b\}$ to $(\mathbb{Z}, +, 0)$ with $\bar f(a) = 2$ and $\bar f(b) = -1$ . What is $\bar f(abbab)$ ?

4. Universal properties

CoreHuman

Let $A, B$ be non-empty sets and $P = A \times B \times \{0, 1\}$ , with $p(a, b, i) = a$ and $q(a, b, i) = b$ . Which part of the universal property of the product does $(P, p, q)$ fail?

Choose one

Uniqueness: for every

X

and every pair

f, g

there are several compatible maps

X \to P

(for non-empty

X

).Existence: some pairs

f, g

have no compatible map.Both existence and uniqueness.Neither — it is a product, isomorphic to

A \times B

5. Universal properties

CoreHuman

In the proof that two universal arrows $(F, \eta)$ and $(F', \eta')$ are isomorphic, we know $U(\psi \circ \varphi) \circ \eta = \eta$ . What exactly lets us conclude $\psi \circ \varphi = \mathrm{id}_F$ ?

Choose one

The uniqueness clause for

(F, \eta)

applied to

f = \eta

: both

\psi \circ \varphi

and

\mathrm{id}_F

are morphisms

g : F \to F

with

U(g) \circ \eta = \eta

.The existence clause for

(F, \eta)

\eta

is a monomorphism, so it can be cancelled.

U

is faithful, so

U(\psi \circ \varphi) = U(\mathrm{id}_F)

implies

\psi \circ \varphi = \mathrm{id}_F

6. Universal properties

CoreHuman

Regard the positive integers ordered by divisibility ( $a \to b$ when $a \mid b$ ) as a category. Which statements are true? Choose all that apply.

Choose all that apply

The product of

12

and

18

6

.The coproduct of

12

and

18

36

1

is an initial object.The product of

12

and

18

12 \cdot 18 = 216

.There is a terminal object.

7. Universal properties

CoreFormal

In the Lean structure UniversalArrow X U, with fields obj, unit : X ⟶ U.obj obj and lift, which field states the uniqueness clause? (Recall unit ≫ U.map g means $U(g) \circ \eta$ .)

Choose one

uniq : ∀ {E} (f : X ⟶ U.obj E) (g : obj ⟶ E), unit ≫ U.map g = f → g = lift ffac : ∀ {E} (f : X ⟶ U.obj E), unit ≫ U.map (lift f) = f∀ {E} (g g' : obj ⟶ E), g = g'∀ {E} (f : X ⟶ U.obj E) (g : obj ⟶ E), g = lift f → unit ≫ U.map g = f

8. Universal properties

StretchComputational

An equivalence relation on a finite set is given by its list of classes, e.g. [{0, 3}, {1, 4}, {2, 5}], and a function by a dict. Write descend(f, classes) that returns the induced function $\bar f$ on classes — a dict from each class (as a frozenset) to a value, with $\bar f([x]) = f(x)$ — or None if $f$ is not constant on some class (so that no $\bar f$ with $\bar f \circ q = f$ exists).

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

Common misconceptionsH

Common misconceptions

Misconception

"A universal property constructs the object." It only characterises it: if an object with the property exists, it is unique up to unique isomorphism. Existence needs a separate construction, and can fail — the fields $\mathbb{F}_2$ and $\mathbb{F}_3$ have no product, and two incomparable elements of a poset may have no meet.

Misconception

"The uniqueness clause is a technicality." Without it the theory collapses. The set $A \times B \times \{0, 1\}$ with the obvious projections receives a compatible map from every $X$ — but never just one, and it is not isomorphic to $A \times B$ . The proof of Theorem 1 uses uniqueness at the decisive step.

Misconception

"The product is one particular set." $A \times B$ built from Kuratowski pairs, and the set $\{0, \dots, |A||B| - 1\}$ with suitable projections, are both products of finite sets $A$ and $B$ . Neither is "the real one"; they are identified by a unique compatible bijection, and every statement made using only the universal property holds for both.

Misconception

"Unique up to isomorphism is the same as unique up to unique isomorphism." The extra word matters. Any two groups of order $5$ are isomorphic, but by four different isomorphisms; there is no canonical choice. Two products of $A$ and $B$ are related by exactly one isomorphism commuting with the projections, so identifying them never involves a choice.

ViewpointsH

Many ways of seeing

Topology— Topologies forced by universal properties: products and gluing

The product topology is the unique topology on $\prod_i X_i$ making it the product in $\cat{Top}$ : a map $Z \to \prod_i X_i$ is continuous iff every component $Z \to X_i$ is. For infinite products the box topology (generated by all products of open sets) is too fine to satisfy this: the diagonal map $\R \to \R^{\N}$ , $t \mapsto (t, t, t, \dots)$ , has continuous components, but the preimage of the box-open set $\prod_n (-1/n, 1/n)$ is $\{0\}$ , which is not open. The universal property picks the right answer.

Dually, the quotient topology on $X/{\sim}$ is the one making $q$ universal: a map out of $X/{\sim}$ is continuous iff its composite with $q$ is. Gluing opposite sides of a square gives a torus, and the universal property says that continuous maps out of the torus are the same as continuous maps out of the square that agree on glued points — equivalently, continuous functions on $\R^2$ that are periodic in both directions (quotient topologies are developed in point-set topology). The universal cover of a space, met with the fundamental group, is another object named for a universal property.

Number theory— gcd, lcm and the Chinese remainder theorem

In the positive integers ordered by divisibility, the product of $a$ and $b$ is $\gcd(a, b)$ (the largest common divisor, in the sense that every common divisor divides it) and the coproduct is $\mathrm{lcm}(a, b)$ . In rings, the Chinese remainder theorem says that for coprime $m, n$ the ring $\Z/mn$ , with the reduction maps to $\Z/m$ and $\Z/n$ , is a product of $\Z/m$ and $\Z/n$ : the map $\Z/mn \to \Z/m \times \Z/n$ given by the universal property of the product ring is injective (if $m \mid x$ and $n \mid x$ then $mn \mid x$ ) and so bijective by counting. See divisibility and gcd. The rationals are the field of fractions of $\Z$ , and the $p$ -adic integers $\Z_p$ are the limit of $\cdots \to \Z/p^3 \to \Z/p^2 \to \Z/p$ , a universal property of the kind studied in limits and colimits.

Algebra— Presentations: free objects modulo relations

Combining two universal properties gives presentations. The group $\langle S \mid R \rangle$ is the quotient of the free group $F(S)$ by the smallest normal subgroup containing the words in $R$ . Its universal property: homomorphisms $\langle S \mid R \rangle \to G$ correspond exactly to functions $S \to G$ under which every relation in $R$ becomes true in $G$ . For example, homomorphisms from the dihedral group $\langle r, s \mid r^n, s^2, (rs)^2 \rangle$ to $G$ are pairs of elements $(\rho, \sigma)$ of $G$ with $\rho^n = \sigma^2 = (\rho\sigma)^2 = e$ . The same pattern defines polynomial rings ( $k[x]$ is the free commutative $k$ -algebra on $x$ ) and quotient rings $k[x]/(x^2 + 1)$ , and lets one construct $\C$ as $\R[x]/(x^2 + 1)$ .

Computation— fold, reduce and MapReduce

The universal property of the free monoid is the fold (or reduce) of functional programming: given a value f(s) for each letter and a monoid $(M, \cdot, 1)$ , there is exactly one way to evaluate every list compatibly with concatenation. Because the result is a monoid homomorphism, a long list can be cut into pieces, each piece reduced on a different machine, and the partial results combined with $\cdot$ — this is the algebra behind parallel "map-reduce" computations, and it works only because the operation is associative. Product types (pairs, records) and sum types (tagged unions) in programming languages are products and coproducts in a category of types.

Logic— And, or, and the quantifiers

In the preorder of propositions ordered by entailment, the product of $P$ and $Q$ is $P \wedge Q$ (it entails both, and anything entailing both entails it), the coproduct is $P \vee Q$ , the terminal object is "true" and the initial object is "false". The rules of natural deduction for $\wedge$ — from $P \wedge Q$ infer $P$ and infer $Q$ ; from $R \vdash P$ and $R \vdash Q$ infer $R \vdash P \wedge Q$ — are exactly the projections and the pairing of the universal property. F. William Lawvere (1969) showed that the quantifiers $\exists$ and $\forall$ are also characterised by universal properties (as adjoints to substitution) — see first-order logic and categorical logic.

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 gradedRemainder familiesSort every integer — positive, negative and zero — into families by its remainder after dividing by 3. If you add a member of one family to a member of another, does the family of the answer depend on which members you chose?Follow the trail

History & global context

History and global context

Many universal constructions are old. The Chinese remainder theorem appears in the Sunzi Suanjing (China, around the 3rd to 5th century), and Indian mathematicians from Āryabhaṭa (499) onwards solved such systems with the kuṭṭaka method. Fractions of integers are ancient; the abstract field of fractions of an integral domain belongs to the algebra of the late 19th and early 20th centuries (Dedekind, Steinitz).
Walther von Dyck (1882) studied groups given by generators and relations; Jakob Nielsen (1921) and Otto Schreier (1927) developed the theory of free groups. Hassler Whitney defined the tensor product of abelian groups in 1938.
Kazimierz Kuratowski gave his definition of the ordered pair in 1921, refining Norbert Wiener's of 1914.
Pierre Samuel, in "On universal mappings and free topological groups" (1948), formulated universal mapping problems in general, and the Bourbaki group made them a standard tool. Daniel Kan's adjoint functors (1958) showed that universal arrows for every object assemble into a functor, and Saunders Mac Lane's Categories for the Working Mathematician (1971) made universal properties the organising principle of category theory.

What is an ordered pair, really?

The best solution to a problem

Definitions

Examples

Uniqueness, existence and non-existence

Universal properties in Lean and Mathlib

Existence and uniqueness, counted

Explore: maps into a product, maps out of a quotient

Exercises

Common misconceptions

Many ways of seeing

Wonder Trails

History and global context

Further reading