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.

A pointwise Kan extension along a fully faithful functor genuinely extends the original functor

Statement

Let $K : C \to D$ be fully faithful.

If $(L, η)$ is a pointwise left Kan extension of $F : C \to E$ along $K$ , then for every object $c$ of $C$ the unit component

$η_{c} : F (c) ⟶ L (K c)$

is an isomorphism.

If $(R, ε)$ is a pointwise right Kan extension of $F$ along $K$ , then for every object $c$ the counit component

$ε_{c} : R (K c) ⟶ F (c)$

is an isomorphism.

So a pointwise Kan extension along a fully faithful functor really does restrict back to the original functor.

Facts & Assumptions

Given: A fully faithful functor $K : C \to D$ ; a pointwise left Kan extension $(L, η)$ of $F$ along $K$ ; and a pointwise right Kan extension $(R, ε)$ of $F$ along $K$ .

[F1]

A functor is fully faithful when every map $C (c, c^{'}) \to D (K c, K c^{'})$ is bijective (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors).

[F2]

The objects of $(K ↓ K c)$ are arrows $u : K c^{'} \to K c$ , and the objects of $(K c ↓ K)$ are arrows $u : K c \to K c^{'}$ (Comma category, slice category, and coslice category).

[L1]

A pointwise left Kan extension value is the colimit of the diagram over $(K ↓ K c)$ , with leg at $(c, 1_{K c})$ equal to $η_{c}$ ; dually, a pointwise right Kan extension value is the limit over $(K c ↓ K)$ , with leg at $(c, 1_{K c})$ equal to $ε_{c}$ (Pointwise Kan extensions by the comma-category formula).

[F3]

A colimit over a category with a terminal object is the value at that object, and dually a limit over a category with an initial object is the value there, by the universal property of colimits and limits (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

Proof

technique · direct

1.1

In $(K ↓ K c)$ the object $(c, 1_{K c})$ is terminal: for any object $(c^{'}, u : K c^{'} \to K c)$ , full faithfulness [F1] gives a unique arrow $a : c^{'} \to c$ with $K (a) = u$ , and that arrow is exactly the unique morphism $(c^{'}, u) \to (c, 1_{K c})$ in the comma category [F2]. Dually, in $(K c ↓ K)$ the object $(c, 1_{K c})$ is initial, by the same full-faithfulness argument.

F1F2

2.1

By [F3], the colimit of the diagram over $(K ↓ K c)$ is the value of the diagram at its terminal object $(c, 1_{K c})$ , namely $F (c)$ , and the colimit leg there is an isomorphism. Since [L1] identifies $L (K c)$ with that colimit and $η_{c}$ with that leg, $η_{c}$ is an isomorphism. The dual statement for $ε_{c}$ follows from the initial object in $(K c ↓ K)$ and the limit clause of [F3].

F3L1step 1.1

3.1

Therefore both the left and right pointwise Kan extensions along a fully faithful functor restrict back to the original functor by isomorphism on every object of the image.

step 2.1∎

Depends on

Used by

A left Kan extension along a full subcategory inclusion of preorders Example
FALSE: a left Kan extension along a fully faithful functor always restricts back to the original functor False statement
FALSE: every Kan extension is pointwise False statement
The presheaf category on a small category is the free cocompletion Theorem

Dependency tree · two levels

12 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., Corollary 6.2.16 (standard reference, not scraped)