Kan extensions · The Lumenary

Lens

MotivationH

Extending as well as possible

Here are three problems that look unrelated.

You know a function only on the integers, say $n \mapsto n$ , and you want a monotone function on all of $\mathbb{R}$ that is “as close as possible” to it. From below, the answer is $\lfloor x \rfloor$ ; from above, $\lceil x \rceil$ .
A subgroup $H$ of a group $G$ acts on a set or a vector space $V$ . You want a $G$ -action that is “freely generated” by the $H$ -action. The answer is the induced representation $\mathrm{Ind}_H^G V$ .
You know a topological space $\Delta^n$ for each standard simplex $[n]$ , and you want to turn every simplicial set into a space, gluing simplices the way the simplicial set says. The answer is geometric realisation.

In each case there is a functor $F : \mathcal{C} \to \mathcal{E}$ defined on a “small piece” $\mathcal{C}$ , a functor $K : \mathcal{C} \to \mathcal{D}$ embedding (or merely mapping) that piece into a larger world, and we want the best functor $\mathcal{D} \to \mathcal{E}$ that extends $F$ . In general no functor extends $F$ on the nose — but there is a best approximation from the left and a best approximation from the right. These are the left and right Kan extensions, and they turn out to be so universal that Saunders Mac Lane ended the first edition of Categories for the Working Mathematician (1971) with a section titled “All concepts are Kan extensions”.

This lesson assumes adjunctions, limits and colimits and the Yoneda lemma.

IntuitionH

The picture: a triangle that need not commute

Draw $F$ and $K$ as two sides of a triangle. We want to fill in the third side.

A left Kan extension fills the triangle up to a universal natural transformation

\eta : F \Rightarrow (\mathrm{Lan}_K F) \circ K

, not up to equality.

Asking for $L \circ K = F$ is usually hopeless: if $K$ sends two objects $a, b$ to the same object $d$ , then $L(d)$ would have to equal both $F(a)$ and $F(b)$ . Category theory's answer is to ask instead for a natural transformation $F \Rightarrow L \circ K$ — “ $L$ is at least as big as $F$ along $K$ ” — and to take the smallest such $L$ . Dually, a right Kan extension is the largest $R$ with $R \circ K \Rightarrow F$ .

The poset case makes this concrete. A poset is a category with at most one arrow between two objects, a functor between posets is a monotone map, and a natural transformation $f \Rightarrow g$ exists exactly when $f \le g$ pointwise. The smallest monotone $L$ with $f(c) \le L(k(c))$ is forced: $L(d)$ must be at least $f(c)$ whenever $k(c) \le d$ , so the best choice is

L(d) = \bigvee \{\, f(c) \mid k(c) \le d \,\}.

That supremum is the poset shadow of the general formula: a left Kan extension at $d$ is the colimit of everything that maps to $d$ .

DefinitionsH

Definitions

Throughout, $K : \mathcal{C} \to \mathcal{D}$ and $F : \mathcal{C} \to \mathcal{E}$ are functors. For a functor $G : \mathcal{D} \to \mathcal{E}$ , write $GK = G \circ K$ , and for a natural transformation $\sigma : G \Rightarrow G'$ write $\sigma K : GK \Rightarrow G'K$ for the whiskered transformation with components $(\sigma K)_c = \sigma_{Kc}$ .

Definition— left Kan extension

A left Kan extension of $F$ along $K$ is a functor $L : \mathcal{D} \to \mathcal{E}$ together with a natural transformation $\eta : F \Rightarrow LK$ (the unit) such that for every functor $G : \mathcal{D} \to \mathcal{E}$ and every natural transformation $\alpha : F \Rightarrow GK$ there is a unique natural transformation $\sigma : L \Rightarrow G$ with

\alpha = (\sigma K) \circ \eta, \qquad\text{i.e.}\qquad \alpha_c = \sigma_{Kc} \circ \eta_c \ \text{ for all } c.

Equivalently, $\sigma \mapsto (\sigma K) \circ \eta$ is a bijection $\mathrm{Nat}(L, G) \cong \mathrm{Nat}(F, GK)$ for every $G$ . We write $L = \mathrm{Lan}_K F$ ; it is unique up to unique isomorphism, as any universal object is.

The universal property, drawn in the functor category

[\mathcal{C}, \mathcal{E}]

: every

\alpha

factors uniquely through the unit

\eta

Definition— right Kan extension

A right Kan extension of $F$ along $K$ is a functor $R = \mathrm{Ran}_K F : \mathcal{D} \to \mathcal{E}$ with a natural transformation $\varepsilon : RK \Rightarrow F$ (the counit) such that for every $G$ and every $\beta : GK \Rightarrow F$ there is a unique $\sigma : G \Rightarrow R$ with $\beta = \varepsilon \circ (\sigma K)$ . Equivalently, $\mathrm{Nat}(G, R) \cong \mathrm{Nat}(GK, F)$ .

If every $F : \mathcal{C} \to \mathcal{E}$ has a left (respectively right) Kan extension along $K$ , the bijections above say precisely that $\mathrm{Lan}_K$ and $\mathrm{Ran}_K$ are the left and right adjoints of restriction along $K$ , the functor $K^* : [\mathcal{D}, \mathcal{E}] \to [\mathcal{C}, \mathcal{E}]$ , $G \mapsto GK$ :

\mathrm{Lan}_K \;\dashv\; K^* \;\dashv\; \mathrm{Ran}_K .

To compute Kan extensions we need comma categories.

Definition— comma categories over and under an object

For an object $d \in \mathcal{D}$ , the comma category $(K \downarrow d)$ has as objects the pairs $(c, f)$ with $c \in \mathcal{C}$ and $f : Kc \to d$ ; a morphism $(c, f) \to (c', f')$ is a morphism $u : c \to c'$ with $f' \circ K(u) = f$ . It comes with the projection $\pi_d : (K \downarrow d) \to \mathcal{C}$ , $(c, f) \mapsto c$ . Dually, $(d \downarrow K)$ has objects $(c, f : d \to Kc)$ and morphisms $u$ with $K(u) \circ f = f'$ . (Mathlib calls these CostructuredArrow K d and StructuredArrow d K.)

Definition— pointwise Kan extension

The left Kan extension is pointwise when, for every $d$ ,

(\mathrm{Lan}_K F)(d) = \operatorname*{colim}_{(c,\, f) \in (K \downarrow d)} F(c),

the colimit of $F \circ \pi_d$ , and dually $(\mathrm{Ran}_K F)(d) = \lim_{(c, f) \in (d \downarrow K)} F(c)$ . In words: the left Kan extension at $d$ glues together the values $F(c)$ of everything that maps to $d$ , identified along the arrows between them.

Worked examplesH

Examples, non-examples and boundary cases

Example— Floor and ceiling

Let $K : \mathbb{Z} \hookrightarrow \mathbb{R}$ be the inclusion and $F : \mathbb{Z} \to \overline{\mathbb{Z}} = \mathbb{Z} \cup \{\pm\infty\}$ the inclusion into the complete lattice of extended integers. By the poset formula,

(\mathrm{Lan}_K F)(x) = \sup\{\, n \in \mathbb{Z} \mid n \le x \,\} = \lfloor x \rfloor, \qquad (\mathrm{Ran}_K F)(x) = \inf\{\, n \in \mathbb{Z} \mid x \le n \,\} = \lceil x \rceil.

Every monotone $g : \mathbb{R} \to \overline{\mathbb{Z}}$ that agrees with $F$ on the integers satisfies $\lfloor x \rfloor \le g(x) \le \lceil x \rceil$ : the Kan extensions are the extreme extensions. Since $K$ is an order embedding, both restrict back to $F$ on $\mathbb{Z}$ .

The floor function (solid) is the left Kan extension of the integers along ℤ ⊂ ℝ, the ceiling (dashed) the right Kan extension. They agree exactly at the integers, where both extend the original function.

Example— Limits and colimits

Let $\mathbf{1}$ be the terminal category and $! : J \to \mathbf{1}$ the unique functor. A functor $c : \mathbf{1} \to \mathcal{E}$ is an object $c$ , and a natural transformation $c \circ {!} \Rightarrow F$ is a family of maps $c \to F(j)$ compatible with all $F(u)$ — a cone over $F$ with vertex $c$ . The universal property of $\mathrm{Ran}_! F$ says that there is a universal cone. Hence

