Structure-preserving maps: homomorphisms and isomorphisms

Lens

MotivationH

Multiplying by adding

In 1614 the Scottish mathematician John Napier published tables of logarithms; the Swiss clockmaker Jost Bürgi published similar tables in 1620. Their purpose was practical. Astronomers, navigators and surveyors spent days multiplying long numbers by hand, and a logarithm table turned every multiplication into an addition:

\log(x \cdot y) = \log x + \log y.

To multiply $x$ by $y$ , look up $\log x$ and $\log y$ , add them, and look the sum up backwards. A slide rule does the same with two sliding logarithmic scales, and engineers used slide rules until pocket calculators replaced them in the 1970s.

A second, much older trick: to check $3847 \times 26 = 100\,022$ , add the digits. $3 + 8 + 4 + 7 = 22$ , and $2 + 2 = 4$ ; $2 + 6 = 8$ ; $4 \times 8 = 32$ , and $3 + 2 = 5$ . On the other side, $1 + 0 + 0 + 0 + 2 + 2 = 5$ . They agree, so the product passes the check. This is casting out nines, and it works because replacing a number by its digit sum does not change its remainder on division by $9$ .

Both tricks rest on the same idea: a map from one number world to another that respects the operations, so that you can do a calculation in whichever world is easier. Such maps are called homomorphisms, and they are among the most important ideas in mathematics.

IntuitionH

Translate, calculate, translate back

Imagine two worlds, each with its own way of combining things. A map $f$ from the first world to the second preserves the operation if these two routes always agree:

combine $x$ and $y$ in the first world, then translate the result with $f$ ;
translate $x$ and $y$ with $f$ first, then combine them in the second world.

For logarithms, route 1 is "multiply, then take the log" and route 2 is "take logs, then add". For casting out nines, route 1 is "multiply, then reduce mod $9$ " and route 2 is "reduce mod $9$ , then multiply".

DefinitionsH

Homomorphisms and isomorphisms

A binary operation on a set $A$ is a rule $\ast$ that combines any two elements $x, y \in A$ into an element $x \ast y \in A$ — like $+$ or $\times$ on numbers, or composition of symmetries.

Definition— operation-preserving map (homomorphism)

Let $\ast$ be an operation on $A$ and $\star$ an operation on $B$ . A function $f : A \to B$ preserves the operation, and is called a homomorphism from $(A, \ast)$ to $(B, \star)$ , if

f(x \ast y) = f(x) \star f(y) \qquad \text{for all } x, y \in A.

If a set carries several operations (such as $+$ and $\times$ ), a homomorphism must preserve each of them.

Combine then translate (top, then right) equals translate then combine (left, then bottom):

f(x \ast y) = f(x) \star f(y)

Structures can also be built from relations rather than operations: an order $\le$ , or the edges of a graph. For relations, "preserving" means that related inputs have related outputs.

Definition— order-preserving map; graph homomorphism

A function $f$ between ordered sets is order-preserving if $x \le y$ implies $f(x) \le f(y)$ . A graph homomorphism from a graph $G$ to a graph $H$ is a function from the vertices of $G$ to the vertices of $H$ that sends adjacent vertices to adjacent vertices.

Definition— isomorphism; isomorphic

An isomorphism is a structure-preserving bijection whose inverse is also structure-preserving. Two structures are isomorphic, written $A \cong B$ , if there is an isomorphism between them.

The clause about the inverse looks fussy. For operations it turns out to be automatic (Theorem 3); for relations it is not (Example after Theorem 3).

Worked examplesH

Worked examples and non-examples

Example— Reduction modulo n

Write $\Z/n$ for clock arithmetic with $n$ hours: the remainders $0, 1, \dots, n - 1$ , added and multiplied "mod $n$ ". The map $r : \Z \to \Z/n$ sending each integer to its remainder preserves both operations:

r(a + b) = r(a) + r(b), \qquad r(a \cdot b) = r(a) \cdot r(b) \qquad \text{(computed mod } n).

For instance with $n = 12$ : $r(17 + 20) = r(37) = 1$ , and $r(17) + r(20) = 5 + 8 = 13$ , which is $1$ mod $12$ . Reduction is not injective: $r(0) = r(12) = r(24) = 0$ . It forgets information — on purpose. Casting out nines is the case $n = 9$ , with the extra fact that a number and its digit sum have the same remainder mod $9$ (because $10 \equiv 1$ ).

Example— exp and ln

The exponential function satisfies $e^{x + y} = e^x e^y$ , so $\exp : (\R, +) \to (\R_{>0}, \times)$ is a homomorphism from the real numbers under addition to the positive real numbers under multiplication. It is a bijection, with inverse $\ln$ (see exponential and logarithmic functions), and $\ln(uv) = \ln u + \ln v$ says the inverse is also a homomorphism. So $\exp$ is an isomorphism: as far as their operations are concerned, $(\R, +)$ and $(\R_{>0}, \times)$ are the same structure. Under this dictionary, $0$ corresponds to $1$ , and the negative $-x$ to the reciprocal $1/e^x$ .

Example— Doubling

$d : \Z \to \Z$ , $d(x) = 2x$ , preserves addition: $2(x + y) = 2x + 2y$ . It is injective but not surjective; its image is the set $2\Z$ of even numbers. So $d$ is an isomorphism from $(\Z, +)$ to $(2\Z, +)$ — a structure isomorphic to a proper part of itself. But $d$ does not preserve multiplication: $d(3 \cdot 5) = 30$ , while $d(3) \cdot d(5) = 60$ . Preserving one operation says nothing about another.

Example— Signs

The sign map $\operatorname{sgn} : (\R \setminus \{0\}, \times) \to (\{1, -1\}, \times)$ , with $\operatorname{sgn}(x) = 1$ for $x > 0$ and $-1$ for $x < 0$ , preserves multiplication: this is the sign rule "negative times negative is positive" (proved in Integers) packaged as a homomorphism.

Example— Non-examples

