Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Left adjoints preserve left Kan extensions

Statement

Let K:CD and F:CE be functors, and let (L,η) be a left Kan extension of F along K.

If S:EZ is left adjoint to R:ZE, then (SL,Sη) is a left Kan extension of SF along K.

The right-handed dual is obtained by reversing the arrows, but it is not used as a separate dependency on this page.

Facts & Assumptions

Given: A left Kan extension (L,η) of F along K, and an adjunction SR with unit and counit.

[L1]

A left Kan extension (L,η) of F along K is initial among pairs (M,α) with α:FMK (Left and right Kan extensions).

[F2]

Under an adjunction SR, the right adjunct of u:SXY is u=R(u)ηX, and the left adjunct of v:XRY is v=εYS(v) (Adjuncts and transposition under an adjunction).

Proof

technique · direct
1.1

Let α:SFMK be any natural transformation. By [F2], each component αc:S(Fc)M(Kc) has a right adjunct αc:FcR(M(Kc)), and these components form a natural transformation α:F(RM)K. Since (L,η) is a left Kan extension, [L1] gives a unique natural transformation τ:LRM with α=(τK)η.

F2L1
2.1

Let σ:SLM be the left adjunct of τ. Then (σK)Sη has right adjunct (τK)η=α, so by uniqueness of adjuncts it equals α. If σ:SLM also satisfied (σK)Sη=α, then its right adjunct would satisfy the same factorization equation as τ, and [L1] would force that adjunct to equal τ; applying [F2] again gives σ=σ. Therefore (SL,Sη) is initial among pairs (M,α), hence a left Kan extension of SF along K.

F2L1step 1.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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