Functors · The Lumenary

Lens

MotivationH

How do you prove two things are different?

Are the groups $\Z/4$ and $\Z/2 \times \Z/2$ the same? Both have four elements, both are abelian. To show they are not isomorphic, checking that one particular bijection fails to be a homomorphism is not enough — we must rule out all $24$ bijections at once. Is the surface of a doughnut the same as the surface of a ball? Can a drum skin be continuously squashed onto its rim while every point of the rim stays where it is?

The common strategy is to find an invariant: something computable — a number, a set, a group — attached to each object in such a way that isomorphic objects get isomorphic invariants. Then different invariants prove that the objects are different.

A functor is an invariant done properly. It assigns to each object of one category an object of another, and — this is the crucial extra — to each morphism a morphism, compatibly with composition and identities. That compatibility is what makes isomorphic objects go to isomorphic objects, and, as we will see, it can prove much more than non-isomorphism: it can prove that certain maps cannot exist at all.

DefinitionsH

Definitions

Definition— functor

A functor $F : \cat{C} \to \cat{D}$ between categories assigns

to each object $A$ of $\cat{C}$ an object $F(A)$ of $\cat{D}$ , and
to each morphism $f : A \to B$ of $\cat{C}$ a morphism $F(f) : F(A) \to F(B)$ of $\cat{D}$ ,

such that $F(g \circ f) = F(g) \circ F(f)$ for all composable $f, g$ , and $F(\id_A) = \id_{F(A)}$ for all $A$ .

A functor carries every commuting triangle in

\mathcal{C}

to a commuting triangle in

\mathcal{D}

So a functor carries commutative diagrams to commutative diagrams. Functors compose: if $F : \cat{C} \to \cat{D}$ and $G : \cat{D} \to \cat{E}$ , then $G \circ F$ , defined by $(G \circ F)(A) = G(F(A))$ and $(G \circ F)(f) = G(F(f))$ , is a functor, because $G(F(g \circ f)) = G(F(g) \circ F(f)) = G(F(g)) \circ G(F(f))$ . Composition of functors is associative and the identity functors are neutral, so small categories and functors form a category, called $\cat{Cat}$ .

Definition— contravariant functor

A contravariant functor $F$ from $\cat{C}$ to $\cat{D}$ assigns to each object $A$ an object $F(A)$ and to each $f : A \to B$ a morphism $F(f) : F(B) \to F(A)$ in the opposite direction, with $F(g \circ f) = F(f) \circ F(g)$ and $F(\id_A) = \id_{F(A)}$ . Ordinary functors are then called covariant.

Theorem— Proposition (contravariant = functor out of the opposite)

A contravariant functor from $\cat{C}$ to $\cat{D}$ is the same thing as a (covariant) functor $\cat{C}^{\mathrm{op}} \to \cat{D}$ .

Proof

A morphism $f^{\mathrm{op}} : B \to A$ of $\cat{C}^{\mathrm{op}}$ is a morphism $f : A \to B$ of $\cat{C}$ , so in both cases the data are: an object $F(A)$ for each $A$ , and a morphism $F(B) \to F(A)$ for each $f : A \to B$ . The conditions agree too: composition in $\cat{C}^{\mathrm{op}}$ is $f^{\mathrm{op}} \circ g^{\mathrm{op}} = (g \circ f)^{\mathrm{op}}$ , so the covariant law $F(f^{\mathrm{op}} \circ g^{\mathrm{op}}) = F(f^{\mathrm{op}}) \circ F(g^{\mathrm{op}})$ says exactly $F(g \circ f) = F(f) \circ F(g)$ ; and identities of $\cat{C}^{\mathrm{op}}$ are those of $\cat{C}$ .

∎

Definition— hom functors

Let $\cat{C}$ be locally small and $A$ an object. The hom functor $\Hom(A, -) : \cat{C} \to \cat{Set}$ sends an object $B$ to the set $\Hom(A, B)$ and a morphism $f : B \to B'$ to the function "compose with $f$ ": $\Hom(A, f)(g) = f \circ g$ . The contravariant hom functor $\Hom(-, A) : \cat{C}^{\mathrm{op}} \to \cat{Set}$ sends $f : B' \to B$ to "precompose with $f$ ": $g \mapsto g \circ f$ .

Two adjectives are useful. A functor is faithful if each map $\Hom(A, B) \to \Hom(F(A), F(B))$ is injective, and full if each is surjective. Nothing in the definition of a functor requires either, nor injectivity on objects.

Worked examplesH

A gallery of functors

Example— The power set, two ways

Covariant. $\mathcal{P} : \cat{Set} \to \cat{Set}$ sends a set $X$ to its power set and $f : X \to Y$ to the direct-image map $\mathcal{P}(f)(S) = f(S) = \{ f(s) \mid s \in S \}$ . Check: $\mathcal{P}(\id)(S) = S$ , and $\mathcal{P}(g \circ f)(S) = \{ g(f(s)) \} = g(f(S)) = (\mathcal{P}(g) \circ \mathcal{P}(f))(S)$ .

Contravariant. $\mathcal{P}^\ast : \cat{Set}^{\mathrm{op}} \to \cat{Set}$ sends $X$ to its power set and $f : X \to Y$ to the preimage map $\mathcal{P}^\ast(f)(T) = f^{-1}(T)$ , which goes from subsets of $Y$ to subsets of $X$ . Check: $(g \circ f)^{-1}(T) = f^{-1}(g^{-1}(T))$ , so $\mathcal{P}^\ast(g \circ f) = \mathcal{P}^\ast(f) \circ \mathcal{P}^\ast(g)$ — the order reverses.

Preimages are better behaved than images: $f^{-1}$ preserves unions, intersections and complements, while $f(S \cap S')$ can be smaller than $f(S) \cap f(S')$ .

Example— Forgetful functors

$U : \cat{Grp} \to \cat{Set}$ sends a group to its underlying set and a homomorphism to its underlying function. The functor laws hold because composition and identities in $\cat{Grp}$ are composition and identities of functions. Likewise $\cat{Top} \to \cat{Set}$ , $\cat{Vect}_k \to \cat{Set}$ , $\cat{Ring} \to \cat{Grp}$ (keep only addition) and $\cat{Ring} \to \cat{Mon}$ (keep only multiplication). Forgetful functors are faithful but rarely full: not every function between groups is a homomorphism.

Example— Free functors