$s(x) = x + 1$ on $(\Z, +)$ : $s(0 + 0) = 1$ , but $s(0) + s(0) = 2$ .
$q(x) = x^2$ on $(\R, +)$ : $q(1 + 1) = 4$ , but $q(1) + q(1) = 2$ . (On $(\R, \times)$ , however, $q$ is a homomorphism: $(xy)^2 = x^2 y^2$ .)
$g(x) = 3x + 1$ on $(\R, +)$ : $g(0 + 0) = 1 \ne 2 = g(0) + g(0)$ . Only the lines through the origin, $x \mapsto cx$ , preserve addition on $\R$ — the first glimpse of linear maps (linear algebra).

Example— Colourings are graph homomorphisms

Let $K_3$ be the triangle graph, with three vertices called red, green, blue, each adjacent to the other two. A graph homomorphism $G \to K_3$ sends adjacent vertices of $G$ to adjacent, hence different, colours. That is exactly a proper colouring of $G$ with three colours. So "can $G$ be 3-coloured?" is the question "is there a homomorphism $G \to K_3$ ?" — and indeed the Lean library Mathlib defines colourings this way.

Explore

First, reduction modulo $k$ . Colour every integer by its remainder, then add a member of one family to a member of another — again and again. The family of the sum depends only on the two families. That sentence is the statement that reduction mod $k$ preserves addition.

Remainder families

Colour each integer by its remainder after dividing by k. Every integer lands in exactly one family.

Divide by k = 3

−15−14−13−12−11−10−9−8−7−6−5−4−3−2−10123456789101112131415

[0]{ …, −15, −12, −9, −6, −3, 0, … }
[1]{ …, −14, −11, −8, −5, −2, 1, … }
[2]{ …, −13, −10, −7, −4, −1, 2, … }

Add a member of one family to a member of another…

Second, graph homomorphisms. Colour the vertices so that adjacent vertices get different colours. Each proper colouring with $k$ colours is a homomorphism to the complete graph $K_k$ . Which graphs have a homomorphism to $K_2$ , a single edge? Which need $K_4$ ?

A colouring is a homomorphism to a complete graph

Dots joined by lines: count degrees, walk along edges, colour vertices, grow spanning trees and count walks with a matrix.

Graph

|V| = 6|E| = 6Click a vertex to change its colour (Delete removes it).

colours used

clashes

uncoloured

Give every vertex a colour so that the two ends of each edge differ.

This graph is planar: it can be drawn with no edges crossing. The Four Colour Theorem says every planar graph can be coloured with at most four colours. Kenneth Appel and Wolfgang Haken proved it in 1976 with essential help from a computer, which checked well over a thousand cases; in 2005 Georges Gonthier completed a fully computer-checked proof in the Coq proof assistant.

Third, $\exp$ and $\ln$ . The two graphs are mirror images in the line $y = x$ , as the graphs of inverse functions always are. Under the isomorphism, $0 \mapsto 1$ (identity to identity) — find both points.

exp and ln undo each other

Move the sliders and trace along the curves to read off values.

y = eˣ
y = ln x
y = x

Trace along xx = 1

y = eˣ: y = 2.7183
y = ln x: y = 0
y = x: y = 1

ProofH

The theorems, with proofs

Theorem— Theorem 1 (composites and identities)

If $f : (A, \ast) \to (B, \star)$ and $g : (B, \star) \to (C, \bullet)$ are homomorphisms, then so is $g \circ f : (A, \ast) \to (C, \bullet)$ . Every identity map $\mathrm{id}_A : (A, \ast) \to (A, \ast)$ is a homomorphism.

Proof

For all $x, y \in A$ :

(g \circ f)(x \ast y) = g\big(f(x \ast y)\big) = g\big(f(x) \star f(y)\big) = g(f(x)) \bullet g(f(y)) = (g \circ f)(x) \bullet (g \circ f)(y),

using first that $f$ is a homomorphism, then that $g$ is. For the identity, both sides of $\mathrm{id}(x \ast y) = \mathrm{id}(x) \ast \mathrm{id}(y)$ equal $x \ast y$ .

∎

Theorem— Theorem 2 (homomorphisms of groups)

Let $A$ and $B$ be groups written additively (identity $0$ , inverse $-x$ ), and let $f : A \to B$ preserve addition. Then $f(0) = 0$ and $f(-x) = -f(x)$ for every $x$ .

Proof

$f(0) + f(0) = f(0 + 0) = f(0) = f(0) + 0$ . Adding $-f(0)$ on the left of both sides gives $f(0) = 0$ . Then $f(-x) + f(x) = f(-x + x) = f(0) = 0$ , so $f(-x)$ is the additive inverse of $f(x)$ ; inverses in a group are unique, so $f(-x) = -f(x)$ .

∎

So a map preserving the operation automatically preserves the identity and inverses. For $\exp$ this says $e^0 = 1$ and $e^{-x} = 1/e^x$ — consequences of $e^{x+y} = e^x e^y$ alone.

Theorem— Theorem 3 (inverses of bijective homomorphisms)

Let $f : (A, \ast) \to (B, \star)$ be a bijective homomorphism, with inverse $g : B \to A$ . Then $g$ is a homomorphism. Hence a bijective homomorphism of groups or rings — or of any sets with operations — is an isomorphism.

Proof

Let $u, v \in B$ . Since $f(g(u)) = u$ and $f(g(v)) = v$ ,

g(u \star v) = g\big(f(g(u)) \star f(g(v))\big) = g\big(f(g(u) \ast g(v))\big) = g(u) \ast g(v).

The second equality uses that $f$ is a homomorphism (read from right to left), the third that $g(f(a)) = a$ for every $a \in A$ . If there are several operations, apply the argument to each.

∎

For instance, $\ln(uv) = \ln u + \ln v$ follows from $e^{x + y} = e^x e^y$ by Theorem 3, without looking at how $\ln$ is defined.

Example— Counterexample: for relations the inverse can fail

Let $G$ be the graph with two vertices $a, b$ and no edge, and $H$ the graph with two vertices $a, b$ joined by an edge. The identity map on vertices, $G \to H$ , is a bijection, and it is a graph homomorphism (there are no edges in $G$ to check). Its inverse $H \to G$ is not a homomorphism: the edge $ab$ of $H$ goes to a non-edge of $G$ . So $G$ and $H$ are not isomorphic, although there is a structure-preserving bijection between them.

The same happens for orders (the Lean section uses $\{\text{false}, \text{true}\}$ with "only $x \le x$ " versus "false $\le$ true") and for spaces: the map $t \mapsto (\cos t, \sin t)$ from $[0, 2\pi)$ onto the circle is a continuous bijection whose inverse is not continuous — it tears the circle open at $(1, 0)$ .

