Limits and colimits · The Lumenary

MotivationH

Solving, intersecting, gluing, approximating

Here are some constructions from across mathematics.

The solution set $\{x \in X : f(x) = g(x)\}$ of an equation between two maps.
The kernel of a homomorphism, and the intersection of two subgroups or subspaces.
The preimage $f^{-1}(B')$ of a subset, and the fibre product $\{(a, b) : f(a) = g(b)\}$ .
The $p$ -adic integers, built from the rings $\Z/p\Z \leftarrow \Z/p^2\Z \leftarrow \Z/p^3\Z \leftarrow \cdots$ by taking all compatible sequences of residues.
Quotients $Y/{\sim}$ , the sphere obtained by gluing two discs along their boundary circles, the rationals as a union of the groups $\frac{1}{n}\Z$ .

The first four "carve out" a piece of a product by equations; the last group "glues" pieces of a disjoint union together. Category theory shows that each of them is a limit or a colimit — one universal property, applied to diagrams of different shapes. The payoff is threefold: one proof of uniqueness for all of them; one theorem constructing all of them from two basic ones (products and equalisers); and a precise way to say which constructions a functor respects. That last point already decides questions such as whether a functor can have an adjoint, the subject of the next lesson.

IntuitionH

Cones: compatible families, everywhere at once

A diagram is a picture of objects and arrows in a category — a cospan $A \to C \leftarrow B$ , a parallel pair $X \rightrightarrows Y$ , a tower $\cdots \to D_3 \to D_2 \to D_1$ . A cone over the diagram is an object $X$ with one arrow to each object of the diagram, compatible with all the arrows of the diagram: whichever path you follow from $X$ to an object, you get the same arrow. The limit is the best cone: every other cone factors through it in exactly one way.

In $\cat{Set}$ , take $X = \{\ast\}$ . A cone from the one-point set is just a choice of one element in each object of the diagram, compatible with all the arrows — a compatible family. So the limit of a diagram of sets is the set of compatible families. For the cospan $A \xrightarrow{f} C \xleftarrow{g} B$ , a compatible family is $(a, b, c)$ with $f(a) = c = g(b)$ : the fibre product. For the tower of rings $\Z/p^n\Z$ , it is a sequence of residues, each reducing to the previous one: a $p$ -adic integer.

Colimits reverse every arrow. A cocone is an object receiving an arrow from every object of the diagram, compatibly, and the colimit is the best cocone. In $\cat{Set}$ it is the disjoint union of all the objects, with $x$ glued to $D(u)(x)$ for every arrow $u$ of the diagram.

Limits carve out, colimits glue together.

DefinitionsH

Definitions

Throughout, $\mathcal{C}$ is a category and $\mathcal{J}$ a small category, the shape. Composition is written $g \circ f$ .

Definition— diagram

A diagram of shape $\mathcal{J}$ in $\mathcal{C}$ is a functor $D : \mathcal{J} \to \mathcal{C}$ . For an object $X$ of $\mathcal{C}$ , the constant diagram $\Delta X : \mathcal{J} \to \mathcal{C}$ sends every object to $X$ and every arrow to $\mathrm{id}_X$ .

Definition— cone and limit

A cone over $D$ with apex $X$ is a natural transformation $\lambda : \Delta X \Rightarrow D$ . Concretely: arrows $\lambda_j : X \to D(j)$ , one for each object $j$ of $\mathcal{J}$ , with $D(u) \circ \lambda_i = \lambda_j$ for every arrow $u : i \to j$ of $\mathcal{J}$ . A morphism of cones $(X, \lambda) \to (X', \lambda')$ is an arrow $h : X \to X'$ with $\lambda'_j \circ h = \lambda_j$ for all $j$ . A limit of $D$ is a terminal object $(\lim D, \pi)$ of the category of cones: for every cone $(X, \lambda)$ there is a unique $h : X \to \lim D$ with $\pi_j \circ h = \lambda_j$ for all $j$ .

A cone

\lambda

with apex

X

factors uniquely through the limit cone

\pi

; all triangles commute.

Definition— cocone and colimit

A cocone under $D$ is a natural transformation $D \Rightarrow \Delta Y$ , and a colimit $\operatorname{colim} D$ is an initial cocone. Equivalently, a colimit of $D$ is a limit of $D^{\mathrm{op}} : \mathcal{J}^{\mathrm{op}} \to \mathcal{C}^{\mathrm{op}}$ .

Definition— the basic shapes

shape $\mathcal{J}$	limit	colimit
no objects	terminal object	initial object
two objects, no arrows	product $A \times B$	coproduct $A \sqcup B$
parallel pair $\bullet \rightrightarrows \bullet$	equaliser of $f, g$	coequaliser of $f, g$
cospan $\bullet \to \bullet \leftarrow \bullet$	pullback $A \times_C B$	—
span $\bullet \leftarrow \bullet \to \bullet$	—	pushout $A \sqcup_C B$
tower $\cdots \to \bullet \to \bullet$ ( $\N^{\mathrm{op}}$ )	inverse limit $\varprojlim D_n$	—
chain $\bullet \to \bullet \to \cdots$ ( $\N$ )	—	direct (sequential) limit $\varinjlim D_n$

Unpacked, an equaliser of $f, g : X \to Y$ is an arrow $e : E \to X$ with $f e = g e$ such that every $h : W \to X$ with $f h = g h$ factors as $h = e \circ k$ for a unique $k$ . (The leg to $Y$ is forced to be $f e = g e$ .) A pullback of $f : A \to C$ and $g : B \to C$ is an object $P$ with $p_1 : P \to A$ , $p_2 : P \to B$ , $f p_1 = g p_2$ , through which every such commuting square factors uniquely:

The pullback: every pair

a, b

with

f a = g b

factors through

A \times_C B

by a unique

u

.

Definition— complete, cocomplete, preservation

$\mathcal{C}$ is complete if every diagram of every small shape has a limit, and cocomplete if every such diagram has a colimit. A functor $F : \mathcal{C} \to \mathcal{D}$ preserves a limit $(\lim D, \pi)$ if $(F(\lim D), F\pi)$ is a limit of $F \circ D$ ; it preserves limits if it preserves every limit that exists. Preservation of colimits is defined dually.

Worked examplesH

Examples

Example— Limits and colimits of sets

For $D : \mathcal{J} \to \cat{Set}$ ,

\lim D = \Big\{ (x_j) \in \prod_j D(j) \;:\; D(u)(x_i) = x_j \text{ for all } u : i \to j \Big\}, \qquad \operatorname{colim} D = \Big( \bigsqcup_j D(j) \Big) \Big/ {\sim},

where $\sim$ is the equivalence relation generated by $x \sim D(u)(x)$ for $x \in D(i)$ , $u : i \to j$ . The equaliser of $f, g : X \to Y$ is $\{x : f(x) = g(x)\}$ ; the pullback of $f, g$ is $\{(a, b) \in A \times B : f(a) = g(b)\}$ ; the coequaliser of $f, g$ is $Y$ modulo the equivalence relation generated by $f(x) \sim g(x)$ ; the pushout of $A \xleftarrow{f} C \xrightarrow{g} B$ is $A \sqcup B$ with $f(c)$ glued to $g(c)$ .

Example— Special pullbacks: preimages and intersections

If $m : B' \hookrightarrow B$ is the inclusion of a subset and $f : A \to B$ , the pullback of $m$ along $f$ is $\{(a, b') : f(a) = b'\} \cong f^{-1}(B')$ . If $A', B' \subseteq X$ , the pullback of the two inclusions is $A' \cap B'$ . In $\cat{Grp}$ the kernel of $\varphi : G \to H$ is the equaliser of $\varphi$ and the trivial homomorphism, and also the pullback of $\varphi$ along $1 \to H$ .

