Diagrams where paths agree

Wanjiru sells hand-woven baskets in Nairobi. A basket costs $1000$ Kenyan shillings before tax, and Kenya adds $16\%$ value-added tax (VAT). A visitor wants to know the price in US dollars. To keep the numbers simple, suppose the exchange rate is $125$ shillings to the dollar (real rates change every day).

There are two routes from “price before tax, in shillings” to “price with tax, in dollars”:

• add VAT, then convert: $1000 \times 1.16 = 1160$ shillings, and $1160 \div 125 = 9.28$ dollars;
• convert, then add VAT: $1000 \div 125 = 8$ dollars, and $8 \times 1.16 = 9.28$ dollars.

Same answer! Now Wanjiru adds a delivery fee of $200$ shillings. “Add the fee, then convert” gives $1200 \div 125 = 9.60$ dollars. But “convert, then add $200$” gives $8 + 200 = 208$ dollars — absurd. The fee has to be converted too: on the dollar route we must add $200 \div 125 = 1.60$ dollars.

Pictures of routes like these, and the question “do the routes always agree?”, are the subject of this lesson. They are called commutative diagrams, and they are one of the most widely used pictures in modern mathematics.

Draw each set as a corner and each function as an arrow. The VAT story becomes a square:

Start at the top left. One route goes across, then down; the other goes down, then across. Both end at the bottom right. The square commutes if the two routes always give the same result.

With the delivery fee, the square only commutes if the bottom arrow adds the converted fee:

A carpenter in Kumasi measures two planks: $1.2$ m and $0.85$ m. Laid end to end they make $2.05$ m, which is $205$ cm. Measured in centimetres they are $120$ cm and $85$ cm, which make $205$ cm. Converting and adding can be done in either order:

This is a commuting square too — but its left-hand corners hold pairs of lengths $(a, b)$:

Some functions preserve addition and many do not:

• $x \mapsto 100x$ (metres to centimetres) preserves addition: that is the distributive law.
• $x \mapsto x + 1$ does not: with $a = b = 0$, “add then apply” gives $1$ but “apply then add” gives $1 + 1 = 2$.
• $x \mapsto x^2$ does not: $(1 + 1)^2 = 4$ but $1^2 + 1^2 = 2$.
• $x \mapsto 100x$ preserves addition but not multiplication: $100 \cdot (1 \cdot 1) = 100$, while $(100 \cdot 1) \cdot (100 \cdot 1) = 10\,000$. That is why $1\ \mathrm{m}^2 = 10\,000\ \mathrm{cm}^2$, not $100\ \mathrm{cm}^2$: an area is a product of two lengths.
• Celsius to Fahrenheit, $C \mapsto 1.8\,C + 32$, does not preserve addition: $10\,^\circ\mathrm{C}$ and $20\,^\circ\mathrm{C}$ give $50$ and $68$, which add to $118$, but $30\,^\circ\mathrm{C}$ is $86\,^\circ\mathrm{F}$. (The differences of temperatures do convert by $\times 1.8$ alone.)
• “Take the last digit” preserves addition if the bottom route adds digits with wrap-around (keeping only the last digit of the sum): the last digit of $47 + 38 = 85$ is $5$, and $7 + 8 = 15$ also ends in $5$.
• Squares can even change the operation. $2^{a + b} = 2^a \cdot 2^b$: “add, then raise $2$ to that power” equals “raise $2$ to each power, then multiply”.

In words: we slide the route across the rectangle one square at a time, and each slide is allowed because that square commutes.

So among all functions from $\Z$ to $\Z$, the ones that preserve addition are exactly the multiplications $x \mapsto mx$. A single value, $f(1)$, determines everything.

A square is described by its four arrows; it commutes when the two routes agree at every input. In Lean that is a definition, word for word:

/-- The square with `top : A → B`, `right : B → D`, `left : A → C` and `bottom : C → D`
**commutes** when the two routes from `A` to `D` agree for every input: going along the top and
then down the right gives the same as going down the left and then along the bottom. -/
def SquareCommutes {A B C D : Type} (top : A → B) (right : B → D) (left : A → C)
    (bottom : C → D) : Prop :=
  ∀ a, right (top a) = bottom (left a)

/-- The triangle with `f : A → B`, `g : B → C` and `h : A → C` **commutes** when the two-step
route equals the direct route: `g (f a) = h a` for every `a`. -/
def TriangleCommutes {A B C : Type} (f : A → B) (g : B → C) (h : A → C) : Prop :=
  ∀ a, g (f a) = h a