The free monoid. For a set $X$ , let $X^\ast$ be the set of finite words $x_1 x_2 \cdots x_k$ in the letters of $X$ , a monoid under concatenation with the empty word as unit. A function $f : X \to Y$ induces $f^\ast : X^\ast \to Y^\ast$ , "apply $f$ letter by letter": $f^\ast(x_1 \cdots x_k) = f(x_1) \cdots f(x_k)$ . It is a monoid homomorphism ( $f^\ast(vw) = f^\ast(v) f^\ast(w)$ ), and $(g \circ f)^\ast = g^\ast \circ f^\ast$ , $\id^\ast = \id$ . So $X \mapsto X^\ast$ is a functor $\cat{Set} \to \cat{Mon}$ . Why "free" is the right word is the subject of the lesson on universal properties.

The free vector space. For a set $X$ and a field $k$ , let $k[X]$ be the vector space of formal finite linear combinations $\sum_{x} a_x\, x$ (equivalently, functions $X \to k$ that vanish outside a finite set); $X$ is a basis. A function $f : X \to Y$ induces the linear map $k[f]\big(\sum a_x\, x\big) = \sum a_x\, f(x)$ — on basis vectors it is just $f$ . Then $k[g \circ f] = k[g] \circ k[f]$ because both agree on the basis. So $X \mapsto k[X]$ is a functor $\cat{Set} \to \cat{Vect}_k$ .

Example— Functors between small categories you already know

A functor between preorders regarded as categories is exactly a monotone map: it must send $x \le y$ (a morphism) to $F(x) \le F(y)$ ; the laws are automatic.
A functor between monoids regarded as one-object categories is exactly a monoid homomorphism: $F(y \circ x) = F(y) \circ F(x)$ says $F(yx) = F(y) F(x)$ , and $F(\id) = \id$ says $F(1) = 1$ . For instance $\det : \mathrm{GL}_n(\R) \to \R^{\times}$ .
A functor from a group $G$ (a one-object category) to $\cat{Set}$ is a set $X = F(\star)$ with a bijection $F(g) : X \to X$ for each $g$ , such that $F(gh) = F(g) \circ F(h)$ and $F(1) = \id$ : a group action of $G$ on $X$ .

Example— Functors from algebra and topology

Abelianisation. $G \mapsto G^{\mathrm{ab}} = G/[G, G]$ is a functor $\cat{Grp} \to \cat{Ab}$ : a homomorphism $f$ sends commutators to commutators, so it induces $G^{\mathrm{ab}} \to H^{\mathrm{ab}}$ .
Units. $R \mapsto R^{\times}$ is a functor $\cat{Ring} \to \cat{Grp}$ : a ring homomorphism preserving $1$ sends units to units.
The fundamental group. $\pi_1$ is a functor from pointed spaces $(X, x_0)$ and base-point-preserving continuous maps to groups: a map $f$ sends a loop $\gamma$ at $x_0$ to the loop $f \circ \gamma$ at $f(x_0)$ , and $\pi_1(f)[\gamma] = [f \circ \gamma]$ is a homomorphism with $\pi_1(g \circ f) = \pi_1(g) \circ \pi_1(f)$ — see the fundamental group. Homology groups are functors in the same way.

Example— A non-example: the centre

Sending a group $G$ to its centre $Z(G) = \{ z \mid zg = gz \text{ for all } g \}$ is a perfectly good assignment on objects, but there is no way to make it a functor by restricting homomorphisms. Let $f : \Z/2 \to S_3$ send the generator to the transposition $(1\,2)$ . Then $Z(\Z/2) = \Z/2$ , but $Z(S_3)$ is trivial, and $f$ maps the non-identity element of the centre outside the centre. The restriction of $f$ is not a map $Z(\Z/2) \to Z(S_3)$ at all.

ProofH

Functoriality proves impossibility

Theorem— Theorem 1 (functors preserve isomorphisms)

If $f : A \to B$ is an isomorphism in $\cat{C}$ and $F : \cat{C} \to \cat{D}$ is a functor, then $F(f)$ is an isomorphism, with inverse $F(f^{-1})$ . Consequently, if $A \cong B$ then $F(A) \cong F(B)$ .

Proof

$F(f^{-1}) \circ F(f) = F(f^{-1} \circ f) = F(\id_A) = \id_{F(A)}$ , and similarly $F(f) \circ F(f^{-1}) = F(\id_B) = \id_{F(B)}$ .

∎

Read contrapositively: if $F(A) \not\cong F(B)$ for some functor $F$ , then $A \not\cong B$ . That is how invariants work. (For a contravariant functor the same proof applies in $\cat{C}^{\mathrm{op}}$ .)

Example— Z/4 is not Z/2 × Z/2

Apply the hom functor $\Hom(\Z/2, -) : \cat{Grp} \to \cat{Set}$ . A homomorphism $\Z/2 \to G$ is determined by the image $g$ of the generator, which can be any element with $g^2 = e$ . So $|\Hom(\Z/2, G)| = \#\{ g \in G \mid g^2 = e \}$ . For $\Z/4$ this is $2$ (the elements $0, 2$ ); for $\Z/2 \times \Z/2$ it is $4$ . Isomorphic groups would give sets of the same size (bijections are the isomorphisms of $\cat{Set}$ ), so $\Z/4 \not\cong \Z/2 \times \Z/2$ . No bijection had to be checked.

Example— Z[i] is not Z[√2]

Apply the units functor $R \mapsto R^{\times}$ . In the Gaussian integers $\Z[i]$ , $u = a + bi$ is a unit only if $|u|^2 = a^2 + b^2 = 1$ (because $|u|^2|u^{-1}|^2 = 1$ with both factors positive integers), so $\Z[i]^{\times} = \{\pm 1, \pm i\}$ is cyclic of order $4$ . In $\Z[\sqrt 2]$ , $(1 + \sqrt 2)(-1 + \sqrt 2) = 1$ , so $1 + \sqrt 2$ is a unit, and its powers $(1 + \sqrt 2)^n$ are all different (they grow without bound), so $\Z[\sqrt 2]^{\times}$ is infinite. Hence the rings are not isomorphic — even though both are free abelian groups of rank $2$ under addition.

The next theorem shows functoriality doing more than distinguishing objects. A retraction of $i : S \to D$ is a morphism $r : D \to S$ with $r \circ i = \id_S$ .

Theorem— Theorem 2 (functors preserve retractions)