Example— Groups and spaces

In $\cat{Grp}$ , limits are computed as in $\cat{Set}$ : the equaliser of $\varphi, \psi : G \to H$ is the subgroup $\{g : \varphi(g) = \psi(g)\}$ , the pullback is the subgroup $\{(a, b) : \varphi(a) = \psi(b)\}$ of $A \times B$ . Colimits are not: the coequaliser of $\varphi, \psi$ is $H / N$ , where $N$ is the normal subgroup generated by the elements $\varphi(g)\psi(g)^{-1}$ , and the pushout of $A \leftarrow C \to B$ is the amalgamated free product $A *_C B$ . In $\cat{Top}$ , limits carry the coarsest topology making the legs continuous (subspaces of products), and colimits the finest making the legs continuous (quotients of disjoint unions): the pushout of $D^2 \hookleftarrow S^1 \hookrightarrow D^2$ is the sphere $S^2$ , and the coequaliser identifying the endpoints of $[0, 1]$ is the circle.

Example— Inverse limits

The $p$ -adic integers: $\Z_p = \varprojlim \Z/p^n\Z$ , the set of sequences $(x_n)$ with $x_n \in \Z/p^n\Z$ and $x_{n+1} \equiv x_n \pmod{p^n}$ , with componentwise ring operations. In $\Z_5$ , $-1 = (4, 24, 124, \dots)$ ; in $\Z_2$ , $\tfrac13 = (1, 3, 3, 11, 11, 43, \dots)$ because $3 \cdot 11 = 33 \equiv 1 \pmod{16}$ .
The Cantor set is homeomorphic to $\varprojlim \{0,1\}^n$ (finite discrete spaces, truncation maps), i.e. to $\{0,1\}^{\N}$ with the product topology.
The profinite integers $\widehat{\Z} = \varprojlim_n \Z/n\Z$ , over the positive integers ordered by divisibility; by the Chinese remainder theorem $\widehat{\Z} \cong \prod_p \Z_p$ .