/-- "Double, then add 2" equals "add 1, then double": `2x + 2 = 2(x + 1)` for every integer. -/
theorem double_add_square :
    SquareCommutes (fun x : Int => 2 * x) (fun x => x + 2) (fun x => x + 1) (fun x => 2 * x) := by
  intro a
  show 2 * a + 2 = 2 * (a + 1)
  omega

/-- "Add 1, then double" is **not** "double, then add 1": at `0` the routes give `2` and `1`.
One input where the routes disagree is enough to show a square does not commute. -/
theorem add_double_not_square :
    ¬ SquareCommutes (fun x : Int => x + 1) (fun x => 2 * x) (fun x => 2 * x) (fun x => x + 1) := by
  intro h
  have h0 := h 0
  revert h0
  decide

/-- Agreeing at some inputs is not enough. The routes "square" and "double" agree at `0` and at
`2` (`0² = 2·0` and `2² = 2·2`), but the square does not commute: at `1` they give `1` and `2`. -/
theorem agree_twice_not_square :
    (0 * 0 = 2 * 0 ∧ 2 * 2 = 2 * (2 : Int)) ∧
      ¬ SquareCommutes (fun x : Int => x * x) id id (fun x => 2 * x) := by
  refine ⟨by decide, ?_⟩
  intro h
  have h1 := h 1
  revert h1
  decide

/-- Hours to minutes (`× 60`), then minutes to seconds (`× 60`), is hours to seconds (`× 3600`). -/
theorem hours_triangle :
    TriangleCommutes (fun h : Nat => 60 * h) (fun m => 60 * m) (fun h => 3600 * h) := by
  intro h
  show 60 * (60 * h) = 3600 * h
  omega

/-- **What day is it in 100 days?** Number the days, and let a day's remainder on division by `7`
be its weekday. The square "add 100 days, then take the weekday" = "take the weekday, then move
on 2 weekdays" commutes, because `100 = 14 · 7 + 2`. -/
theorem weekday_square :
    SquareCommutes (fun n : Nat => n + 100) (fun n => n % 7) (fun n => n % 7)
      (fun r => (r + 2) % 7) := by
  intro n
  show (n + 100) % 7 = (n % 7 + 2) % 7
  omega

Preserving addition, and the fact that it is a commuting square (the corners on the left hold pairs of integers, Int × Int):

/-- `f` **preserves addition** if `f (a + b) = f a + f b` for all `a` and `b`. -/
def PreservesAdd (f : Int → Int) : Prop := ∀ a b, f (a + b) = f a + f b

/-- Preserving addition **is** a commuting square. Its corners hold pairs of numbers on the left
and single numbers on the right: along the top, add the pair, then apply `f`; down the left,
apply `f` to both numbers, then add. -/
theorem preserves_add_iff_square (f : Int → Int) :
    PreservesAdd f ↔
      SquareCommutes (fun p : Int × Int => p.1 + p.2) f (fun p => (f p.1, f p.2))
        (fun p => p.1 + p.2) := by
  constructor
  · intro h p
    exact h p.1 p.2
  · intro h a b
    exact h (a, b)

/-- Converting metres to centimetres, `x ↦ 100x`, preserves addition: `100(a + b) = 100a + 100b`.
This is the distributive law, core Lean's `Int.mul_add`. -/
theorem cm_preserves_add : PreservesAdd (fun x => 100 * x) :=
  fun a b => Int.mul_add 100 a b

/-- `x ↦ x + 1` does **not** preserve addition: with `a = b = 0`, the routes give
`(0 + 0) + 1 = 1` and `(0 + 1) + (0 + 1) = 2`. -/
theorem add_one_not_preserves : ¬ PreservesAdd (fun x => x + 1) := by
  intro h
  have h00 := h 0 0
  revert h00
  decide

/-- Exactly which functions `x ↦ mx + c` preserve addition? Those with `c = 0`.
The two routes give `m(a + b) + c` and `(ma + c) + (mb + c)`, which differ by `c`. -/
theorem affine_preserves_add_iff (m c : Int) : PreservesAdd (fun x => m * x + c) ↔ c = 0 := by
  constructor
  · intro h
    have h00 : m * (0 + 0) + c = (m * 0 + c) + (m * 0 + c) := h 0 0
    rw [Int.zero_add, Int.mul_zero, Int.zero_add] at h00
    omega
  · intro hc a b
    show m * (a + b) + c = (m * a + c) + (m * b + c)
    rw [hc, Int.mul_add, Int.add_zero, Int.add_zero, Int.add_zero]