If $r \circ i = \id_S$ , then $F(r) \circ F(i) = \id_{F(S)}$ for every functor $F$ . In particular, if $F$ takes values in $\cat{Set}$ , then $F(i)$ is injective; if $F$ takes values in $\cat{Grp}$ , then $F(i)$ is an injective homomorphism and $F(S)$ is isomorphic to a subgroup of $F(D)$ .

Proof

$F(r) \circ F(i) = F(r \circ i) = F(\id_S) = \id_{F(S)}$ . A function (or homomorphism) with a left inverse is injective: if $F(i)(a) = F(i)(b)$ then $a = F(r)(F(i)(a)) = F(r)(F(i)(b)) = b$ .

∎

Theorem— Theorem 3 (no retraction of the disc onto its boundary)

Let $D^2 = \{ x \in \R^2 \mid |x| \le 1 \}$ and $S^1 = \{ x \mid |x| = 1 \}$ , with inclusion $i : S^1 \to D^2$ . There is no continuous map $r : D^2 \to S^1$ with $r(x) = x$ for all $x \in S^1$ .

Proof

We use two facts proved in the lesson on the fundamental group: $\pi_1(D^2, p)$ is trivial (every loop in the convex set $D^2$ shrinks to a point along straight lines), and $\pi_1(S^1, p) \cong \Z$ (loops are classified by their winding number). Fix $p \in S^1$ . A retraction $r$ would satisfy $r \circ i = \id_{S^1}$ as maps of pointed spaces, since $r(p) = p$ . By Theorem 2, $\pi_1(i) : \pi_1(S^1, p) \to \pi_1(D^2, p)$ would be injective. But it is a map from a group isomorphic to $\Z$ into the trivial group, which is not injective. Contradiction.

∎