The tower $\cdots \to \Z/8 \to \Z/4 \to \Z/2 \to \Z/1$ drawn as a tree: each residue mod $2^n$ has two lifts mod $2^{n+1}$. A $2$-adic integer is an infinite path from the root; the highlighted path $1, 3, 3, \dots$ is $\tfrac13$.

Example— Direct limits

$\Z[\tfrac1p] = \varinjlim (\Z \xrightarrow{p} \Z \xrightarrow{p} \Z \to \cdots)$ : the $n$ -th copy of $\Z$ is $p^{-n}\Z \subset \Q$ .
The Prüfer group $\Z(p^\infty) = \varinjlim (\Z/p \xrightarrow{p} \Z/p^2 \xrightarrow{p} \Z/p^3 \to \cdots) \cong \Z[\tfrac1p]/\Z$ , the group of $p$ -power roots of unity.
$\Q$ is the colimit of the groups $\frac1n \Z$ over the positive integers ordered by divisibility. In a poset, a colimit of an increasing sequence is its supremum.

ProofH

Theorems and proofs

Theorem— Theorem 1 (uniqueness)

If $(L, \pi)$ and $(L', \pi')$ are limits of $D$ , there is a unique isomorphism $\varphi : L \to L'$ with $\pi'_j \circ \varphi = \pi_j$ for all $j$ . Dually for colimits.

Proof

Both are terminal objects of the category of cones over $D$ , and terminal objects are unique up to unique isomorphism: the unique cone morphisms $\varphi : L \to L'$ and $\psi : L' \to L$ compose to cone endomorphisms of $L$ and $L'$ , which must be the identities by uniqueness. (This is the argument for products in the previous lesson, now for every shape at once.)

∎

Theorem— Theorem 2 (Set is complete and cocomplete)

The formulas in the first example are a limit and a colimit of $D : \mathcal{J} \to \cat{Set}$ for every small $\mathcal{J}$ , with legs the projections $\pi_j$ and the maps $\iota_j : D(j) \to \operatorname{colim} D$ , $x \mapsto [x]$ .

Proof

Limit. The projections form a cone because $D(u)(x_i) = x_j$ for elements of $\lim D$ . Given a cone $(X, \lambda)$ , each $x \in X$ gives a compatible family $(\lambda_j(x))_j$ , so $h(x) = (\lambda_j(x))_j$ defines $h : X \to \lim D$ with $\pi_j h = \lambda_j$ ; and any such $h$ must have $j$ -th coordinate $\lambda_j(x)$ . Colimit. $\iota_j(x) = [x]$ is a cocone since $[x] = [D(u)(x)]$ . Given a cocone $\mu_j : D(j) \to Y$ , define $k[x] = \mu_j(x)$ for $x \in D(j)$ ; this is well defined because the relation $\{(x, y) : \mu(x) = \mu(y)\}$ is an equivalence relation containing the generating pairs $x \sim D(u)(x)$ (as $\mu_j \circ D(u) = \mu_i$ ), hence containing $\sim$ . Uniqueness: $k$ is determined on every class $[x]$ .

