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 and be functors, and let be a left Kan extension of along .
If is left adjoint to , then is a left Kan extension of along .
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 of along , and an adjunction with unit and counit.
A left Kan extension of along is initial among pairs with (Left and right Kan extensions).
Under an adjunction , the right adjunct of is , and the left adjunct of is (Adjuncts and transposition under an adjunction).
Proof
Let be any natural transformation. By [F2], each component has a right adjunct , and these components form a natural transformation . Since is a left Kan extension, [L1] gives a unique natural transformation with .
Let be the left adjunct of . Then has right adjunct , so by uniqueness of adjuncts it equals . If also satisfied , then its right adjunct would satisfy the same factorization equation as , and [L1] would force that adjunct to equal ; applying [F2] again gives . Therefore is initial among pairs , hence a left Kan extension of along .
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
- E. Riehl, Category Theory in Context, 2nd ed., Lemma 6.3.2 (standard reference, not scraped)
- B. Richter, From Categories to Homotopy Theory, §4.3 (standard reference, not scraped)