\mathrm{Ran}_! F = \lim F, \qquad \mathrm{Lan}_! F = \operatorname{colim} F,

each existing exactly when the (co)limit does. (A full proof is in the next section.) For $J$ the discrete category on two objects this gives products and coproducts: the right Kan extension of $(A, B)$ to $\mathbf{1}$ is $A \times B$ — the universal property explored in the trail The product, by its maps.

Example— Extending along a non-injective functor: no strict extension

Let $K : \{a, b\} \to \mathbf{1}$ (discrete source) and $F : \{a, b\} \to \mathbf{Set}$ with $|F(a)| = 2$ , $|F(b)| = 3$ . Then $(\mathrm{Lan}_K F)(\ast) = F(a) \sqcup F(b)$ has $5$ elements and $(\mathrm{Ran}_K F)(\ast) = F(a) \times F(b)$ has $6$ . Neither restricts back to $F$ : $(\mathrm{Lan}_K F)K(a)$ has $5$ elements, not $2$ . The unit $\eta_a : F(a) \to F(a) \sqcup F(b)$ is the coproduct inclusion — a genuine map, not an identity.

Example— Induced and coinduced actions

A group $G$ is a category $\mathbf{B}G$ with one object $\ast$ and one arrow for each $g \in G$ ; a functor $\mathbf{B}G \to \mathbf{Set}$ is a $G$ -set. For a subgroup $H \le G$ with inclusion $i : \mathbf{B}H \to \mathbf{B}G$ and an $H$ -set $X$ :

The comma category $(i \downarrow \ast)$ has one object for each $g \in G$ (an arrow $i(\ast) \to \ast$ ), and an arrow $g'h \to g'$ for each $h \in H$ . Its colimit glues $(g'h, x)$ to $(g', h x)$ , so $(\mathrm{Lan}_i X)(\ast) = G \times_H X$ , the induced $G$ -set, with $[G : H]\,|X|$ elements when $G$ is finite.
Dually $(\mathrm{Ran}_i X)(\ast) = \mathrm{Hom}_H(G, X)$ , the coinduced $G$ -set of $H$ -equivariant maps, with $|X|^{[G:H]}$ elements.

For $H = 1$ and $X = \{\ast\}$ , $\mathrm{Lan}_i X = G$ acting on itself: the free $G$ -set on one generator. The experiment below computes all of these as colimits and limits.

Example— Non-example: a Kan extension that does not exist

Let $k$ be the inclusion of the discrete poset $\{a, b\}$ into $\{a, b, \top\}$ with $a, b \le \top$ , and let $f$ send $a \mapsto x$ , $b \mapsto y$ in the discrete two-element poset $\{x, y\}$ . A monotone $g$ with $f \le g \circ k$ would need $x \le g(a) \le g(\top)$ and $y \le g(b) \le g(\top)$ , which is impossible. So there is no extension at all, and certainly no Kan extension. The pointwise formula fails precisely because the join $x \vee y$ does not exist.

ProofH

The main theorems

Theorem— Theorem 1 (the pointwise formula)

Suppose that for every $d \in \mathcal{D}$ the colimit $L(d) = \operatorname{colim}(F \circ \pi_d)$ over $(K \downarrow d)$ exists, with coprojections $\iota_{(c, f)} : F(c) \to L(d)$ . Then $d \mapsto L(d)$ extends uniquely to a functor $L : \mathcal{D} \to \mathcal{E}$ with $L(g) \circ \iota_{(c, f)} = \iota_{(c,\, g f)}$ , and with $\eta_c = \iota_{(c,\, \mathrm{id}_{Kc})}$ the pair $(L, \eta)$ is a left Kan extension of $F$ along $K$ .

Proof

Functoriality. An arrow $g : d \to d'$ induces a functor $g_* : (K \downarrow d) \to (K \downarrow d')$ , $(c, f) \mapsto (c, gf)$ , with $\pi_{d'} \circ g_* = \pi_d$ . The maps $\iota_{(c, gf)} : F(c) \to L(d')$ therefore form a cocone over $F \circ \pi_d$ , so there is a unique $L(g) : L(d) \to L(d')$ with $L(g) \circ \iota_{(c, f)} = \iota_{(c, gf)}$ . Both $L(\mathrm{id})$ and $\mathrm{id}$ , and both $L(g'g)$ and $L(g') L(g)$ , satisfy the same equations on coprojections, so they agree by the uniqueness clause of the colimit.

The unit is natural. For $u : c \to c'$ in $\mathcal{C}$ we must show $L(Ku) \circ \eta_c = \eta_{c'} \circ F(u)$ . The left side is $\iota_{(c, Ku)}$ by definition of $L(Ku)$ . On the right, $u$ is a morphism $(c, Ku) \to (c', \mathrm{id}_{Kc'})$ of $(K \downarrow Kc')$ , so the cocone condition gives $\iota_{(c', \mathrm{id})} \circ F(u) = \iota_{(c, Ku)}$ .

Existence of factorisations. Let $G : \mathcal{D} \to \mathcal{E}$ and $\alpha : F \Rightarrow GK$ . For fixed $d$ , the maps $G(f) \circ \alpha_c : F(c) \to G(d)$ form a cocone over $F \circ \pi_d$ : if $u : (c, f) \to (c', f')$ , then $f' \circ K(u) = f$ , and naturality of $\alpha$ gives

G(f') \circ \alpha_{c'} \circ F(u) = G(f') \circ G(Ku) \circ \alpha_c = G(f) \circ \alpha_c .

So there is a unique $\sigma_d : L(d) \to G(d)$ with $\sigma_d \circ \iota_{(c, f)} = G(f) \circ \alpha_c$ . It is natural in $d$ , because for $g : d \to d'$ both $\sigma_{d'} \circ L(g)$ and $G(g) \circ \sigma_d$ send $\iota_{(c,f)}$ to $G(gf) \circ \alpha_c$ . Finally $\sigma_{Kc} \circ \eta_c = \sigma_{Kc} \circ \iota_{(c, \mathrm{id})} = G(\mathrm{id}) \circ \alpha_c = \alpha_c$ .

Uniqueness. If $\sigma' : L \Rightarrow G$ also satisfies $\sigma'_{Kc} \circ \eta_c = \alpha_c$ , then, using $\iota_{(c, f)} = L(f) \circ \iota_{(c, \mathrm{id})} = L(f) \circ \eta_c$ and naturality of $\sigma'$ ,

\sigma'_d \circ \iota_{(c, f)} = \sigma'_d \circ L(f) \circ \eta_c = G(f) \circ \sigma'_{Kc} \circ \eta_c = G(f) \circ \alpha_c = \sigma_d \circ \iota_{(c, f)} ,

so $\sigma'_d = \sigma_d$ by the uniqueness of maps out of a colimit.

∎

Theorem— Corollary (existence)

If $\mathcal{C}$ is small, $\mathcal{D}$ is locally small and $\mathcal{E}$ has all small colimits, then every $F : \mathcal{C} \to \mathcal{E}$ has a pointwise left Kan extension along every $K$ , so $\mathrm{Lan}_K \dashv K^*$ . Dually, if $\mathcal{E}$ has all small limits, $K^* \dashv \mathrm{Ran}_K$ .

Proof

Each $(K \downarrow d)$ is small: its objects form the set $\coprod_{c} \mathcal{D}(Kc, d)$ (a set because $\mathcal{C}$ is small and $\mathcal{D}$ locally small), and its morphisms are among those of $\mathcal{C}$ . So the colimits in Theorem 1 exist. The dual statement is Theorem 1 applied to $K^{\mathrm{op}}$ and $F^{\mathrm{op}}$ .

∎

Theorem— Proposition 2 (extension along a fully faithful functor)

If $K$ is fully faithful and $\mathrm{Lan}_K F$ is pointwise, then the unit $\eta : F \Rightarrow (\mathrm{Lan}_K F) K$ is a natural isomorphism: the Kan extension really extends $F$ .

Proof

In $(K \downarrow Kc)$ the object $(c, \mathrm{id}_{Kc})$ is terminal: given $(c', f : Kc' \to Kc)$ , full faithfulness gives a unique $u : c' \to c$ with $K(u) = f$ , which is exactly a unique morphism $(c', f) \to (c, \mathrm{id})$ . The colimit of a diagram over a category with a terminal object $t$ is its value at $t$ , with coprojection at $t$ an isomorphism. Here that coprojection is $\iota_{(c, \mathrm{id})} = \eta_c$ .