∎

Theorem— Theorem 3 (limits from products and equalisers)

If $\mathcal{C}$ has all small products and all equalisers, then $\mathcal{C}$ has all small limits. Explicitly, for $D : \mathcal{J} \to \mathcal{C}$ , let

s, t : \prod_{j \in \mathrm{Ob}\,\mathcal{J}} D(j) \;\rightrightarrows\; \prod_{u : i \to j \text{ in } \mathcal{J}} D(j), \qquad \mathrm{pr}_u \circ s = \mathrm{pr}_j, \quad \mathrm{pr}_u \circ t = D(u) \circ \mathrm{pr}_i

(for $u : i \to j$ ; $\mathrm{pr}$ denotes product projections). Then the equaliser $e : E \to \prod_j D(j)$ of $s$ and $t$ , with legs $\pi_j = \mathrm{pr}_j \circ e$ , is a limit of $D$ .

Proof

Cone. For $u : i \to j$ : $D(u) \circ \pi_i = D(u) \circ \mathrm{pr}_i \circ e = \mathrm{pr}_u \circ t \circ e = \mathrm{pr}_u \circ s \circ e = \mathrm{pr}_j \circ e = \pi_j$ , using $t e = s e$ .

Universal. Let $(X, \lambda)$ be a cone. By the universal property of the product there is a unique $\ell : X \to \prod_j D(j)$ with $\mathrm{pr}_j \circ \ell = \lambda_j$ . For every $u : i \to j$ ,

\mathrm{pr}_u \circ s \circ \ell = \mathrm{pr}_j \circ \ell = \lambda_j = D(u) \circ \lambda_i = D(u) \circ \mathrm{pr}_i \circ \ell = \mathrm{pr}_u \circ t \circ \ell,

so $s \ell = t \ell$ (maps into a product are determined by their components). By the universal property of the equaliser, $\ell = e \circ h$ for a unique $h : X \to E$ , and then $\pi_j \circ h = \mathrm{pr}_j \circ e \circ h = \lambda_j$ . If also $\pi_j \circ h' = \lambda_j$ for all $j$ , then $\mathrm{pr}_j \circ (e h') = \lambda_j$ for all $j$ , so $e h' = \ell = e h$ , and $h' = h$ because an equaliser is a monomorphism (by the uniqueness in its universal property).

∎

In $\cat{Set}$ this is exactly the formula of Theorem 2: compatible families are the tuples on which "move along $u$ " and "look at the target" agree. Dually, coproducts and coequalisers give all colimits. The same proof with finite products shows that a terminal object, binary products and equalisers give all finite limits; and since the pullback of $f : A \to C$ , $g : B \to C$ is the equaliser of $f \circ \pi_1$ and $g \circ \pi_2$ on $A \times B$ , products and equalisers in particular give pullbacks.

Theorem— Theorem 4 (hom functors preserve limits)

For every object $A$ of a locally small category $\mathcal{C}$ , the functor $\Hom(A, -) : \mathcal{C} \to \cat{Set}$ preserves all limits that exist. Dually, $\Hom(-, B) : \mathcal{C}^{\mathrm{op}} \to \cat{Set}$ sends colimits in $\mathcal{C}$ to limits in $\cat{Set}$ : $\Hom(\operatorname{colim} D, B) \cong \lim \Hom(D(-), B)$ .

Proof

Let $(L, \pi)$ be a limit of $D$ . By Theorem 2, $\lim \Hom(A, D(-))$ is the set of compatible families $(\lambda_j : A \to D(j))_j$ — that is, the set of cones over $D$ with apex $A$ . The map $\Hom(A, L) \to \lim \Hom(A, D(-))$ , $h \mapsto (\pi_j \circ h)_j$ , is a bijection: that is precisely the universal property of $(L, \pi)$ tested on cones with apex $A$ . For the dual statement apply this to $\mathcal{C}^{\mathrm{op}}$ .

∎

So limits can be computed "elementwise", using generalised elements $A \to L$ : maps into a limit are compatible families of maps. For example $\Hom(A, X \times Y) \cong \Hom(A, X) \times \Hom(A, Y)$ , and $\Hom(V \oplus W, U) \cong \Hom(V, U) \times \Hom(W, U)$ for vector spaces.

