Natural transformations · The Lumenary

Lens

MotivationH

Canonical, or just convenient?

Every finite-dimensional vector space $V$ over a field $k$ is isomorphic to its dual $V^* = \Hom(V, k)$ : both have dimension $n = \dim V$ . It is also isomorphic to its double dual $V^{**}$ . Yet working mathematicians treat these two isomorphisms completely differently. Nobody hesitates to identify $V$ with $V^{**}$ ; identifying $V$ with $V^*$ is regarded as a choice, made only when extra structure (an inner product, a basis) is around.

What is the difference? To write down $V \cong V^*$ you must choose something — a basis $e_1, \dots, e_n$ , giving $e_i \mapsto e_i^*$ — and a different basis gives a different isomorphism. The map $V \to V^{**}$ needs no choice at all:

\mathrm{ev}_V(v) = \big(\varphi \mapsto \varphi(v)\big).

It is defined by the same recipe for every vector space at once, and it is compatible with every linear map between them. In 1945 Samuel Eilenberg and Saunders Mac Lane turned this feeling into a definition, and the definition needed a whole new language: to say what "the same recipe for every space, compatible with all maps" means, they had to define categories and functors first. This lesson is about the notion they were really after — the natural transformation — and about the notion of "sameness" of categories it makes possible: equivalence.

IntuitionH

Morphisms between functors

A functor $F : \mathcal{C} \to \mathcal{D}$ draws a picture of $\mathcal{C}$ inside $\mathcal{D}$ : each object $A$ becomes $F(A)$ , each arrow $f : A \to B$ becomes $F(f) : F(A) \to F(B)$ . Given two such pictures $F$ and $G$ of the same category, a natural transformation $\alpha : F \Rightarrow G$ is a way of sliding the first picture onto the second: an arrow $\alpha_A : F(A) \to G(A)$ for each object $A$ , chosen so that sliding is compatible with every arrow of the picture. Compatibility is a single equation, drawn as a square:

The naturality square of

\alpha

f : A \to B

: going right then down equals going down then right,

G(f) \circ \alpha_A = \alpha_B \circ F(f)

Two slogans help, as long as you remember that they are slogans and the square is the definition.

Natural means uniform. A natural family cannot treat different objects by different ad hoc rules, because the arrows between objects force the components to agree. We will see that the only natural ways of turning a pair $(a, b)$ of elements of an arbitrary set $X$ into one element of $X$ are "take $a$ " and "take $b$ ": every other rule, such as "take the smaller one", needs extra structure on $X$ .
Natural means basis-free. In linear algebra, the arrows include all changes of basis. A natural construction cannot depend on a basis, because it must commute with every change of basis.

There is also a geometric picture, made precise in the topology viewpoint below: a natural transformation is to functors what a homotopy is to continuous maps — a continuous deformation of one into the other, through a "cylinder" $\mathcal{C} \times \{0 \to 1\}$ .

DefinitionsH

Definitions

Throughout, $\mathcal{C}$ , $\mathcal{D}$ , $\mathcal{E}$ are categories and composition is written $g \circ f$ (" $g$ after $f$ ").

Definition— natural transformation

Let $F, G : \mathcal{C} \to \mathcal{D}$ be functors. A natural transformation $\alpha : F \Rightarrow G$ is a family of morphisms of $\mathcal{D}$ , the components

\alpha_A : F(A) \to G(A) \qquad (A \text{ an object of } \mathcal{C}),

such that for every morphism $f : A \to B$ of $\mathcal{C}$ the naturality square commutes:

G(f) \circ \alpha_A = \alpha_B \circ F(f).

Definition— natural isomorphism

A natural transformation $\alpha : F \Rightarrow G$ is a natural isomorphism if every component $\alpha_A$ is an isomorphism in $\mathcal{D}$ . We then write $\alpha : F \cong G$ and say $F$ and $G$ are naturally isomorphic. A family of isomorphisms $F(A) \cong G(A)$ that is not natural is sometimes called "unnatural", and the phrase "naturally isomorphic" always refers to some pair of functors.

Definition— vertical composition and the functor category

If $\alpha : F \Rightarrow G$ and $\beta : G \Rightarrow H$ , their vertical composite $\beta \circ \alpha : F \Rightarrow H$ has components $(\beta \circ \alpha)_A = \beta_A \circ \alpha_A$ . The identity $1_F : F \Rightarrow F$ has components $\mathrm{id}_{F(A)}$ . When $\mathcal{C}$ is small, the functor category $[\mathcal{C}, \mathcal{D}]$ (also written $\mathcal{D}^{\mathcal{C}}$ ) has the functors $\mathcal{C} \to \mathcal{D}$ as objects and the natural transformations between them as morphisms.

Definition— whiskering

For $\alpha : F \Rightarrow G$ with $F, G : \mathcal{C} \to \mathcal{D}$ , and functors $K : \mathcal{B} \to \mathcal{C}$ , $H : \mathcal{D} \to \mathcal{E}$ , the whiskered transformations $\alpha K : FK \Rightarrow GK$ and $H\alpha : HF \Rightarrow HG$ have components $(\alpha K)_X = \alpha_{K(X)}$ and $(H\alpha)_A = H(\alpha_A)$ . Both are natural (apply $K$ to the arrow, or $H$ to the square).

Definition— full, faithful, essentially surjective

A functor $F : \mathcal{C} \to \mathcal{D}$ is faithful if each map $\Hom_{\mathcal{C}}(A, B) \to \Hom_{\mathcal{D}}(FA, FB)$ , $f \mapsto F(f)$ , is injective; full if each is surjective; fully faithful if each is bijective. It is essentially surjective if every object of $\mathcal{D}$ is isomorphic to $F(A)$ for some object $A$ of $\mathcal{C}$ .

Definition— equivalence of categories

An equivalence of categories is a functor $F : \mathcal{C} \to \mathcal{D}$ together with a functor $G : \mathcal{D} \to \mathcal{C}$ (a quasi-inverse) and natural isomorphisms

\eta : \mathrm{id}_{\mathcal{C}} \cong G \circ F, \qquad \varepsilon : F \circ G \cong \mathrm{id}_{\mathcal{D}}.

$\mathcal{C}$ and $\mathcal{D}$ are equivalent, $\mathcal{C} \simeq \mathcal{D}$ , if there is an equivalence between them. An isomorphism of categories is the stricter notion $G \circ F = \mathrm{id}$ and $F \circ G = \mathrm{id}$ on the nose.

Note

Equivalence is the right notion of sameness for categories precisely because it is phrased with isomorphisms instead of equalities of objects. Asking two objects of a category to be equal is almost never meaningful; asking them to be isomorphic is. Equivalence applies the same principle one level up.

Worked examplesH

Examples and non-examples

Example— The double dual

Let $\cat{Vect}_k$ be the category of vector spaces over $k$ and linear maps. The double dual is a covariant functor $(-)^{**} : \cat{Vect}_k \to \cat{Vect}_k$ : a linear map $f : V \to W$ gives $f^* : W^* \to V^*$ , $\varphi \mapsto \varphi \circ f$ , and then $f^{**} : V^{**} \to W^{**}$ , $\xi \mapsto \xi \circ f^*$ . The maps $\mathrm{ev}_V : V \to V^{**}$ form a natural transformation $\mathrm{ev} : \mathrm{id} \Rightarrow (-)^{**}$ : for $v \in V$ and $\varphi \in W^*$ ,

\big(f^{**} \circ \mathrm{ev}_V\big)(v)(\varphi) = \mathrm{ev}_V(v)\big(f^*\varphi\big) = (\varphi \circ f)(v) = \varphi(f v) = \mathrm{ev}_W(f v)(\varphi) = \big(\mathrm{ev}_W \circ f\big)(v)(\varphi).

On the full subcategory $\cat{FinVect}_k$ of finite-dimensional spaces every $\mathrm{ev}_V$ is an isomorphism, so $\mathrm{ev}$ is a natural isomorphism $\mathrm{id} \cong (-)^{**}$ there.

Example— The determinant, natural in the ring

Fix $n \ge 1$ . For a commutative ring $R$ , let $\mathrm{GL}_n(R)$ be the group of invertible $n \times n$ matrices over $R$ and $R^\times$ the group of units. Both are functors $\cat{CRing} \to \cat{Grp}$ : a ring homomorphism $\varphi : R \to S$ acts on matrices entrywise and on units by restriction. The determinant $\det_R : \mathrm{GL}_n(R) \to R^\times$ is a group homomorphism, and the naturality square says

\det_S\big(\varphi(M)\big) = \varphi\big(\det_R M\big) \qquad \text{for all } M \in \mathrm{GL}_n(R).

This holds because $\det M = \sum_{\sigma \in S_n} \operatorname{sgn}(\sigma) \prod_i M_{i, \sigma(i)}$ is a polynomial with integer coefficients in the entries, and $\varphi$ preserves sums, products and integers. So $\det : \mathrm{GL}_n \Rightarrow (-)^\times$ is natural. By contrast, "the trace of $M$ , as an element of $R^\times$ " is not even a family of maps $\mathrm{GL}_n(R) \to R^\times$ (the trace of an invertible matrix need not be a unit), and the trace $\mathrm{GL}_n(R) \to R$ is not a group homomorphism: naturality is a condition on families of morphisms in the target category.