/-- Squaring does not preserve addition: `(1 + 1)² = 4`, but `1² + 1² = 2`. -/
theorem square_not_preserves : ¬ PreservesAdd (fun x => x * x) := by
  intro h
  have h11 := h 1 1
  revert h11
  decide

/-- `x ↦ 100x` preserves addition but **not** multiplication: `100 · (1 · 1) = 100`, while
`(100 · 1) · (100 · 1) = 10000`. This is why `1 m² = 10 000 cm²`, not `100 cm²`. -/
theorem cm_not_preserves_mul : ¬ ∀ a b : Int, 100 * (a * b) = (100 * a) * (100 * b) := by
  intro h
  have h11 := h 1 1
  revert h11
  decide

Theorem 4, with the induction written out:

/-- **Every addition-preserving function `ℤ → ℤ` is multiplication by a fixed number**, namely
by `f 1`. Steps: `f 0 = 0` (from `f (0 + 0) = f 0 + f 0`); `f (n + 1) = f n + f 1`, so by induction
`f n = f 1 · n` for every natural number `n`; and `f (−x) = −f x` (because
`f x + f (−x) = f 0 = 0`), which handles the negative numbers. -/
theorem preserves_add_is_mul (f : Int → Int) (h : PreservesAdd f) : ∀ x, f x = f 1 * x := by
  have h0 : f 0 = 0 := by
    have e := h 0 0
    rw [Int.add_zero] at e
    omega
  have hnat : ∀ n : Nat, f n = f 1 * n := by
    intro n
    induction n with
    | zero =>
      show f 0 = f 1 * 0
      rw [h0, Int.mul_zero]
    | succ k ih =>
      have hk : ((k + 1 : Nat) : Int) = (k : Int) + 1 := by omega
      rw [hk, h, ih, Int.mul_add, Int.mul_one]
  have hneg : ∀ x, f (-x) = -f x := by
    intro x
    have e := h x (-x)
    rw [Int.add_right_neg, h0] at e
    omega
  intro x
  obtain ⟨n, hn | hn⟩ := Int.eq_nat_or_neg x
  · rw [hn, hnat]
  · rw [hn, hneg, hnat, Int.mul_neg]

Two squares that change one operation into another — remainders, and powers of $2$:

/-- Taking remainders on division by `7` turns `+` into "add, then take the remainder":
`(a + b) % 7 = (a % 7 + b % 7) % 7`. This applies core Lean's `Nat.add_mod`. -/
theorem remainder_preserves_add (a b : Nat) : (a + b) % 7 = (a % 7 + b % 7) % 7 :=
  Nat.add_mod a b 7

/-- A square that turns addition into multiplication: `2^(a + b) = 2^a · 2^b`. This applies core
Lean's `Nat.pow_add`. -/
theorem pow_turns_add_into_mul (a b : Nat) : 2 ^ (a + b) = 2 ^ a * 2 ^ b :=
  Nat.pow_add 2 a b

Finally, pasting — the calc block is the human proof, one square per line — and the counterexample to its converse:

/-- **Pasting.** Put two commuting squares side by side, sharing the middle arrow `b`:

    A --f--> B --g--> C
    |a       |b       |c
    v        v        v
    D --f'-> E --g'-> F

If the left square (`b (f x) = f' (a x)`) and the right square (`c (g y) = g' (b y)`) commute,
then so does the outer rectangle: `c (g (f x)) = g' (b (f x)) = g' (f' (a x))`. -/
theorem paste {A B C D E F : Type} {f : A → B} {g : B → C} {f' : D → E} {g' : E → F}
    {a : A → D} {b : B → E} {c : C → F}
    (hleft : SquareCommutes f b a f') (hright : SquareCommutes g c b g') :
    SquareCommutes (fun x => g (f x)) c a (fun x => g' (f' x)) := by
  intro x
  calc c (g (f x)) = g' (b (f x)) := hright (f x)
    _ = g' (f' (a x)) := by rw [hleft x]