∎

The hypothesis matters: the two-point example above shows what happens for a $K$ that is not injective on objects.

Theorem— Proposition 3 (limits are right Kan extensions)

For $F : J \to \mathcal{E}$ , an object $\ell$ with a cone $\lambda : \ell \circ {!} \Rightarrow F$ is a right Kan extension of $F$ along $! : J \to \mathbf{1}$ if and only if $(\ell, \lambda)$ is a limit of $F$ .

Proof

Functors $\mathbf{1} \to \mathcal{E}$ are objects, and natural transformations between them are morphisms. A transformation $\beta : c \circ {!} \Rightarrow F$ is a cone with vertex $c$ , and for $\sigma : c \to \ell$ the composite $\lambda \circ (\sigma\, {!})$ is the cone $(\lambda_j \circ \sigma)_j$ . So the universal property of $\mathrm{Ran}_!$ — every $\beta$ equals $\lambda \circ (\sigma\, !)$ for a unique $\sigma$ — is word for word the universal property of a limit.

∎

Theorem— Theorem 4 (adjoints are Kan extensions; Mac Lane)

A functor $G : \mathcal{A} \to \mathcal{X}$ has a left adjoint if and only if the right Kan extension $(R, \varepsilon) = \mathrm{Ran}_G \mathrm{id}_{\mathcal{A}}$ exists and is preserved by $G$ , meaning that $(GR, G\varepsilon)$ is a right Kan extension of $G$ along $G$ . In that case $R$ is the left adjoint, with counit $\varepsilon$ . In fact, if $F \dashv G$ then $(F, \varepsilon)$ is preserved by every functor out of $\mathcal{A}$ .

Proof

( $\Rightarrow$ ) Let $F \dashv G$ with unit $\eta : \mathrm{id}_{\mathcal{X}} \Rightarrow GF$ , counit $\varepsilon : FG \Rightarrow \mathrm{id}_{\mathcal{A}}$ , and triangle identities $G\varepsilon \circ \eta G = 1_G$ and $\varepsilon F \circ F\eta = 1_F$ . Let $P : \mathcal{A} \to \mathcal{B}$ be any functor; we show $(PF, P\varepsilon)$ is a right Kan extension of $P$ along $G$ . Given $H : \mathcal{X} \to \mathcal{B}$ and $\beta : HG \Rightarrow P$ , put $\sigma_x = \beta_{Fx} \circ H(\eta_x) : H(x) \to PF(x)$ . Then, by naturality of $\beta$ at $\varepsilon_a$ and the first triangle identity,

P(\varepsilon_a) \circ \sigma_{Ga} = P(\varepsilon_a) \circ \beta_{FGa} \circ H(\eta_{Ga}) = \beta_a \circ HG(\varepsilon_a) \circ H(\eta_{Ga}) = \beta_a \circ H\big(G(\varepsilon_a) \circ \eta_{Ga}\big) = \beta_a .

If $\sigma'$ is another solution, the second triangle identity and naturality of $\sigma'$ at $\eta_x$ give

\sigma'_x = P(\varepsilon_{Fx}) \circ PF(\eta_x) \circ \sigma'_x = P(\varepsilon_{Fx}) \circ \sigma'_{GFx} \circ H(\eta_x) = \beta_{Fx} \circ H(\eta_x) = \sigma_x .

Taking $P = \mathrm{id}$ shows $(F, \varepsilon) = \mathrm{Ran}_G \mathrm{id}$ ; taking $P = G$ shows that $G$ preserves it.

( $\Leftarrow$ ) Suppose $(R, \varepsilon : RG \Rightarrow \mathrm{id}_{\mathcal{A}})$ is $\mathrm{Ran}_G \mathrm{id}$ and $(GR, G\varepsilon)$ is $\mathrm{Ran}_G G$ . Apply the universal property of $(GR, G\varepsilon)$ to the identity transformation $1_G : \mathrm{id}_{\mathcal{X}} G \Rightarrow G$ : there is a unique $\eta : \mathrm{id}_{\mathcal{X}} \Rightarrow GR$ with $G\varepsilon \circ \eta G = 1_G$ , which is one triangle identity. For the other, both $1_R$ and $\tau = \varepsilon R \circ R\eta$ are transformations $R \Rightarrow R$ , and the universal property of $(R, \varepsilon)$ says there is only one $\tau$ with $\varepsilon \circ \tau G = \varepsilon$ . The identity qualifies, and so does $\tau$ : by naturality of $\varepsilon$ at the arrow $\varepsilon_a$ ,

\varepsilon_a \circ \varepsilon_{RGa} \circ R(\eta_{Ga}) = \varepsilon_a \circ RG(\varepsilon_a) \circ R(\eta_{Ga}) = \varepsilon_a \circ R\big(G(\varepsilon_a) \circ \eta_{Ga}\big) = \varepsilon_a .

Hence $\varepsilon R \circ R\eta = 1_R$ . Both triangle identities hold, so $R \dashv G$ with unit $\eta$ and counit $\varepsilon$ .

∎

Note the twist: a left adjoint is a right Kan extension, $F = \mathrm{Ran}_G \mathrm{id}$ , and dually a right adjoint is a left Kan extension, $G = \mathrm{Lan}_F \mathrm{id}$ . In posets: the ceiling function, left adjoint to $\mathbb{Z} \hookrightarrow \mathbb{R}$ , is an infimum; the floor, right adjoint, is a supremum.

Theorem— Theorem 5 (extending along the Yoneda embedding)

Let $\mathcal{C}$ be small, $\mathcal{E}$ cocomplete and locally small, $F : \mathcal{C} \to \mathcal{E}$ , and $y : \mathcal{C} \to \widehat{\mathcal{C}} = [\mathcal{C}^{\mathrm{op}}, \mathbf{Set}]$ the Yoneda embedding. Then $L = \mathrm{Lan}_y F$ exists and is given by

L(P) = \operatorname*{colim}_{(c,\, x) \in \int P} F(c),

the colimit over the category of elements of $P$ (objects: pairs $c \in \mathcal{C}$ , $x \in P(c)$ ). Moreover $L \circ y \cong F$ ; $L$ is left adjoint to the “nerve” $N_F : \mathcal{E} \to \widehat{\mathcal{C}}$ , $N_F(e) = \mathcal{E}(F(-), e)$ ; and $L$ is, up to isomorphism, the unique colimit-preserving functor $\widehat{\mathcal{C}} \to \mathcal{E}$ whose composite with $y$ is isomorphic to $F$ .

Proof

Sketch. By the Yoneda lemma an arrow $y(c) \to P$ is the same as an element $x \in P(c)$ , and this identifies the comma category $(y \downarrow P)$ with $\int P$ (up to size: $\widehat{\mathcal{C}}$ is locally small because $\mathcal{C}$ is small, so $\int P$ is small). Theorem 1 gives the formula. The Yoneda embedding is fully faithful, so Proposition 2 gives $Ly \cong F$ . For the adjunction, maps out of a colimit are compatible families:

\mathcal{E}(L P, e) \cong \lim_{(c, x) \in \int P} \mathcal{E}(F c, e) \cong \mathrm{Nat}\big(P, \mathcal{E}(F(-), e)\big),

the second step because a natural transformation $P \Rightarrow N_F(e)$ is exactly an assignment $x \mapsto (Fc \to e)$ compatible with restriction. Being a left adjoint, $L$ preserves colimits. Uniqueness: every presheaf is canonically the colimit of representables over its category of elements (the density theorem, which is the case $F = y$ ), so a colimit-preserving functor is determined by its values on representables. Full details: Riehl (2016), Chapter 6, or Mac Lane and Moerdijk (1992), Chapter I.

∎

This “nerve and realisation” pattern appears all over mathematics: with $F : \Delta \to \mathbf{Top}$ , $[n] \mapsto \Delta^n$ , it gives geometric realisation $|{-}| \dashv \mathrm{Sing}$ ; with $F : \Delta \to \mathbf{Cat}$ , $[n] \mapsto$ the poset $\{0 < \dots < n\}$ , it gives the nerve of a category and its left adjoint.

Formal mathematicsF

Kan extensions in Lean

