TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Comma-category limit and colimit formulae compute Kan extensions

Statement

Let $K : C \to D$ and $F : C \to E$ be functors, and fix $d \in D$ .

For the comma category $(K ↓ d)$ , let

$π_{d} : (K ↓ d) ⟶ C ⟶ E$

be the diagram sending $(c, u : K c \to d)$ to $F (c)$ .

If $π_{d}$ has a colimit cocone $λ_{(c, u)} : F (c) \to L_{d}$ , then $L_{d}$ has the objectwise universal property of the left Kan extension value at $d$ : for every functor $M : D \to E$ and natural transformation $α : F \Rightarrow M K$ , there is a unique morphism ${\overline{α}}_{d} : L_{d} \to M (d)$ with

${\overline{α}}_{d} \circ λ_{(c, u)} = M (u) \circ α_{c} .$

Dually, if the diagram

$σ_{d} : (d ↓ K) ⟶ C ⟶ E$

has a limit cone $ρ_{(c, u)} : R_{d} \to F (c)$ , then $R_{d}$ has the objectwise universal property of the right Kan extension value at $d$ : for every functor $M : D \to E$ and natural transformation $β : M K \Rightarrow F$ , there is a unique morphism ${\overline{β}}_{d} : M (d) \to R_{d}$ with

$ρ_{(c, u)} \circ {\overline{β}}_{d} = β_{c} \circ M (u) .$

If such colimits, respectively limits, are supplied for every $d$ , then their values and the uniquely forced arrow maps assemble into a functor ${Lan}_{K} F$ , respectively ${Ran}_{K} F$ . The left unit component $η_{c} : F (c) \to {Lan}_{K} F (K c)$ is the leg at $(c, 1_{K c})$ , and the right counit component $ε_{c} : {Ran}_{K} F (K c) \to F (c)$ is the leg at $(c, 1_{K c})$ .

Facts & Assumptions

Given: Functors $K : C \to D$ and $F : C \to E$ ; an object $d$ of $D$ ; the comma categories $(K ↓ d)$ and $(d ↓ K)$ ; and the diagrams $π_{d}$ and $σ_{d}$ described in the Statement.

[F1]

The objects of $(K ↓ d)$ are pairs $(c, u : K c \to d)$ and the objects of $(d ↓ K)$ are pairs $(c, u : d \to K c)$ , with the usual commuting-arrow morphisms (Comma category, slice category, and coslice category).

[F2]

A colimit is an initial cocone and a limit is a terminal cone: morphisms out of a colimit, and into a limit, are uniquely determined by their composites with the structure maps (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties, Constant diagrams, cones, cocones, and their morphisms).

[F3]

A left Kan extension $(L, η)$ of $F$ along $K$ is initial among pairs $(M, α)$ with $α : F \Rightarrow M K$ , and a right Kan extension $(R, ε)$ is terminal among pairs $(M, β)$ with $β : M K \Rightarrow F$ (Left and right Kan extensions).

Proof

technique · direct

1.1

Let $α : F \Rightarrow M K$ . For each object $(c, u : K c \to d)$ of $(K ↓ d)$ , the morphism $M (u) \circ α_{c} : F (c) \to M (d)$ is natural in $(c, u)$ because $α$ is natural, so it is a cocone under $π_{d}$ . By [F2] there is a unique morphism ${\overline{α}}_{d} : L_{d} \to M (d)$ with ${\overline{α}}_{d} λ_{(c, u)} = M (u) α_{c}$ for every $(c, u)$ . This is exactly the left objectwise universal property at $d$ .

F1F2F3

1.2

Let $β : M K \Rightarrow F$ . For each object $(c, u : d \to K c)$ of $(d ↓ K)$ , the morphism $β_{c} \circ M (u) : M (d) \to F (c)$ is natural in $(c, u)$ , hence a cone over $σ_{d}$ . By [F2] there is a unique morphism ${\overline{β}}_{d} : M (d) \to R_{d}$ with $ρ_{(c, u)} {\overline{β}}_{d} = β_{c} M (u)$ for every $(c, u)$ . This is exactly the right objectwise universal property at $d$ .

F1F2F3

2.1

Suppose the colimits are supplied for all $d$ . For $v : d \to d^{'}$ , the family $λ_{(c, v u)} : F (c) \to L_{d^{'}}$ is a cocone under $π_{d}$ , so [F2] gives a unique morphism ${Lan}_{K} F (v) : L_{d} \to L_{d^{'}}$ with ${Lan}_{K} F (v) λ_{(c, u)} = λ_{(c, v u)}$ ; uniqueness makes identities and composition hold, so the values assemble into a functor, and the leg at $(c, 1_{K c})$ is the unit component $η_{c}$ . The same argument with the cones of step 1.2 assembles the supplied limits into ${Ran}_{K} F$ , with counit component $ε_{c}$ the leg at $(c, 1_{K c})$ .

F1F2step 1.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

E. Riehl, Category Theory in Context, 2nd ed., Theorem 6.2.1 (standard reference, not scraped)
B. Richter, From Categories to Homotopy Theory, §§4.1-4.2 (standard reference, not scraped)