Theorem— Corollary (Brouwer's fixed-point theorem, dimension 2)

Every continuous map $f : D^2 \to D^2$ has a fixed point.

Proof

Sketch. Suppose $f(x) \neq x$ for all $x$ . For each $x$ , follow the ray that starts at $f(x)$ and passes through $x$ until it meets $S^1$ , and call that point $r(x)$ . If $x \in S^1$ , then $r(x) = x$ . Solving the quadratic equation for where the ray meets the circle gives an explicit formula for $r(x)$ that depends continuously on $x$ and $f(x)$ , so $r$ is a continuous retraction of $D^2$ onto $S^1$ , contradicting Theorem 3. (The details of the continuity are in Hatcher, Algebraic Topology, §1.1.)

∎

Notice the shape of the argument: a question about continuous maps (hard: there are uncountably many) became a question about group homomorphisms $\Z \to 0 \to \Z$ (easy: there is only one). That is the purpose of functors in algebraic topology — and, as Eilenberg and Mac Lane realised, the reason category theory was invented.

Theorem— Theorem 4 (functors need not reflect isomorphisms)

There are functors $F$ and morphisms $f$ such that $F(f)$ is an isomorphism but $f$ is not.

Proof

(i) In the category $\mathbf{2}$ (the poset $0 < 1$ ), the morphism $0 \to 1$ is not an isomorphism, since there is no morphism $1 \to 0$ . The functor from $\mathbf{2}$ to $\cat{Set}$ sending both objects to a one-element set and every morphism to the identity is a functor, and it sends $0 \to 1$ to an isomorphism. (ii) A natural example: the forgetful functor $\cat{Top} \to \cat{Set}$ sends the identity map from $\R$ with the discrete topology to $\R$ with the usual topology — a continuous bijection whose inverse is not continuous — to a bijection.

∎

Similarly, $F(A) \cong F(B)$ does not imply $A \cong B$ : an invariant that says "same" proves nothing. The computation below finds two groups of order 16 that every functor $\Hom(\Z/n, -)$ fails to tell apart.

Formal mathematicsF

Functors in Lean and Mathlib

Mathlib's functors F : C ⥤ D have fields obj, map, map_id and map_comp. Since Mathlib composes diagrammatically (f ≫ g is "first f, then g"), the law $F(g \circ f) = F(g) \circ F(f)$ appears as F.map (f ≫ g) = F.map f ≫ F.map g.

Theorem 1, proved from the two functor laws, then packaged as an isomorphism of objects, and Mathlib's version:

map_inverseLean 4Proved here from basic factsFormally verified

/-- **Functors carry inverse pairs to inverse pairs.** If `g` is a two-sided inverse of `f`,
then `F(g)` is a two-sided inverse of `F(f)`:
`F(g) ∘ F(f) = F(g ∘ f) = F(id) = id`, and the same the other way round. Only the two functor
laws are used. -/
theorem map_inverse {C : Type u} [Category.{v} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D)
    {X Y : C} {f : X ⟶ Y} {g : Y ⟶ X} (h₁ : f ≫ g = 𝟙 X) (h₂ : g ≫ f = 𝟙 Y) :
    F.map f ≫ F.map g = 𝟙 (F.obj X) ∧ F.map g ≫ F.map f = 𝟙 (F.obj Y) := by
  constructor
  · rw [← F.map_comp, h₁, F.map_id]
  · rw [← F.map_comp, h₂, F.map_id]

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

iso_of_isoLean 4Proved here from basic factsFormally verified

/-- **Functors preserve isomorphic objects.** An isomorphism `e : X ≅ Y` in `C` gives an
isomorphism `F(X) ≅ F(Y)` in `D`, built from `map_inverse`. Read backwards this is the
impossibility tool of the lesson: if `F(X)` and `F(Y)` are *not* isomorphic, neither are `X`
and `Y`. (Mathlib's name for this construction is `Functor.mapIso`.) -/
theorem iso_of_iso {C : Type u} [Category.{v} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D)
    {X Y : C} (e : X ≅ Y) : Nonempty (F.obj X ≅ F.obj Y) :=
  ⟨⟨F.map e.hom, F.map e.inv, (map_inverse F e.hom_inv_id e.inv_hom_id).1,
    (map_inverse F e.hom_inv_id e.inv_hom_id).2⟩⟩

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

map_isIso_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's version: if `f` is an isomorphism then so is `F.map f`. This applies the instance
`CategoryTheory.Functor.map_isIso`. -/
theorem map_isIso_library {C : Type u} [Category.{v} C] {D : Type u₂} [Category.{v₂} D]
    (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] : IsIso (F.map f) :=
  Functor.map_isIso F f

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

The non-isomorphism of $\Z/4$ and $\Z/2 \times \Z/2$ , with the functorial argument unwound to elements (every element $y$ of $\Z/2 \times \Z/2$ has $y + y = 0$ , checked by decide):

zmod4_not_iso_kleinLean 4Proved here from basic factsFormally verified

/-- **`ℤ/4` and `ℤ/2 × ℤ/2` are not isomorphic groups.** The lesson's argument applies the
functor `G ↦ 2G = {x + x}` (or, dually, `Hom(ℤ/2, −)`): it sends `ℤ/4` to a group with two
elements and `ℤ/2 × ℤ/2` to the trivial group. Unwound to elements: in `ℤ/2 × ℤ/2` every
`y` has `y + y = 0`, so an additive isomorphism `e` would give `e(2) = e(1) + e(1) = 0 = e(0)`,
and injectivity would force `2 = 0` in `ℤ/4`, which is false. -/
theorem zmod4_not_iso_klein : IsEmpty (ZMod 4 ≃+ ZMod 2 × ZMod 2) := by
  constructor
  intro e
  have hdouble : ∀ y : ZMod 2 × ZMod 2, y + y = 0 := by decide
  have h2 : e 2 = e 0 := by
    calc e 2 = e (1 + 1) := rfl
      _ = e 1 + e 1 := map_add e 1 1
      _ = 0 := hdouble (e 1)
      _ = e 0 := (map_zero e).symm
  have : (2 : ZMod 4) = 0 := e.injective h2
  exact absurd this (by decide)

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

The functors of the gallery, with the functor laws proved. In this version of Mathlib a morphism in the category Type u wraps a function, and ↾f makes a morphism out of the function f:

powersetLean 4Formally verified

/-- **The covariant power-set functor** `P : Set → Set`. It sends a set `X` to the set of its
subsets, and a function `f : X → Y` to the direct-image map `S ↦ f(S)`.
The functor laws are `id(S) = S` (`Set.image_id`) and `(g ∘ f)(S) = g(f(S))` (`Set.image_comp`). -/
def powerset : Type u ⥤ Type u where
  obj X := Set X
  map f := ↾(fun S => (fun x => f x) '' S)
  map_id X := by
    ext S
    simp
  map_comp f g := by
    ext S
    simp [Set.image_image]

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

powersetContraLean 4Formally verified

/-- **The contravariant power-set functor** `P* : Setᵒᵖ → Set`. It sends a function
`f : X → Y` to the preimage map `T ↦ f⁻¹(T)`, which goes the *other way*, from subsets of `Y`
to subsets of `X`. So it is a functor out of the opposite category: the laws are
`id⁻¹(T) = T` and `(g ∘ f)⁻¹(T) = f⁻¹(g⁻¹(T))` — note the reversed order. -/
def powersetContra : (Type u)ᵒᵖ ⥤ Type u where
  obj X := Set X.unop
  map f := ↾(fun T => (fun x => f.unop x) ⁻¹' T)
  map_id X := by
    ext T
    simp
  map_comp f g := by
    ext T
    simp [Set.preimage_preimage]

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

listFunctorLean 4Formally verified

/-- **The list functor.** It sends a set `X` to the set `List X` of finite words in `X`, and a
function `f` to "apply `f` letter by letter" (`List.map f`). The laws are `List.map_id` and
`List.map_map`. `List X` with concatenation is the free monoid on `X` (see `list_map_append`
and the lesson on universal properties). -/
def listFunctor : Type u ⥤ Type u where
  obj X := List X
  map f := ↾(List.map (fun x => f x))
  map_id X := by
    ext l
    simp
  map_comp f g := by
    ext l
    simp [List.map_map, Function.comp_def]

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

list_map_appendLean 4Applies a library theoremFormally verified

/-- `List.map f` is a **monoid homomorphism** for concatenation: it preserves the empty word
and `map f (l ++ m) = map f l ++ map f m`. So the list functor really lands in monoids. This
applies `List.map_nil` and `List.map_append`. -/
theorem list_map_append {X Y : Type u} (f : X → Y) (l m : List X) :
    List.map f [] = [] ∧ List.map f (l ++ m) = List.map f l ++ List.map f m :=
  ⟨List.map_nil, List.map_append⟩

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

free_monoid_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's **free monoid functor** `MonCat.free : Type u ⥤ MonCat` sends a set `X` to the free
monoid `FreeMonoid X` (lists with concatenation) and a function to the homomorphism that renames
letters: a one-letter word `[a]` goes to `[f a]`. This applies `MonCat.free` and
`FreeMonoid.map_of`. -/
theorem free_monoid_library {X Y : Type u} (f : X ⟶ Y) (a : X) :
    (MonCat.free.map f).hom (FreeMonoid.of a) = FreeMonoid.of (f a) :=
  FreeMonoid.map_of _ a

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

homFunctorLean 4Formally verified

/-- **The hom functor** `Hom(A, −) : C → Set`. It sends an object `B` to the set of morphisms
`A ⟶ B`, and a morphism `f : B ⟶ B'` to "compose with `f`": `g ↦ f ∘ g` (`g ≫ f` in Mathlib).
The functor laws are exactly the axioms of a category: `id ∘ g = g` (`Category.comp_id`) and
`(f' ∘ f) ∘ g = f' ∘ (f ∘ g)` (`Category.assoc`). Mathlib calls it `coyoneda.obj (op A)`. -/
def homFunctor {C : Type u} [Category.{v} C] (A : C) : C ⥤ Type v where
  obj B := A ⟶ B
  map f := ↾(fun g => g ≫ f)
  map_id B := by
    ext g
    simp
  map_comp f f' := by
    ext g
    simp

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

homFunctorContraLean 4Formally verified

/-- **The contravariant hom functor** `Hom(−, A) : Cᵒᵖ → Set`, sending `f : B' ⟶ B` to
"precompose with `f`": `g ↦ g ∘ f`. Precomposition reverses the direction of arrows, so this is
a functor out of `Cᵒᵖ`. Mathlib calls it `yoneda.obj A`. -/
def homFunctorContra {C : Type u} [Category.{v} C] (A : C) : Cᵒᵖ ⥤ Type v where
  obj B := B.unop ⟶ A
  map f := ↾(fun g => f.unop ≫ g)
  map_id B := by
    ext g
    simp
  map_comp f f' := by
    ext g
    simp

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

comp_assoc_libraryLean 4Applies a library theoremFormally verified

/-- **Functors compose, associatively.** `F ⋙ G` is "first `F`, then `G`", and composition of
functors is associative (on the nose). Together with identity functors this makes small
categories and functors into a category, Mathlib's `Cat`. This applies `Functor.assoc`. -/
theorem comp_assoc_library {A : Type u} [Category.{v} A] {B : Type u₂} [Category.{v₂} B]
    {C : Type w} [Category.{w} C] {D : Type u} [Category.{v} D]
    (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) : (F ⋙ G) ⋙ H = F ⋙ (G ⋙ H) :=
  Functor.assoc F G H

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

Theorems 2 and 3 in abstract form: a functor to sets turns a retraction into an injective map, so no retraction exists when the functor sends $D$ to a set with at most one element and $S$ to a set with two. The topological instance needs $\pi_1(D^2) = 0$ and $\pi_1(S^1) \cong \Z$ ; Mathlib has the fundamental group (FundamentalGroup) and, recently, the isomorphism $\pi_1(\R/\Z) \cong \Z$ (AddCircle.windingNumberIso), which the Lumenary lesson on the fundamental group uses. Here we formalise the categorical core:

map_injective_of_retractionLean 4Proved here from basic factsFormally verified

/-- **Functors preserve retractions.** If `r ∘ i = id_S` (here `i ≫ r = 𝟙 S`), then
`F(r) ∘ F(i) = id_{F(S)}` for every functor `F`; for a functor to sets this makes `F(i)`
injective, since `F(i)(a) = F(i)(b)` gives `a = F(r)(F(i)(a)) = F(r)(F(i)(b)) = b`. -/
theorem map_injective_of_retraction {C : Type u} [Category.{v} C] (F : C ⥤ Type w) {S D : C}
    (i : S ⟶ D) (r : D ⟶ S) (h : i ≫ r = 𝟙 S) : Function.Injective (F.map i) := by
  have hFr : F.map i ≫ F.map r = 𝟙 (F.obj S) := by
    rw [← F.map_comp, h, F.map_id]
  intro a b hab
  calc a = (F.map i ≫ F.map r) a := by rw [hFr]; rfl
    _ = F.map r (F.map i a) := rfl
    _ = F.map r (F.map i b) := by rw [hab]
    _ = (F.map i ≫ F.map r) b := rfl
    _ = b := by rw [hFr]; rfl

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

no_retractionLean 4Proved here from basic factsFormally verified

/-- **The shape of the no-retraction theorem.** Suppose a functor `F` to sets sends `D` to a set
with at most one element and `S` to a set with two different elements. Then there is **no**
retraction `r : D → S` of any `i : S → D` (no `r` with `r ∘ i = id_S`): `F(i)` would be an
injective map from a set with two elements into a set with one.
For the circle `S¹` inside the disc `D²` and `F = π₁` (fundamental group, a functor from pointed
spaces to groups, then to sets): `π₁(D²)` is trivial and `π₁(S¹) ≅ ℤ` is not, so the disc does not
retract onto its boundary circle. -/
theorem no_retraction {C : Type u} [Category.{v} C] (F : C ⥤ Type w) {S D : C} (i : S ⟶ D)
    [Subsingleton (F.obj D)] {a b : F.obj S} (hab : a ≠ b) : ¬ ∃ r : D ⟶ S, i ≫ r = 𝟙 S := by
  rintro ⟨r, h⟩
  exact hab (map_injective_of_retraction F i r h (Subsingleton.elim _ _))

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

Theorem 4(i):

not_reflects_isoLean 4Proved here from basic factsFormally verified

/-- **A functor can send a non-isomorphism to an isomorphism.** In the poset `0 < 1` (Lean's
`Fin 2`) regarded as a category, the morphism `0 ⟶ 1` is not an isomorphism (an inverse would be
a morphism `1 ⟶ 0`, that is `1 ≤ 0`). But the constant functor to a one-element set sends it to
the identity map, which is an isomorphism. So `F(f)` invertible does not force `f` invertible. -/
theorem not_reflects_iso :
    ∃ (F : Fin 2 ⥤ Type) (f : (0 : Fin 2) ⟶ 1), IsIso (F.map f) ∧ ¬ IsIso f := by
  have h01 : (0 : Fin 2) ≤ 1 := by decide
  refine ⟨(Functor.const (Fin 2)).obj PUnit, homOfLE h01, ?_, ?_⟩
  · -- the constant functor sends every morphism to an identity
    show IsIso (𝟙 PUnit)
    infer_instance
  · intro hf
    have h10 : (1 : Fin 2) ≤ 0 := leOfHom (inv (homOfLE h01))
    exact absurd h10 (by decide)

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

Not formalised here: the free vector space functor (Mathlib has it as Finsupp and ModuleCat.free), abelianisation and the units functor (Mathlib's Abelianization and Units.map), and Brouwer's theorem.

ComputationC

Counting homomorphisms to tell groups apart

The functor $\Hom(\Z/n, -)$ turns a group $G$ into the set of elements with $g^n = e$ . Counting these sets for every $n$ gives a list of invariants. The experiment computes them for the five groups of order 8 — which they separate completely — and for two groups of order 16, $\Z/4 \times \Z/4$ and $\Z/2 \times Q_8$ (where $Q_8 = \{\pm 1, \pm i, \pm j, \pm k\}$ is the quaternion group), which they cannot separate. A different hom functor, $\Hom(\Z \times \Z, -)$ , whose values are the pairs of commuting elements, then does the job.

Telling groups apart with hom functorsPythonExact computationExhaustive finite checkComputationally tested

"""Telling groups apart with hom functors, and where that fails.

A functor sends isomorphic objects to isomorphic objects. For the hom
functor Hom(Z/n, -) from groups to sets this means: if G and H are
isomorphic, then |Hom(Z/n, G)| = |Hom(Z/n, H)|. A homomorphism Z/n -> G is
determined by the image g of 1, which can be any g with g^n = e, so the
count is #{g in G : g^n = e}. We compute these counts for the five groups of
order 8, which they tell apart completely, and for Z/4 x Z/4 and Z/2 x Q8 of
order 16, which they cannot tell apart. A different hom functor,
Hom(Z x Z, -) (commuting pairs), separates that last pair. Exact computation
on finite groups.
"""

from itertools import product

def cyclic(n):
    """The cyclic group Z/n: (elements, multiplication, identity)."""
    return list(range(n)), (lambda a, b: (a + b) % n), 0

def direct_product(g, h):
    """The direct product of two groups, with coordinatewise operation."""
    (ge, gm, g1), (he, hm, h1) = g, h
    elements = list(product(ge, he))
    return elements, (lambda a, b: (gm(a[0], b[0]), hm(a[1], b[1]))), (g1, h1)

def dihedral8():
    """Symmetries of a square: (r, s) means rotate by r quarter turns, then
    reflect if s = 1."""
    def mul(a, b):
        r1, s1 = a
        r2, s2 = b
        return ((r1 + (r2 if s1 == 0 else -r2)) % 4, (s1 + s2) % 2)
    return list(product(range(4), range(2))), mul, (0, 0)

def quaternion8():
    """Q8 = {+-1, +-i, +-j, +-k} as unit quaternions (a, b, c, d)."""
    def mul(p, q):
        a1, b1, c1, d1 = p
        a2, b2, c2, d2 = q
        return (a1 * a2 - b1 * b2 - c1 * c2 - d1 * d2,
                a1 * b2 + b1 * a2 + c1 * d2 - d1 * c2,
                a1 * c2 - b1 * d2 + c1 * a2 + d1 * b2,
                a1 * d2 + b1 * c2 - c1 * b2 + d1 * a2)
    units = []
    for k in range(4):
        for sign in (1, -1):
            units.append(tuple(sign if i == k else 0 for i in range(4)))
    return units, mul, (1, 0, 0, 0)

def power(group, g, n):
    """g^n in the group, by repeated multiplication."""
    _, mul, one = group
    result = one
    for _ in range(n):
        result = mul(result, g)
    return result

def hom_count_cyclic(group, n):
    """|Hom(Z/n, G)| = number of g with g^n = e."""
    elements, _, one = group
    return sum(1 for g in elements if power(group, g, n) == one)

def commuting_pairs(group):
    """|Hom(Z x Z, G)| = number of pairs (a, b) with ab = ba."""
    elements, mul, _ = group
    return sum(1 for a in elements for b in elements if mul(a, b) == mul(b, a))

def groups_of_order_8():
    """The five groups of order 8, up to isomorphism, with names."""
    z2, z4 = cyclic(2), cyclic(4)
    return [
        ("Z/8", cyclic(8)),
        ("Z/4 x Z/2", direct_product(z4, z2)),
        ("Z/2 x Z/2 x Z/2", direct_product(direct_product(z2, z2), z2)),
        ("D4 (square)", dihedral8()),
        ("Q8", quaternion8()),
    ]

def main():
    print("|Hom(Z/n, G)| = #{g : g^n = e}")
    print(f"{'G':<18}{'n=1':>5}{'n=2':>5}{'n=4':>5}{'n=8':>5}")
    signatures = []
    for name, group in groups_of_order_8():
        row = [hom_count_cyclic(group, n) for n in (1, 2, 4, 8)]
        signatures.append(tuple(row))
        print(f"{name:<18}" + "".join(f"{c:>5}" for c in row))
    distinct = len(set(signatures)) == len(signatures)
    print(f"All five rows differ, so no two are isomorphic: {distinct}")
    print()
    z2, z4 = cyclic(2), cyclic(4)
    pair = [("Z/4 x Z/4", direct_product(z4, z4)),
            ("Z/2 x Q8", direct_product(z2, quaternion8()))]
    print("Order 16:")
    for name, group in pair:
        row = [hom_count_cyclic(group, n) for n in (1, 2, 4, 8, 16)]
        print(f"  {name:<10} |Hom(Z/n, G)|, n = 1, 2, 4, 8, 16: {row}")
    for name, group in pair:
        print(f"  {name:<10} |Hom(Z x Z, G)| = {commuting_pairs(group)}")
    print("Hom(Z/n, -) cannot separate them; Hom(Z x Z, -) can.")
    print()
    print("Epistemic status: exact counts for these finite groups. Different")
    print("counts prove non-isomorphism, because functors preserve")
    print("isomorphisms. Equal counts prove nothing: Z/4 x Z/4 is abelian and")
    print("Z/2 x Q8 is not, yet every Hom(Z/n, -) gives the same numbers.")

if __name__ == "__main__":
    main()

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

The counts are exact, and different counts are a proof of non-isomorphism, because functors preserve isomorphisms. Equal counts are no evidence of isomorphism at all — which is the lesson of the last two rows.

Explore

Explore: invariants that see shape

The fundamental group of the punctured plane. The functor $\pi_1$ turns loops into elements of a group. For the plane with one hole the group is $\Z$ , and the integer attached to a loop is its winding number. Play the loop and watch the radius vector from the hole: it turns once for the circle, twice for "twice", and zero times for the crescent that curls around the hole without enclosing it. Try drawing your own loop. A continuous deformation of the loop that never crosses the hole cannot change the winding number — this is what makes it an invariant, and what powers the proof of Theorem 3.

Winding numbers: π₁ of the punctured plane is ℤ

Follow a closed loop and count how many times it goes around each hole: counter-clockwise turns minus clockwise turns.

Drag a hole to move it. Press Play to send the point around the loop, or use the slider. The small square marks the start.

Position on the loop

Winding number around p₁1

(1/2πi)∮ dz/(z − p₁) ≈ 1.000 + 0.000i

Turns swept so far by each dashed arrow:

p₁: 0.00

The winding number is found by adding up the small changes in direction of the arrow from the hole to the moving point, and dividing the total by 360°. Counter-clockwise counts as positive.

Two loops in the plane with one hole can be deformed into each other, without ever crossing the hole, exactly when they have the same winding number. In the language of topology: the fundamental group of the punctured plane — like that of a circle — is the integers, π₁ = ℤ.

A link to complex analysis: think of the plane as the complex numbers and of a hole as a point a. Then (1/2πi)∮ dz/(z − a) equals the winding number around a. The values above are computed numerically along the loop.

Counting homomorphisms distinguishes knots. A valid 3-colouring of a knot diagram (at each crossing the three arcs are all the same colour or all different) is the same as a homomorphism from the knot's fundamental quandle — an algebraic object built from the diagram — to the three-element "dihedral quandle". Isotopic knots have isomorphic quandles (Joyce and Matveev, 1982), so the number of colourings is an invariant, exactly like $|\Hom(\Z/2, G)|$ for groups. Count the colourings of the unknot and the trefoil: $3$ and $9$ . They are different, so the trefoil is knotted. The figure-eight knot also has only $3$ , yet it is knotted: one invariant saying "same" proves nothing.

Colouring knots with three colours

Colour every arc of the diagram. At each crossing, the three arcs that meet must be all the same colour or all different.

Click an arc to change its colour (or focus it and press Enter, or 1, 2, 3). An arc runs from one under-crossing to the next.

colour 1 (terracotta, circle)colour 2 (violet, triangle)colour 3 (teal, square)

Trefoil3₁

Crossings in this diagram: 3
Crossing number (fewest possible): 3

Arcs coloured: 0 of 3.

Why this rule? Any two diagrams of the same knot are related by three kinds of local moves, the Reidemeister moves: adding or removing a twist, sliding one strand over another, and sliding a strand past a crossing. Each move turns a valid colouring with two or more colours into another one.

The trefoil can be tricoloured and the unknot cannot. Because tricolourability is an invariant, no amount of wiggling turns the trefoil into the unknot: the trefoil really is knotted.

So tricolourability is a knot invariant: if one diagram of a knot can be tricoloured, every diagram of it can. A plain circle has just one arc, so the unknot cannot be tricoloured.

Exercises

1. Functors

Warm-upHuman

Which of these are functors? Choose all that apply.

Choose all that apply

\mathbf{Grp} \to \mathbf{Set}

: a group goes to its underlying set, a homomorphism to its underlying function.

\mathbf{Set} \to \mathbf{Set}

X

goes to the set of finite lists in

X

, and

f

to "apply

f

to every entry".

\mathbf{Grp} \to \mathbf{Grp}

G

goes to its centre

Z(G)

, and

f

to its restriction to the centre.Between two posets regarded as categories: a monotone map

p

, with

x \le y

sent to

p(x) \le p(y)

\mathbf{Set} \to \mathbf{Set}

X

goes to its power set, and

f : X \to Y

to the preimage map

T \mapsto f^{-1}(T)

2. Functors

Warm-upHuman

How many group homomorphisms are there from $\mathbb{Z}/2$ to $\mathbb{Z}/6$ ? (That is, what is $|\mathrm{Hom}(\mathbb{Z}/2, \mathbb{Z}/6)|$ ?)

3. Functors

CoreHuman

Which argument correctly proves that the groups $\mathbb{Z}/4$ and $\mathbb{Z}/2 \times \mathbb{Z}/2$ are not isomorphic?

Choose one

|\mathrm{Hom}(\mathbb{Z}/2, \mathbb{Z}/4)| = 2

but

|\mathrm{Hom}(\mathbb{Z}/2, \mathbb{Z}/2 \times \mathbb{Z}/2)| = 4

, and the functor

\mathrm{Hom}(\mathbb{Z}/2, -)

would send an isomorphism to a bijection.They have different orders.One is abelian and the other is not.The bijection

0 \mapsto (0,0)

1 \mapsto (1,0)

2 \mapsto (0,1)

3 \mapsto (1,1)

is not a homomorphism.

4. Functors

CoreHuman

For the contravariant power-set functor $\mathcal{P}^\ast$ (which sends $f : X \to Y$ to the preimage map $\mathcal{P}^\ast(f)(T) = f^{-1}(T)$ ), and functions $f : X \to Y$ , $g : Y \to Z$ , which equation holds for all $T \subseteq Z$ ?

Choose one

(g \circ f)^{-1}(T) = f^{-1}\big(g^{-1}(T)\big)

, i.e.

\mathcal{P}^\ast(g \circ f) = \mathcal{P}^\ast(f) \circ \mathcal{P}^\ast(g)

(g \circ f)^{-1}(T) = g^{-1}\big(f^{-1}(T)\big)

(g \circ f)^{-1}(T) = g\big(f(T)\big)

None — preimages do not compose.

5. Functors

CoreHuman

Which of the following are morphisms $f$ that are not isomorphisms, but whose image $F(f)$ under the indicated functor is an isomorphism? Choose all that apply.

Choose all that apply

The identity map from

\mathbb{R}

with the discrete topology to

\mathbb{R}

with the usual topology, and

F

the forgetful functor

\mathbf{Top} \to \mathbf{Set}

.The morphism

0 \to 1

in the poset

\{0 < 1\}

, and

F

the functor to

\mathbf{Set}

sending both objects to

\{\ast\}

.A bijective group homomorphism, and

F

the forgetful functor

\mathbf{Grp} \to \mathbf{Set}

.A matrix

A \in \mathrm{GL}_2(\mathbb{R})

with

\det A = 1

, regarded as a morphism of the one-object category

\mathrm{GL}_2(\mathbb{R})

, and

F = \det

6. Functors

CoreFormal

In Lean/Mathlib, which type is right for the preimage power-set functor, which sends $f : X \to Y$ to $T \mapsto f^{-1}(T)$ ?

Choose one

(Type u)ᵒᵖ ⥤ Type uType u ⥤ Type u(Type u)ᵒᵖ ⥤ (Type u)ᵒᵖType u → Type u

7. Functors

StretchHuman

In the proof that there is no retraction $r : D^2 \to S^1$ (with $r \circ i = \mathrm{id}_{S^1}$ ), which facts are used? Choose the most complete correct answer.

Choose one

Functoriality of

\pi_1

gives

\pi_1(r) \circ \pi_1(i) = \mathrm{id}

\pi_1(S^1) \cong \mathbb{Z}

; this identity would factor through

\pi_1(D^2) = 0

, which is impossible.

\pi_1

preserves isomorphisms, and

D^2

is not isomorphic to

S^1

D^2

is compact and

S^1

is not.

S^1

minus a point is connected, so

r

cannot be continuous.

8. Functors

CoreComputational

Functions between finite sets are stored as Python dicts. Write image(f, S) (the set $f(S)$ ) and preimage(f, T) (the set $f^{-1}(T)$ ), and compose(g, f) (first f, then g). The tests check the functor laws: images compose covariantly, $(g \circ f)(S) = g(f(S))$ , and preimages contravariantly, $(g \circ f)^{-1}(T) = f^{-1}(g^{-1}(T))$ .

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

Common misconceptionsH

Common misconceptions

Misconception

"A functor must be injective on objects or on morphisms." Not at all. The forgetful functor $\cat{Grp} \to \cat{Set}$ sends the many different groups with underlying set $\{0, 1, 2, 3\}$ to the same set. The functor from any category to $\mathbf{1}$ collapses everything. A functor only has to respect composition and identities.

Misconception

"If $F(f)$ is invertible then $f$ is invertible." Functors preserve isomorphisms; they need not reflect them. The forgetful functor $\cat{Top} \to \cat{Set}$ sends a continuous bijection with discontinuous inverse to a bijection, and a constant functor sends every morphism to an identity. (Functors that do reflect isomorphisms are called conservative; the forgetful functor $\cat{Grp} \to \cat{Set}$ is one, because the inverse of a bijective homomorphism is a homomorphism.)

Misconception

"If $F(A) \cong F(B)$ then $A \cong B$ ." Only the converse holds. $\Z/4 \times \Z/4$ and $\Z/2 \times Q_8$ have the same number of homomorphisms from every $\Z/n$ , yet one is abelian and the other is not; the unknot and the figure-eight knot have the same number of 3-colourings.

Misconception

"Contravariant functors are a different kind of object." A contravariant functor from $\cat{C}$ to $\cat{D}$ is just a functor $\cat{C}^{\mathrm{op}} \to \cat{D}$ ; every theorem about functors applies to it.

Misconception

"Any natural-looking construction on objects is a functor." The centre of a group is not functorial for arbitrary homomorphisms (see the gallery). Being a functor requires a rule on morphisms satisfying the laws, and that is a genuine condition.

ViewpointsH

Many ways of seeing

Topology— Algebraic topology is the study of functors from spaces to algebra

The fundamental group, homology $H_n$ , cohomology $H^n$ and homotopy groups $\pi_n$ are functors from (pointed) spaces to groups. Each turns topological questions into algebraic ones. Theorem 3 generalises with homology: $H_{n-1}(S^{n-1}) \cong \Z$ while $H_{n-1}(D^n) = 0$ for $n \ge 2$ , so the ball $D^n$ does not retract onto its boundary sphere, and Brouwer's fixed-point theorem holds in every dimension. Functoriality also explains homotopy invariance: homotopic maps induce the same homomorphism, so homotopy-equivalent spaces have isomorphic invariants. Eilenberg and Steenrod characterised homology by a handful of functorial axioms. See algebraic topology.

Analysis— The chain rule is functoriality

Consider the category whose objects are pointed open sets $(U, a)$ with $U \subseteq \R^n$ open and $a \in U$ , and whose morphisms $(U, a) \to (V, b)$ are differentiable maps $f$ with $f(a) = b$ . Sending $(U, a)$ to the vector space $\R^n$ and $f$ to its derivative $Df(a)$ , a linear map, is a functor to $\cat{Vect}_\R$ : the identity has derivative the identity, and the chain rule $D(g \circ f)(a) = Dg(f(a)) \circ Df(a)$ is precisely the functor law. Theorem 1 then gives at once: if $f$ is a diffeomorphism near $a$ (with a differentiable inverse), then $Df(a)$ is invertible — so $\R^m$ and $\R^n$ are not diffeomorphic for $m \neq n$ , since an invertible linear map needs $m = n$ . See multivariable calculus. On smooth manifolds the same idea is the tangent functor $M \mapsto TM$ .

Number theory— Units, and counting solutions

The units functor $R \mapsto R^\times$ distinguishes rings of integers, as with $\Z[i]$ and $\Z[\sqrt 2]$ above; Dirichlet's unit theorem describes $\mathcal{O}_K^\times$ for every number field $K$ . Hom functors appear in number theory as solution sets: for a polynomial equation such as $x^2 + y^2 = 1$ , the set of solutions in a commutative ring $R$ is $\Hom(\Z[x, y]/(x^2 + y^2 - 1), R)$ , and a ring homomorphism $R \to R'$ (for instance reduction $\Z \to \Z/p$ ) sends solutions to solutions functorially. This "functor of points" view is the starting point of modern algebraic geometry.

Computation— Functors in programming

In Haskell, a type constructor f is a Functor if it comes with fmap :: (a -> b) -> f a -> f b satisfying fmap id = id and fmap (g . f) = fmap g . fmap f — exactly the functor laws for an endofunctor of the category of types. Lists (fmap = map, our free monoid functor), optional values (Maybe) and trees are examples. The laws are not checked by the compiler; programmers prove them, or test them on examples, because optimisers rely on them (for instance to fuse two passes map g . map f into one pass map (g . f)).

Physics— Topological quantum field theories

Michael Atiyah (1988), building on work of Edward Witten and Graeme Segal, axiomatised a topological quantum field theory in dimension $n$ as a functor $Z$ from a category of cobordisms — objects are closed $(n-1)$ -dimensional manifolds ("space"), morphisms are $n$ -dimensional manifolds whose boundary is split into an incoming and an outgoing part ("spacetime") — to the category of finite-dimensional vector spaces ("state spaces"). Gluing spacetimes end to end is composition, and $Z(\text{glued}) = Z(\text{second}) \circ Z(\text{first})$ is the functor law; physically it says that evolving in two steps is the same as evolving at once. (A TQFT is moreover required to respect disjoint unions and tensor products — a symmetric monoidal functor.) This is a mathematical framework inspired by physics, not a derivation of physical law; it has produced knot and 3-manifold invariants such as those of Reshetikhin and Turaev.

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

Henri Poincaré introduced the fundamental group in Analysis Situs (1895). In the 1920s, prompted by Emmy Noether, topologists began to treat Betti numbers as ranks of homology groups, and to study the homomorphisms induced by continuous maps — functors in all but name.
L. E. J. Brouwer proved his fixed-point theorem in all dimensions around 1911 (the three-dimensional case is due to Piers Bohl, 1904, and Jacques Hadamard gave a proof in 1910).
Samuel Eilenberg and Saunders Mac Lane defined functors and natural transformations in 1945. Mac Lane later recalled that the word "functor" was borrowed from the philosopher Rudolf Carnap, and "category" from Aristotle and Kant.
Units like those of $\Z[\sqrt 2]$ are much older than categories. They correspond to solutions of Pell-type equations $x^2 - 2y^2 = \pm 1$ , studied in India by Brahmagupta (628), whose composition rule (bhāvanā) multiplies solutions, and by the chakravala method described by Jayadeva (11th century) and Bhāskara II (12th century). Dirichlet's unit theorem (1846) describes the units of every ring of algebraic integers.
Atiyah's axioms for topological quantum field theories (1988) and the Reshetikhin–Turaev invariants (1991) brought functors into mathematical physics.

How do you prove two things are different?

Definitions

A gallery of functors

Functoriality proves impossibility

Functors in Lean and Mathlib

Counting homomorphisms to tell groups apart

Explore: invariants that see shape

Exercises

Common misconceptions

Many ways of seeing

Wonder Trails

History and global context

Further reading