The Lean module has two parts.

Part 1 (independent): the thin case. For preorders $C, D$ and a complete lattice $E$ , everything above can be proved from scratch, because in a thin category a natural transformation exists exactly when there is a pointwise inequality, and colimits and limits in a complete lattice are suprema and infima. The definitions are the pointwise formulas:

lanLean 4Formally verified

/-- The **pointwise left Kan extension** of `f : C → E` along `k : C → D`, for a preorder `D`
and a complete lattice `E` (the order of `C`, if any, plays no role in the formula):
`lan k f d = ⨆ { f c | k c ≤ d }`.
This is the formula `(Lan_k f)(d) = colim_{(k ↓ d)} f`: in a thin category the comma category
`(k ↓ d)` is the set of `c` with `k c ≤ d`, and a colimit in a complete lattice is a supremum. -/
def lan (k : C → D) (f : C → E) (d : D) : E :=
  ⨆ (c : C) (_ : k c ≤ d), f c

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

ranLean 4Formally verified

/-- The **pointwise right Kan extension**: `ran k f d = ⨅ { f c | d ≤ k c }`, the limit of `f`
over the comma category `(d ↓ k)`. -/
def ran (k : C → D) (f : C → E) (d : D) : E :=
  ⨅ (c : C) (_ : d ≤ k c), f c

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

lan k f is a functor, the unit exists, and the universal property holds — the poset shadow of Theorem 1:

lan_monotoneLean 4Proved here from basic factsFormally verified

/-- `lan k f` is a functor, i.e. monotone: if `d ≤ d'` then every `c` with `k c ≤ d` also has
`k c ≤ d'`, so the supremum can only grow. (This is how a pointwise Kan extension acts on
arrows: an arrow `d → d'` induces a functor `(k ↓ d) → (k ↓ d')` and hence a map of colimits.) -/
theorem lan_monotone (k : C → D) (f : C → E) : Monotone (lan k f) := by
  intro d d' h
  exact iSup₂_le fun c hc => le_iSup₂_of_le c (hc.trans h) le_rfl

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

le_lan_compLean 4Proved here from basic factsFormally verified

/-- The **unit** `f ⇒ (Lan_k f) ∘ k`: `f c ≤ lan k f (k c)`, because `c` itself lies in the
comma category `(k ↓ k c)` (via the identity `k c ≤ k c`). -/
theorem le_lan_comp (k : C → D) (f : C → E) (c : C) : f c ≤ lan k f (k c) :=
  le_iSup₂_of_le c le_rfl le_rfl

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

lan_le_iffLean 4Proved here from basic factsFormally verified

/-- The **universal property** of the left Kan extension. For every monotone `g : D → E`:
`Lan_k f ≤ g` if and only if `f ≤ g ∘ k`.
(→) compose with the unit: `f c ≤ lan k f (k c) ≤ g (k c)`.
(←) each term `f c` with `k c ≤ d` satisfies `f c ≤ g (k c) ≤ g d` by monotonicity of `g`.
In a thin category, arrows are unique when they exist, so this *is* the statement that every
`f ⇒ g ∘ k` factors uniquely through the unit. -/
theorem lan_le_iff (k : C → D) (f : C → E) {g : D → E} (hg : Monotone g) :
    lan k f ≤ g ↔ ∀ c, f c ≤ g (k c) := by
  constructor
  · intro h c
    exact (le_lan_comp k f c).trans (h (k c))
  · intro h d
    exact iSup₂_le fun c hc => (h c).trans (hg hc)

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

Any functor with this universal property is lan k f (uniqueness of universal objects), and along an order embedding the extension restricts back to f (Proposition 2):

lan_uniqueLean 4Proved here from basic factsFormally verified

/-- **Uniqueness**: any monotone `L : D → E` with the universal property of a left Kan
extension equals the pointwise formula. As always with universal properties, the proof plays
the two universal properties against each other. -/
theorem lan_unique (k : C → D) (f : C → E) {L : D → E} (hL : Monotone L)
    (huniv : ∀ g : D → E, Monotone g → (L ≤ g ↔ ∀ c, f c ≤ g (k c))) :
    L = lan k f := by
  apply le_antisymm
  · exact (huniv (lan k f) (lan_monotone k f)).2 (le_lan_comp k f)
  · exact (lan_le_iff k f hL).2 ((huniv L hL).1 le_rfl)

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

lan_comp_of_embeddingLean 4Proved here from basic factsFormally verified