Example— Equivariant maps are natural transformations

A group $G$ is a category $\mathbf{B}G$ with one object $\ast$ and one invertible arrow for each element of $G$ . A functor $X : \mathbf{B}G \to \cat{Set}$ is a set $X(\ast)$ with an action of $G$ , i.e. a $G$ -set. A natural transformation $\alpha : X \Rightarrow Y$ has one component $\alpha_\ast : X(\ast) \to Y(\ast)$ , and naturality at the arrow $g$ says $\alpha(g \cdot x) = g \cdot \alpha(x)$ : natural transformations between $G$ -sets are exactly the $G$ -equivariant maps. So the functor category $[\mathbf{B}G, \cat{Set}]$ is the category of $G$ -sets, and $[\mathbf{B}G, \cat{Vect}_k]$ is the category of linear representations of $G$ .

Example— Commutative squares are natural transformations

Let $\mathbf{2}$ be the category $0 \to 1$ with one non-identity arrow. A functor $\mathbf{2} \to \mathcal{D}$ is an arrow $u : D_0 \to D_1$ of $\mathcal{D}$ , and a natural transformation from $u$ to $u' : D'_0 \to D'_1$ is a pair $(a_0, a_1)$ with $u' \circ a_0 = a_1 \circ u$ — a commutative square. The functor category $[\mathbf{2}, \mathcal{D}]$ is the arrow category of $\mathcal{D}$ .

Example— Polymorphic functions

On $\cat{Set}$ , let $L(X)$ be the set of finite lists of elements of $X$ , with $L(f)$ applying $f$ to every entry. Reversal $\mathrm{rev}_X : L(X) \to L(X)$ is natural: relabelling the entries and then reversing gives the same list as reversing and then relabelling. So is $X \to L(X)$ , $x \mapsto [x, x]$ , and $L(X) \to L(X)$ , "drop the first entry". "Sort the list in increasing order" is not a natural transformation of $L$ : it is not even defined for an arbitrary set $X$ , since it needs an order on $X$ , and on $L(\Z)$ it fails to commute with $f(n) = -n$ .

Example— Abelianisation is natural; the centre is not even a functor

For a group $G$ let $G^{\mathrm{ab}} = G/[G, G]$ . A homomorphism $f : G \to H$ maps commutators to commutators, so it induces $f^{\mathrm{ab}}$ , and the quotient maps $q_G : G \to G^{\mathrm{ab}}$ satisfy $f^{\mathrm{ab}} \circ q_G = q_H \circ f$ : $q : \mathrm{id}_{\cat{Grp}} \Rightarrow (-)^{\mathrm{ab}}$ is natural. The centre $Z(G)$ looks just as canonical, but $G \mapsto Z(G)$ cannot be made into a functor $\cat{Grp} \to \cat{Grp}$ at all, whatever we try to do on morphisms: the composite $\Z/2 \hookrightarrow S_3 \twoheadrightarrow \Z/2$ (a transposition generates the first copy; the sign map is the second) is the identity, while $Z(\Z/2) = \Z/2$ and $Z(S_3) = 1$ , so a functor would have to factor $\mathrm{id}_{Z(\Z/2)} = Z(\mathrm{id})$ through the trivial group $Z(S_3)$ . (On the groupoid of groups and isomorphisms the centre is a functor, and the inclusions $Z(G) \hookrightarrow G$ are natural there: which arrows are allowed matters.)

Example— Non-example: a basis is not natural

Given a basis $e_1, \dots, e_n$ of $V$ , the dual basis gives an isomorphism $\theta_V : V \to V^*$ , $e_i \mapsto e_i^*$ . Already the shape of a naturality square is wrong: a linear map $f : V \to W$ gives $f^* : W^* \to V^*$ , pointing the other way, so there is no square $\theta_W \circ f \overset{?}{=} f^{\ast} \circ \theta_V$ to check. The best we can ask is $f^* \circ \theta_W \circ f = \theta_V$ , i.e. that $f$ preserves the bilinear form $\langle v, w \rangle = \theta_V(v)(w)$ . For the dot product on $k^n$ this holds only for orthogonal $f$ — 8 of the 48 invertible maps of $\mathbb{F}_3^2$ , as the computation below shows.

Example— Equivalent but not isomorphic

Let $\cat{Mat}_k$ be the category whose objects are the natural numbers, with $\Hom(m, n)$ the set of $n \times m$ matrices over $k$ and composition matrix multiplication. The functor $\cat{Mat}_k \to \cat{FinVect}_k$ , $n \mapsto k^n$ , $A \mapsto (x \mapsto Ax)$ , is an equivalence (proved below). The two categories are not isomorphic: $\cat{Mat}_k$ has one object of each dimension, $\cat{FinVect}_k$ has a proper class of them. In the same way, $\cat{FinSet}$ is equivalent to its full subcategory on the sets $\{1, \dots, n\}$ , and a nonempty category in which all objects are isomorphic and every object has only the identity as endomorphism is equivalent to the category $\mathbf{1}$ with one object and one arrow.

ProofH

Theorems and proofs

Theorem— Theorem 1 (the functor category)

For categories $\mathcal{C}$ and $\mathcal{D}$ , vertical composition of natural transformations is well defined, associative and unital, so functors $\mathcal{C} \to \mathcal{D}$ and natural transformations form a category $[\mathcal{C}, \mathcal{D}]$ . If $\mathcal{C}$ is small and $\mathcal{D}$ locally small, its hom-classes are sets.

Proof

Let $\alpha : F \Rightarrow G$ and $\beta : G \Rightarrow H$ , and $f : A \to B$ . Using naturality of $\beta$ and then of $\alpha$ ,

H(f) \circ (\beta_A \circ \alpha_A) = \beta_B \circ G(f) \circ \alpha_A = \beta_B \circ \alpha_B \circ F(f) = (\beta_B \circ \alpha_B) \circ F(f),

so $\beta \circ \alpha$ is natural. The identity components $\mathrm{id}_{F(A)}$ are natural because $F(f) \circ \mathrm{id} = \mathrm{id} \circ F(f)$ . Associativity and the unit laws hold componentwise, because they hold in $\mathcal{D}$ . If $\mathcal{C}$ is small and $\mathcal{D}$ locally small, the natural transformations $F \Rightarrow G$ are elements of the set $\prod_A \Hom_{\mathcal{D}}(FA, GA)$ , so they form a set.

∎

Theorem— Theorem 2 (natural isomorphisms are the isomorphisms of the functor category)

A natural transformation $\alpha : F \Rightarrow G$ is an isomorphism in $[\mathcal{C}, \mathcal{D}]$ if and only if every component $\alpha_A$ is an isomorphism in $\mathcal{D}$ .

Proof

If $\beta$ is inverse to $\alpha$ in the functor category, then componentwise $\beta_A \circ \alpha_A = \mathrm{id}$ and $\alpha_A \circ \beta_A = \mathrm{id}$ . Conversely, suppose each $\alpha_A$ is invertible and put $\beta_A = \alpha_A^{-1}$ . We must show that $\beta$ is natural: $F(f) \circ \beta_A = \beta_B \circ G(f)$ for $f : A \to B$ . Start from the naturality of $\alpha$ , $\alpha_B \circ F(f) = G(f) \circ \alpha_A$ , compose with $\beta_B$ on the left and with $\beta_A$ on the right:

F(f) \circ \beta_A = \beta_B \circ \alpha_B \circ F(f) \circ \beta_A = \beta_B \circ G(f) \circ \alpha_A \circ \beta_A = \beta_B \circ G(f).

The point is that inverses of components are automatically natural; nothing new must be checked.

∎

Theorem— Theorem 3 (naturality forces uniformity)

(a) Let $P : \cat{Set} \to \cat{Set}$ be the functor $P(X) = X \times X$ , $P(f) = f \times f$ . Every natural transformation $\alpha : P \Rightarrow \mathrm{id}_{\cat{Set}}$ is one of the two projections: either $\alpha_X(a, b) = a$ for all $X, a, b$ , or $\alpha_X(a, b) = b$ for all $X, a, b$ .

(b) The only natural transformation $\mathrm{id}_{\cat{Set}} \Rightarrow \mathrm{id}_{\cat{Set}}$ is the identity.

Proof

(a) Let $B = \{0, 1\}$ and let $c = \alpha_B(0, 1) \in B$ . Given any set $X$ and $(a, b) \in X \times X$ , let $f : B \to X$ be the function $f(0) = a$ , $f(1) = b$ . Then $P(f)(0, 1) = (a, b)$ , and naturality at $f$ gives

\alpha_X(a, b) = \alpha_X\big(P(f)(0, 1)\big) = f\big(\alpha_B(0, 1)\big) = f(c).

If $c = 0$ this is $a$ for every $X, a, b$ ; if $c = 1$ it is $b$ . Both projections are indeed natural, since $f \times f$ followed by a projection is the projection followed by $f$ .