This is why the definition of isomorphism demands a structure-preserving inverse. Next: what is an isomorphism good for?

Theorem— Theorem 4 (isomorphisms transfer structure)

Let $f : (A, \ast) \to (B, \star)$ be a surjective homomorphism.

If $\ast$ is commutative, so is $\star$ .
If $e$ is an identity for $\ast$ , then $f(e)$ is an identity for $\star$ .

If $f$ is an isomorphism, then moreover, for every $x \in A$ : $x \ast x = e$ if and only if $f(x) \star f(x) = f(e)$ ; so $A$ and $B$ have the same number of elements with $x \ast x = e$ .

Proof

Let $u, v \in B$ . By surjectivity $u = f(x)$ and $v = f(y)$ for some $x, y$ . Then $u \star v = f(x) \star f(y) = f(x \ast y) = f(y \ast x) = f(y) \star f(x) = v \star u$ .
With $u = f(x)$ : $f(e) \star u = f(e) \star f(x) = f(e \ast x) = f(x) = u$ , and similarly $u \star f(e) = u$ .

For the last part, $f(x) \star f(x) = f(x \ast x)$ , and since $f$ is injective, $f(x \ast x) = f(e)$ exactly when $x \ast x = e$ . So $f$ restricts to a bijection between the two sets of such elements.

∎

The same argument works for any property stated purely in terms of the operation: isomorphic structures share every structural property. This gives a powerful way to prove that two structures are not isomorphic: find a structural property that one has and the other lacks.

Example— Two groups of four elements that are not the same

Compare clock arithmetic $\Z/4 = \{0, 1, 2, 3\}$ under addition with the symmetries of a non-square rectangle: do nothing ( $e$ ), the half turn ( $h$ ), and the reflections in the horizontal and vertical axes ( $r$ , $s$ ), combined by doing one after the other. Each has four elements, and each is commutative. But in the rectangle group, every symmetry is undone by repeating it: $e \circ e = h \circ h = r \circ r = s \circ s = e$ . In $\Z/4$ only two elements satisfy $x + x = 0$ , namely $0$ and $2$ ; for instance $1 + 1 = 2 \ne 0$ . By Theorem 4 an isomorphism would preserve the number of such elements, so $\Z/4$ and the rectangle group are not isomorphic, even though they have the same size.

On the other hand, the rectangle group is isomorphic to $\Z/2 \times \Z/2$ (pairs of bits added coordinatewise), via $e \mapsto (0,0)$ , $h \mapsto (1,1)$ , $r \mapsto (1,0)$ , $s \mapsto (0,1)$ . And $\Z/4$ is isomorphic to $\{1, 2, 3, 4\}$ under multiplication mod $5$ , via $k \mapsto 2^k \bmod 5$ : $0 \mapsto 1$ , $1 \mapsto 2$ , $2 \mapsto 4$ , $3 \mapsto 3$ . That last one is a logarithm table for clock arithmetic — the two ideas of the motivation, in one example.