/-- **Kan extension along a fully faithful functor is a genuine extension.** If `k` is an order
embedding (`k c ≤ k c' ↔ c ≤ c'`, the thin version of "fully faithful") and `f` is monotone,
then `lan k f (k c) = f c`: the unit is an isomorphism. The comma category `(k ↓ k c)` then
has the terminal object `c`, and a colimit over a category with a terminal object is the value
there. -/
theorem lan_comp_of_embedding [Preorder C] {k : C → D} (hk : ∀ c c', k c ≤ k c' ↔ c ≤ c') {f : C → E}
    (hf : Monotone f) (c : C) : lan k f (k c) = f c := by
  apply le_antisymm
  · exact iSup₂_le fun c' hc' => hf ((hk c' c).1 hc')
  · exact le_lan_comp k f c

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

Read as an adjunction between the preorders of monotone maps, the universal property is $\mathrm{Lan}_k \dashv k^*$ :

lan_gcLean 4Proved here from basic factsFormally verified

/-- **`Lan_k` is left adjoint to restriction along `k`.** On monotone maps (functors),
`Lan_k ⊣ k^*` where `k^* g = g ∘ k`: this is a Galois connection between the preorders of
functors `C →o E` and `D →o E` (ordered pointwise, i.e. by the existence of natural
transformations). It is `lan_le_iff` read as an adjunction. -/
theorem lan_gc [Preorder C] (k : C →o D) :
    GaloisConnection (fun f : C →o E => (⟨lan k f, lan_monotone k f⟩ : D →o E))
      (fun g : D →o E => g.comp k) := by
  intro f g
  exact lan_le_iff k f g.monotone

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

The right Kan extension is dual, and limits and colimits are Kan extensions along the map to Unit (Proposition 3):

ran_monotoneLean 4Proved here from basic factsFormally verified

/-- `ran k f` is monotone: if `d ≤ d'`, every `c` with `d' ≤ k c` also has `d ≤ k c`, so the
infimum defining `ran k f d` is taken over a larger family and can only be smaller. -/
theorem ran_monotone (k : C → D) (f : C → E) : Monotone (ran k f) := by
  intro d d' h
  exact le_iInf₂ fun c hc => iInf₂_le_of_le c (h.trans hc) le_rfl

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

ran_comp_leLean 4Proved here from basic factsFormally verified

/-- The **counit** of the right Kan extension: `(Ran_k f) ∘ k ⇒ f`, i.e.
`ran k f (k c) ≤ f c`, because `c` lies in `(k c ↓ k)`. -/
theorem ran_comp_le (k : C → D) (f : C → E) (c : C) : ran k f (k c) ≤ f c :=
  iInf₂_le_of_le c le_rfl le_rfl

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

le_ran_iffLean 4Proved here from basic factsFormally verified

/-- The universal property of the **right** Kan extension, dual to `lan_le_iff`: for monotone
`g : D → E`, `g ≤ Ran_k f` if and only if `g ∘ k ≤ f`. -/
theorem le_ran_iff (k : C → D) (f : C → E) {g : D → E} (hg : Monotone g) :
    g ≤ ran k f ↔ ∀ c, g (k c) ≤ f c := by
  constructor
  · intro h c
    exact (h (k c)).trans (ran_comp_le k f c)
  · intro h d
    exact le_iInf₂ fun c hc => (hg hc).trans (h c)

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

ran_const_eq_iInfLean 4Proved here from basic factsFormally verified

/-- **A limit is a right Kan extension along the functor to the terminal category.** Along
`! : C → Unit`, the comma category `(() ↓ !)` is all of `C`, so `Ran_! f` at the unique object
is `⨅ c, f c`, the infimum — which is the limit of `f` in the complete lattice `E`. -/
theorem ran_const_eq_iInf (f : C → E) : ran (fun _ : C => ()) f () = ⨅ c, f c := by
  simp [ran]

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

lan_const_eq_iSupLean 4Proved here from basic factsFormally verified

/-- Dually, a **colimit is a left Kan extension along `! : C → Unit`**: `Lan_! f () = ⨆ c, f c`. -/
theorem lan_const_eq_iSup (f : C → E) : lan (fun _ : C => ()) f () = ⨆ c, f c := by
  simp [lan]

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

Theorem 4 for complete lattices, where adjunctions are Galois connections: a left adjoint is $\mathrm{Ran}_G \mathrm{id}$ , a right adjoint is $\mathrm{Lan}_F \mathrm{id}$ , and $G$ has a left adjoint exactly when it preserves $\mathrm{Ran}_G \mathrm{id}$ . The last result is the adjoint functor theorem for complete lattices.

left_adjoint_eq_ranLean 4Proved here from basic factsFormally verified

/-- **A left adjoint is a right Kan extension of the identity.** If `F ⊣ G` (a Galois
connection `F x ≤ a ↔ x ≤ G a`), then `F = Ran_G id`, i.e.
`F x = ⨅ { a | x ≤ G a }`. In words: `F x` is the best approximation of `x` from above by
things of the form "an `a` with `x ≤ G a`". -/
theorem left_adjoint_eq_ran {F : X → A} {G : A → X} (gc : GaloisConnection F G) :
    F = ran G id := by
  funext x
  apply le_antisymm
  · exact le_iInf₂ fun a hx => (gc x a).2 hx
  · exact iInf₂_le_of_le (F x) (gc.le_u_l x) le_rfl

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

right_adjoint_eq_lanLean 4Proved here from basic factsFormally verified

/-- Dually, **a right adjoint is a left Kan extension of the identity**: if `F ⊣ G` then
`G = Lan_F id`, i.e. `G a = ⨆ { x | F x ≤ a }` — the best approximation of `a` from below. -/
theorem right_adjoint_eq_lan {F : X → A} {G : A → X} (gc : GaloisConnection F G) :
    G = lan F id := by
  funext a
  apply le_antisymm
  · exact le_iSup₂_of_le (G a) (gc.l_u_le a) le_rfl
  · exact iSup₂_le fun x hx => (gc x a).1 hx

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

exists_left_adjoint_iffLean 4Proved here from basic factsFormally verified

/-- **Mac Lane's criterion for adjoints, for complete lattices.** A monotone `G : A → X` has a
left adjoint if and only if `G` *preserves* the right Kan extension `Ran_G id`, meaning
`G ∘ Ran_G id = Ran_G G`:
`G (⨅ { a | x ≤ G a }) = ⨅ { G a | x ≤ G a }` for every `x`.
In a complete lattice `Ran_G id` always exists (it is the formula); the content is preservation.
The left adjoint is then `Ran_G id` (see `left_adjoint_eq_ran`). -/
theorem exists_left_adjoint_iff {G : A → X} (hG : Monotone G) :
    (∃ F : X → A, GaloisConnection F G) ↔ ∀ x, G (ran G id x) = ran G G x := by
  constructor
  · rintro ⟨F, gc⟩ x
    rw [← left_adjoint_eq_ran gc]
    apply le_antisymm
    · exact le_iInf₂ fun a hx => hG ((gc x a).2 hx)
    · exact iInf₂_le_of_le (F x) (gc.le_u_l x) le_rfl
  · intro h
    refine ⟨ran G id, fun x a => ⟨fun hxa => ?_, fun hxa => iInf₂_le_of_le a hxa le_rfl⟩⟩
    -- `x ≤ G (Ran_G id x)` because `G` preserves the infimum, and each term is `≥ x`.
    have hx : x ≤ G (ran G id x) := by
      rw [h x]
      exact le_iInf₂ fun _ hc => hc
    exact hx.trans (hG hxa)

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

exists_left_adjoint_of_map_sInfLean 4Proved here from basic factsFormally verified

/-- **The adjoint functor theorem for complete lattices.** If `G : A → X` preserves all
infima, then `G` has a left adjoint. Preserving all infima includes preserving the particular
infimum `Ran_G id x = ⨅ { a | x ≤ G a }`, so this follows from `exists_left_adjoint_iff`;
monotonicity comes from preserving binary infima. -/
theorem exists_left_adjoint_of_map_sInf {G : A → X}
    (hG : ∀ s : Set A, G (sInf s) = ⨅ a ∈ s, G a) : ∃ F : X → A, GaloisConnection F G := by
  have mono : Monotone G := by
    intro a b hab
    have h := hG {a, b}
    rw [sInf_pair, inf_eq_left.2 hab] at h
    rw [h]
    exact iInf₂_le b (by simp)
  refine (exists_left_adjoint_iff mono).2 fun x => ?_
  have hs : ran G id x = sInf { a | x ≤ G a } := by
    simp [ran, sInf_eq_iInf]
  rw [hs, hG]
  simp [ran]

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

Part 2 (library): the general theory. Mathlib has Kan extensions for arbitrary categories (Functor.LeftExtension, Functor.IsLeftKanExtension, Functor.leftKanExtension, pointwise Kan extensions in Mathlib.CategoryTheory.Functor.KanExtension.Pointwise). Two results of this lesson, in full generality, by applying Mathlib's theorems: $\mathrm{Lan}_L$ is left adjoint to restriction, and the pointwise formula with its existence conditions (Theorem 1 and its corollary).

lan_isLeftAdjointLean 4Applies a library theoremFormally verified

/-- **In general, `Lan_L` is left adjoint to restriction along `L`.** For any functor
`L : C ⥤ D` such that every `F : C ⥤ H` has a left Kan extension along `L`, the functor
`L.lan : (C ⥤ H) ⥤ (D ⥤ H)` is a left adjoint; its right adjoint is precomposition with `L`.
This applies Mathlib's `Functor.lanAdjunction` (with `Adjunction.isLeftAdjoint`). -/
theorem lan_isLeftAdjoint {C D H : Type*} [Category C] [Category D] [Category H]
    (L : C ⥤ D) [∀ F : C ⥤ H, L.HasLeftKanExtension F] :
    (L.lan : (C ⥤ H) ⥤ (D ⥤ H)).IsLeftAdjoint :=
  (L.lanAdjunction H).isLeftAdjoint

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

lan_obj_iso_colimitLean 4Applies a library theoremFormally verified

/-- **The pointwise formula, in general.** If `C` is small, `D` is locally small (its
hom-sets live in the same universe) and `H` has all small colimits, then the left Kan extension
of `F : C ⥤ H` along `L : C ⥤ D` exists and its value at `d` is the colimit of `F` over the
comma category `(L ↓ d)` (`CostructuredArrow L d` in Mathlib).
This applies Mathlib's `Functor.leftKanExtensionObjIsoColimit`; the existence of the colimits
is found by instance search from `HasColimits H`. -/
theorem lan_obj_iso_colimit {C D H : Type*} [SmallCategory C] [Category D] [Category H]
    (L : C ⥤ D) (F : C ⥤ H) (d : D) [HasColimits H] :
    Nonempty ((L.leftKanExtension F).obj d ≅ colimit (CostructuredArrow.proj L d ⋙ F)) :=
  ⟨L.leftKanExtensionObjIsoColimit F d⟩

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

What is and is not formalised. Theorems 1–4 are proved here independently only in the thin case (posets valued in complete lattices); the general pointwise formula and adjunction are cited from Mathlib. Theorem 4 in general (with absolute Kan extensions) and Theorem 5 (extension along Yoneda) are not formalised in this module.

ComputationC

Computing Kan extensions of finite sets

For functors into finite sets the pointwise formulas are algorithms: a colimit is a disjoint union glued along the arrows (a union–find computation), and a limit is the set of compatible families. The experiment computes Lan and Ran along a map of finite posets, a colimit over a diagram with a terminal object, and induced and coinduced actions of the subgroups of $S_3$ .

Pointwise Kan extensions of finite sets: colimits and limitsPythonExact computationExhaustive finite checkComputationally tested

"""Pointwise Kan extensions of finite set-valued functors, computed exactly.

The pointwise formulas say that a left Kan extension is a colimit over a
comma category and a right Kan extension is a limit. For diagrams of finite
sets both can be computed exactly: a colimit is a disjoint union glued by a
union-find structure, a limit is the set of compatible families. We use this
to (1) compare Lan and Ran along an inclusion of finite posets (coproducts
versus products, initial versus terminal objects), (2) see that a colimit over
a category with a terminal object is the value there, and (3) induce and
coinduce actions of subgroups H of S3, checking |G x_H X| = [G:H] |X| and
|Hom_H(G, X)| = |X|^[G:H]. This is exact, exhaustive computation in finite
cases; the general theorems are proved in the lesson.
"""

from itertools import permutations, product

def colimit(sets, arrows):
    """Colimit of a finite diagram of finite sets.

    ``sets`` maps each object to a list of elements; ``arrows`` is a list of
    ``(source, target, function)``. Returns the equivalence classes of the
    disjoint union {(object, element)} under (s, x) ~ (t, function(x)).
    """
    parent = {(o, x): (o, x) for o in sets for x in sets[o]}

    def find(a):
        while parent[a] != a:
            parent[a] = parent[parent[a]]
            a = parent[a]
        return a

    for source, target, fn in arrows:
        for x in sets[source]:
            ra, rb = find((source, x)), find((target, fn(x)))
            if ra != rb:
                parent[ra] = rb
    classes = {}
    for a in parent:
        classes.setdefault(find(a), set()).add(a)
    return [frozenset(c) for c in classes.values()]

def limit(sets, arrows):
    """Limit of a finite diagram of finite sets: all compatible families.

    A family picks one element of each set; it is compatible when
    ``function(family[source]) == family[target]`` for every arrow. The empty
    diagram has exactly one (empty) family: the limit is a one-point set.
    """
    objects = list(sets)
    families = []
    for values in product(*(sets[o] for o in objects)):
        family = dict(zip(objects, values))
        if all(fn(family[s]) == family[t] for s, t, fn in arrows):
            families.append(family)
    return families

def thin_diagram(objects, leq, sets, fmap):
    """Restrict a functor on a poset to ``objects`` (all arrows c < c')."""
    arrows = [
        (c, c2, (lambda x, c=c, c2=c2: fmap(c, c2, x)))
        for c in objects
        for c2 in objects
        if c != c2 and leq(c, c2)
    ]
    return {c: sets[c] for c in objects}, arrows

def lan_size(C, leq_c, k, leq_d, d, sets, fmap):
    """|Lan_k F (d)|: the colimit of F over the comma category (k | d)."""
    comma = [c for c in C if leq_d(k(c), d)]
    return len(colimit(*thin_diagram(comma, leq_c, sets, fmap)))

def ran_size(C, leq_c, k, leq_d, d, sets, fmap):
    """|Ran_k F (d)|: the limit of F over the comma category (d | k)."""
    comma = [c for c in C if leq_d(d, k(c))]
    return len(limit(*thin_diagram(comma, leq_c, sets, fmap)))

def compose(p, q):
    """Composite permutation p o q (first q, then p) of tuples."""
    return tuple(p[i] for i in q)

S3 = sorted(permutations(range(3)))

def induced_diagram(G, H, X, act):
    """F o proj on the comma category (i | *) for i : BH -> BG.

    Objects are g in G; for g2 in G and h in H there is an arrow
    g2 h -> g2 acting on X by h. Its colimit is G x_H X.
    """
    sets = {g: list(X) for g in G}
    arrows = [(compose(g2, h), g2, (lambda x, h=h: act(h, x)))
              for g2 in G for h in H]
    return sets, arrows

def coinduced_diagram(G, H, X, act):
    """F o proj on (* | i): arrows g -> h g acting by h; limit Hom_H(G, X)."""
    sets = {g: list(X) for g in G}
    arrows = [(g, compose(h, g), (lambda x, h=h: act(h, x)))
              for g in G for h in H]
    return sets, arrows

def sign(p):
    """Sign of a permutation tuple (+1 or -1), by counting inversions."""
    inv = sum(1 for i in range(len(p)) for j in range(i) if p[j] > p[i])
    return -1 if inv % 2 else 1

# Poset example: C = {a, b} discrete inside D = {bot < a, b < top}.
POSET_C = ["a", "b"]
POSET_D = ["bot", "a", "b", "top"]
POSET_SETS = {"a": [0, 1], "b": [0, 1, 2]}

def leq_d(x, y):
    """The order of D = {bot < a, b < top}."""
    return x == y or x == "bot" or y == "top"

def leq_discrete(x, y):
    """The discrete order: only x <= x."""
    return x == y

# Chain example: 0 < 1 < 2 with F(0) -> F(1) -> F(2).
CHAIN = [0, 1, 2]
CHAIN_SETS = {0: list(range(4)), 1: list(range(3)), 2: list(range(2))}

def chain_map(c, c2, x):
    """F(c <= c2): halve from F(0) to F(1), take parity from F(1) to F(2)."""
    if c == 0 and c2 >= 1:
        x, c = x // 2, 1
    if c == 1 and c2 == 2:
        x = x % 2
    return x

def subgroup_cases():
    """(name, H, X, action) for the induction table."""
    swap = [(0, 1, 2), (1, 0, 2)]
    a3 = [p for p in S3 if sign(p) == 1]
    return [
        ("H = <(0 1)>, X = {+1,-1}, sign", swap, [1, -1],
         lambda h, x: sign(h) * x),
        ("H = A3, X = {0,1,2}, rotation", a3, [0, 1, 2],
         lambda h, x: h[x]),
        ("H = 1, X = {*}", [(0, 1, 2)], ["*"], lambda h, x: x),
    ]

def main():
    print("1. Lan and Ran along C = {a, b} (discrete) -> D = {bot < a, b < top}")
    print("   with |F a| = 2, |F b| = 3:")
    print("   d     |Lan F(d)|  |Ran F(d)|")
    for d in POSET_D:
        lan = lan_size(POSET_C, leq_discrete, lambda c: c, leq_d, d,
                       POSET_SETS, None)
        ran = ran_size(POSET_C, leq_discrete, lambda c: c, leq_d, d,
                       POSET_SETS, None)
        print(f"   {d:<5} {lan:>10}  {ran:>10}")
    print("   Lan(top) is the coproduct 2 + 3, Ran(bot) the product 2 x 3;")
    print("   Lan(bot) = 0 is an empty colimit, Ran(top) = 1 an empty limit.")
    print()
    print("2. Along C = {0 < 1 < 2} -> 1 with |F| = 4, 3, 2:")
    sets, arrows = thin_diagram(CHAIN, lambda x, y: x <= y, CHAIN_SETS,
                                chain_map)
    print(f"   colim F has {len(colimit(sets, arrows))} elements = |F(2)|"
          f" (2 is terminal); lim F has {len(limit(sets, arrows))} = |F(0)|.")
    print()
    print("3. Kan extension along BH -> BG, G = S3 (|G| = 6):")
    print("   case                                 [G:H]  |Lan|  |Ran|")
    for name, H, X, act in subgroup_cases():
        index = len(S3) // len(H)
        lan = len(colimit(*induced_diagram(S3, H, X, act)))
        ran = len(limit(*coinduced_diagram(S3, H, X, act)))
        print(f"   {name:<37} {index:>5}  {lan:>5}  {ran:>5}")
    print("   Lan = G x_H X has [G:H]|X| elements; Ran = Hom_H(G, X) has")
    print("   |X|^[G:H]. For H = 1, Lan is G acting on itself: the free G-set.")
    print()
    print("Epistemic status: exact computation of finite colimits and limits;")
    print("it confirms the pointwise formulas and the induction counts only in")
    print("these finite examples. The general statements (the pointwise")
    print("formula and its consequences) are theorems proved in the lesson.")

if __name__ == "__main__":
    main()

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

What to notice: at the top of the poset, Lan gives the coproduct ( $2 + 3$ ); at the bottom, Ran gives the product ( $2 \times 3$ ); at $a$ and $b$ , both restrict back to $F$ , as Proposition 2 predicts for an order embedding. For groups, induction multiplies by the index while coinduction exponentiates. This is exact computation in finitely many cases — it illustrates the theorems but does not prove them.

Explore

Seeing the pointwise formula

A left Kan extension at $d$ is a colimit: each object $(c, f)$ of $(K \downarrow d)$ contributes a coprojection, and each morphism $u : (c, f) \to (c', f')$ forces a triangle to commute.

The colimit cocone over the comma category: whenever

f' \circ K(u) = f

, the triangle commutes.

In the poset example of the experiment ( $C = \{a, b\}$ discrete inside $\{\bot < a, b < \top\}$ ), the comma category at $\top$ is $\{a, b\}$ and the one under $\bot$ is $\{a, b\}$ as well, so the two extensions produce the two universal constructions on the pair $F(a), F(b)$ :

Right Kan extension at the bottom is a limit (product); left Kan extension at the top is a colimit (coproduct).

Try it yourself: in the experiment's code, change the sizes of $F(a)$ and $F(b)$ in POSET_SETS and predict the table before running it. Then compare part 2 of the experiment: there the indexing category is the chain $0 < 1 < 2$ , which has the terminal object $2$ , so the colimit is $F(2)$ and, dually, the limit is the value $F(0)$ at the initial object.

Exercises

1. Kan extensions

Warm-upHuman

Let $C$ and $D$ be posets, $E$ a complete lattice, $k : C \to D$ monotone and $f : C \to E$ monotone, all viewed as thin categories and functors. Which formula gives the pointwise left Kan extension $(\mathrm{Lan}_k f)(d)$ ?

Choose one

\bigvee \{\, f(c) \mid k(c) \le d \,\}

\bigwedge \{\, f(c) \mid d \le k(c) \,\}

\bigvee \{\, f(c) \mid d \le k(c) \,\}

f(c)

for the unique

c

with

k(c) = d

2. Kan extensions

Warm-upHuman

Let $K : \{a, b\} \to \mathbf{1}$ be the functor from the discrete category with two objects to the terminal category, and let $F : \{a, b\} \to \mathbf{Set}$ have $|F(a)| = 3$ and $|F(b)| = 4$ . How many elements does $(\mathrm{Lan}_K F)(\ast)$ have?

3. Kan extensions

CoreHuman

Let $H$ be a subgroup of index $3$ in a finite group $G$ , let $i : \mathbf{B}H \to \mathbf{B}G$ be the inclusion of one-object categories, and let $X$ be an $H$ -set (a functor $\mathbf{B}H \to \mathbf{Set}$ ) with $|X| = 2$ . How many elements does the right Kan extension $(\mathrm{Ran}_i X)(\ast) = \mathrm{Hom}_H(G, X)$ have?

4. Kan extensions

CoreHuman

In the proof that the pointwise formula gives a left Kan extension, given $G : \mathcal{D} \to \mathcal{E}$ and $\alpha : F \Rightarrow G K$ , we define $\sigma_d : (\mathrm{Lan}_K F)(d) \to G(d)$ by $\sigma_d \circ \iota_{(c,f)} = G(f) \circ \alpha_c$ . For this to make sense, the maps $G(f) \circ \alpha_c$ must form a cocone over $(K \downarrow d)$ : for $u : (c, f) \to (c', f')$ we need $G(f') \circ \alpha_{c'} \circ F(u) = G(f) \circ \alpha_c$ . Which fact gives this?

Choose one

Naturality of

\alpha

, together with

f' \circ K(u) = f

The universal property of the colimit

(\mathrm{Lan}_K F)(d)

The triangle identities of an adjunction

K

is fully faithful

5. Kan extensions

CoreHuman

Which situation gives a functor $F$ with no left Kan extension along $K$ ?

Choose one

K

is the inclusion of the discrete poset

\{a, b\}

into

\{a, b, \top\}

(with

a, b \le \top

), and

F

sends

a, b

to the two elements of the discrete poset

\{x, y\}

\mathcal{C}

small,

\mathcal{D}

locally small,

\mathcal{E} = \mathbf{Set}

C, D

posets and

E

a complete lattice

K = \mathrm{id}_{\mathcal{C}}

6. Kan extensions

CoreHuman

Which of these are Kan extensions? (Choose all that apply.)

Choose all that apply

The limit of

F : J \to \mathcal{C}

, as a functor

\mathbf{1} \to \mathcal{C}

A left adjoint

F

G : \mathcal{A} \to \mathcal{X}

The floor function

\mathbb{R} \to \mathbb{Z} \cup \{\pm\infty\}

Every functor

G : \mathcal{D} \to \mathcal{E}

is the left Kan extension of

G \circ K

along

K

, for every

K

7. Kan extensions

StretchHuman

Suppose $F \dashv G$ with $G : \mathcal{A} \to \mathcal{X}$ , unit $\eta$ and counit $\varepsilon$ . Which statement is correct?

Choose one

(F, \varepsilon)

is a right Kan extension of

\mathrm{id}_{\mathcal{A}}

along

G

, and it is preserved by every functor out of

\mathcal{A}

(F, \eta)

is a left Kan extension of

\mathrm{id}_{\mathcal{X}}

along

G

(F, \varepsilon)

is a right Kan extension of

\mathrm{id}_{\mathcal{A}}

along

G

, but only if

\mathcal{A}

is completeLeft adjoints are left Kan extensions and right adjoints are right Kan extensions

8. Kan extensions

CoreFormal

In the lesson's Lean file, lan k f d = ⨆ (c : C) (_ : k c ≤ d), f c. Which Lean statement says that $\mathrm{Lan}_k$ is left adjoint to restriction along $k$ (for monotone $k : C \to D$ , on monotone maps into a complete lattice $E$ )?

Choose one

GaloisConnection (fun f : C →o E => (⟨lan k f, lan_monotone k f⟩ : D →o E)) (fun g : D →o E => g.comp k)GaloisConnection (fun g : D →o E => g.comp k) (fun f : C →o E => (⟨lan k f, lan_monotone k f⟩ : D →o E))∀ f : C → E, ∀ c, lan k f (k c) = f c∀ f : C → E, lan k f ≤ ran k f

9. Kan extensions

CoreComputational

Let $C$ be a finite set of sample points in $\mathbb{R}$ , $k : C \hookrightarrow \mathbb{R}$ the inclusion and $f : C \to \mathbb{R} \cup \{\pm\infty\}$ any function, given as a dictionary {point: value}. Write lan_value(f, d) returning $(\mathrm{Lan}_k f)(d) = \sup\{ f(c) \mid c \le d \}$ (use float('-inf') for an empty supremum) and ran_value(f, d) returning $(\mathrm{Ran}_k f)(d) = \inf\{ f(c) \mid c \ge d \}$ (float('inf') if empty). Then check: when $f$ is not monotone, $\mathrm{Lan}_k f$ is its running maximum, the smallest monotone function above $f$ on the sample points.

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

Common misconceptionsH

Common misconceptions

Misconception

“Kan extensions always exist.” They do not: the two-point example above has no extension at all, because the target lacks a join. The standard sufficient condition is: $\mathcal{C}$ small, $\mathcal{D}$ locally small, and $\mathcal{E}$ cocomplete (for $\mathrm{Lan}$ ) or complete (for $\mathrm{Ran}$ ). The local smallness of $\mathcal{D}$ is easy to forget: it is what makes the comma categories $(K \downarrow d)$ small. Not every Kan extension that exists is pointwise either; in practice the pointwise ones are the ones that behave well.

Misconception

Confusing left and right. Left Kan extensions are computed by colimits over $(K \downarrow d)$ — “everything that maps to $d$ ” — and right Kan extensions by limits over $(d \downarrow K)$ . Mnemonic: floor is $\mathrm{Lan}$ , ceiling is $\mathrm{Ran}$ . But beware the twist: a left adjoint is a right Kan extension, $F = \mathrm{Ran}_G \mathrm{id}$ , because its counit $FG \Rightarrow \mathrm{id}$ has the shape of a Kan extension counit.

Misconception

“A Kan extension restricts back to the original functor.” Only when the unit is an isomorphism, which holds for pointwise extensions along fully faithful $K$ (Proposition 2). Along $K : \{a, b\} \to \mathbf{1}$ , $(\mathrm{Lan}_K F)K(a) = F(a) \sqcup F(b) \neq F(a)$ .

Misconception

“A Kan extension is just some extension.” The universal property is the point: $\mathrm{Lan}_K F$ is the initial functor equipped with $F \Rightarrow (-)K$ . In the floor example infinitely many monotone functions extend the integers; the Kan extensions are the two extreme ones.

ViewpointsH

Viewpoints

Algebra— Induction, Frobenius reciprocity and extension of scalars

For a subgroup $H \le G$ and the inclusion $i : \mathbf{B}H \to \mathbf{B}G$ , restriction $i^*$ is restriction of representations from $G$ to $H$ . For functors into $\mathrm{Vect}_k$ , the pointwise formula gives

\mathrm{Lan}_i V = k[G] \otimes_{k[H]} V = \mathrm{Ind}_H^G V, \qquad \mathrm{Ran}_i V = \mathrm{Hom}_{k[H]}(k[G], V) = \mathrm{CoInd}_H^G V,

and the adjunctions $\mathrm{Lan}_i \dashv i^* \dashv \mathrm{Ran}_i$ are Frobenius reciprocity: $\mathrm{Hom}_G(\mathrm{Ind}_H^G V, W) \cong \mathrm{Hom}_H(V, \mathrm{Res}^G_H W)$ , and its dual. For linear representations and $[G:H] < \infty$ , induction and coinduction are isomorphic; for $G$ -sets they are not ( $[G:H]\,|X|$ versus $|X|^{[G:H]}$ elements), which the experiment shows. More generally, a ring homomorphism $R \to S$ is a functor between one-object $\mathbf{Ab}$ -enriched categories, and the enriched left Kan extension of a module along it is extension of scalars $S \otimes_R M$ , with coextension $\mathrm{Hom}_R(S, M)$ on the right; this needs the enriched theory of enriched categories, where Kan extensions are coends.

Topology— Inverse images of presheaves and geometric realisation

Let $f : X \to Y$ be continuous and write $\mathcal{O}(X)$ for the poset of open sets. Preimage is a monotone map $f^{-1} : \mathcal{O}(Y) \to \mathcal{O}(X)$ . For a presheaf $\mathcal{F}$ on $Y$ , the pushforward is just precomposition, $f_*\mathcal{F} = \mathcal{F} \circ (f^{-1})^{\mathrm{op}}$ , so its left adjoint is a left Kan extension along $(f^{-1})^{\mathrm{op}}$ . The pointwise formula computes it: the comma category at an open $U \subseteq X$ consists of the opens $V \subseteq Y$ with $U \subseteq f^{-1}(V)$ , i.e. $f(U) \subseteq V$ , so

(f^{-1}_{\mathrm{pre}} \mathcal{F})(U) = \operatorname*{colim}_{V \supseteq f(U)} \mathcal{F}(V),

the familiar formula for the presheaf inverse image (the sheaf inverse image is its sheafification; see sheaves). Geometric realisation of simplicial sets is the left Kan extension of $[n] \mapsto \Delta^n$ along the Yoneda embedding $\Delta \to \mathbf{sSet}$ (Theorem 5), with right adjoint the singular complex. Beyond this lesson: in homotopy theory one needs homotopy Kan extensions (derived functors of $\mathrm{Lan}$ , such as homotopy colimits), and in ∞-categories Kan extensions are defined up to coherent homotopy.

Analysis— Best approximations from below and above

Let $f : \mathbb{Q} \to \mathbb{R}$ be monotone and $k : \mathbb{Q} \hookrightarrow \mathbb{R}$ the inclusion, with values in the complete lattice $[-\infty, \infty]$ . Then

(\mathrm{Lan}_k f)(x) = \sup_{q \le x} f(q), \qquad (\mathrm{Ran}_k f)(x) = \inf_{q \ge x} f(q).

Both extend $f$ (since $k$ is an order embedding), every monotone extension $g$ of $f$ satisfies $\mathrm{Lan}_k f \le g \le \mathrm{Ran}_k f$ , and at an irrational $x$ the two are the one-sided limits $f(x^-)$ and $f(x^+)$ . They differ exactly at the jumps of $f$ , and a monotone real-valued function has at most countably many jumps (disjoint open intervals each contain a rational). So the monotone extension of $f$ to $\mathbb{R}$ is unique if and only if $f$ has no jumps at irrational points. The Python exercise computes these envelopes on finitely many sample points.

Logic— Quantifiers are Kan extensions

Regard a function $f : X \to Y$ as a functor between discrete categories, and a predicate on $X$ as a functor $P : X \to \mathbf{2} = \{\bot \le \top\}$ . Then the pointwise formulas give

(\mathrm{Lan}_f P)(y) = \exists x\, \big(f(x) = y \wedge P(x)\big), \qquad (\mathrm{Ran}_f P)(y) = \forall x\, \big(f(x) = y \Rightarrow P(x)\big),

and $\mathrm{Lan}_f \dashv f^* \dashv \mathrm{Ran}_f$ is Lawvere's discovery that $\exists_f \dashv f^* \dashv \forall_f$ : quantifiers are adjoint to substitution. For a projection $X \times Y \to X$ these are the ordinary quantifiers over $Y$ . See categorical logic.

Computation— Codensity monads and faster programs

For any functor $G : \mathcal{A} \to \mathcal{X}$ , if the right Kan extension $T = \mathrm{Ran}_G G$ exists it carries a canonical monad structure, the codensity monad of $G$ ; when $G$ has a left adjoint $F$ , $T \cong GF$ is the monad of the adjunction (by Theorem 4, applied with $P = G$ ). A classical example (Kennison and Gildenhuys, 1971): the codensity monad of the inclusion $\mathbf{FinSet} \hookrightarrow \mathbf{Set}$ is the ultrafilter monad. In functional programming, Haskell's Codensity m a = forall b. (a -> m b) -> m b is $\mathrm{Ran}_m m$ written as an end, and Voigtländer (2008) used it to turn left-nested binds of free monads from quadratic into linear time.

Category-theoretic connectionH

All concepts are Kan extensions

Mac Lane's slogan collects the results of this lesson:

limits and colimits are Kan extensions along $J \to \mathbf{1}$ (Proposition 3);
adjoints are Kan extensions of identities, $F = \mathrm{Ran}_G \mathrm{id}$ and $G = \mathrm{Lan}_F \mathrm{id}$ (Theorem 4);
density and Yoneda: the density theorem says $\mathrm{Lan}_y\, y \cong \mathrm{id}_{\widehat{\mathcal{C}}}$ — every presheaf is canonically a colimit of representables (Theorem 5 with $F = y$ );
monads arise as codensity monads $\mathrm{Ran}_G G$ .

Even Kan extensions are Kan extensions: the definition uses only functors, natural transformations and their composites, so it makes sense in any 2-category, and the pointwise formula becomes a weighted colimit (a coend, $\int^{c} \mathcal{D}(Kc, d) \cdot F(c)$ ) in the enriched setting of Kelly (1982). The slogan is an exaggeration — not every concept is usefully a Kan extension — but it records how often a construction turns out to be “the best approximation along a functor”.

Wonder Trails

Wonder Trail

The product $A \times B$ is the right Kan extension of the pair $(A, B)$ along the functor from the two-object discrete category to $\mathbf{1}$ . This trail explores its universal property from first principles.

Wonder Trail · Optional · never gradedThe product, by its mapsCan you describe the set of pairs

A \times B

without ever looking inside it — only by how functions go into it?Follow the trail

History & global context

History and global context

Daniel M. Kan (born in the Netherlands, later at MIT) introduced adjoint functors in his paper Adjoint functors (Transactions of the American Mathematical Society, 1958), working in homotopy theory and simplicial sets. The same paper constructs what are now called Kan extensions, by the colimit and limit formulas.
In the 1960s, the Grothendieck school's work on topos theory (SGA 4, 1963–64) made systematic use of extending functors from a site to all presheaves by colimits, and F. William Lawvere showed that quantifiers are adjoint to substitution (1969).
Saunders Mac Lane's Categories for the Working Mathematician (1971) ends its chapter on Kan extensions with the section “All concepts are Kan extensions”.
Eduardo Dubuc (Argentina) developed Kan extensions in enriched category theory (Springer Lecture Notes 145, 1970), and G. M. Kelly (Sydney) made pointwise enriched Kan extensions central in Basic Concepts of Enriched Category Theory (1982).
Today Kan extensions are basic tools in homotopy theory (homotopy Kan extensions, ∞-categorical Kan extensions in Lurie's Higher Topos Theory, 2009), in representation theory, in algebraic geometry, and in functional programming.

Extending as well as possible

The picture: a triangle that need not commute

Definitions

Examples, non-examples and boundary cases

The main theorems

Kan extensions in Lean

Computing Kan extensions of finite sets

Seeing the pointwise formula

Exercises

Common misconceptions

Viewpoints

All concepts are Kan extensions

Wonder Trail

History and global context

Further reading