Categories · The Lumenary

Lens

MotivationH

The same pattern, again and again

Here are five facts from five different corners of mathematics.

If $f : A \to B$ and $g : B \to C$ are functions, then so is $g \circ f : A \to C$ ; composing is associative, and the identity function changes nothing.
If $f : G \to H$ and $g : H \to K$ are group homomorphisms, so is $g \circ f$ ; the identity of a group is a homomorphism.
If $f$ and $g$ are continuous maps of spaces, so is $g \circ f$ ; the identity map is continuous.
If $A$ is an $n \times m$ matrix and $B$ a $p \times n$ matrix, then $BA$ is a $p \times m$ matrix; $(CB)A = C(BA)$ , and the identity matrix is neutral.
If $x \le y$ and $y \le z$ then $x \le z$ ; and $x \le x$ .

The last two involve no functions at all — yet they have the same shape: things, arrows between things, a way to chain arrows end to end that does not care about brackets, and arrows that do nothing. In the lesson on composition you met this shape for sets and functions; in the lesson on structure-preserving maps you saw that homomorphisms compose too.

A category is exactly this shape, made precise. Studying it pays twice. First, a theorem proved once for all categories is proved for sets, groups, spaces, matrices and orders at the same time. Second, it changes how we ask questions: instead of looking inside an object at its elements, we look at how it relates to everything else through arrows. Surprisingly much can be seen that way — even whether a function is injective.

IntuitionH

Dots, arrows and paths

Picture a category as a diagram of dots (the objects) and arrows between them (the morphisms). Every path of arrows laid end to end can be shortened to a single arrow, its composite, and it does not matter in which order you do the shortening. Each dot has a loop that "stays put", which you can insert into or delete from any path.

Two warnings, to be taken seriously from the start.

The arrows need not be functions. In the category built from $(\Z, \le)$ there is one arrow $3 \to 7$ because $3 \le 7$ , and no arrow $7 \to 3$ . The arrow is not a rule that transforms anything; it is just the fact $3 \le 7$ .
The objects need not have elements. In the category of matrices below, the objects are the natural numbers $0, 1, 2, \dots$ , and a morphism $m \to n$ is an $n \times m$ matrix. Asking for "the elements of the object $3$ " makes no sense.

So everything we say about a category must be said with objects, arrows, composition and identities alone. That restriction is the source of category theory's power: a definition phrased only with arrows can be applied in every category at once.

DefinitionsH

Definitions

Definition— category

A category $\cat{C}$ consists of

a collection of objects $A, B, C, \dots$ ;
for each pair of objects $A, B$ , a collection $\Hom_{\cat{C}}(A, B)$ of morphisms (or arrows) from $A$ to $B$ ; we write $f : A \to B$ ;
for each object $A$ , an identity morphism $\id_A : A \to A$ ;
for each pair $f : A \to B$ , $g : B \to C$ , a composite $g \circ f : A \to C$ ;

such that for all $f : A \to B$ , $g : B \to C$ , $h : C \to D$ :

h \circ (g \circ f) = (h \circ g) \circ f \qquad \text{(associativity)}, \qquad f \circ \id_A = f = \id_B \circ f \qquad \text{(unit laws)}.

Only composable pairs have a composite: $g \circ f$ is defined when the target of $f$ is the source of $g$ . A category is small if its objects and morphisms form sets, and locally small if each $\Hom(A, B)$ is a set. ( $\cat{Set}$ itself is locally small but not small: there is no set of all sets.)

Definition— isomorphism

A morphism $f : A \to B$ is an isomorphism if there is a morphism $g : B \to A$ with $g \circ f = \id_A$ and $f \circ g = \id_B$ . Such a $g$ is called an inverse of $f$ . Objects $A$ and $B$ are isomorphic, $A \cong B$ , if there is an isomorphism between them.

Definition— monomorphism and epimorphism

A morphism $f : A \to B$ is a monomorphism (or is monic) if it can be cancelled on the left:

f \circ g = f \circ h \implies g = h \qquad \text{for all objects } T \text{ and all } g, h : T \to A.

It is an epimorphism (or is epic) if it can be cancelled on the right: $g \circ f = h \circ f \implies g = h$ for all $g, h : B \to T$ .

f

is monic if

f \circ g = f \circ h

forces

g = h

; epic if

k \circ f = l \circ f

forces

k = l

Definition— opposite category

The opposite $\cat{C}^{\mathrm{op}}$ of a category $\cat{C}$ has the same objects, and one morphism $f^{\mathrm{op}} : B \to A$ for each morphism $f : A \to B$ of $\cat{C}$ . Composition is reversed: $f^{\mathrm{op}} \circ g^{\mathrm{op}} = (g \circ f)^{\mathrm{op}}$ , and $\id_A^{\mathrm{op}}$ is the identity.

The axioms for $\cat{C}^{\mathrm{op}}$ are the axioms for $\cat{C}$ read backwards, so $\cat{C}^{\mathrm{op}}$ is a category, and $(\cat{C}^{\mathrm{op}})^{\mathrm{op}} = \cat{C}$ .

Worked examplesH

Examples, and some non-examples

Example— Categories of structured sets

Category	Objects	Morphisms
$\cat{Set}$	sets	functions
$\cat{Grp}$	groups	group homomorphisms
$\cat{Ring}$	rings with $1$	ring homomorphisms preserving $1$
$\cat{Vect}_k$	vector spaces over a field $k$	linear maps
$\cat{Top}$	topological spaces	continuous maps

In each case composition is composition of functions and the identities are identity functions. So associativity and the unit laws are inherited from $\cat{Set}$ (proved in the composition lesson); what must be checked is closure: that composites and identities are again morphisms. For $\cat{Grp}$ : if $f, g$ are homomorphisms then $(g \circ f)(xy) = g(f(x) f(y)) = g(f(x))\, g(f(y))$ , and $\id_G(xy) = xy = \id_G(x)\id_G(y)$ . For $\cat{Top}$ : if $U$ is open then $(g \circ f)^{-1}(U) = f^{-1}(g^{-1}(U))$ is open, and $\id^{-1}(U) = U$ . For $\cat{Vect}_k$ : composites and identities of linear maps are linear.

Example— Matrices: objects without elements

