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

FALSE: a left Kan extension along a fully faithful functor always restricts back to the original functor

Statement refuted

That for every fully faithful K:C→D and every left Kan extension (L,η) of F along K, the unit components ηc:F(c)→L(Kc) are automatically isomorphisms.

The published positive theorem A pointwise Kan extension along a fully faithful functor genuinely extends the original functor shows this is true only under the pointwise hypothesis.

Facts & Assumptions

Given: The discrete category A with objects ℓ and r; the walking span D with objects ℓ,m,r and non-identity arrows s:m→ℓ and t:m→r; the fully faithful inclusion K:A↪D; the category E with objects L,L′,M,R′,R, identities, and exactly four non-identity arrows f:L→L′, g:M→L′, h:M→R′, and k:R→R′; the functor F:A→E with F(ℓ)=L and F(r)=R; the functor G:D→E with G(ℓ)=L′, G(m)=M, G(r)=R′, G(s)=g, and G(t)=h; and the natural transformation λ:F⇒GK with components λℓ=f and λr=k.

[F1]

A left Kan extension is initial among pairs (M,α) with α:F⇒MK (Left and right Kan extensions).

[L1]

If such a left Kan extension were pointwise, then the unit component at r would be an isomorphism (A pointwise Kan extension along a fully faithful functor genuinely extends the original functor).

Refutation

technique · direct
1.1F2given

The inclusion K is fully faithful because A is discrete and D has no non-identity arrows between the image objects ℓ and r, so each hom-set map is bijective as required by [F2].

2.1F1step 1.1

The pair (G,λ) is a left Kan extension of F along K. Let M:D→E and α:F⇒MK. Because D has arrows m→ℓ and m→r, the object M(m) must admit arrows to both M(ℓ) and M(r). In E the only object with arrows to two targets is M, via g:M→L′ and h:M→R′. Therefore M(m)=M, M(ℓ)=L′, M(r)=R′, and the two span arrows must be sent to g and h. So M=G. Then αℓ:L→L′ and αr:R→R′ are forced to be f and k, whence α=λ. Since the only endomorphisms of L′, M, and R′ are identities, the only natural transformation G⇒M=G is the identity. Thus (G,λ) satisfies the universal property [F1].

3.1L1step 2.1∎

The components λℓ=f:L→L′ and λr=k:R→R′ are not isomorphisms, since E has no arrows L′→L or R′→R. Therefore the unrestricted claim is false. By [L1], this also shows that the witness is not pointwise.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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