Alphabeta Math
False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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.

FALSE: every Kan extension is pointwise

Statement refuted

That every left or right Kan extension is pointwise.

The witness below is a left Kan extension along a fully faithful functor which is not pointwise.

Facts & Assumptions

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

[F1]

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

[F2]

A left Kan extension is initial among pairs (M,α) with α:F⇒MK, while pointwise left Kan extensions are computed by the comma-category formula (Left and right Kan extensions, Pointwise Kan extensions by the comma-category formula, The comma-category and representable-preservation notions of pointwise Kan extension agree).

[F3]

A pointwise left Kan extension along a fully faithful functor would restrict back by isomorphism to the original functor (A pointwise Kan extension along a fully faithful functor genuinely extends the original functor).

[F4]

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

Refutation

technique · direct
1.1F1F2given

The inclusion K is fully faithful by [F1], and the pair (L,η) with ηℓ=1a and ηr=1b is a left Kan extension of F along K: if α:F⇒MK exists, then necessarily M(ℓ)=a and M(r)=b, since a has no non-identity arrow out of it and neither does b; and because M must carry the arrows m→ℓ and m→r to arrows into a and b, necessarily M(m)=c, the only object of E with arrows to both. Thus M=L and α is forced to be the identity on ℓ and r, so there is exactly one natural transformation L⇒M.

2.1F2F4step 1.1assume-hyp

But (K↓m) is empty: there is no arrow ℓ→m and no arrow r→m in D. If (L,η) were pointwise, [F2] would make L(m)=c the colimit of the empty diagram, hence an initial object of E. This is impossible by [F4], since there is no morphism c→d. Therefore (L,η) is a left Kan extension which is not pointwise.

3.1F3step 2.1∎

So the claim that every Kan extension is pointwise is false. The pointwise hypothesis in [F3] is genuinely needed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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