Fix a field $k$ . The category $\cat{Mat}_k$ has as objects the natural numbers. A morphism $m \to n$ is an $n \times m$ matrix over $k$ (it turns column vectors of length $m$ into column vectors of length $n$ ); composition is matrix multiplication, $B \circ A = BA$ , and $\id_n = I_n$ . The axioms are $C(BA) = (CB)A$ and $AI_m = A = I_n A$ . An isomorphism $m \to n$ is an invertible matrix, which forces $m = n$ (rank–nullity). The objects are bare numbers: this category is not "sets with structure".

Example— Preorders and posets

A preorder is a set $P$ with a reflexive, transitive relation $\le$ . It becomes a category: the objects are the elements of $P$ , and there is exactly one morphism $x \to y$ if $x \le y$ , and none otherwise. Composition exists by transitivity, identities by reflexivity, and the laws hold automatically because between two objects there is at most one morphism, so any two parallel composites are equal.

Conversely, a category with at most one morphism between any two objects is a preorder: put $x \le y$ when there is a morphism $x \to y$ . Examples: $(\R, \le)$ ; the subsets of a set ordered by $\subseteq$ ; the positive integers ordered by divisibility, where $2 \to 6$ and $3 \to 6$ but neither $2 \to 3$ nor $3 \to 2$ .

In a preorder, $x \cong y$ exactly when $x \le y$ and $y \le x$ . In a poset (antisymmetric preorder) isomorphic objects are therefore equal.

Example— Monoids: categories with one object

A monoid $(M, \cdot, 1)$ — see algebraic structures — gives a category $\mathbf{B}M$ with a single object $\star$ , morphisms $\star \to \star$ the elements of $M$ , composition $y \circ x = y \cdot x$ and $\id_\star = 1$ . Associativity and the unit laws of the category are the monoid axioms. Conversely, the morphisms $A \to A$ of any category form a monoid under composition, the endomorphism monoid $\mathrm{End}(A)$ ; so a category with one object is the same thing as a monoid.

Examples: $(\N, +, 0)$ — morphisms are numbers, and "first $3$ , then $5$ " is $8$ ; the clock monoid $(\Z/12, +, 0)$ ; strings of letters under concatenation; the $2^2 = 4$ functions $\{0, 1\} \to \{0, 1\}$ under composition, a monoid that is not commutative. An isomorphism in $\mathbf{B}M$ is an element with a two-sided inverse — a unit of $M$ . A group is a one-object category in which every morphism is an isomorphism.

Example— Two very small categories

The category $\mathbf{1}$ has one object and only its identity. The category $\mathbf{2}$ has two objects $0, 1$ and, besides the identities, one morphism $0 \to 1$ ; it is the poset $\{0 < 1\}$ . The morphism $0 \to 1$ is both monic and epic (there is nothing to cancel), but it is not an isomorphism. So "monic and epic" does not imply "isomorphism" in general — although in $\cat{Set}$ it does.

Example— Non-examples

The integers with an arrow $m \to n$ whenever $m < n$ (strictly): composites exist, but there is no identity $n \to n$ . Not a category.
Sets, with morphisms the functions that are at most two-to-one. Identities qualify, but a composite of two two-to-one maps can be four-to-one. Composition is not closed. Not a category.
A directed graph by itself is not a category: it has arrows but no rule for composing them. (Every directed graph does generate a category, whose morphisms are the paths — the free category on the graph.)

ProofH

Isomorphisms, monos and epis

Theorem— Theorem 1 (inverses are unique)

Let $f : A \to B$ . If $g : B \to A$ satisfies $g \circ f = \id_A$ (a left inverse) and $h : B \to A$ satisfies $f \circ h = \id_B$ (a right inverse), then $g = h$ . In particular an isomorphism has exactly one inverse, written $f^{-1}$ .

Proof

Using only the unit laws and associativity,

g = g \circ \id_B = g \circ (f \circ h) = (g \circ f) \circ h = \id_A \circ h = h.

If $g$ and $g'$ are both two-sided inverses of $f$ , then $g$ is a left inverse and $g'$ a right inverse, so $g = g'$ .

∎

This is the same calculation that proves inverses in a monoid or group are unique — and now we see why: it uses nothing but the category axioms. The same goes for the next fact. If $f : A \to B$ and $g : B \to C$ are isomorphisms, so is $g \circ f$ , with inverse $f^{-1} \circ g^{-1}$ : indeed $(f^{-1} \circ g^{-1}) \circ (g \circ f) = f^{-1} \circ (g^{-1} \circ g) \circ f = f^{-1} \circ f = \id_A$ , and similarly on the other side. Hence $\cong$ is an equivalence relation on objects.

Theorem— Theorem 2 (monos and epis in Set)

In $\cat{Set}$ , a function $f : A \to B$ is a monomorphism if and only if it is injective, and an epimorphism if and only if it is surjective.

Proof