/-- The converse fails: the outer rectangle can commute although the left square does not.
Take every map to be the identity, except `b = (· + 1)` and `c = g' = 0` (constant). The outer
routes both give `0`, but the left square needs `x + 1 = x`. -/
theorem paste_converse_false :
    ∃ f g f' g' a b c : Int → Int,
      SquareCommutes (fun x => g (f x)) c a (fun x => g' (f' x)) ∧ ¬ SquareCommutes f b a f' := by
  refine ⟨id, id, id, fun _ => 0, id, fun x => x + 1, fun _ => 0, ?_, ?_⟩
  · intro x
    rfl
  · intro h
    have h0 := h 0
    revert h0
    decide

What is formalised: every theorem and worked example of this lesson for integers and natural numbers, using core Lean only. In Mathlib, Lean's large mathematical library, functions that preserve addition are called additive homomorphisms (AddMonoidHom), and commuting squares in any category are described by CategoryTheory.CommSq.

"""Do the paths agree? Testing squares of functions by computer.

A square of functions commutes when both routes give the same output for
every input. The experiment (1) tests three squares on the integers -50..50
and reports the first input where the routes disagree; (2) hunts for
counterexamples to "f(a + b) = f(a) + f(b)"; (3) checks all 3125 functions
from {0, ..., 4} to itself and finds exactly 5 that preserve addition with
remainders, each "multiply by m"; (4) checks every way of filling a pair of
squares with functions on {0, 1}: pasting always works, the converse does
not. Parts 3 and 4 are exhaustive; parts 1 and 2 are evidence or refutation.
"""

from fractions import Fraction
from itertools import product

def around_zero(n):
    """The integers -n..n, ordered 0, -1, 1, -2, 2, ... so that searches
    report the smallest counterexample first."""
    return sorted(range(-n, n + 1), key=lambda x: (abs(x), x))

def first_disagreement(route1, route2, inputs):
    """The first input where the two routes differ, or None if they agree."""
    for x in inputs:
        if route1(x) != route2(x):
            return x
    return None

def add_counterexample(f, values, add=lambda a, b: a + b):
    """A pair (a, b) with f(a + b) != f(a) + f(b), or None. `add` is the
    addition used after applying f (for remainders it wraps around)."""
    for a in values:
        for b in values:
            if f(a + b) != add(f(a), f(b)):
                return (a, b)
    return None

def additive_maps_mod(n):
    """All functions f on {0..n-1} with f((a+b) % n) == (f(a)+f(b)) % n."""
    found = []
    for outputs in product(range(n), repeat=n):
        if all(outputs[(a + b) % n] == (outputs[a] + outputs[b]) % n
               for a in range(n) for b in range(n)):
            found.append(outputs)
    return found

def square_commutes(top, right, left, bottom, inputs):
    """right(top(x)) == bottom(left(x)) for every x; maps are tuples."""
    return all(right[top[x]] == bottom[left[x]] for x in inputs)

def pasting_counts():
    """Fill the two squares (7 maps on {0, 1}) in every way. Return
    (both squares commute, ... and the rectangle commutes too,
    rectangle commutes but the left square does not)."""
    maps = list(product((0, 1), repeat=2))
    both = both_and_outer = outer_not_left = 0
    for f, g, f2, g2, a, b, c in product(maps, repeat=7):
        left = square_commutes(f, b, a, f2, (0, 1))
        right = square_commutes(g, c, b, g2, (0, 1))
        gf = tuple(g[f[x]] for x in (0, 1))
        g2f2 = tuple(g2[f2[x]] for x in (0, 1))
        outer = square_commutes(gf, c, a, g2f2, (0, 1))
        if left and right:
            both += 1
            both_and_outer += outer
        if outer and not left:
            outer_not_left += 1
    return both, both_and_outer, outer_not_left

