CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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 fully faithful left Kan extension that is not pointwise

Statement refuted

That a left Kan extension along a fully faithful functor is automatically pointwise.

The witness is a fully faithful inclusion $K : A ↪ D$ and a left Kan extension $(L, η)$ of a functor $F : A \to E$ such that $(K ↓ m)$ is empty while $L (m)$ is not initial.

Facts & Assumptions

Given: The discrete category $A$ on two objects $ℓ, r$ ; the category $D$ with objects $ℓ, m, r$ and only the arrows $m \to ℓ$ and $m \to r$ besides identities; the inclusion $K : A ↪ D$ ; the category $E$ with objects $a, b, c, d$ , identities, and only the two non-identity arrows $c \to a$ and $c \to b$ ; the functor $F$ with $F (ℓ) = a$ and $F (r) = b$ ; and the extension $L$ with $L (ℓ) = a$ , $L (r) = b$ , $L (m) = c$ , carrying the arrows of $D$ to $c \to a$ and $c \to b$ .

[F1]

A left Kan extension is initial among pairs $(M, α)$ with $α : F \Rightarrow M K$ (Left and right Kan extensions).

[F2]

A pointwise left Kan extension value at $m$ is the colimit of the comma-category diagram on $(K ↓ m)$ (Pointwise Kan extensions by the comma-category formula).

[F3]

A fully faithful functor is bijective on each hom-set (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors).

[F4]

An initial object must have a morphism to every object (Initial object, terminal object, and zero object).

Counterexample

technique · direct

1.1

The inclusion $K$ is fully faithful by [F3].

F3given

2.1

The pair $(L, η)$ with $η_{ℓ} = 1_{a}$ and $η_{r} = 1_{b}$ is a left Kan extension of $F$ along $K$ . Indeed, if $α : F \Rightarrow M K$ exists, then $M (ℓ) = a$ and $M (r) = b$ , because $a$ and $b$ have no non-identity arrows out of them; and the arrows $m \to ℓ$ and $m \to r$ force $M (m) = c$ , the only object of $E$ with arrows to both $a$ and $b$ . So $M = L$ , and then $α$ is forced to be the identity on $ℓ$ and $r$ , which leaves exactly one natural transformation $L \Rightarrow M$ . This is the universal property [F1].

F1step 1.1

3.1

But $(K ↓ m)$ is empty, because there is no arrow from $ℓ$ to $m$ and none from $r$ to $m$ in $D$ . If $(L, η)$ were pointwise, [F2] would make $L (m) = c$ the colimit of the empty diagram and hence an initial object of $E$ . That is impossible by [F4], since there is no morphism $c \to d$ . So this left Kan extension is not pointwise.

F2F4step 2.1assume-hyp

4.1

Therefore the claim is false: a fully faithful left Kan extension need not be pointwise.

step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

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., Example 6.2.17 (standard reference, not scraped)