Theorem— Theorem 5 (forgetful functors and limits)

The forgetful functor $U : \cat{Grp} \to \cat{Set}$ preserves all limits. It preserves neither the initial object nor binary coproducts: $U(\Z * \Z)$ is not the disjoint union $U(\Z) \sqcup U(\Z)$ .

Proof

$U$ is naturally isomorphic to $\Hom_{\cat{Grp}}(\Z, -)$ , since a homomorphism $\Z \to G$ is determined by the image of $1$ , which can be any element. So Theorem 4 applies. (Directly: the set of compatible families in $\prod_j D(j)$ is a subgroup, and it is the limit in $\cat{Grp}$ .) The initial object of $\cat{Grp}$ is the trivial group, whose underlying set has one element, not zero. For coproducts, compare the canonical map $c : U(\Z) \sqcup U(\Z) \to U(\Z * \Z)$ sending the two summands by $\iota_1, \iota_2$ . If $U$ preserved this coproduct, $c$ would be a bijection. Let $x = \iota_1(1)$ , $y = \iota_2(1)$ , and map $\Z * \Z \to S_3$ by $x \mapsto \sigma = (1\,2)$ , $y \mapsto \tau = (2\,3)$ . Every element in the image of $c$ goes to a power of $\sigma$ (which fixes $3$ ) or a power of $\tau$ (which fixes $1$ ); but $xy$ goes to $\sigma\tau = (1\,2\,3)$ , which fixes neither. So $xy \notin \operatorname{im} c$ .

∎

Theorem— Theorem 6 (units of the p-adic integers)

In $\Z_p = \varprojlim \Z/p^n\Z$ , an element $x = (x_n)_n$ is a unit if and only if $x_1 \neq 0$ in $\Z/p\Z$ . In particular every integer, and every fraction $a/b$ with $p \nmid b$ , defines an element of $\Z_p$ .

Proof

If $xy = 1$ then $x_1 y_1 = 1$ in $\Z/p$ , so $x_1 \neq 0$ . Conversely, if $x_1 \neq 0$ , then for each $n$ the residue $x_n$ is prime to $p$ (it reduces to $x_1$ ), so it has an inverse $y_n$ in $\Z/p^n$ . The family $(y_n)$ is compatible: $y_{n+1} \bmod p^n$ is an inverse of $x_{n+1} \bmod p^n = x_n$ , and inverses are unique, so it equals $y_n$ . By the description of limits of rings as compatible families (limits in rings are computed as in sets), $y = (y_n) \in \Z_p$ , and $xy = 1$ componentwise. For $a/b$ , take $x = a \cdot b^{-1}$ , where $b = (b \bmod p^n)_n$ is a unit.

∎

The same "solve level by level, then use compatibility" strategy is Hensel's lemma: if $f$ is a polynomial with integer coefficients, $f(x_1) \equiv 0$ and $f'(x_1) \not\equiv 0 \pmod p$ , then $x_1$ lifts uniquely to a compatible tower of roots, i.e. to a root in $\Z_p$ . The computation below lifts the root $2$ of $x^2 + 1$ modulo $5$ to $\sqrt{-1} = (2, 7, 57, 182, \dots) \in \Z_5$ .

Formal mathematicsF

Limits and colimits in Lean

In the category of types, the constructions of Theorem 2 can be written down directly: subtypes carve out, quotients glue.

equalizer_universalLean 4Proved here from basic factsFormally verified