def main():
    xs = around_zero(50)
    print("1. Two routes around a square, inputs -50..50")
    tests = [
        ("double, +2  vs  +1, double", lambda x: 2 * x + 2, lambda x: 2 * (x + 1)),
        ("+1, double  vs  double, +1", lambda x: 2 * (x + 1), lambda x: 2 * x + 1),
        ("square      vs  double    ", lambda x: x * x, lambda x: 2 * x),
    ]
    for name, r1, r2 in tests:
        bad = first_disagreement(r1, r2, xs)
        agree = sum(r1(x) == r2(x) for x in xs)
        verdict = "agree on all 101" if bad is None else f"differ at {bad}"
        print(f"   {name}: {verdict} (agree on {agree})")
    print()
    print("2. Does f(a + b) = f(a) + f(b)? Search a, b in -20..20")
    vals = around_zero(20)
    rules = [("100x", lambda x: 100 * x), ("x + 1", lambda x: x + 1),
             ("x * x", lambda x: x * x), ("-3x", lambda x: -3 * x),
             ("C to F", lambda x: Fraction(9, 5) * x + 32)]
    for name, f in rules:
        cx = add_counterexample(f, vals)
        print(f"   {name:<7}", "no counterexample" if cx is None
              else f"fails at a, b = {cx[0]}, {cx[1]}")
    print()
    maps = additive_maps_mod(5)
    print("3. All 5^5 = 3125 functions on {0..4}, adding with remainders mod 5")
    print(f"   preserving addition: {len(maps)}")
    for m in maps:
        print(f"   {m}  = multiply by {m[1]}:",
              all(m[x] == m[1] * x % 5 for x in range(5)))
    print()
    both, outer, converse = pasting_counts()
    print("4. Pasting: all 4^7 = 16384 ways to fill two squares on {0, 1}")
    print(f"   both squares commute: {both}; rectangle commutes too: {outer}")
    print(f"   rectangle commutes but the left square does not: {converse}")
    print()
    print("Epistemic status: parts 3 and 4 are exhaustive, so they prove their")
    print("claims for these small sets; parts 1 and 2 refute with one")
    print("counterexample but only test the others. The lesson proves that")
    print("pasting always works and that additive maps are multiplications.")

if __name__ == "__main__":
    main()

Parts 1 and 2 are refutations or evidence: a disagreement found at one input settles “does not commute” for good, but “no counterexample among $-20$ to $20$” is only a hint. Parts 3 and 4 are exhaustive. Part 3 is Theorem 4 in miniature: of all $3125$ functions on $\{0, 1, 2, 3, 4\}$, exactly $5$ preserve addition (with remainders on division by $5$), and each one is “multiply by $m$”. Part 4 confirms pasting for every one of the $1664$ fillings where both squares commute, and finds thousands of fillings where the rectangle commutes although the left square does not.

Graph each route as a function of the input $x$. The square commutes exactly when the two graphs are the same line. Here the routes are “add $a$, then multiply by $m$” and “multiply by $m$, then add $a$”:

Things to try: find all settings of $m$ and $a$ where the lines coincide. (You should find $a = 0$ with any $m$, and $m = 1$ with any $a$ — can you explain why from the formulas $mx + ma$ and $mx + a$?) When they don't coincide, the lines are parallel or cross at one point — and crossing at one point means the routes agree for one input only, which is not enough.

The machines below run two functions in both orders, which is exactly the square with $f, g$ across the top and right and $g, f$ down the left and bottom. Look for pairs of machines whose square commutes.

Commutative diagrams are the everyday language of category theory, where they state equations between composites of arrows (see categories). A famous example is the naturality square. Suppose a translation $\eta$ turns objects of one kind into objects of another, and $f$ is a change on the first side with a matching change $f'$ on the other side. Then $\eta$ is “natural” if translating and changing can be done in either order:

Our VAT square is an example in spirit: converting currency is natural with respect to adding a percentage, but not with respect to adding a fixed fee unless the fee is converted too. And the pasting theorem is used constantly: big diagrams are proved to commute by breaking them into small squares and triangles, each of which commutes.

• The idea that a calculation can be checked by doing it “downstairs”, with remainders, is old. Casting out nines was used by medieval arithmeticians writing in Arabic and explained by Leonardo of Pisa (Fibonacci) in Liber Abaci (1202).
• John Napier published his tables of logarithms in 1614, and the slide rule followed in the 1620s, with William Oughtred among its inventors. Both rest on a square that turns multiplication into addition.
• Diagrams of arrows that commute became a standard tool in algebraic topology in the 1940s and 1950s. Samuel Eilenberg and Saunders Mac Lane introduced categories in 1945, and Eilenberg and Norman Steenrod's book Foundations of Algebraic Topology (1952) used commutative diagrams throughout, helping to make them part of every mathematician's toolkit.

• F. William Lawvere and Stephen H. Schanuel, Conceptual Mathematics: A First Introduction to Categories (2nd edition, 2009) — diagrams of sets and maps from the first chapter, for beginners.
• Eugenia Cheng, How to Bake Pi: An Edible Exploration of the Mathematics of Mathematics (2015) — category theory for everyone.
• Eugenia Cheng, The Joy of Abstraction: An Exploration of Math, Category Theory, and Life (2022) — a longer, gentle introduction with many diagrams.
• David I. Spivak, Category Theory for the Sciences (2014) — diagrams as a modelling language.