(b) If $\alpha_X : X \to X$ is natural, take $x \in X$ and $f : \{\ast\} \to X$ with $f(\ast) = x$ . Naturality gives $\alpha_X(x) = \alpha_X(f(\ast)) = f(\alpha_{\{\ast\}}(\ast)) = f(\ast) = x$ .

∎

The proof used a single test object: a two-element set and one well-chosen element of $P(B)$ . This is the first appearance of the Yoneda lemma: $X \times X \cong \Hom(B, X)$ naturally in $X$ , and natural transformations out of $\Hom(B, -)$ correspond to elements of the target at $B$ .

Example— Natural endomorphisms of the identity on abelian groups

The same test-object argument computes the natural transformations $\alpha : \mathrm{id}_{\cat{Ab}} \Rightarrow \mathrm{id}_{\cat{Ab}}$ . Let $m = \alpha_\Z(1)$ . For an abelian group $A$ and $a \in A$ , the homomorphism $f : \Z \to A$ , $1 \mapsto a$ , gives $\alpha_A(a) = \alpha_A(f(1)) = f(\alpha_\Z(1)) = f(m) = m a$ . Conversely, multiplication by any $m \in \Z$ is natural. So these natural transformations are exactly "multiplication by $m$ ", $m \in \Z$ , and composition corresponds to multiplication of integers. On $\cat{Grp}$ the same argument shows $\alpha_G(g) = g^m$ ; but $g \mapsto g^m$ is a homomorphism for every group only when $m = 0$ or $m = 1$ (look at the free group on two letters), so the identity functor of $\cat{Grp}$ has just two natural endomorphisms.

Theorem— Theorem 4 (the double dual)

$\mathrm{ev} : \mathrm{id} \Rightarrow (-)^{**}$ is a natural transformation on $\cat{Vect}_k$ , and a natural isomorphism on $\cat{FinVect}_k$ .

Proof

Naturality is the calculation in the first example. For $\dim V = n < \infty$ : if $v \neq 0$ , extend $v$ to a basis and let $\varphi$ be the coordinate functional of $v$ ; then $\mathrm{ev}_V(v)(\varphi) = 1 \neq 0$ , so $\mathrm{ev}_V$ is injective. Since $\dim V^{**} = \dim V^* = n$ , an injective linear map $V \to V^{**}$ is bijective.

∎