Finally, a counting theorem that uses everything so far. (It needs Euclid's lemma from divisibility and gcd.)

Theorem— Theorem 5 (homomorphisms between clocks)

The number of homomorphisms $(\Z/m, +) \to (\Z/n, +)$ is $\gcd(m, n)$ .

Proof

Let $f$ be a homomorphism and $a = f(1)$ . Every $k \in \Z/m$ is $1 + 1 + \cdots + 1$ ( $k$ times), so $f(k) = a + \cdots + a = ka$ (mod $n$ ): $f$ is determined by $a$ . Moreover, adding $1$ to itself $m$ times gives $0$ in $\Z/m$ , so $ma \equiv f(0) = 0 \pmod n$ by Theorem 2. That is, $n$ divides $ma$ .

Conversely, if $n \mid ma$ , define $f(k) = ka \bmod n$ for $k = 0, \dots, m - 1$ . For $k, l \in \Z/m$ the sum in $\Z/m$ is $k + l - \varepsilon m$ with $\varepsilon \in \{0, 1\}$ , so $f(k + l) \equiv (k + l)a - \varepsilon\, ma \equiv ka + la \pmod n$ , because $n \mid ma$ . So $f$ is a homomorphism. Homomorphisms therefore correspond to the values $a \in \{0, 1, \dots, n - 1\}$ with $n \mid ma$ .

Count them. Let $d = \gcd(m, n)$ , $m = dm'$ , $n = dn'$ , so $\gcd(m', n') = 1$ . Then $n \mid ma \iff n' \mid m'a \iff n' \mid a$ , the last step by Euclid's lemma. The multiples of $n'$ in $\{0, \dots, n - 1\}$ are $0, n', 2n', \dots, (d - 1)n'$ : there are exactly $d$ of them.

∎

For example, there are $\gcd(4, 6) = 2$ homomorphisms $\Z/4 \to \Z/6$ : $a = 0$ (everything to $0$ ) and $a = 3$ . And there are $\gcd(m, n) = 1$ — only the zero map — when $m$ and $n$ have no common factor.

Formal mathematicsF

Homomorphisms in Lean

We define "preserves the operation" directly, for any two operations on any two types:

PreservesOpLean 4Formally verified

/-- `PreservesOp f opA opB` says that `f : A → B` **preserves the operation**: combining first
and then mapping gives the same as mapping first and then combining,
`f (x ∗ y) = f x ⋆ f y` for all `x y`, where `∗` is `opA` and `⋆` is `opB`. -/
def PreservesOp {A : Type u} {B : Type v} (f : A → B) (opA : A → A → A) (opB : B → B → B) :
    Prop :=
  ∀ x y, f (opA x y) = opB (f x) (f y)

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

Theorems 1 and 3 are then short calc proofs that follow the human proofs line by line:

preservesOp_idLean 4Proved here from basic factsFormally verified

/-- The identity map preserves every operation: both sides are `x ∗ y`. -/
theorem preservesOp_id {A : Type u} (op : A → A → A) : PreservesOp id op op :=
  fun _ _ => rfl

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

compLean 4Proved here from basic factsFormally verified

/-- **Composites of homomorphisms are homomorphisms.** If `f` turns `∗` into `⋆` and `g` turns
`⋆` into `•`, then `g ∘ f` turns `∗` into `•`:
`g(f(x ∗ y)) = g(f x ⋆ f y) = g(f x) • g(f y)`. -/
theorem PreservesOp.comp {A : Type u} {B : Type v} {C : Type w}
    {opA : A → A → A} {opB : B → B → B} {opC : C → C → C} {f : A → B} {g : B → C}
    (hf : PreservesOp f opA opB) (hg : PreservesOp g opB opC) :
    PreservesOp (g ∘ f) opA opC := by
  intro x y
  calc (g ∘ f) (opA x y) = g (f (opA x y)) := rfl
    _ = g (opB (f x) (f y)) := by rw [hf]
    _ = opC (g (f x)) (g (f y)) := hg _ _

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

inverseLean 4Proved here from basic factsFormally verified

/-- **The inverse of a bijective homomorphism is a homomorphism.** Let `g` be a two-sided inverse
of `f` (`g (f x) = x` and `f (g u) = u`). For `u v` in `B`, write `u = f (g u)` and
`v = f (g v)`; then
`g (u ⋆ v) = g (f (g u) ⋆ f (g v)) = g (f (g u ∗ g v)) = g u ∗ g v`.
Nothing about groups is used: this holds for any binary operations. -/
theorem PreservesOp.inverse {A : Type u} {B : Type v} {opA : A → A → A} {opB : B → B → B}
    {f : A → B} {g : B → A} (hf : PreservesOp f opA opB)
    (hgf : Function.LeftInverse g f) (hfg : Function.RightInverse g f) :
    PreservesOp g opB opA := by
  intro u v
  calc g (opB u v) = g (opB (f (g u)) (f (g v))) := by rw [hfg u, hfg v]
    _ = g (f (opA (g u) (g v))) := by rw [hf]
    _ = opA (g u) (g v) := hgf _

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

Reduction modulo $n$ preserves both operations by two library facts about the map ℤ → ZMod n (Mathlib's name for $\Z/n$ ), and it is not injective:

reduce_addLean 4Applies a library theoremFormally verified

/-- Reduction modulo `n`, `ℤ → ℤ/n`, preserves addition. This is core Mathlib's `Int.cast_add`
(the map `ℤ → ZMod n` is the canonical "cast"). -/
theorem reduce_add (n : ℕ) : PreservesOp (fun a : ℤ => (a : ZMod n)) (· + ·) (· + ·) :=
  fun a b => Int.cast_add a b

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

reduce_mulLean 4Applies a library theoremFormally verified

/-- Reduction modulo `n` also preserves multiplication: Mathlib's `Int.cast_mul`. -/
theorem reduce_mul (n : ℕ) : PreservesOp (fun a : ℤ => (a : ZMod n)) (· * ·) (· * ·) :=
  fun a b => Int.cast_mul a b

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

reduce_not_injectiveLean 4Proved here from basic factsFormally verified

/-- …but for `n ≠ 0` it is **not injective**: `n` and `0` have the same remainder. So reduction
mod `n` is a homomorphism, not an isomorphism. -/
theorem reduce_not_injective (n : ℕ) (hn : n ≠ 0) :
    ¬ Function.Injective (fun a : ℤ => (a : ZMod n)) := by
  intro hinj
  have h : ((n : ℤ) : ZMod n) = ((0 : ℤ) : ZMod n) := by
    rw [Int.cast_natCast, ZMod.natCast_self, Int.cast_zero]
  have h' : (n : ℤ) = 0 := hinj h
  exact hn (by exact_mod_cast h')

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

Theorem 2, for additive groups, and part 1 of Theorem 4:

map_zero_of_preservesOpLean 4Proved here from basic factsFormally verified

/-- An addition-preserving map between additive groups sends `0` to `0`:
`f 0 + f 0 = f (0 + 0) = f 0 = f 0 + 0`, and cancelling `f 0` gives `f 0 = 0`.
(Mathlib: `map_zero` for bundled homomorphisms.) -/
theorem map_zero_of_preservesOp {A : Type u} {B : Type v} [AddGroup A] [AddGroup B] {f : A → B}
    (hf : PreservesOp f (· + ·) (· + ·)) : f 0 = 0 := by
  have h : f 0 + f 0 = f 0 + 0 :=
    calc f 0 + f 0 = f (0 + 0) := (hf 0 0).symm
      _ = f 0 := by rw [add_zero]
      _ = f 0 + 0 := (add_zero _).symm
  exact add_left_cancel h

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

map_neg_of_preservesOpLean 4Proved here from basic factsFormally verified

/-- …and it sends negatives to negatives: `f (-x) + f x = f (-x + x) = f 0 = 0`, so
`f (-x) = -f x`. (Mathlib: `map_neg`.) -/
theorem map_neg_of_preservesOp {A : Type u} {B : Type v} [AddGroup A] [AddGroup B] {f : A → B}
    (hf : PreservesOp f (· + ·) (· + ·)) (x : A) : f (-x) = -f x := by
  have h : f (-x) + f x = 0 :=
    calc f (-x) + f x = f (-x + x) := (hf (-x) x).symm
      _ = f 0 := by rw [neg_add_cancel]
      _ = 0 := map_zero_of_preservesOp hf
  exact eq_neg_of_add_eq_zero_left h

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

comm_of_surjectiveLean 4Proved here from basic factsFormally verified

/-- **Structure transfers along homomorphisms.** If `f` preserves the operation and is
surjective, and `∗` is commutative, then so is `⋆`: write `u = f x`, `v = f y`; then
`u ⋆ v = f (x ∗ y) = f (y ∗ x) = v ⋆ u`. In particular isomorphic structures are either both
commutative or both not. -/
theorem comm_of_surjective {A : Type u} {B : Type v} {opA : A → A → A} {opB : B → B → B}
    {f : A → B} (hf : PreservesOp f opA opB) (hsurj : Function.Surjective f)
    (hcomm : ∀ x y, opA x y = opA y x) : ∀ u v, opB u v = opB v u := by
  intro u v
  obtain ⟨x, rfl⟩ := hsurj u
  obtain ⟨y, rfl⟩ := hsurj v
  rw [← hf, ← hf, hcomm]

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

Now $\exp$ and $\ln$ . We build the positive reals as a subtype — the reals together with a proof of positivity — and show that $\ln(uv) = \ln u + \ln v$ follows from $e^{x+y} = e^x e^y$ via Theorem 3:

exp_preservesLean 4Applies a library theoremFormally verified

/-- `exp : (ℝ, +) → (ℝ, ×)` turns sums into products: Mathlib's `Real.exp_add`. -/
theorem exp_preserves : PreservesOp Real.exp (· + ·) (· * ·) :=
  Real.exp_add

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

posMulLean 4Formally verified

/-- The positive reals `ℝ>0`, as the subtype `{y : ℝ // 0 < y}`, with multiplication
(a product of positive numbers is positive, `mul_pos`). -/
def posMul (u v : {y : ℝ // 0 < y}) : {y : ℝ // 0 < y} :=
  ⟨u.1 * v.1, mul_pos u.2 v.2⟩

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

expPosLean 4Formally verified

/-- `exp` as a map `ℝ → ℝ>0` (its values are positive, `Real.exp_pos`). -/
noncomputable def expPos (x : ℝ) : {y : ℝ // 0 < y} :=
  ⟨Real.exp x, Real.exp_pos x⟩

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

logPosLean 4Formally verified

/-- `ln` as a map `ℝ>0 → ℝ`. -/
noncomputable def logPos (u : {y : ℝ // 0 < y}) : ℝ :=
  Real.log u.1

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

expPos_preservesLean 4Proved here from basic factsFormally verified

/-- `exp : (ℝ, +) → (ℝ>0, ×)` preserves the operations; two elements of a subtype are equal
when their values are (`Subtype.ext`), so this is `Real.exp_add` again. -/
theorem expPos_preserves : PreservesOp expPos (· + ·) posMul :=
  fun x y => Subtype.ext (Real.exp_add x y)

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

log_exp_inverseLean 4Proved here from basic factsFormally verified

/-- `ln` and `exp` are inverse to each other between `ℝ` and `ℝ>0`:
`ln (exp x) = x` (`Real.log_exp`) and `exp (ln u) = u` for `u > 0` (`Real.exp_log`). -/
theorem log_exp_inverse :
    Function.LeftInverse logPos expPos ∧ Function.RightInverse logPos expPos :=
  ⟨fun x => Real.log_exp x, fun u => Subtype.ext (Real.exp_log u.2)⟩

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

logPos_preservesLean 4Proved here from basic factsFormally verified

/-- **`ln (uv) = ln u + ln v`, for free.** `exp` is a bijective homomorphism, so by
`PreservesOp.inverse` its inverse `ln` is a homomorphism `(ℝ>0, ×) → (ℝ, +)`. We never touch
the definition of the logarithm. -/
theorem logPos_preserves : PreservesOp logPos posMul (· + ·) :=
  expPos_preserves.inverse log_exp_inverse.1 log_exp_inverse.2

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

Isomorphic or not? $\Z/4$ is not isomorphic to $\Z/2 \times \Z/2$ (the rectangle group in disguise), while $\Z/6 \cong \Z/2 \times \Z/3$ . The latter is checked case by case by decide, and Mathlib proves the general Chinese remainder theorem:

no_injective_hom_zmod4_kleinLean 4Proved here from basic factsFormally verified

/-- **Clock arithmetic mod 4 is not isomorphic to the Klein four-group** `ℤ/2 × ℤ/2` — not even
by an injective homomorphism. In `ℤ/2 × ℤ/2` every element satisfies `x + x = 0`. If `f`
preserved addition, then `f (1 + 1) = f 1 + f 1 = 0 = f 0 + f 0 = f (0 + 0)`, and injectivity
would give `1 + 1 = 0` in `ℤ/4`, which is false. -/
theorem no_injective_hom_zmod4_klein :
    ¬ ∃ f : ZMod 4 → ZMod 2 × ZMod 2, Function.Injective f ∧ PreservesOp f (· + ·) (· + ·) := by
  rintro ⟨f, hinj, hf⟩
  have hdouble : ∀ x : ZMod 2 × ZMod 2, x + x = 0 := by decide
  have h : f (1 + 1) = f (0 + 0) :=
    calc f (1 + 1) = f 1 + f 1 := hf 1 1
      _ = 0 := hdouble _
      _ = f 0 + f 0 := (hdouble _).symm
      _ = f (0 + 0) := (hf 0 0).symm
  exact absurd (hinj h) (by decide)

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

zmod4_not_iso_kleinLean 4Proved here from basic factsFormally verified

/-- The same fact for Mathlib's bundled isomorphisms of additive groups (`≃+`): there is no
`e : ZMod 4 ≃+ ZMod 2 × ZMod 2`, because `e` would be an injective homomorphism. -/
theorem zmod4_not_iso_klein (e : ZMod 4 ≃+ ZMod 2 × ZMod 2) : False :=
  no_injective_hom_zmod4_klein ⟨e, e.injective, fun x y => map_add e x y⟩

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

crt6Lean 4Formally verified

/-- The map `ℤ/6 → ℤ/2 × ℤ/3`, `x ↦ (x mod 2, x mod 3)`. (`ZMod.cast` reduces a residue
mod 6 to a residue mod 2 or mod 3; this is well defined because 2 and 3 divide 6.) -/
def crt6 (x : ZMod 6) : ZMod 2 × ZMod 3 :=
  (ZMod.cast x, ZMod.cast x)

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

crt6_isoLean 4Proved here from basic factsFormally verified

/-- **`ℤ/6 ≅ ℤ/2 × ℤ/3`**: `crt6` is a bijection and preserves addition and multiplication.
All three facts are finite checks over the 6 (or 36) cases, done by `decide`. -/
theorem crt6_iso :
    Function.Bijective crt6 ∧ PreservesOp crt6 (· + ·) (· + ·) ∧
      PreservesOp crt6 (· * ·) (· * ·) := by
  unfold PreservesOp
  decide

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

crt6LibraryLean 4Applies a library theoremFormally verified

/-- Mathlib's version: the **Chinese remainder theorem** `ZMod.chineseRemainder` gives a ring
isomorphism `ℤ/(mn) ≃+* ℤ/m × ℤ/n` whenever `m` and `n` are coprime. -/
def crt6Library : ZMod 6 ≃+* ZMod 2 × ZMod 3 :=
  ZMod.chineseRemainder (by decide : Nat.Coprime 2 3)

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

Relations, and the counterexample to "bijective homomorphisms are isomorphisms":

PreservesRelLean 4Formally verified

/-- For a **relation** (an order, the edges of a graph…), "preserving" means: related inputs have
related outputs, `r x y → s (f x) (f y)`. -/
def PreservesRel {A : Type u} {B : Type v} (f : A → B) (r : A → A → Prop) (s : B → B → Prop) :
    Prop :=
  ∀ x y, r x y → s (f x) (f y)

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

bijection_not_isoLean 4Proved here from basic factsFormally verified

/-- **A structure-preserving bijection whose inverse does not preserve structure.** On `Bool`,
compare the "discrete" order in which only `x ≤ x` holds (the relation `=`) with the usual order
`false ≤ true`. The identity map is a bijection and preserves order from the discrete order to
the usual one; but its inverse (the identity again, read backwards) sends `false ≤ true` to
`false = true`, which fails. So for relations, "bijective and preserving" does not imply
"isomorphism". -/
theorem bijection_not_iso :
    Function.Bijective (id : Bool → Bool) ∧ PreservesRel (id : Bool → Bool) (· = ·) (· ≤ ·) ∧
      ¬ PreservesRel (id : Bool → Bool) (· ≤ ·) (· = ·) := by
  refine ⟨Function.bijective_id, ?_, ?_⟩
  · intro x y h
    subst h
    exact le_refl x
  · intro h
    have hft : false = true := h false true (by decide)
    exact Bool.false_ne_true hft

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

coloring_is_homLean 4Applies a library theoremFormally verified

/-- In Mathlib, a **colouring** of a graph `G` with colours `α` is *defined* to be a graph
homomorphism from `G` to the complete graph on `α` (adjacent vertices must go to adjacent, that
is, different, colours). This holds by Mathlib's definition `SimpleGraph.Coloring`. -/
theorem coloring_is_hom {V : Type u} (G : SimpleGraph V) (α : Type v) :
    G.Coloring α = (G →g SimpleGraph.completeGraph α) :=
  rfl

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

ComputationC

Hunting homomorphisms by brute force

Hunting homomorphisms and isomorphisms by brute forcePythonExhaustive finite checkCounterexampleComputationally tested

"""Searching all maps between small structures for homomorphisms and isomorphisms.

A finite structure is a set with an operation table. We list every map
between two structures and keep those that preserve the operation. First,
additive maps Z/m -> Z/n for m, n <= 6: their number turns out to be
gcd(m, n). Second, we test every bijection between four 4-element groups -
clock arithmetic mod 4, the Klein four-group Z/2 x Z/2, the symmetries of a
non-square rectangle, and multiplication mod 5 on {1, 2, 3, 4} - and count
the isomorphisms. An invariant (how many x satisfy x * x = identity) explains
the zeros. Exhaustive search: complete for these structures, but the gcd
pattern for other m, n needs the lesson's proof.

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

from itertools import permutations, product
from math import gcd
import textwrap

def cyclic(n):
    """Z/n under addition: (elements, table) with table[(x, y)] = x + y mod n."""
    elems = list(range(n))
    return elems, {(x, y): (x + y) % n for x in elems for y in elems}

def klein():
    """Z/2 x Z/2 under componentwise addition mod 2."""
    elems = [(a, b) for a in (0, 1) for b in (0, 1)]
    table = {(x, y): ((x[0] + y[0]) % 2, (x[1] + y[1]) % 2)
             for x in elems for y in elems}
    return elems, table

def rectangle():
    """Symmetries of a non-square rectangle, as permutations of its corners.

    Corners 0, 1, 2, 3 go round the rectangle. The four symmetries are the
    identity, the half turn and the two mirror reflections; the operation
    is composition, (s * t)(c) = s(t(c)).
    """
    elems = [(0, 1, 2, 3), (2, 3, 0, 1), (1, 0, 3, 2), (3, 2, 1, 0)]
    table = {(s, t): tuple(s[t[c]] for c in range(4))
             for s in elems for t in elems}
    return elems, table

def units_mod5():
    """{1, 2, 3, 4} under multiplication mod 5."""
    elems = [1, 2, 3, 4]
    return elems, {(x, y): (x * y) % 5 for x in elems for y in elems}

def preserves(f, table_a, table_b):
    """True if f(x * y) = f(x) * f(y) for all x, y (f is a dict)."""
    return all(f[z] == table_b[(f[x], f[y])] for (x, y), z in table_a.items())

def homomorphisms(sa, sb):
    """Every operation-preserving map from structure sa to structure sb."""
    (ea, ta), (eb, tb) = sa, sb
    maps = (dict(zip(ea, values)) for values in product(eb, repeat=len(ea)))
    return [f for f in maps if preserves(f, ta, tb)]

def isomorphisms(sa, sb):
    """Every bijection sa -> sb that preserves the operation."""
    (ea, ta), (eb, tb) = sa, sb
    if len(ea) != len(eb):
        return []
    maps = (dict(zip(ea, perm)) for perm in permutations(eb))
    return [f for f in maps if preserves(f, ta, tb)]

def identity_element(s):
    """The element e with e * x = x * e = x for all x (None if there is none)."""
    elems, table = s
    for e in elems:
        if all(table[(e, x)] == x == table[(x, e)] for x in elems):
            return e
    return None

def squares_to_identity(s):
    """How many x satisfy x * x = e - a number every isomorphism preserves."""
    elems, table = s
    e = identity_element(s)
    return sum(1 for x in elems if table[(x, x)] == e)

def main():
    print("1. Additive maps Z/m -> Z/n, found by listing all n^m maps")
    print("   m\\n " + " ".join(f"{n:>3}" for n in range(1, 7)))
    agree = True
    for m in range(1, 7):
        row = [len(homomorphisms(cyclic(m), cyclic(n))) for n in range(1, 7)]
        agree &= row == [gcd(m, n) for n in range(1, 7)]
        print(f"   {m:>3} " + " ".join(f"{c:>3}" for c in row))
    print(f"   Every entry equals gcd(m, n): {agree}")
    print()
    groups = [("Z/4 (clock mod 4)", cyclic(4)), ("Z/2 x Z/2 (Klein)", klein()),
              ("rectangle symmetries", rectangle()),
              ("{1,2,3,4} times mod 5", units_mod5())]
    print("2. Isomorphisms among groups of order 4 (24 bijections tested each)")
    for i, (na, sa) in enumerate(groups):
        for nb, sb in groups[i + 1:]:
            print(f"   {na:<22} -> {nb:<22} {len(isomorphisms(sa, sb)):>2}")
    print()
    print("3. Invariant: number of x with x * x = identity")
    for name, s in groups:
        print(f"   {name:<22} {squares_to_identity(s)}")
    print()
    print(textwrap.fill(
        "Epistemic status: exhaustive-finite. Every map in each case was "
        "tested, so these counts are certain for these structures. That the "
        "number of homomorphisms Z/m -> Z/n is gcd(m, n) for all m and n is "
        "a pattern here, which the lesson then proves. The invariant in part 3 "
        "explains the zeros in part 2, since isomorphisms preserve it.",
        width=78,
    ))

if __name__ == "__main__":
    main()

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

The table is the experiment that suggests Theorem 5; the theorem's proof is what makes it true for every $m$ and $n$ . The zeros in part 2 are explained by the invariant in part 3, exactly as in Theorem 4. This is exhaustive-finite evidence: certain for these structures, silent about others.

Exercises

1. Structure-preserving maps: homomorphisms and isomorphisms

Warm-upHuman

Which of these maps $f : \Z \to \Z$ preserve addition, i.e. satisfy $f(x + y) = f(x) + f(y)$ for all $x, y$ ? (Choose all that apply.)

Choose all that apply

2. Structure-preserving maps: homomorphisms and isomorphisms

Warm-upHuman

Use reduction modulo $9$ without multiplying out: $47 \equiv 2$ and $85 \equiv 4 \pmod 9$ (digit sums $11 \to 2$ and $13 \to 4$ ). What is the remainder of $47 \times 85$ on division by $9$ ?

3. Structure-preserving maps: homomorphisms and isomorphisms

Warm-upHuman

$\exp : (\R, +) \to (\R_{>0}, \times)$ is an isomorphism. Under it, the additive inverse $-x$ of $x$ corresponds to which element of $\R_{>0}$ ?

Choose one

1/e^x

, the multiplicative inverse of

e^x

-e^x

e^{1/x}

0

4. Structure-preserving maps: homomorphisms and isomorphisms

CoreHuman

How many homomorphisms $(\Z/4, +) \to (\Z/6, +)$ are there?

5. Structure-preserving maps: homomorphisms and isomorphisms

CoreHuman

Why is $(\Z/4, +)$ not isomorphic to the symmetry group of a non-square rectangle?

Choose one

In the rectangle group every element

x

satisfies

x \circ x = e

; in

\Z/4

the element

1

has

1 + 1 = 2 \ne 0

. Isomorphisms preserve this property.They have different numbers of elements.

\Z/4

is commutative but the rectangle group is not.There is no bijection between them.

6. Structure-preserving maps: homomorphisms and isomorphisms

CoreHuman

In the proof of Theorem 3, $\; g(u \star v) \overset{(1)}{=} g\big(f(g(u)) \star f(g(v))\big) \overset{(2)}{=} g\big(f(g(u) \ast g(v))\big) \overset{(3)}{=} g(u) \ast g(v)$ . Which step uses that $f$ is a homomorphism?

Choose one

Step (2)Step (1)Step (3)No step — the proof only uses that

g

is the inverse of

f

7. Structure-preserving maps: homomorphisms and isomorphisms

StretchHuman

Which of these is a structure-preserving bijection whose inverse is not structure-preserving?

Choose one

The identity on vertices, from the graph with vertices

a, b

and no edge to the graph with vertices

a, b

and one edge

ab

\exp : (\R, +) \to (\R_{>0}, \times)

Reduction

\Z \to \Z/5

x \mapsto -x

(\Z, +)

8. Structure-preserving maps: homomorphisms and isomorphisms

CoreFormal

Which Lean proposition says that f : ℤ → ℤ preserves addition?

Choose one

∀ x y : ℤ, f (x + y) = f x + f y∀ x : ℤ, f (x + x) = f x + f x∃ x y : ℤ, f (x + y) = f x + f y∀ x y : ℤ, f x + f y = x + y

9. Structure-preserving maps: homomorphisms and isomorphisms

CoreComputational

Write preserves_addition(f, m, n), where f is a list of length m with f[k] in range(n), describing a map $\Z/m \to \Z/n$ . Return True if $f((x + y) \bmod m) = (f(x) + f(y)) \bmod n$ for all $x, y$ , else False. Then use it to count the homomorphisms $\Z/6 \to \Z/4$ (the tests do this for you).

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

10. Structure-preserving maps: homomorphisms and isomorphisms

StretchHuman

The map $\Z/6 \to \Z/2 \times \Z/3$ , $x \mapsto (x \bmod 2, \; x \bmod 3)$ is an isomorphism (of rings, even). Which $x \in \Z/6$ is sent to $(1, 2)$ ?

Choose one

x = 5

x = 3

x = 2

x = 1

Common misconceptionsH

Common misconceptions

Misconception

"Same number of elements, so isomorphic." $\Z/4$ and the symmetries of a non-square rectangle both have four elements, but they are not isomorphic: in the rectangle group every element is its own inverse, and in $\Z/4$ the element $1$ is not. Size is just one structural property among many.

Misconception

"Isomorphic means equal." Isomorphic structures can have entirely different elements — numbers and symmetries, sums and products. An isomorphism is a dictionary between them, and different dictionaries can exist (there are two isomorphisms $\Z/4 \to \{1, 2, 3, 4\}$ under multiplication mod $5$ ).

Misconception

"Every structure-preserving bijection has a structure-preserving inverse." True for operations (Theorem 3), false for relations: the bijection from the edgeless two-vertex graph to the one-edge graph preserves edges, but its inverse does not.

Misconception

"A homomorphism must be injective" (or surjective). Reduction mod $n$ is surjective but far from injective, and the zero map $x \mapsto 0$ is a homomorphism that is usually neither. A homomorphism only has to respect the operation. Losing information on purpose is what makes casting out nines quick.

Misconception

"Preserving one operation means preserving all of them." Doubling preserves addition but not multiplication; squaring preserves multiplication but not addition. For a ring, a homomorphism must preserve each operation separately.

ViewpointsH

The same idea, seen by others

Algebra— Kernels and the first isomorphism theorem

The kernel of a group homomorphism $f$ is the set of elements sent to the identity. For reduction $\Z \to \Z/n$ it is $n\Z$ , the multiples of $n$ . The kernel measures exactly what $f$ forgets: $f(x) = f(y)$ if and only if $x - y$ is in the kernel. The first isomorphism theorem says that the image of any group homomorphism is isomorphic to the domain "divided by" the kernel; for reduction, this is the statement that $\Z/n$ is $\Z$ with multiples of $n$ treated as zero. See algebraic structures and groups.

Geometry— Klein: geometry is what isomorphisms preserve

The structure-preserving bijections of the Euclidean plane are the isometries — maps preserving distance: translations, rotations, reflections and glide reflections. Two figures are congruent when an isometry carries one to the other, and Euclidean geometry studies exactly the properties that isometries preserve (length, angle, area). Felix Klein's Erlangen programme (1872) turned this into a definition: a geometry is a space together with a group of transformations, and its theorems are the statements invariant under that group. Allow all similarities and you get the geometry of shape without size; allow all projective maps and only properties such as incidence and cross-ratio survive. See transformation geometry.

Topology— Homeomorphisms

For spaces, the structure is nearness, the structure-preserving maps are the continuous maps, and the isomorphisms are the homeomorphisms: continuous bijections with continuous inverses. The map $t \mapsto (\cos t, \sin t)$ from $[0, 2\pi)$ to the circle is a continuous bijection but not a homeomorphism, and indeed an interval and a circle are not homeomorphic: removing a point from the inside of an interval disconnects it, while removing any one point of a circle leaves it connected. "A coffee mug is a doughnut" is a slogan for one homeomorphism. See point-set topology.

Number theory— The Chinese remainder theorem

The map $\Z/6 \to \Z/2 \times \Z/3$ , $x \mapsto (x \bmod 2, x \bmod 3)$ , is a ring isomorphism: knowing a number's remainders mod $2$ and mod $3$ is the same as knowing its remainder mod $6$ . More generally $\Z/mn \cong \Z/m \times \Z/n$ whenever $\gcd(m, n) = 1$ . The theorem is named after the Sunzi Suanjing (China, written between the 3rd and 5th centuries), which asks for a number leaving remainders $2, 3, 2$ on division by $3, 5, 7$ . It is the product of products by maps meeting the isomorphisms of this lesson.

Logic— Same sentences, different structures

If two structures are isomorphic, they satisfy exactly the same statements written in the language of their structure (first-order sentences). The converse fails: the ordered sets $(\Q, <)$ and $(\R, <)$ satisfy exactly the same first-order sentences about $<$ — both are dense linear orders without endpoints — but they are not isomorphic, because $\Q$ is countable and $\R$ is not (countability). Telling structures apart, and deciding which properties first-order logic can see, is the subject of model theory.

Computation— Is there an isomorphism? An algorithmic question

Deciding whether two graphs with $n$ vertices are isomorphic by trying all $n!$ bijections is hopeless already for $n = 30$ . Clever invariants (degree sequences, numbers of triangles, colour refinement) rule out most pairs quickly, but no invariant computable in polynomial time is known to separate all non-isomorphic graphs. In 2015 László Babai announced an algorithm running in quasi-polynomial time, $\exp\big((\log n)^{O(1)}\big)$ ; whether graph isomorphism can be decided in polynomial time remains open. See computational complexity.

Category-theoretic connectionH

Isomorphisms in a category

Groups with homomorphisms form a category; so do rings with ring homomorphisms, ordered sets with order-preserving maps, graphs with graph homomorphisms and spaces with continuous maps — Theorem 1 is precisely what makes each of these a category (see Composition). In any category, an isomorphism is an arrow $f : A \to B$ with an arrow $g : B \to A$ such that $g \circ f = \mathrm{id}_A$ and $f \circ g = \mathrm{id}_B$ .

This one definition gives the right notion everywhere: bijections for sets, group isomorphisms for groups, homeomorphisms for spaces. Theorem 3 says that in the category of groups, the isomorphisms are exactly the bijective arrows; the graph counterexample shows that in the category of graphs, being bijective is not enough. Category theory's lesson is to define "the same" by arrows, never by elements — which is also the lesson of products by maps.

Wonder Trails

Wonder Trail · Optional · never gradedInverses and structureEvery integer can be added to another integer to get

0

. So why can almost no integer be multiplied by another integer to get

1

?Follow the trail Wonder Trail · Optional · never gradedClock arithmeticIt's 9 o'clock. What time will it be in 5 hours — and in 29 hours? Can a clock teach us a whole new kind of arithmetic?Follow the trail

History & global context

History and global context

Remainder arithmetic is ancient. The Sunzi Suanjing (China, 3rd–5th century) solved simultaneous remainder problems; Indian astronomers including Āryabhaṭa (499) and Brahmagupta (628) developed methods (kuṭṭaka) for related problems. The check by nines was used by arithmeticians writing in Arabic and reached Europe in Fibonacci's Liber Abaci (1202).
Logarithms: John Napier (1614) and Jost Bürgi (1620) published the first tables; Henry Briggs's base-10 tables (1617, 1624) became standard for three centuries.
Isomorphism as a word for "the same group" appears in Camille Jordan's Traité des substitutions (1870). Felix Klein's Erlangen programme (1872) organised geometry by groups of structure-preserving transformations.
In the 1920s, Emmy Noether and her students in Göttingen made homomorphisms and the isomorphism theorems the backbone of algebra, an approach spread worldwide by Bartel van der Waerden's Moderne Algebra (1930–31).

Multiplying by adding

Translate, calculate, translate back

Homomorphisms and isomorphisms

Worked examples and non-examples

Explore

The theorems, with proofs

Homomorphisms in Lean

Hunting homomorphisms by brute force

Exercises

Common misconceptions

The same idea, seen by others

Isomorphisms in a category

Wonder Trails

History and global context

Further reading