Mono $\Leftrightarrow$ injective. Suppose $f$ is injective and $f \circ g = f \circ h$ for $g, h : T \to A$ . For each $t \in T$ , $f(g(t)) = f(h(t))$ , so $g(t) = h(t)$ ; hence $g = h$ . Conversely suppose $f$ is monic and $f(a) = f(a')$ . Let $T = \{\ast\}$ be a one-element set and $g, h : T \to A$ the maps with $g(\ast) = a$ , $h(\ast) = a'$ . Then $f \circ g = f \circ h$ , so $g = h$ , so $a = a'$ .

Epi $\Leftrightarrow$ surjective. Suppose $f$ is surjective and $k \circ f = l \circ f$ for $k, l : B \to S$ . Each $b \in B$ is $f(a)$ for some $a$ , so $k(b) = k(f(a)) = l(f(a)) = l(b)$ ; hence $k = l$ . Conversely suppose $f$ is epic. Let $S = \{0, 1\}$ , let $k : B \to S$ be the indicator of the image, $k(b) = 1$ if $b = f(a)$ for some $a$ and $0$ otherwise, and let $l$ be constant at $1$ . Then $k \circ f = l \circ f$ (both are constantly $1$ ), so $k = l$ , so every $b$ is in the image.

∎

The one-element set and the two-element set did all the work: elements of $A$ are maps $\{\ast\} \to A$ , and subsets of $B$ are maps $B \to \{0, 1\}$ . That is how arrows can see inside objects in $\cat{Set}$ .

In other categories, monos and epis can behave differently. In $\cat{Grp}$ , $\cat{Vect}_k$ and $\cat{Top}$ the monomorphisms are again the injective morphisms. In $\cat{Grp}$ every epimorphism is surjective too, but the standard proof is a genuinely clever argument with permutations of the cosets of the image; we do not give it here. In rings, it fails:

Theorem— Theorem 3 (an epimorphism that is not surjective)

In $\cat{Ring}$ , the inclusion $\iota : \Z \to \Q$ is an epimorphism, but it is not surjective.

Proof

It is not surjective because $\tfrac12 \notin \Z$ .

Let $k, l : \Q \to R$ be ring homomorphisms with $k \circ \iota = l \circ \iota$ , i.e. $k(n) = l(n)$ for every integer $n$ . Take $q = a/b$ with $a, b \in \Z$ , $b \neq 0$ . In $\Q$ , $\tfrac1b \cdot b = 1 = b \cdot \tfrac1b$ , so in $R$ the element $k(\tfrac1b)$ is a two-sided inverse of $k(b)$ , and $l(\tfrac1b)$ is a two-sided inverse of $l(b) = k(b)$ . Inverses in the monoid $(R, \cdot)$ are unique (Theorem 1 for the one-object category $\mathbf{B}(R, \cdot)$ ), so $k(\tfrac1b) = l(\tfrac1b)$ . Therefore $k(q) = k(a)\,k(\tfrac1b) = l(a)\,l(\tfrac1b) = l(q)$ . So $k = l$ .

∎

The same argument shows that the inclusion of monoids $(\N, +) \to (\Z, +)$ is an epimorphism of monoids: a homomorphism out of $\Z$ is determined by its values on $\N$ , because $-n$ must go to the inverse of the image of $n$ .

Theorem— Theorem 4 (isomorphisms in monoids and preorders)

(a) In the one-object category $\mathbf{B}M$ of a monoid, a morphism $x$ is an isomorphism exactly when $x$ is a unit of $M$ . (b) In a poset regarded as a category, $x \cong y$ implies $x = y$ .

Proof

(a) An inverse of the morphism $x$ is a morphism $y$ with $y \circ x = yx = 1$ and $x \circ y = xy = 1$ : precisely a two-sided inverse in $M$ . (b) An isomorphism $x \to y$ provides morphisms $x \to y$ and $y \to x$ , that is $x \le y$ and $y \le x$ ; antisymmetry gives $x = y$ .

∎

So in $\mathbf{B}(\Z, \times)$ only $1$ and $-1$ are isomorphisms (compare the lesson on integers), and in $\mathbf{B}(\Z/n, \times)$ the isomorphisms are the residues coprime to $n$ .

Duality

Every statement about categories has a dual, obtained by reversing every arrow and every composite: " $f : A \to B$ " becomes " $f : B \to A$ ", " $g \circ f$ " becomes " $f \circ g$ ", and the rest of the statement is kept. For instance, the dual of " $f$ is a monomorphism" is " $f$ is an epimorphism", and the dual of " $A$ has exactly one morphism to every object" is "every object has exactly one morphism to $A$ ".

Theorem— Theorem 5 (the duality principle)

If a statement about objects and morphisms holds in every category, so does its dual.

Proof

A statement $\Sigma$ holds of morphisms in $\cat{C}^{\mathrm{op}}$ exactly when its dual $\Sigma^{\mathrm{op}}$ holds of the corresponding morphisms in $\cat{C}$ , because composition in $\cat{C}^{\mathrm{op}}$ is composition in $\cat{C}$ reversed. For example, $f^{\mathrm{op}}$ is monic in $\cat{C}^{\mathrm{op}}$ iff $f^{\mathrm{op}} \circ g^{\mathrm{op}} = f^{\mathrm{op}} \circ h^{\mathrm{op}} \Rightarrow g^{\mathrm{op}} = h^{\mathrm{op}}$ , i.e. iff $g \circ f = h \circ f \Rightarrow g = h$ , i.e. iff $f$ is epic in $\cat{C}$ . Now suppose $\Sigma$ holds in every category, and let $\cat{C}$ be any category. Then $\Sigma$ holds in $\cat{C}^{\mathrm{op}}$ , so $\Sigma^{\mathrm{op}}$ holds in $(\cat{C}^{\mathrm{op}})^{\mathrm{op}} = \cat{C}$ .

∎

Example— One proof, two theorems

Claim: a composite of monomorphisms is a monomorphism. If $f : A \to B$ , $g : B \to C$ are monic and $(g \circ f) \circ x = (g \circ f) \circ y$ , then $g \circ (f \circ x) = g \circ (f \circ y)$ , so $f \circ x = f \circ y$ (cancel $g$ ), so $x = y$ (cancel $f$ ).

Dual claim, for free: a composite of epimorphisms is an epimorphism. Likewise, "if $g \circ f$ is monic then $f$ is monic" dualises to "if $g \circ f$ is epic then $g$ is epic", and "every isomorphism is monic" dualises to "every isomorphism is epic".

Formal mathematicsF

Categories in Lean and Mathlib

Mathlib has a large library of category theory built on the class CategoryTheory.Category. Two conventions to know before reading the code: composition is written in diagrammatic order, f ≫ g meaning "first f, then g" (our $g \circ f$ ), and the identity on X is 𝟙 X.

Theorem 1 is the calculation of the lesson, line by line, followed by its corollary and Mathlib's version:

left_inv_eq_right_invLean 4Proved here from basic factsFormally verified

/-- **A left inverse equals a right inverse.** In any category, if `g ∘ f = id_X` and
`f ∘ h = id_Y` then `g = h`. In Mathlib's diagrammatic notation `g ∘ f` is `f ≫ g`.
The proof is the one-line calculation of the lesson:
`g = g ∘ id_Y = g ∘ (f ∘ h) = (g ∘ f) ∘ h = id_X ∘ h = h`, using only the identity and
associativity axioms. Consequently an isomorphism has exactly one inverse. -/
theorem left_inv_eq_right_inv {C : Type u} [Category.{v} C] {X Y : C} {f : X ⟶ Y}
    {g h : Y ⟶ X} (hg : f ≫ g = 𝟙 X) (hh : h ≫ f = 𝟙 Y) : g = h :=
  calc g = 𝟙 Y ≫ g := (Category.id_comp g).symm
    _ = (h ≫ f) ≫ g := by rw [hh]
    _ = h ≫ (f ≫ g) := Category.assoc h f g
    _ = h ≫ 𝟙 X := by rw [hg]
    _ = h := Category.comp_id h

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

inverse_uniqueLean 4Proved here from basic factsFormally verified

/-- **Inverses are unique.** If `g` and `g'` are both two-sided inverses of `f`, then `g = g'`.
This is `left_inv_eq_right_inv` applied to the left inverse `g` and the right inverse `g'`. -/
theorem inverse_unique {C : Type u} [Category.{v} C] {X Y : C} {f : X ⟶ Y} {g g' : Y ⟶ X}
    (hg : f ≫ g = 𝟙 X ∧ g ≫ f = 𝟙 Y) (hg' : f ≫ g' = 𝟙 X ∧ g' ≫ f = 𝟙 Y) : g = g' :=
  left_inv_eq_right_inv hg.1 hg'.2

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

inv_eq_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's version: if `f` is an isomorphism (`IsIso f`), its chosen inverse `inv f` equals
any `g` with `f ≫ g = 𝟙 X`. This applies `CategoryTheory.IsIso.inv_eq_of_hom_inv_id`. -/
theorem inv_eq_library {C : Type u} [Category.{v} C] {X Y : C} (f : X ⟶ Y) [IsIso f]
    (g : Y ⟶ X) (hg : f ≫ g = 𝟙 X) : inv f = g :=
  IsIso.inv_eq_of_hom_inv_id hg

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

The category of matrices is a genuine instance of Mathlib's class. Its objects are natural numbers (wrapped in a structure so Lean does not confuse them with the order on $\N$ ); the proofs of the axioms are the laws of matrix multiplication:

MatLean 4Formally verified

/-- The objects of the category of matrices: one object for each natural number `dim`
(a wrapper around `ℕ`, so that Lean does not confuse this category with the order on `ℕ`). -/
structure Mat where
  /-- The size of the column vectors at this object. -/
  dim : ℕ

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

matCategoryLean 4Formally verified

/-- **The category of rational matrices.** Objects are natural numbers `m, n, …`; a morphism
`m ⟶ n` is an `n × m` matrix (it turns column vectors of length `m` into vectors of length
`n`); composition is matrix multiplication (`f ≫ g = g * f`, "first `f`, then `g`") and the
identity on `n` is the identity matrix. The axioms are the associativity and unit laws of
matrix multiplication (`Matrix.mul_assoc`, `Matrix.one_mul`, `Matrix.mul_one`). The objects are
just numbers: a morphism is not a function between sets of elements. -/
instance matCategory : Category.{0} Mat where
  Hom m n := Matrix (Fin n.dim) (Fin m.dim) ℚ
  id n := (1 : Matrix (Fin n.dim) (Fin n.dim) ℚ)
  comp f g := g * f
  id_comp f := Matrix.mul_one f
  comp_id f := Matrix.one_mul f
  assoc f g h := (Matrix.mul_assoc h g f).symm

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

Mathlib already regards every preorder as a category and every monoid as a one-object category (SingleObj). We use these to check two claims of the lesson: parallel morphisms in a preorder are equal, isomorphic elements of a poset are equal, and isomorphisms in $\mathbf{B}M$ are the units of $M$ :

preorder_hom_uniqueLean 4Applies a library theoremFormally verified

/-- In a preorder regarded as a category (Mathlib's instance `Preorder.smallCategory`), there is
a morphism `x ⟶ y` exactly when `x ≤ y`, and **any two morphisms `x ⟶ y` are equal**: a morphism
carries no information beyond the fact `x ≤ y`. This applies `Subsingleton.elim` to Mathlib's
instance saying that hom-types of a preorder category are subsingletons. -/
theorem preorder_hom_unique {α : Type u} [Preorder α] {x y : α} (f g : x ⟶ y) : f = g :=
  Subsingleton.elim f g

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

preorder_iso_eqLean 4Proved here from basic factsFormally verified

/-- In a **partial order** regarded as a category, isomorphic objects are equal: an isomorphism
`x ≅ y` provides morphisms `x ⟶ y` and `y ⟶ x`, that is `x ≤ y` and `y ≤ x`, and antisymmetry
gives `x = y`. (In a preorder that is not antisymmetric, distinct objects can be isomorphic.) -/
theorem preorder_iso_eq {α : Type u} [PartialOrder α] {x y : α} (e : x ≅ y) : x = y :=
  le_antisymm (leOfHom e.hom) (leOfHom e.inv)

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

monoid_compLean 4Applies a library theoremFormally verified

/-- **A monoid is a category with one object.** Mathlib's `SingleObj M` has a single object
`star M`; its morphisms are the elements of `M`, the identity is `1` and composition is
multiplication: "first `x`, then `y`" is `y * x`. This applies `SingleObj.comp_as_mul`. -/
theorem monoid_comp (M : Type u) [Monoid M] (x y : SingleObj.star M ⟶ SingleObj.star M) :
    x ≫ y = y * x :=
  SingleObj.comp_as_mul M x y

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

monoid_isIso_iffLean 4Proved here from basic factsFormally verified

/-- In the one-object category of a monoid `M`, **the isomorphisms are exactly the invertible
elements (units) of `M`.** An inverse of the morphism `x` is an element `y` with
`x ≫ y = y * x = 1` and `y ≫ x = x * y = 1`. So "isomorphism" generalises "invertible element"
— for the monoid `(ℤ, ×)` only `1` and `-1` are isomorphisms. -/
theorem monoid_isIso_iff (M : Type u) [Monoid M] (x : SingleObj.star M ⟶ SingleObj.star M) :
    IsIso x ↔ IsUnit (show M from x) := by
  constructor
  · intro hx
    -- the inverse of `x` in the category is a two-sided inverse in the monoid
    have h1 : x * inv x = 1 := IsIso.inv_hom_id x
    have h2 : inv x * x = 1 := IsIso.hom_inv_id x
    exact ⟨⟨x, inv x, h1, h2⟩, rfl⟩
  · rintro ⟨u, hu⟩
    refine ⟨⟨(u⁻¹ : Mˣ), ?_, ?_⟩⟩
    · show (u⁻¹ : Mˣ) * x = 1
      rw [← hu, Units.inv_mul]
    · show x * (u⁻¹ : Mˣ) = 1
      rw [← hu, Units.mul_inv]

Axioms used: Classical.choiceformal/Lumenary/Categories.leanTry it in the Lean web editor

Theorem 2, for Lean types and functions (the type-theoretic counterpart of $\cat{Set}$ ). The proofs use exactly the test objects of the lesson: the one-element type PUnit, and the type of propositions (truth values) in place of $\{0, 1\}$ . Mathlib's category Type u wraps its morphisms in a structure, and it proves the same facts there:

mono_iff_injectiveLean 4Proved here from basic factsFormally verified

/-- **In sets, the monomorphisms are the injections.** A function `f : X → Y` is a
monomorphism if it can be cancelled on the left: `f ∘ g = f ∘ h` implies `g = h` for all
`g, h : Z → X`. (Stated here for Lean types and functions, the type-theoretic version of
**Set**.) If `f` is a monomorphism and `f a = f b`, test it against the two maps from a
one-element set picking out `a` and `b`; conversely an injection can be cancelled pointwise. -/
theorem mono_iff_injective {X Y : Type u} (f : X → Y) :
    (∀ (Z : Type u) (g h : Z → X), f ∘ g = f ∘ h → g = h) ↔ Function.Injective f := by
  constructor
  · intro hf a b hab
    -- test maps from the one-element type `PUnit`
    have := hf PUnit (fun _ => a) (fun _ => b) (funext fun _ => hab)
    exact congrFun this PUnit.unit
  · intro hf Z g h hgh
    funext z
    exact hf (congrFun hgh z)

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

epi_iff_surjectiveLean 4Proved here from basic factsFormally verified

/-- **In sets, the epimorphisms are the surjections.** A function `f : X → Y` is an
epimorphism if `g ∘ f = h ∘ f` implies `g = h` for all `g, h : Y → Z`.
If `f` is an epimorphism, compare two maps into the two-element "set of truth values":
`g y = (y is in the image of f)` and `h y = true`. They agree after `f`, so they agree, so every
`y` is in the image. Conversely, if `f` is surjective, every `y` is some `f x`, where `g` and `h`
agree. (`ULift` only moves the type of propositions into the universe of `Y`.) -/
theorem epi_iff_surjective {X Y : Type u} (f : X → Y) :
    (∀ (Z : Type u) (g h : Y → Z), g ∘ f = h ∘ f → g = h) ↔ Function.Surjective f := by
  constructor
  · intro hf y
    let g : Y → ULift.{u} Prop := fun y => ULift.up (∃ x, f x = y)
    let h : Y → ULift.{u} Prop := fun _ => ULift.up True
    have hgh : g ∘ f = h ∘ f := by
      funext x
      simp only [Function.comp, g, h, ULift.up.injEq, eq_iff_iff, iff_true]
      exact ⟨x, rfl⟩
    have hy : g y = h y := congrFun (hf _ g h hgh) y
    simp only [g, h, ULift.up.injEq, eq_iff_iff, iff_true] at hy
    exact hy
  · intro hf Z g h hgh
    funext y
    obtain ⟨x, rfl⟩ := hf y
    exact congrFun hgh x

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

types_mono_epi_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's versions for its category `Type u` (whose morphisms wrap functions): a morphism is
a monomorphism iff it is injective and an epimorphism iff it is surjective. This applies
`CategoryTheory.mono_iff_injective` and `CategoryTheory.epi_iff_surjective`. -/
theorem types_mono_epi_library {X Y : Type u} (f : X ⟶ Y) :
    (Mono f ↔ Function.Injective f) ∧ (Epi f ↔ Function.Surjective f) :=
  ⟨CategoryTheory.mono_iff_injective f, CategoryTheory.epi_iff_surjective f⟩

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

Theorem 3: the independent proof follows the lesson (inverses are unique), then states the result as an epimorphism in Mathlib's category RingCat. Mathlib knows something stronger — any two ring homomorphisms out of $\Q$ are equal — because they automatically agree on $\Z$ :

rat_hom_eq_of_eq_on_intLean 4Proved here from basic factsFormally verified

/-- **The inclusion `ℤ → ℚ` is an epimorphism of rings**: two ring homomorphisms
`f, g : ℚ → R` that agree on the integers agree everywhere.
Proof, as in the lesson: write `q = a / b` with `b ≠ 0`. In `R`, `f (1/b)` is a two-sided
inverse of `f b`, and `g (1/b)` is a two-sided inverse of `g b = f b`; inverses in a monoid are
unique (Mathlib's monoid lemma `left_inv_eq_right_inv`), so `f (1/b) = g (1/b)`, and then
`f q = f a · f (1/b) = g a · g (1/b) = g q`. -/
theorem rat_hom_eq_of_eq_on_int {R : Type u} [Ring R] (f g : ℚ →+* R)
    (h : ∀ n : ℤ, f n = g n) : f = g := by
  ext q
  have hb : (q.den : ℚ) ≠ 0 := by exact_mod_cast q.den_nz
  -- `f (1/b)` and `g (1/b)` are inverses of the same element `f b = g b`
  have hfb : f (q.den : ℚ) = g (q.den : ℚ) := by
    exact_mod_cast h q.den
  have hinv : f (q.den : ℚ)⁻¹ = g (q.den : ℚ)⁻¹ := by
    have left : f (q.den : ℚ)⁻¹ * f (q.den : ℚ) = 1 := by
      rw [← map_mul, inv_mul_cancel₀ hb, map_one]
    have right : g (q.den : ℚ) * g (q.den : ℚ)⁻¹ = 1 := by
      rw [← map_mul, mul_inv_cancel₀ hb, map_one]
    rw [hfb] at left
    exact _root_.left_inv_eq_right_inv left right
  calc f q = f ((q.num : ℚ) * (q.den : ℚ)⁻¹) := by rw [← div_eq_mul_inv, Rat.num_div_den]
    _ = f q.num * f (q.den : ℚ)⁻¹ := by rw [map_mul]
    _ = g q.num * g (q.den : ℚ)⁻¹ := by rw [h q.num, hinv]
    _ = g ((q.num : ℚ) * (q.den : ℚ)⁻¹) := by rw [map_mul]
    _ = g q := by rw [← div_eq_mul_inv, Rat.num_div_den]

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

int_to_rat_epiLean 4Proved here from basic factsFormally verified

/-- The same fact stated in Mathlib's category `RingCat` of rings: the morphism
`ℤ ⟶ ℚ` given by the inclusion is an epimorphism (`Epi`). Two morphisms `g, h : ℚ ⟶ R` with
`ι ≫ g = ι ≫ h` agree on every integer `n`, so `rat_hom_eq_of_eq_on_int` makes them equal. -/
theorem int_to_rat_epi : Epi (RingCat.ofHom (Int.castRingHom ℚ)) := by
  constructor
  intro R g h hgh
  apply RingCat.hom_ext
  apply rat_hom_eq_of_eq_on_int
  intro n
  have := congrArg (fun φ => φ.hom n) hgh
  simp only [RingCat.hom_comp, RingCat.hom_ofHom, RingHom.comp_apply, Int.coe_castRingHom]
    at this
  exact this

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

rat_hom_ext_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's stronger statement: *any* two ring homomorphisms from `ℚ` to a semiring are equal
(they automatically agree on `ℤ`). This applies `RingHom.ext_rat`. -/
theorem rat_hom_ext_library {R : Type u} [Semiring R] (f g : ℚ →+* R) : f = g :=
  RingHom.ext_rat f g

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

int_cast_not_surjectiveLean 4Proved here from basic factsFormally verified

/-- …but the inclusion `ℤ → ℚ` is **not surjective**: `1/2` is not an integer. If `n = 1/2` in
`ℚ`, then `2n = 1` in `ℚ`, hence in `ℤ`, which is impossible for an integer `n`. So in the
category of rings, epimorphisms need not be surjective. -/
theorem int_cast_not_surjective : ¬ Function.Surjective (Int.cast : ℤ → ℚ) := by
  intro hsurj
  obtain ⟨n, hn⟩ := hsurj (1 / 2)
  have h2 : ((2 * n : ℤ) : ℚ) = 1 := by
    push_cast
    rw [hn]
    norm_num
  have h3 : 2 * n = 1 := by exact_mod_cast h2
  omega

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

Finally, composites of monos, and duality: f.op is the morphism of the opposite category Cᵒᵖ corresponding to f.

mono_compLean 4Proved here from basic factsFormally verified

/-- **A composite of monomorphisms is a monomorphism.** If `f : X ⟶ Y` and `g : Y ⟶ Z` are
monomorphisms and `a ≫ (f ≫ g) = b ≫ (f ≫ g)`, then `(a ≫ f) ≫ g = (b ≫ f) ≫ g`, so cancelling
`g` gives `a ≫ f = b ≫ f`, and cancelling `f` gives `a = b`. By duality (reverse every arrow)
the same proof shows that a composite of epimorphisms is an epimorphism. -/
theorem mono_comp {C : Type u} [Category.{v} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : Mono f) (hg : Mono g) : Mono (f ≫ g) := by
  constructor
  intro W a b hab
  have h1 : (a ≫ f) ≫ g = (b ≫ f) ≫ g := by
    rw [Category.assoc, Category.assoc]
    exact hab
  have h2 : a ≫ f = b ≫ f := hg.right_cancellation _ _ h1
  exact hf.right_cancellation _ _ h2

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

epi_comp_libraryLean 4Applies a library theoremFormally verified

/-- The dual statement, as Mathlib states it: a composite of epimorphisms is an epimorphism.
This applies the instance `CategoryTheory.epi_comp`. -/
theorem epi_comp_library {C : Type u} [Category.{v} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
    [Epi f] [Epi g] : Epi (f ≫ g) :=
  epi_comp f g

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

mono_iff_epi_opLean 4Proved here from basic factsFormally verified

/-- **Duality.** A morphism `f : X ⟶ Y` of `C` is a monomorphism exactly when the corresponding
morphism `f.op : Y ⟶ X` of the opposite category `Cᵒᵖ` is an epimorphism. Composition in `Cᵒᵖ`
is composition in `C` reversed (`(g ≫ f).op = f.op ≫ g.op`), so "cancellable on the left" in
`C` is literally "cancellable on the right" in `Cᵒᵖ`. -/
theorem mono_iff_epi_op {C : Type u} [Category.{v} C] {X Y : C} (f : X ⟶ Y) :
    Mono f ↔ Epi f.op := by
  constructor
  · intro hf
    constructor
    intro Z g h hgh
    -- `f.op ≫ g = (g.unop ≫ f).op`
    apply Quiver.Hom.unop_inj
    apply hf.right_cancellation
    exact Quiver.Hom.op_inj (by simp at hgh ⊢; exact hgh)
  · intro hf
    constructor
    intro Z g h hgh
    apply Quiver.Hom.op_inj
    apply hf.left_cancellation
    simpa using congrArg Quiver.Hom.op hgh

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

op_epi_iff_libraryLean 4Applies a library theoremFormally verified

/-- Mathlib's version of the same duality, `CategoryTheory.op_epi_iff`. -/
theorem op_epi_iff_library {C : Type u} [Category.{v} C] {X Y : C} (f : X ⟶ Y) :
    Epi f.op ↔ Mono f :=
  CategoryTheory.op_epi_iff f

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

What is not formalised here: the duality principle as a single meta-theorem about all statements (it is a statement about the language we use, and Lean expresses each instance separately), and the theorem that epimorphisms of groups are surjective.

ComputationC

Deciding mono and epi by brute force

The definitions of monomorphism and epimorphism quantify over every test object $T$ . For finite sets a computer can simply try them. The experiment below lists every function between sets with at most three elements, tests both cancellation properties against every map from or to a set with at most two elements, and compares the results with injectivity and surjectivity. It also asks which test sets are needed — and finds the one-element and two-element sets of the proof.

Monos and epis in finite sets, by brute forcePythonExact computationExhaustive finite checkComputationally tested

"""Monomorphisms and epimorphisms in finite sets, decided by brute force.

A function f : A -> B is a monomorphism if f . g = f . h forces g = h for
all maps g, h : T -> A, and an epimorphism if g . f = h . f forces g = h
for all maps g, h : B -> T. Both definitions quantify over *every* test
set T. This experiment enumerates every function between sets with at most
three elements, tests the definitions against all test sets with at most
two elements, and compares the answers with injectivity and surjectivity.
It also shows which test sets are needed: a one-element T already detects
monos, but epis need a two-element T. The evidence is exhaustive for these
small sets; the lesson's proof covers all sets.
"""

from itertools import product

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

def compose(g, f):
    """The composite g . f of tuples: first f, then g."""
    return tuple(g[x] for x in f)

def is_mono(f, n, test_sizes):
    """Is f : m -> n left-cancellable against maps from sets of these sizes?"""
    m = len(f)
    for t in test_sizes:
        maps = functions(t, m)
        for g in maps:
            for h in maps:
                if g != h and compose(f, g) == compose(f, h):
                    return False
    return True

def is_epi(f, n, test_sizes):
    """Is f : m -> n right-cancellable against maps to sets of these sizes?"""
    for t in test_sizes:
        maps = functions(n, t)
        for g in maps:
            for h in maps:
                if g != h and compose(g, f) == compose(h, f):
                    return False
    return True

def is_injective(f):
    """No two inputs share an output."""
    return len(set(f)) == len(f)

def is_surjective(f, n):
    """Every element of {0..n-1} is a value."""
    return set(f) == set(range(n))

def tally(m, n, test_sizes=(0, 1, 2)):
    """Counts (functions, monos, injections, epis, surjections) for m -> n."""
    fs = functions(m, n)
    return (
        len(fs),
        sum(is_mono(f, n, test_sizes) for f in fs),
        sum(is_injective(f) for f in fs),
        sum(is_epi(f, n, test_sizes) for f in fs),
        sum(is_surjective(f, n) for f in fs),
    )

def main():
    print("|A| |B|  maps  monos  injective  epis  surjective")
    agree = True
    for m in range(4):
        for n in range(4):
            total, mono, inj, epi, surj = tally(m, n)
            agree = agree and mono == inj and epi == surj
            print(f"{m:>3} {n:>3} {total:>5} {mono:>6} {inj:>10}"
                  f" {epi:>5} {surj:>11}")
    print(f"monos = injections and epis = surjections: {agree}")
    print()
    print("Which test sets T are needed?")
    fake = sum(is_epi(f, 3, (1,)) for f in functions(2, 3))
    print(f"  with |T| = 1 only, {fake} of the 9 maps 2 -> 3 pass the epi test,")
    print("  although none of them is surjective")
    ok = all(is_mono(f, 3, (1,)) == is_injective(f) for f in functions(3, 3))
    print(f"  |T| = 1 already decides mono for all 27 maps 3 -> 3: {ok}")
    print()
    print("Epistemic status: exhaustive and exact for sets with at most three")
    print("elements, testing against all sets with at most two elements. It is")
    print("evidence, not proof, that the pattern continues; the lesson proves")
    print("mono = injective and epi = surjective for all sets, using a")
    print("one-element and a two-element test set exactly as found here.")

if __name__ == "__main__":
    main()

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

This is exhaustive evidence for small sets, not a proof for all sets. But notice what it suggests and what the proof confirms: one-element test sets suffice for monos, while epis need a two-element test set (against one-element test sets every function looks epic).

Explore

Explore: paths compose

Build composites along paths in a small diagram of finite sets. Choose arrows one after another; the widget refuses a step when the arrows do not line up (the target of one must be the source of the next). Compare the two bracketings of $h \circ g \circ f$ , and insert identities anywhere in a path to see that nothing changes. Then ask yourself which of the arrows are monomorphisms or epimorphisms of $\cat{Set}$ .

Arrows that compose

Click arrows to build a path. Every path composes to a single arrow — and brackets never matter.

Your composite

Start by clicking any arrow.

Two ways to bracket h ∘ g ∘ f

x	(g∘f)(x)	h((g∘f)(x))	(h∘g)(f(x))
1	x	1	1
2	z	0	0
3	x	1	1

The last two columns always agree: h ∘ (g ∘ f) = (h ∘ g) ∘ f. That is associativity.

Exercises

1. Categories

Warm-upHuman

Which of these are categories (with the obvious composition)? Choose all that apply.

Choose all that apply

Objects: positive integers. One morphism

m \to n

exactly when

m

divides

n

.Objects: integers. One morphism

m \to n

exactly when

m < n

.Objects: sets. Morphisms: injective functions.Objects: sets. Morphisms: functions that are at most two-to-one.Objects: natural numbers. Morphisms

m \to n

n \times m

real matrices, composed by multiplication.

2. Categories

Warm-upHuman

Regard the set $\{1, 2, 3, 6\}$ , ordered by divisibility, as a category. How many morphisms does it have in total, including the identities?

3. Categories

CoreHuman

Let $M = (\mathbb{Z}/12, \times, 1)$ be the monoid of residues modulo $12$ under multiplication, and $\mathbf{B}M$ its one-object category. How many of the $12$ morphisms of $\mathbf{B}M$ are isomorphisms?

4. Categories

CoreHuman

In the proof that a left inverse $g$ and a right inverse $h$ of $f : A \to B$ are equal, $g = g \circ \mathrm{id}_B = g \circ (f \circ h) = (g \circ f) \circ h = \mathrm{id}_A \circ h = h,$ which axiom justifies the step $g \circ (f \circ h) = (g \circ f) \circ h$ ?

Choose one

Associativity of compositionThe unit lawsCommutativity of compositionThe hypothesis

f \circ h = \mathrm{id}_B

5. Categories

CoreHuman

Which of these are epimorphisms that are not surjective? Choose all that apply.

Choose all that apply

The inclusion

\mathbb{Z} \to \mathbb{Q}

in the category of ringsThe inclusion

(\mathbb{N}, +) \to (\mathbb{Z}, +)

in the category of monoidsThe inclusion

\{0\} \to \{0, 1\}

\mathbf{Set}

The homomorphism

n \mapsto 2n

from

(\mathbb{Z}, +)

(\mathbb{Z}, +)

in the category of groups

6. Categories

CoreHuman

Theorem: in every category, if $g \circ f$ is a monomorphism then $f$ is a monomorphism. What does the duality principle give us for free?

Choose one

g \circ f

is an epimorphism then

g

is an epimorphism.If

g \circ f

is an epimorphism then

f

is an epimorphism.If

f

is a monomorphism then

g \circ f

is a monomorphism.If

g \circ f

is an isomorphism then

f

is an isomorphism.

7. Categories

CoreFormal

Mathlib writes composition in diagrammatic order: a ≫ f means "first a, then f", i.e. $f \circ a$ . Which statement says that f : X ⟶ Y is a monomorphism?

Choose one

∀ (T : C) (a b : T ⟶ X), a ≫ f = b ≫ f → a = b∀ (T : C) (a b : Y ⟶ T), f ≫ a = f ≫ b → a = b∀ x y : X, f x = f y → x = y∃ g : Y ⟶ X, f ≫ g = 𝟙 X

8. Categories

StretchComputational

A function between finite sets $\{0, \dots, m-1\} \to \{0, \dots, n-1\}$ is stored as a tuple f of length $m$ with values in range(n). Write is_epi(f, n) that decides whether f is an epimorphism directly from the definition, by testing cancellation against all pairs of maps $k, l : \{0, \dots, n-1\} \to \{0, 1\}$ (that is, k ∘ f == l ∘ f must force k == l). Do not test surjectivity directly!

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

Common misconceptionsH

Common misconceptions

Misconception

"Morphisms are functions." In many categories they are, but not in general. In a poset regarded as a category, a morphism $x \to y$ is just the fact that $x \le y$ ; in $\cat{Mat}_k$ it is a matrix; in the category of a monoid it is an element. Definitions must use only composition and identities.

Misconception

"Epimorphisms are surjective." True in $\cat{Set}$ and $\cat{Grp}$ , false in general: the inclusion $\Z \to \Q$ is an epimorphism of rings, and $\N \to \Z$ an epimorphism of monoids. Being epic means being cancellable on the right, nothing more.

Misconception

"Objects have elements." The objects of $\cat{Mat}_k$ are numbers and the single object of $\mathbf{B}M$ is a placeholder. Even in $\cat{Set}$ , category theory recovers elements of $A$ only as morphisms $\{\ast\} \to A$ .

Misconception

"Monic and epic means isomorphism." In $\cat{Set}$ yes (a bijection has an inverse function). But in the category $\mathbf{2} = \{0 \to 1\}$ the arrow $0 \to 1$ is monic and epic and not invertible, and in $\cat{Ring}$ the inclusion $\Z \to \Q$ is monic and epic and not an isomorphism.

Misconception

"Being an isomorphism is a property of the underlying function." It depends on the category. The identity map from $\R$ with the discrete topology to $\R$ with the usual topology is a continuous bijection — an isomorphism in $\cat{Set}$ — but not an isomorphism in $\cat{Top}$ , because its inverse is not continuous.

ViewpointsH

Many ways of seeing

Topology— Homeomorphisms, and paths as morphisms

In $\cat{Top}$ the isomorphisms are the homeomorphisms: continuous bijections whose inverses are continuous. The extra condition matters. The map $t \mapsto (\cos 2\pi t, \sin 2\pi t)$ from $[0, 1)$ to the circle $S^1$ is a continuous bijection, but $[0, 1)$ and $S^1$ are not homeomorphic: removing any point disconnects $[0, 1)$ unless it is the endpoint $0$ , while removing any point of $S^1$ leaves it connected — and connectedness of complements is preserved by homeomorphisms. So "isomorphic" means "the same as objects of this category", and topology needs its own notion.

Topology also supplies categories whose morphisms are not maps at all. In the fundamental groupoid $\Pi_1(X)$ of a space, the objects are the points of $X$ and a morphism $x \to y$ is a path from $x$ to $y$ up to homotopy with fixed ends; composition is "follow one path, then the other". Associativity holds only up to homotopy for actual paths — which is why one passes to homotopy classes — and every morphism is invertible (run the path backwards). The automorphisms of a point $x$ form the fundamental group $\pi_1(X, x)$ : see homotopy and the fundamental group.

Geometry— Groups are one-object categories of symmetries

A group is a category with one object in which every morphism is invertible. Geometrically, think of the object as a shape and the morphisms as its symmetries: for a square, the eight rotations and reflections of the dihedral group $D_4$ , composed by doing one motion after another. Klein's Erlangen programme (1872) organised geometry by groups of transformations: Euclidean geometry studies what is invariant under isometries, affine geometry what is invariant under affine maps, projective geometry under projective maps. Category theory generalises this from one shape and its symmetries to many shapes and the structure-preserving maps between them — see transformation geometry.

Algebra— Matrices are the category of finite-dimensional vector spaces

Choosing a basis of each finite-dimensional vector space identifies a linear map $k^m \to k^n$ with an $n \times m$ matrix and composition of linear maps with matrix multiplication. So the category $\cat{Mat}_k$ , whose objects are mere numbers, captures all of finite-dimensional linear algebra: every finite-dimensional space is isomorphic to some $k^n$ , and the isomorphisms $n \to n$ form the general linear group $\mathrm{GL}_n(k)$ . (Making "captures" precise needs the notion of an equivalence of categories, a later topic.) Algebra is full of such recognitions: monoids are one-object categories, groups are one-object categories with inverses, and a ring is a one-object category whose hom-set is an abelian group with bilinear composition — a preadditive category with one object — which is the starting point of the categorical approach to homological algebra.

Logic— Propositions and proofs

Logical propositions ordered by entailment form a preorder, hence a category: there is a morphism $P \to Q$ when $Q$ follows from $P$ , identities are " $P$ entails $P$ ", and composition is chaining entailments. Refining this, one can keep track of which proof shows $Q$ from $P$ : propositions as objects, proofs (up to a suitable equivalence) as morphisms, composition as substituting one proof into another. This is the beginning of categorical logic and of the Curry–Howard–Lambek correspondence between proofs, programs and morphisms of cartesian closed categories — see categorical logic.

Computation— Types and programs compose

In a typed programming language, take the types as objects and the (total, side-effect-free) functions between them as morphisms; composition is running one function on the output of another, and the identity function returns its input. This is why many functional programming languages put composition (. in Haskell, >> in F#) at the centre, and why notions such as functors and monads moved from category theory into programming. The analogy has honest limits: real programs may loop forever or have side effects, so the actual category of a language must be defined with care.

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, 1913) and Saunders Mac Lane (born in Connecticut, 1909) introduced categories, functors and natural transformations in "General theory of natural equivalences" (Transactions of the AMS, 1945). Their goal was to make precise the word "natural" in algebraic topology; categories were introduced, as they later said, to be able to define functors, and functors to define natural transformations.
In the 1950s category theory became a working language. Eilenberg and Norman Steenrod axiomatised homology theory with it (announced 1945, in book form 1952); Alexander Grothendieck's "Tôhoku paper" (1957) introduced abelian categories to unify sheaf cohomology and homological algebra; Daniel Kan (1958) introduced adjoint functors.
F. William Lawvere's thesis (1963) and later work used categories as a foundation for algebra and logic; topos theory followed (Lawvere and Myles Tierney, around 1970). Major schools developed in many places, among them the Sydney school of Max Kelly and Ross Street, and Montreal, Louvain-la-Neuve and Genoa.
Mac Lane's Categories for the Working Mathematician (1971) became the standard reference. Today categories are used across algebra, topology, logic, computer science and mathematical physics.

The same pattern, again and again

Dots, arrows and paths

Definitions

Examples, and some non-examples

Isomorphisms, monos and epis

Duality

Categories in Lean and Mathlib

Deciding mono and epi by brute force

Explore: paths compose

Exercises

Common misconceptions

Many ways of seeing

Wonder Trails

History and global context

Further reading