/-- **The equaliser in the category of types** of `f g : X → Y` is the subtype
`{x // f x = g x}` with its inclusion. Universal property: every `h : W → X` with
`f ∘ h = g ∘ h` factors through the inclusion by exactly one map `u`, namely
`u w = ⟨h w, _⟩`; uniqueness holds because an element of a subtype is determined by its value. -/
theorem equalizer_universal (f g : X → Y) (h : W → X) (hh : f ∘ h = g ∘ h) :
    ∃! u : W → {x : X // f x = g x}, Subtype.val ∘ u = h := by
  refine ⟨fun w => ⟨h w, congr_fun hh w⟩, rfl, ?_⟩
  intro u hu
  funext w
  exact Subtype.ext (congr_fun hu w)

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

homEqualizerEquivLean 4Formally verified

/-- **Maps into an equaliser are maps that equalise.** For every type `W`, maps
`W → {x // f x = g x}` correspond bijectively to maps `h : W → X` with `f ∘ h = g ∘ h`. In other
words the hom functor `Hom(W, −)` sends the equaliser of `f, g` to the equaliser of
`f ∘ −, g ∘ −` — the simplest case of "hom functors preserve limits". -/
def homEqualizerEquiv (f g : X → Y) (W : Type u) :
    (W → {x : X // f x = g x}) ≃ {h : W → X // f ∘ h = g ∘ h} where
  toFun u := ⟨Subtype.val ∘ u, funext fun w => (u w).2⟩
  invFun h := fun w => ⟨h.1 w, congr_fun h.2 w⟩
  left_inv _ := rfl
  right_inv _ := rfl

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

pullback_universalLean 4Proved here from basic factsFormally verified

/-- **The pullback in the category of types** of `f : A → C` and `g : B → C` is the subtype
`{(a, b) // f a = g b}` of `A × B` — the equaliser of `f ∘ fst` and `g ∘ snd`, exactly the
construction "limits from products and equalisers". Universal property: maps `a : W → A`,
`b : W → B` with `f ∘ a = g ∘ b` factor through it by exactly one map, `w ↦ (a w, b w)`. -/
theorem pullback_universal (f : A → C) (g : B → C) (a : W → A) (b : W → B)
    (hab : f ∘ a = g ∘ b) :
    ∃! u : W → {p : A × B // f p.1 = g p.2},
      (fun w => (u w).1.1) = a ∧ (fun w => (u w).1.2) = b := by
  refine ⟨fun w => ⟨(a w, b w), congr_fun hab w⟩, ⟨rfl, rfl⟩, ?_⟩
  rintro u ⟨h₁, h₂⟩
  funext w
  exact Subtype.ext (Prod.ext (congr_fun h₁ w) (congr_fun h₂ w))

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

CoeqRelLean 4Formally verified

/-- The relation generating the **coequaliser** of `f g : X → Y`: `f x` is related to `g x`. -/
def CoeqRel (f g : X → Y) : Y → Y → Prop :=
  fun y y' => ∃ x, f x = y ∧ g x = y'

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

coequalizer_universalLean 4Proved here from basic factsFormally verified

/-- **The coequaliser in the category of types** is the quotient `Quot (CoeqRel f g)` of `Y` by
the equivalence relation generated by `f x ~ g x`, with the quotient map. Universal property:
every `h : Y → Z` with `h ∘ f = h ∘ g` factors through the quotient by exactly one map
(`Quot.lift`); uniqueness holds because every element of the quotient is a class `[y]`. Colimits
of types glue, limits of types carve out. -/
theorem coequalizer_universal (f g : X → Y) (h : Y → Z) (hh : h ∘ f = h ∘ g) :
    ∃! u : Quot (CoeqRel f g) → Z, u ∘ Quot.mk _ = h := by
  refine ⟨Quot.lift h ?_, rfl, ?_⟩
  · rintro _ _ ⟨x, rfl, rfl⟩
    exact congr_fun hh x
  · intro u hu
    funext q
    induction q using Quot.ind with
    | mk y => exact congr_fun hu y

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

Mathlib's general theory (CategoryTheory.Limits) defines a cone exactly as in the lesson — a natural transformation from a constant functor — and proves Theorems 3 and 4 and the completeness results. Here diagrammatic composition π_j ≫ F.map f means $F(f) \circ \pi_j$ .

cone_naturalityLean 4Applies a library theoremFormally verified

/-- **A cone is a natural transformation from a constant functor.** A cone over `F : J ⥤ C` has
an apex and legs `c.π.app j : apex ⟶ F j`; naturality of `c.π : const apex ⟶ F` at
`f : j ⟶ j'` says exactly that the legs are compatible: `F f ∘ π_j = π_j'`. This is Mathlib's
`Cone.w`. -/
theorem cone_naturality {J : Type*} [Category J] {C : Type*} [Category C] {F : J ⥤ C}
    (c : Cone F) {j j' : J} (f : j ⟶ j') : c.π.app j ≫ F.map f = c.π.app j' :=
  c.w f