For infinite-dimensional $V$ , $\mathrm{ev}_V$ is still injective (the same argument, extending to a basis using Zorn's lemma) but never surjective: by the Erdős–Kaplansky theorem, $\dim V^* > \dim V$ when $\dim V$ is infinite. So naturality and invertibility are different questions — $\mathrm{ev}$ is natural everywhere and invertible only in finite dimension.

Theorem— Theorem 5 (V is not naturally isomorphic to V*)

(a) The dual is a functor $(-)^* : \cat{Vect}_k^{\mathrm{op}} \to \cat{Vect}_k$ , while the identity is a functor $\cat{Vect}_k \to \cat{Vect}_k$ . A natural transformation requires two functors with the same domain and codomain, so " $\mathrm{id} \cong (-)^*$ " is not a meaningful statement.

(b) Restrict to the groupoid $\cat{Vect}_k^{\cong}$ of finite-dimensional spaces and linear isomorphisms, where $D(V) = V^*$ , $D(f) = (f^{-1})^*$ is a covariant functor. If $k$ has more than three elements, there is no natural isomorphism $\mathrm{id} \Rightarrow D$ on $\cat{Vect}_k^{\cong}$ — not even on its full subcategory of one-dimensional spaces.

Proof

(a) is a matter of types: $(-)^*$ reverses the direction of arrows, $\mathrm{id}$ does not.

(b) A natural $\theta : \mathrm{id} \Rightarrow D$ consists of linear maps $\theta_V : V \to V^*$ , i.e. bilinear forms $\langle v, w \rangle_V = \theta_V(v)(w)$ , with $(f^{-1})^* \circ \theta_V = \theta_W \circ f$ for every isomorphism $f : V \to W$ . Evaluating at $v$ and then at $f(w)$ gives

\langle f v, f w \rangle_W = \langle v, w \rangle_V .

Take $V = W = k$ and $f(x) = \lambda x$ for $\lambda \in k^\times$ . Every bilinear form on $k$ is $\langle v, w \rangle = c\, v w$ with $c = \langle 1, 1 \rangle$ , and invariance gives $c \lambda^2 = c$ . A field with more than three elements has some $\lambda \neq 0$ with $\lambda^2 \neq 1$ , because $\lambda^2 = 1$ has at most two roots $\pm 1$ . Then $c = 0$ , so $\theta_k = 0$ is not an isomorphism.

∎

Over $\mathbb{F}_2$ and $\mathbb{F}_3$ every unit satisfies $\lambda^2 = 1$ , and small exceptions really occur: on $\mathbb{F}_2^2$ the pairing $\langle v, w \rangle = v_1 w_2 + v_2 w_1 = \det(v \; w)$ is invariant under all of $\mathrm{GL}_2(\mathbb{F}_2)$ , because every invertible $2 \times 2$ matrix over $\mathbb{F}_2$ has determinant $1$ . The second computation below finds all such exceptions for small $p$ and $n$ . This is why careful statements of " $V \not\cong V^*$ naturally" specify both the morphisms and the field.

Theorem— Theorem 6 (characterisation of equivalences)

A functor $F : \mathcal{C} \to \mathcal{D}$ is part of an equivalence of categories if and only if it is full, faithful and essentially surjective. The "if" direction uses the axiom of choice (for a proper class of objects, a global form of it).

Proof

( $\Rightarrow$ ) Let $G$ , $\eta : \mathrm{id} \cong GF$ and $\varepsilon : FG \cong \mathrm{id}$ be as in the definition.

Faithful. For $f : A \to B$ , naturality of $\eta$ says $GF(f) \circ \eta_A = \eta_B \circ f$ , so $f = \eta_B^{-1} \circ GF(f) \circ \eta_A$ . Thus $f$ is determined by $F(f)$ : if $F(f) = F(g)$ then $f = g$ .

Essentially surjective. Every object $Y$ of $\mathcal{D}$ satisfies $Y \cong F(G(Y))$ , via $\varepsilon_Y^{-1}$ .

Full. By symmetry ( $F$ is a quasi-inverse of $G$ , with $\varepsilon^{-1} : \mathrm{id}_{\mathcal{D}} \cong FG$ ), $G$ is faithful too. Let $h : F(A) \to F(B)$ and put $f = \eta_B^{-1} \circ G(h) \circ \eta_A : A \to B$ . By naturality of $\eta$ ,

GF(f) = \eta_B \circ f \circ \eta_A^{-1} = \eta_B \circ \eta_B^{-1} \circ G(h) \circ \eta_A \circ \eta_A^{-1} = G(h),

and since $G$ is faithful, $F(f) = h$ .

( $\Leftarrow$ ) For each object $Y$ of $\mathcal{D}$ choose an object $G(Y)$ of $\mathcal{C}$ and an isomorphism $\varepsilon_Y : F(G(Y)) \to Y$ (possible by essential surjectivity and choice). For $h : Y \to Y'$ , the arrow $\varepsilon_{Y'}^{-1} \circ h \circ \varepsilon_Y : FG(Y) \to FG(Y')$ is $F$ of a unique arrow $G(Y) \to G(Y')$ , because $F$ is full and faithful; call it $G(h)$ . Uniqueness makes $G$ a functor: $F(G(h') \circ G(h)) = \varepsilon_{Y''}^{-1} h' \varepsilon_{Y'} \varepsilon_{Y'}^{-1} h \varepsilon_Y = F(G(h' h))$ , so $G(h') \circ G(h) = G(h' h)$ , and similarly for identities. By construction $\varepsilon_{Y'} \circ FG(h) = h \circ \varepsilon_Y$ , so $\varepsilon : FG \Rightarrow \mathrm{id}$ is a natural isomorphism.

For an object $A$ of $\mathcal{C}$ , let $\eta_A : A \to GF(A)$ be the unique arrow with $F(\eta_A) = \varepsilon_{F(A)}^{-1}$ . It is an isomorphism: if $\eta'_A$ is the unique arrow with $F(\eta'_A) = \varepsilon_{F(A)}$ , then $F(\eta'_A \circ \eta_A) = \mathrm{id} = F(\mathrm{id})$ , so $\eta'_A \circ \eta_A = \mathrm{id}$ by faithfulness, and likewise in the other order. Naturality of $\eta$ can be checked after applying the faithful functor $F$ : for $f : A \to B$ ,

F\big(GF(f) \circ \eta_A\big) = FGF(f) \circ \varepsilon_{FA}^{-1} = \varepsilon_{FB}^{-1} \circ F(f) = F\big(\eta_B \circ f\big),

where the middle step is naturality of $\varepsilon$ at $F(f)$ . Hence $\eta : \mathrm{id} \cong GF$ , and $F$ is an equivalence.

∎

Theorem— Corollary (linear algebra is matrix algebra)

For every field $k$ the functor $\cat{Mat}_k \to \cat{FinVect}_k$ , $n \mapsto k^n$ , is an equivalence of categories.

Proof

It is fully faithful because linear maps $k^m \to k^n$ correspond bijectively to $n \times m$ matrices, compatibly with composition. It is essentially surjective because a space of dimension $n$ has a basis, i.e. an isomorphism $k^n \cong V$ . Theorem 6 gives a quasi-inverse — which chooses a basis of every finite-dimensional space. That choice is exactly what a quasi-inverse costs, and exactly why basis-free linear algebra and matrix algebra are "the same subject" without being "the same thing".

∎

Formal mathematicsF

Natural transformations in Lean and Mathlib

Mathlib writes a natural transformation $\alpha : F \Rightarrow G$ as α : F ⟶ G — a morphism in the functor category C ⥤ D — with components α.app X and the field α.naturality. Composition is written in diagrammatic order: f ≫ g means "first f, then g", that is $g \circ f$ . So the naturality square $G(f) \circ \alpha_A = \alpha_B \circ F(f)$ appears as F.map f ≫ α.app B = α.app A ≫ G.map f.

Uniformity. First the functor $X \mapsto X \times X$ and Theorem 3, stated twice: once with plain functions (exactly the human proof, using ULift Bool as the two-element test object in the right universe) and once for Mathlib's bundled natural transformations.

sqLean 4Formally verified

/-- The **squaring functor** on types: `X ↦ X × X`, and a function `f : X → Y` acts on pairs
coordinatewise, `(a, b) ↦ (f a, f b)`. (In this Mathlib, morphisms in the category of types are
wrapped functions; `↾g` turns a function `g` into a morphism.) -/
def sq : Type u ⥤ Type u where
  obj X := X × X
  map f := ↾(Prod.map f f)

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

natural_sq_to_idLean 4Proved here from basic factsFormally verified

/-- **Every natural family of maps `X × X → X` is a projection.** Suppose `α X : X × X → X` is
given for every type `X`, and is natural: `α Y (f a, f b) = f (α X (a, b))` for every function
`f : X → Y`. Then either `α X (a, b) = a` for all `X, a, b`, or `α X (a, b) = b` for all.

Proof (as in the lesson). Look at one test case: the pair `(true, false)` in the two-element type
`B`. For any `X` and `(a, b)`, the function `f : B → X` with `f true = a`, `f false = b` sends
`(true, false)` to `(a, b)`, so naturality gives `α X (a, b) = f (α B (true, false))`. Hence the
whole family is decided by one value, `α B (true, false)`, which is `true` (projection to `a`) or
`false` (projection to `b`). `ULift` moves `Bool` into the universe `u`. -/
theorem natural_sq_to_id (α : ∀ X : Type u, X × X → X)
    (nat : ∀ (X Y : Type u) (f : X → Y) (p : X × X), α Y (f p.1, f p.2) = f (α X p)) :
    (∀ (X : Type u) (p : X × X), α X p = p.1) ∨ (∀ (X : Type u) (p : X × X), α X p = p.2) := by
  -- Every component is determined by the single value `α B (true, false)`.
  have key : ∀ (X : Type u) (p : X × X),
      α X p = (if (α (ULift.{u} Bool) (⟨true⟩, ⟨false⟩)).down then p.1 else p.2) := by
    intro X p
    have h := nat (ULift.{u} Bool) X (fun b => if b.down then p.1 else p.2) (⟨true⟩, ⟨false⟩)
    simpa using h
  rcases h : α (ULift.{u} Bool) (⟨true⟩, ⟨false⟩) with ⟨b⟩
  cases b
  · right
    intro X p
    rw [key, h]
    rfl
  · left
    intro X p
    rw [key, h]
    rfl

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

natTrans_sq_to_idLean 4Proved here from basic factsFormally verified

/-- The same theorem for Mathlib's bundled natural transformations: every `α : sq ⟶ 𝟭 (Type u)`
is the first or the second projection. The naturality square of `α` at `f`, applied to an
element (`NatTrans.naturality_apply`), is exactly the hypothesis of `natural_sq_to_id`. -/
theorem natTrans_sq_to_id (α : sq ⟶ 𝟭 (Type u)) :
    (∀ (X : Type u) (p : X × X), α.app X p = p.1) ∨
      (∀ (X : Type u) (p : X × X), α.app X p = p.2) := by
  apply natural_sq_to_id (fun X => α.app X)
  intro X Y f p
  exact NatTrans.naturality_apply α (↾f) p

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

natural_id_to_idLean 4Proved here from basic factsFormally verified

/-- **The identity functor on types has only the identity as natural endo-transformation.**
If `α X : X → X` is natural, then for `x : X` take `f : PUnit → X` with value `x`; naturality
says `α X (f ()) = f (α PUnit ())`, and the right side is `x` whatever `α PUnit ()` is. -/
theorem natural_id_to_id (α : ∀ X : Type u, X → X)
    (nat : ∀ (X Y : Type u) (f : X → Y) (x : X), α Y (f x) = f (α X x)) :
    ∀ (X : Type u) (x : X), α X x = x := by
  intro X x
  exact nat PUnit X (fun _ => x) PUnit.unit

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

natTrans_id_eqLean 4Proved here from basic factsFormally verified

/-- Bundled form: the only natural transformation `𝟭 (Type u) ⟶ 𝟭 (Type u)` is the identity
`𝟙 _`, i.e. the endomorphism monoid of the identity functor on types is trivial. -/
theorem natTrans_id_eq (α : 𝟭 (Type u) ⟶ 𝟭 (Type u)) : α = 𝟙 _ := by
  ext X x
  exact natural_id_to_id (fun X => α.app X)
    (fun X Y f x => by simpa using NatTrans.naturality_apply α (↾f) x) X x

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

List reversal, as a natural transformation of Mathlib's list functor:

reverseNatLean 4Formally verified

/-- **List reversal is a natural transformation** from the list functor to itself
(`ofTypeFunctor List` is Mathlib's functor `X ↦ List X`, acting on functions by `List.map`).
The naturality square says `reverse (map f xs) = map f (reverse xs)`: it does not matter whether
we relabel the entries before or after reversing. This is core Lean's `List.map_reverse`. -/
def reverseNat : ofTypeFunctor List ⟶ ofTypeFunctor List where
  app X := ↾List.reverse
  naturality X Y f := by
    ext xs
    exact (List.map_reverse ..).symm

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

Linear algebra. The double-dual square holds by computation — after applying both sides to v and φ, Lean sees φ (f v) on each side and accepts rfl. Bijectivity in finite dimension is Mathlib's theorem. Then Theorem 5(b), in the form "a line over a field with a unit $\lambda$ , $\lambda^2 \neq 1$ , carries no nonzero automorphism-invariant pairing".

double_dual_naturalityLean 4Proved here from basic factsFormally verified

/-- **The double-dual map is natural.** `Module.Dual.eval R V : V → V**` sends `v` to
"evaluate at `v`", `φ ↦ φ v`. For every linear `f : V → W` the square
`f** ∘ ev_V = ev_W ∘ f` commutes: both sides send `v` and `φ ∈ W*` to `φ (f v)`, since
`f** (ev_V v) φ = ev_V v (f* φ) = (φ ∘ f) v`. Lean checks the two sides agree by computation
(`rfl`) after applying both to `v` and `φ`; Mathlib states the same fact as
`Module.Dual.eval_naturality`. -/
theorem double_dual_naturality {V W : Type u} [AddCommGroup V] [Module R V] [AddCommGroup W]
    [Module R W] (f : V →ₗ[R] W) :
    f.dualMap.dualMap ∘ₗ Module.Dual.eval R V = Module.Dual.eval R W ∘ₗ f := by
  ext v φ
  rfl

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

double_dual_bijectiveLean 4Applies a library theoremFormally verified

/-- **In finite dimension the double-dual map is an isomorphism**, so `ev` is a natural
isomorphism from the identity functor to the double-dual functor on finite-dimensional spaces.
This applies Mathlib's `Module.bijective_dual_eval` (finite-dimensional spaces are reflexive).
Without finite dimension it fails: `ev` is still injective but no longer onto. -/
theorem double_dual_bijective {K V : Type u} [Field K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] : Function.Bijective (Module.Dual.eval K V) :=
  Module.bijective_dual_eval K V

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

no_invariant_pairingLean 4Proved here from basic factsFormally verified

/-- **A line has no automorphism-invariant pairing over a field with more than three elements.**
A natural isomorphism `V → V*` on the groupoid of vector spaces and linear isomorphisms would
give, for `V = K`, a linear map `φ : K → K*` with `φ (μ v) (μ w) = φ v w` for every unit `μ`
(see the lesson). If some unit `λ` has `λ² ≠ 1`, such a `φ` must be zero, so it is not an
isomorphism. Proof: by linearity `φ v w = v w · φ 1 1`; invariance under `λ` gives
`λ² · φ 1 1 = φ 1 1`, so `(λ² − 1) · φ 1 1 = 0` and `φ 1 1 = 0`. -/
theorem no_invariant_pairing {K : Type u} [Field K] (φ : K →ₗ[K] Module.Dual K K)
    (hφ : ∀ (μ : Kˣ) (v w : K), φ (μ * v) (μ * w) = φ v w) (lam : Kˣ) (hlam : lam ^ 2 ≠ 1) :
    φ = 0 := by
  -- Step 1: `φ` is determined by the number `φ 1 1`.
  have h1 : ∀ v w : K, φ v w = v * w * φ 1 1 := by
    intro v w
    have hv : φ v = v • φ 1 := by rw [← map_smul, smul_eq_mul, mul_one]
    rw [hv, LinearMap.smul_apply, smul_eq_mul]
    have hw : φ 1 w = w * φ 1 1 := by rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one]
    rw [hw, mul_assoc]
  -- Step 2: invariance under `λ` forces `φ 1 1 = 0`.
  have h2 : φ 1 1 = 0 := by
    have hinv := hφ lam 1 1
    rw [h1, h1, mul_one, one_mul, one_mul] at hinv
    have h3 : ((lam : K) * lam - 1) * φ 1 1 = 0 := by rw [sub_mul, hinv, one_mul, sub_self]
    rcases mul_eq_zero.mp h3 with h | h
    · exfalso
      apply hlam
      ext
      rw [Units.val_pow_eq_pow_val, pow_two, Units.val_one]
      exact sub_eq_zero.mp h
    · exact h
  refine LinearMap.ext fun v => LinearMap.ext fun w => ?_
  rw [h1, h2, mul_zero]
  rfl

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

The determinant as an honest natural transformation between functors CommRingCat ⥤ GrpCat:

glFunctorLean 4Formally verified

/-- The **general linear group functor** `GLₙ : CommRingCat ⥤ GrpCat`: a commutative ring `R`
goes to the group of invertible `n × n` matrices over `R`, and a ring homomorphism `f : R → S`
goes to the group homomorphism applying `f` to every entry (`Matrix.GeneralLinearGroup.map`). -/
noncomputable def glFunctor : CommRingCat.{u} ⥤ GrpCat.{u} where
  obj R := GrpCat.of (Matrix.GeneralLinearGroup n R)
  map f := GrpCat.ofHom (Matrix.GeneralLinearGroup.map f.hom)

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

unitsFunctorLean 4Formally verified

/-- The **units functor** `(−)ˣ : CommRingCat ⥤ GrpCat`: a ring goes to its group of units, a
ring homomorphism to its restriction to units (`Units.map`). -/
def unitsFunctor : CommRingCat.{u} ⥤ GrpCat.{u} where
  obj R := GrpCat.of Rˣ
  map f := GrpCat.ofHom (Units.map f.hom.toMonoidHom)

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

detNatLean 4Formally verified

/-- **The determinant is natural in the ring.** Its components are the group homomorphisms
`det : GLₙ(R) → Rˣ`; the naturality square for `f : R → S` says
`det (f(M)) = f (det M)`: applying `f` to the entries and then taking the determinant gives the
same as taking the determinant and then applying `f`, because the determinant is a polynomial
in the entries with integer coefficients. This is Mathlib's `Matrix.GeneralLinearGroup.map_det`. -/
noncomputable def detNat : glFunctor.{u} n ⟶ unitsFunctor.{u} where
  app R := GrpCat.ofHom Matrix.GeneralLinearGroup.det
  naturality R S f := by
    ext g
    exact Matrix.GeneralLinearGroup.map_det f.hom g

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

The functor category (Theorems 1 and 2) is built into Mathlib:

comp_appLean 4Applies a library theoremFormally verified

/-- **Vertical composition is computed componentwise.** In the functor category `C ⥤ D`
(Mathlib's instance `Functor.category`), the composite of `α : F ⟶ G` and `β : G ⟶ H` has
components `(α ≫ β).app X = α.app X ≫ β.app X`. This applies Mathlib's `NatTrans.comp_app`. -/
theorem comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
    (α ≫ β).app X = α.app X ≫ β.app X :=
  NatTrans.comp_app α β X

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

isIso_of_componentsLean 4Applies a library theoremFormally verified

/-- **A natural transformation whose components are isomorphisms is a natural isomorphism**:
it is invertible in the functor category, because the inverse components are automatically
natural. This applies Mathlib's `NatIso.isIso_of_isIso_app`. -/
theorem isIso_of_components {F G : C ⥤ D} (α : F ⟶ G) [∀ X : C, IsIso (α.app X)] : IsIso α :=
  NatIso.isIso_of_isIso_app α

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

Equivalences (Theorem 6). The three parts of ( $\Rightarrow$ ) are proved by hand, following the proof above; note how full_of_equivalence reuses faithful_of_unitIso for $G$ , exactly as the human proof says "by symmetry". The ( $\Leftarrow$ ) direction is Mathlib's Functor.asEquivalence, which uses choice (Functor.objPreimage).

faithful_of_unitIsoLean 4Proved here from basic factsFormally verified

/-- **A functor with a quasi-inverse is faithful.** If `η : 𝟭 C ≅ F ⋙ G`, then naturality of `η`
lets us recover every morphism `k : X ⟶ Y` from `F.map k`:
`k = η_X ≫ G.map (F.map k) ≫ η_Y⁻¹` (diagrammatic order: first `η_X`). So `F.map f = F.map g`
forces `f = g`. -/
theorem faithful_of_unitIso (F : C ⥤ D) (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) : F.Faithful where
  map_injective {X Y} {f g} h := by
    have key : ∀ k : X ⟶ Y, k = η.hom.app X ≫ G.map (F.map k) ≫ η.inv.app Y := by
      intro k
      calc k = k ≫ η.hom.app Y ≫ η.inv.app Y := by simp
        _ = (k ≫ η.hom.app Y) ≫ η.inv.app Y := by rw [Category.assoc]
        _ = (η.hom.app X ≫ G.map (F.map k)) ≫ η.inv.app Y := by
          rw [show k ≫ η.hom.app Y = η.hom.app X ≫ G.map (F.map k) from η.hom.naturality k]
        _ = η.hom.app X ≫ G.map (F.map k) ≫ η.inv.app Y := by rw [Category.assoc]
    rw [key f, key g, h]

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

essSurj_of_counitIsoLean 4Proved here from basic factsFormally verified

/-- **A functor with a quasi-inverse is essentially surjective**: every object `Y` of `D` is
isomorphic to `F (G Y)`, by the component `ε_Y` of `ε : G ⋙ F ≅ 𝟭 D`. -/
theorem essSurj_of_counitIso (F : C ⥤ D) (G : D ⥤ C) (ε : G ⋙ F ≅ 𝟭 D) : F.EssSurj where
  mem_essImage Y := ⟨G.obj Y, ⟨ε.app Y⟩⟩

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

full_of_equivalenceLean 4Proved here from basic factsFormally verified

/-- **A functor with a quasi-inverse is full.** Given `h : F X ⟶ F Y`, put
`f = η_X ≫ G.map h ≫ η_Y⁻¹ : X ⟶ Y`. Naturality of `η` gives `G.map (F.map f) = G.map h`, and
`G` is faithful (by `faithful_of_unitIso` applied to `G`, with `ε⁻¹ : 𝟭 D ≅ G ⋙ F`), so
`F.map f = h`. This is the proof in the lesson, step by step. -/
theorem full_of_equivalence (F : C ⥤ D) (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G)
    (ε : G ⋙ F ≅ 𝟭 D) : F.Full where
  map_surjective {X Y} h := by
    have hG : G.Faithful := faithful_of_unitIso G F ε.symm
    refine ⟨η.hom.app X ≫ G.map h ≫ η.inv.app Y, G.map_injective ?_⟩
    -- Naturality of `η` at `f`: `f ≫ η_Y = η_X ≫ G.map (F.map f)`.
    have hnat := η.hom.naturality (η.hom.app X ≫ G.map h ≫ η.inv.app Y)
    simp only [Functor.id_map, Functor.comp_map, Functor.id_obj] at hnat
    calc G.map (F.map (η.hom.app X ≫ G.map h ≫ η.inv.app Y))
        = η.inv.app X ≫ η.hom.app X ≫ G.map (F.map (η.hom.app X ≫ G.map h ≫ η.inv.app Y)) := by
          simp
      _ = η.inv.app X ≫ (η.hom.app X ≫ G.map h ≫ η.inv.app Y) ≫ η.hom.app Y := by rw [hnat]
      _ = G.map h := by simp

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

equivalence_iffLean 4Applies a library theoremFormally verified

/-- **Characterisation of equivalences.** A functor `F` has a quasi-inverse `G` (with natural
isomorphisms `𝟭 C ≅ F ⋙ G` and `G ⋙ F ≅ 𝟭 D`) if and only if it is full, faithful and
essentially surjective. (→) is `Functor.IsEquivalence.mk'` (the three lemmas above prove it by
hand). (←) is Mathlib's `Functor.asEquivalence`, which *chooses* for each object `Y` of `D` an
object `X` with `F X ≅ Y` — this direction uses the axiom of choice. -/
theorem equivalence_iff (F : C ⥤ D) :
    (∃ G : D ⥤ C, Nonempty (𝟭 C ≅ F ⋙ G) ∧ Nonempty (G ⋙ F ≅ 𝟭 D)) ↔
      F.Full ∧ F.Faithful ∧ F.EssSurj := by
  constructor
  · rintro ⟨G, ⟨η⟩, ⟨ε⟩⟩
    have := Functor.IsEquivalence.mk' G η ε
    exact ⟨inferInstance, inferInstance, inferInstance⟩
  · rintro ⟨h₁, h₂, h₃⟩
    have : F.IsEquivalence := {}
    exact ⟨F.inv, ⟨F.asEquivalence.unitIso⟩, ⟨F.asEquivalence.counitIso⟩⟩

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

Finally, equivalent need not mean isomorphic: two isomorphic objects form a category equivalent to the one-object category, but no isomorphism of categories exists.

codiscreteEquivalenceLean 4Formally verified

/-- **Two isomorphic objects are "the same" as one object.** `Codiscrete Bool` is the category
with two objects and exactly one morphism between any two (so the two objects are isomorphic);
`Codiscrete Unit` has one object and only its identity. Collapsing and picking an object are
quasi-inverse functors: any two functors into a codiscrete category are naturally isomorphic
(Mathlib's `Codiscrete.natIso`). -/
def codiscreteEquivalence : Codiscrete Bool ≌ Codiscrete Unit :=
  CategoryTheory.Equivalence.mk (Codiscrete.functorOfFun fun _ => ())
    (Codiscrete.functorOfFun fun _ => true) Codiscrete.natIso Codiscrete.natIso

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

codiscrete_not_isomorphicLean 4Proved here from basic factsFormally verified

/-- **Equivalent categories need not be isomorphic.** There are no functors
`F : Codiscrete Bool ⥤ Codiscrete Unit` and `G` back with `F ⋙ G = 𝟭` (on the nose): `F` would
have to be injective on objects, but it sends both objects to the only object. -/
theorem codiscrete_not_isomorphic :
    ¬ ∃ (F : Codiscrete Bool ⥤ Codiscrete Unit) (G : Codiscrete Unit ⥤ Codiscrete Bool),
      F ⋙ G = 𝟭 _ ∧ G ⋙ F = 𝟭 _ := by
  rintro ⟨F, G, h, -⟩
  have h1 : G.obj (F.obj ⟨true⟩) = ⟨true⟩ := congrArg (fun H => H.obj ⟨true⟩) h
  have h2 : G.obj (F.obj ⟨false⟩) = ⟨false⟩ := congrArg (fun H => H.obj ⟨false⟩) h
  have hU : ∀ a b : Codiscrete Unit, a = b := fun ⟨()⟩ ⟨()⟩ => rfl
  rw [hU (F.obj ⟨true⟩) (F.obj ⟨false⟩), h2] at h1
  exact Bool.false_ne_true (congrArg Codiscrete.as h1)

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

What is not formalised here: the equivalence $\cat{Mat}_k \simeq \cat{FinVect}_k$ , the failure of surjectivity of $\mathrm{ev}$ in infinite dimension, and Theorem 5(b) for the full groupoid (we formalise its key step, the computation on a line).

ComputationC

Experiments: symmetry is not naturality

Theorem 3 says that only the projections are natural maps $X \times X \to X$ . The first experiment searches all $16$ tables on a two-element set and all $3^9 = 19\,683$ tables on a three-element set. Asking only for compatibility with bijections — symmetry — leaves a third operation on $\{0, 1, 2\}$ : $(a, a) \mapsto a$ and $(a, b) \mapsto$ "the third element". Compatibility with all functions $X \to X$ rules it out, and the experiment prints a non-injective map whose square fails. Naturality is stronger than symmetry precisely because it must commute with maps that identify elements.

Natural binary operations on finite sets: symmetry versus naturalityPythonExhaustive finite checkCounterexampleComputationally tested

"""Which ways of combining two elements of a set work for every set at once?

A family of maps alpha_X : X x X -> X, one for each set X, is natural when
alpha_Y(f(a), f(b)) = f(alpha_X(a, b)) for every function f : X -> Y. The
lesson proves that the only natural families are the two projections. Here we
search exhaustively on the finite sets {0, 1} and {0, 1, 2}: first for tables
that commute with every bijection of the set (symmetry), then for tables that
commute with every function from the set to itself (a necessary condition for
naturality). Symmetry alone allows a third operation; the functions kill it,
and we print a square that fails.
"""

from itertools import permutations, product

def all_tables(n):
    """Every map n x n -> n, as a tuple t with t[a * n + b] = alpha(a, b)."""
    return product(range(n), repeat=n * n)

def all_maps(m, n):
    """Every function {0..m-1} -> {0..n-1}, as a tuple of values."""
    return list(product(range(n), repeat=m))

def commutes(t_src, t_dst, f, m, n):
    """Does the square for f : m -> n commute: t_dst(f a, f b) = f(t_src(a, b))?"""
    return all(t_dst[f[a] * n + f[b]] == f[t_src[a * m + b]]
               for a in range(m) for b in range(m))

def natural_tables(n, maps):
    """Tables on n commuting with every endomap in ``maps`` (an exhaustive search)."""
    return [t for t in all_tables(n)
            if all(commutes(t, t, f, n, n) for f in maps)]

def projection(n, k):
    """The k-th projection n x n -> n (k = 0: first, k = 1: second)."""
    return tuple((a, b)[k] for a in range(n) for b in range(n))

def third_element(t):
    """On {0, 1, 2}: is t the operation (a, a) -> a, (a, b) -> the third element?"""
    want = tuple(a if a == b else 3 - a - b for a in range(3) for b in range(3))
    return t == want

def breaking_square(t, n=3):
    """The first endomap f of {0..n-1} and pair (a, b) where the square fails,
    as (f, a, b, alpha(f a, f b), f(alpha(a, b))); None if t is natural."""
    for f in all_maps(n, n):
        for a in range(n):
            for b in range(n):
                lhs, rhs = t[f[a] * n + f[b]], f[t[a * n + b]]
                if lhs != rhs:
                    return f, a, b, lhs, rhs
    return None

def main():
    print("Tables alpha : X x X -> X, searched exhaustively.")
    for n in (2, 3):
        bij = [tuple(p) for p in permutations(range(n))]
        sym = natural_tables(n, bij)
        nat = natural_tables(n, all_maps(n, n))
        print(f"|X| = {n}: {n ** (n * n):>5} tables, {len(sym)} commute with all "
              f"{len(bij)} bijections, {len(nat)} with all {n ** n} self-maps")
    sym3 = natural_tables(3, [tuple(p) for p in permutations(range(3))])
    nat3 = natural_tables(3, all_maps(3, 3))
    projections = {projection(3, 0), projection(3, 1)}
    print(f"On 3 elements the natural tables are the projections: "
          f"{set(nat3) == projections}")
    extra = [t for t in sym3 if t not in projections]
    print(f"The symmetric extra table is 'the third element': "
          f"{len(extra) == 1 and third_element(extra[0])}")
    f, a, b, lhs, rhs = breaking_square(extra[0])
    print(f"Its square fails for f = {f} (i -> f[i]) at the pair ({a}, {b}):")
    print(f"  alpha(f({a}), f({b})) = alpha({f[a]}, {f[b]}) = {lhs},  but  "
          f"f(alpha({a}, {b})) = f({extra[0][a * 3 + b]}) = {rhs}.")
    print("f is not injective: symmetry alone cannot see this failure.")
    print()
    print("Epistemic status: an exhaustive search over all 16 and 19,683 tables on")
    print("sets of sizes 2 and 3 - complete for those sizes, silent about larger")
    print("sets. That only the projections are natural on all sets is proved in")
    print("the lesson (and in Lean), using one test pair in a two-element set.")

if __name__ == "__main__":
    main()

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

The second experiment studies Theorem 5(b) over small prime fields: it counts the non-degenerate bilinear forms on $\mathbb{F}_p^n$ that are invariant under every invertible matrix, and finds the exceptional cases over $\mathbb{F}_2$ and $\mathbb{F}_3$ that the theorem's hypothesis "more than three elements" leaves open.

Invariant pairings: when could V be naturally isomorphic to V*?PythonExact computationExhaustive finite checkComputationally tested

"""Is there a natural isomorphism V -> V*?  Small finite fields answer.

The dual space construction is contravariant, so "V is naturally isomorphic
to V*" cannot even be stated for all linear maps. On the groupoid of
isomorphisms it can be: a natural isomorphism amounts to a non-degenerate
bilinear form B on each space with B(gv, gw) = B(v, w) for every invertible g,
i.e. g^T B g = B. We count such forms on F_p^n for small p and n by exhaustive
search, testing invariance on a generating set of GL_n(F_p). We also count how
many invertible maps preserve the dot product, the pairing a basis gives.
"""

from itertools import product

def mat_mul(a, b, p):
    """Product of square matrices (tuples of row tuples) over F_p."""
    n = len(a)
    return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(n)) % p
                       for j in range(n)) for i in range(n))

def transpose(a):
    """The transpose of a square matrix."""
    return tuple(zip(*a))

def det(a, p):
    """Determinant over F_p by Laplace expansion (fine for n <= 3)."""
    n = len(a)
    if n == 1:
        return a[0][0] % p
    total = 0
    for j in range(n):
        minor = tuple(row[:j] + row[j + 1:] for row in a[1:])
        total += (-1) ** j * a[0][j] * det(minor, p)
    return total % p

def all_matrices(n, p):
    """Every n x n matrix over F_p."""
    for entries in product(range(p), repeat=n * n):
        yield tuple(tuple(entries[i * n:(i + 1) * n]) for i in range(n))

def primitive_root(p):
    """The least generator of the multiplicative group of F_p."""
    for g in range(1, p):
        if len({pow(g, k, p) for k in range(1, p)}) == p - 1:
            return g
    raise ValueError("p must be prime")

def gl_generators(n, p):
    """Transvections I + E_ij (i != j) and diag(g, 1, ..., 1), g a primitive
    root: a standard generating set of GL_n(F_p)."""
    ident = [[int(i == j) for j in range(n)] for i in range(n)]
    gens = []
    for i, j in product(range(n), repeat=2):
        if i != j:
            m = [row[:] for row in ident]
            m[i][j] = 1
            gens.append(tuple(map(tuple, m)))
    d = [row[:] for row in ident]
    d[0][0] = primitive_root(p)
    gens.append(tuple(map(tuple, d)))
    return gens

def invariant(b, g, p):
    """Is the bilinear form with Gram matrix b preserved by g: g^T b g = b?"""
    return mat_mul(mat_mul(transpose(g), b, p), g, p) == b

def invariant_forms(n, p):
    """Non-degenerate forms on F_p^n preserved by every element of GL_n(F_p)."""
    gens = gl_generators(n, p)
    return [b for b in all_matrices(n, p)
            if det(b, p) and all(invariant(b, g, p) for g in gens)]

def dot_preserving(n, p):
    """(number of invertible g with g^T g = I, size of GL_n(F_p))."""
    ident = tuple(tuple(int(i == j) for j in range(n)) for i in range(n))
    invertible = [g for g in all_matrices(n, p) if det(g, p)]
    keep = [g for g in invertible if invariant(ident, g, p)]
    return len(keep), len(invertible)

def main():
    print("Non-degenerate bilinear forms on F_p^n fixed by all of GL_n(F_p):")
    for p, n in [(2, 1), (2, 2), (2, 3), (3, 1), (3, 2), (5, 1), (5, 2)]:
        forms = invariant_forms(n, p)
        shown = " ".join(str([list(r) for r in b]) for b in forms) or "none"
        print(f"  p = {p}, n = {n}: {len(forms)}  {shown}")
    print("Over F_5 the scalar 2 has 2^2 = 4 != 1, so even a line has none;")
    print("on F_2^2 the survivor is the determinant pairing, as det(g) = 1.")
    print()
    print("The dot product (a basis-made pairing) is preserved only by")
    for p, n in [(2, 2), (3, 2), (5, 2)]:
        keep, total = dot_preserving(n, p)
        print(f"  {keep:>2} of the {total:>3} invertible maps of F_{p}^{n}")
    print()
    print("Epistemic status: exact, exhaustive computation for the listed p and n,")
    print("relying on the standard theorem that transvections and one diagonal")
    print("matrix generate GL_n(F_p). It proves nothing about other fields or")
    print("dimensions. The lesson proves that over every field with more than")
    print("three elements even a line has no invariant pairing, so V -> V* is")
    print("not natural even on the groupoid of isomorphisms.")

if __name__ == "__main__":
    main()

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

Explore

Explore: which pairings survive a change of basis?

A natural isomorphism $V \cong V^*$ on the groupoid would be a pairing preserved by every invertible linear map. Try the presets below on the plane $\R^2$ . A shear has determinant $1$ : it preserves area — the pairing $\det(v \; w)$ — but changes lengths and angles, so it does not preserve the dot product. So does the preset scaling (factors $2$ and $\tfrac12$ ). A rotation preserves both the dot product and the area; a reflection preserves the dot product but reverses the sign of the area. Finally edit the entries to the uniform scaling $\begin{pmatrix} 2 & 0 \\ 0 & 2 \end{pmatrix}$ : it multiplies every bilinear form by $4$ , so no non-zero pairing survives all invertible maps — the plane version of Theorem 5(b).

Invariant pairings under change of basis

Shears keep area, rotations keep the dot product, scalings keep neither.

Your own matrix

image of the grid
image of the unit square
image of the flag
before the transformation
invariant line

From the identity I to As = 1

A =

The columns of A are the images of e₁ = (1, 0) and e₂ = (0, 1): Ae₁ = (1, 0), Ae₂ = (1, 1)

det A = ad − bc = 1

The unit square (area 1) becomes a parallelogram of area |det A| = 1. Since det A > 0, orientation is preserved.

Invariant lines (real eigenvectors)

λ = 1, v = (1, 0)

Only one invariant line, with eigenvalue 1: there is no second eigenvector direction.

Exercises

1. Natural transformations

Warm-upHuman

Let $F, G : \mathcal{C} \to \mathcal{D}$ be functors and $\alpha_A : F(A) \to G(A)$ a family of morphisms. Which equation must hold for every $f : A \to B$ for $\alpha$ to be natural?

Choose one

G(f) \circ \alpha_A = \alpha_B \circ F(f)

F(f) \circ \alpha_A = \alpha_B \circ G(f)

\alpha_B \circ G(f) = G(f) \circ \alpha_A

\alpha_A = \alpha_B

whenever there is an arrow

A \to B

2. Natural transformations

CoreHuman

Let $T : \cat{Set} \to \cat{Set}$ be the functor $T(X) = X \times X \times X$ , $T(f) = f \times f \times f$ . How many natural transformations $T \Rightarrow \mathrm{id}_{\cat{Set}}$ are there?

3. Natural transformations

CoreHuman

Which of these families are natural transformations (between the functors indicated)? Select all that apply.

Choose all that apply

\mathrm{rev}_X : L(X) \to L(X)

, reversing a finite list (on

\cat{Set}

, with

L

the list functor)

X \to L(X)

x \mapsto [x, x]

(from

\mathrm{id}_{\cat{Set}}

L

)

q_G : G \to G/[G, G]

(from

\mathrm{id}_{\cat{Grp}}

to abelianisation)sorting a list of integers into increasing order, as a map

L(\Z) \to L(\Z)

“natural in the set of entries”

\det : \mathrm{GL}_n(R) \to R^\times

(from

\mathrm{GL}_n

(-)^\times

, functors

\cat{CRing} \to \cat{Grp}

)

4. Natural transformations

CoreHuman

Let $\alpha : \mathrm{id}_{\cat{Ab}} \Rightarrow \mathrm{id}_{\cat{Ab}}$ be a natural transformation with $\alpha_{\Z}(1) = 7$ . What is $\alpha_{\Z/12}(5)$ ? Give the representative in $\{0, 1, \dots, 11\}$ .

5. Natural transformations

CoreHuman

In the proof that an equivalence $F$ (with $\eta : \mathrm{id} \cong GF$ , $\varepsilon : FG \cong \mathrm{id}$ ) is full, we set $f = \eta_B^{-1} \circ G(h) \circ \eta_A$ for a given $h : F(A) \to F(B)$ and showed $GF(f) = G(h)$ . What is needed to conclude $F(f) = h$ ?

Choose one

That

G

is faithful, which follows from the same argument applied to

G

(using

\varepsilon^{-1}

)That

F

is faithfulThe axiom of choiceNothing:

GF(f) = G(h)

already means

F(f) = h

6. Natural transformations

StretchHuman

Which statement about $\mathrm{ev}_V : V \to V^{**}$ on the category of all vector spaces over a field $k$ is true?

Choose one

\mathrm{ev}

is natural, every component is injective, but for infinite-dimensional

V

it is not surjective

\mathrm{ev}

is a natural isomorphism on all vector spaces

\mathrm{ev}

is natural only on finite-dimensional spaces

\mathrm{ev}_V

fails to be injective for some infinite-dimensional

V

7. Natural transformations

CoreFormal

Mathlib writes composition in diagrammatic order: f ≫ g means “first f, then g”. For α : F ⟶ G between functors C ⥤ D and f : X ⟶ Y in C, which Lean statement is the naturality square?

Choose one

F.map f ≫ α.app Y = α.app X ≫ G.map fα.app Y ≫ F.map f = G.map f ≫ α.app XF.map f ≫ G.map f = α.app X ≫ α.app Yα.app X = α.app Y

8. Natural transformations

StretchHuman

Which pairs of categories are equivalent? Select all that apply.

Choose all that apply

\cat{FinVect}_{\R}

and

\cat{Mat}_{\R}

(objects

n \in \N

, morphisms matrices)

\cat{FinSet}

and its full subcategory on the sets

\{1, \dots, n\}

n \ge 0

\cat{Set}

and

\cat{Set}^{\mathrm{op}}

the category with two objects and exactly one arrow between any two objects, and the category

\mathbf{1}

\mathbf{B}\Z/2

and

\mathbf{B}\Z/3

(one-object categories of the groups)

9. Natural transformations

StretchComputational

A binary operation on $X = \{0, \dots, n-1\}$ is stored as a tuple t with t[a * n + b] $= \alpha(a, b)$ . Write natural_tables(n) returning the list of all such tables that commute with every function $f : X \to X$ , i.e. t[f[a] * n + f[b]] == f[t[a * n + b]] for all $a, b$ (with f a tuple of values). Theorem 3 predicts the answer.

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

Common misconceptionsH

Common misconceptions

Misconception

"Natural" means "obvious" or "canonical-looking". Naturality is a precise condition: a family of morphisms, indexed by objects, making every naturality square commute. Some canonical-looking maps are not natural (the inclusions of centres $Z(G) \hookrightarrow G$ are natural only for isomorphisms: $G \mapsto Z(G)$ is not even a functor on $\cat{Grp}$ ), and some natural transformations look surprising (the two projections are the only natural maps $X \times X \to X$ , but both are equally natural — naturality does not single out one).

Misconception

"Equivalent categories are isomorphic." An equivalence only requires $GF \cong \mathrm{id}$ and $FG \cong \mathrm{id}$ , up to natural isomorphism. $\cat{Mat}_k$ and $\cat{FinVect}_k$ are equivalent but not isomorphic; a category with two isomorphic objects (and one arrow between any two objects) is equivalent to the one-object category but has a different number of objects. Equivalence ignores exactly the information — how many copies of each isomorphism class — that categorical constructions cannot detect.

Misconception

"A natural transformation with injective (or bijective) components is all you need for an isomorphism of whatever you care about." The double-dual map is natural with injective components on all of $\cat{Vect}_k$ , but it is a natural isomorphism only on finite-dimensional spaces. Naturality and invertibility are independent requirements.

Misconception

"If each $F(A)$ is isomorphic to $G(A)$ , then $F \cong G$ ." Objectwise isomorphisms need not assemble into a natural one. On finite-dimensional spaces, $V \cong V^*$ for every $V$ , yet (Theorem 5) there is no natural isomorphism, even on the groupoid of isomorphisms over $\R$ . The isomorphisms must be chosen compatibly with all arrows.

ViewpointsH

Viewpoints

Topology— Natural transformations are homotopies

Let $\mathbf{2} = \{0 \to 1\}$ . A natural transformation $\alpha : F \Rightarrow G$ between functors $\mathcal{C} \to \mathcal{D}$ is the same thing as a functor $H : \mathcal{C} \times \mathbf{2} \to \mathcal{D}$ with $H(-, 0) = F$ and $H(-, 1) = G$ — compare a homotopy $X \times [0, 1] \to Y$ between maps $f$ and $g$ . This is more than an analogy: under the classifying-space construction (the geometric realisation of the nerve), $\mathbf{2}$ becomes the interval, and a natural transformation $F \Rightarrow G$ induces a homotopy $BF \simeq BG$ (Segal, 1968). In particular an equivalence of categories induces a homotopy equivalence of classifying spaces.

Historically the influence ran the other way. In algebraic topology homology is a functor, the connecting maps of the long exact sequence are natural, and the Hurewicz map $\pi_1(X, x) \to H_1(X)$ is natural. The universal coefficient theorem gives isomorphisms $H_n(X; G) \cong (H_n(X) \otimes G) \oplus \mathrm{Tor}(H_{n-1}(X), G)$ that split non-naturally: the short exact sequence behind them is natural in $X$ , but no splitting can be chosen naturally. Making such distinctions precise was exactly Eilenberg and Mac Lane's goal.

Geometry— Klein's principle and the musical isomorphism

Klein's Erlangen programme studies a geometry through the quantities invariant under its symmetry group. Naturality is the same idea with a groupoid (or a category) of symmetries: a construction is natural for a class of maps when it commutes with all of them. On a smooth manifold $M$ , the tangent bundle $TM$ and cotangent bundle $T^*M$ are both functorial (for diffeomorphisms), $T^{**}M \cong TM$ canonically, but an identification $TM \cong T^*M$ — the "musical isomorphism" $v \mapsto v^\flat = g(v, -)$ of Riemannian geometry — requires a metric $g$ , and it is natural only for isometries. This is Theorem 5 in geometric dress: a pairing is a geometric structure, and only the maps preserving it see the identification as natural.

The exceptional pairing on $\mathbb{F}_2^2$ is geometric too: $\det(v \; w)$ is the area form (a symplectic form), preserved exactly by the maps of determinant $1$ , $\mathrm{SL}_2 = \mathrm{Sp}_2$ . Over $\mathbb{F}_2$ every invertible matrix has determinant $1$ , so area is preserved by everything.

Algebra— Determinants, abelianisation and Morita equivalence

Algebra is full of natural transformations: the determinant $\mathrm{GL}_n \Rightarrow (-)^\times$ ; abelianisation $G \to G^{\mathrm{ab}}$ ; the canonical map $M \otimes_R N \to N \otimes_R M$ of modules; the inclusion of a module into its double dual. The test-object computation above shows that the natural endomorphisms of $\mathrm{id}_{\cat{Ab}}$ form the ring $\Z$ , and more generally the natural endomorphisms of the identity functor of $R\text{-}\cat{Mod}$ form the centre $Z(R)$ .

Equivalence of categories gives algebra a coarser and more useful notion of sameness for rings. Morita's theorem (Kiiti Morita, 1958): for every ring $R$ and $n \ge 1$ , the categories of left modules over $R$ and over the matrix ring $M_n(R)$ are equivalent, although the rings are not isomorphic. Properties that depend only on the module category — being semisimple, Noetherian, the centre, the lattice of two-sided ideals — are therefore shared by $R$ and $M_n(R)$ .

Computation— Theorems for free

In a typed functional language, a function of type ∀ a. List a → List a cannot inspect the elements it is given — it does not know their type — so it can only rearrange, copy or drop them by position. Reynolds' parametricity theorem (1983) makes this precise, and Wadler's "Theorems for free!" (1989) draws the consequence: every such function commutes with map f, i.e. it is a natural transformation of the list functor. A function of type ∀ a. (a, a) → a must be fst or snd — the programming counterpart of Theorem 3(a). The two statements have different hypotheses (parametricity is a property of the terms of a language, naturality a property of a family of maps), but they express the same uniformity, and the first computation above shows that symmetry alone is not enough to obtain it.

Category theory— A 2-category, and the Yoneda lemma

Categories, functors and natural transformations form a 2-category $\cat{Cat}$ : besides vertical composition, transformations $\alpha : F \Rightarrow G$ (for $F, G : \mathcal{C} \to \mathcal{D}$ ) and $\beta : H \Rightarrow K$ (for $H, K : \mathcal{D} \to \mathcal{E}$ ) have a horizontal composite $\beta \ast \alpha : HF \Rightarrow KG$ , $(\beta \ast \alpha)_A = \beta_{G A} \circ H(\alpha_A) = K(\alpha_A) \circ \beta_{F A}$ , and the two compositions satisfy the interchange law. Equivalence is the notion of isomorphism appropriate to a 2-category. The "test object" proofs above are instances of the Yoneda lemma: $\mathrm{Nat}(\Hom(A, -), F) \cong F(A)$ , so $\mathrm{Nat}(\Hom(\{0,1\}, -), \mathrm{id}) \cong \{0, 1\}$ has exactly two elements, the two projections. Natural transformations are also the raw material of adjunctions and limits: a cone is a natural transformation from a constant functor.

Wonder Trails

Wonder Trail · Optional · never gradedArrows that composeWhat do functions between sets, maps between groups and continuous maps between shapes have in common? What if we studied only the arrows?Follow the trail

History & global context

History and global context

Samuel Eilenberg (born in Warsaw, trained in the Polish school of topology) and Saunders Mac Lane (USA) began collaborating in the early 1940s on group extensions and their role in the homology of spaces (the groups now called $\mathrm{Ext}$ ). Their 1942 note "Natural isomorphisms in group theory" and their 1945 paper "General theory of natural equivalences" introduced categories, functors and natural transformations, with the double dual as a leading example. Mac Lane later wrote that "category" was defined in order to define "functor", and "functor" in order to define "natural transformation".
Dualities that are now read as equivalences of categories predate the language: Lev Pontryagin's duality for locally compact abelian groups (1934), Marshall Stone's representation of Boolean algebras by spaces (1936), and Israel Gelfand and Mark Naimark's theorem (1943) identifying commutative C*-algebras with algebras of functions on compact Hausdorff spaces.
In the 1950s equivalences became a working tool: Kiiti Morita (1958) characterised when module categories over two rings are equivalent, and Alexander Grothendieck's work in homological algebra and algebraic geometry made "up to equivalence" the default way to compare categories. Daniel Kan's 1958 paper on adjoint functors, the next lesson in this sequence, is built on natural transformations throughout.

Canonical, or just convenient?

Morphisms between functors

Definitions

Examples and non-examples

Theorems and proofs

Natural transformations in Lean and Mathlib

Experiments: symmetry is not naturality

Explore: which pairings survive a change of basis?

Exercises

Common misconceptions

Viewpoints

Wonder Trails

History and global context

Further reading