ExampleConstruction: AI-adaptedVerification: 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.

A left Kan extension along the inclusion of the rationals in the reals

Example

View $Q$ and $R$ as thin categories under their usual order, and let $i : Q ↪ R$ be the inclusion (A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps).

Define a functor $F : Q \to S e t$ by

$F (q) = (- \infty, q) \subseteq R,$

with the structure maps the evident inclusions when $q \leq q^{'}$ .

Then the pointwise left Kan extension of $F$ along $i$ is the functor $L : R \to S e t$ with

$L (x) = (- \infty, x) \subseteq R .$

Facts & Assumptions

Given: The inclusion $i : Q ↪ R$ and the functor $F (q) = (- \infty, q)$ .

[F1]

A preorder gives a thin category, and a monotone map gives a functor (A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps).

[L1]

The comma-category colimit formula computes the left Kan extension value at a real number $x$ (Comma-category limit and colimit formulae compute Kan extensions).

[L2]

Between any two distinct reals there is a rational number (The rationals embed densely in the reals).

Verification

technique · direct

1.1F1L1

For a real $x$ , the comma category $(i ↓ x)$ is the preorder of rationals $q \leq x$ . The induced diagram sends such a $q$ to $(- \infty, q)$ and its colimit in $S e t$ is the union $⋃_{q \leq x, q \in Q} (- \infty, q)$ .

2.1L2step 1.1

This union is exactly $(- \infty, x)$ . If $r < x$ , [L2] gives a rational $q$ with $r < q < x$ , so $r \in (- \infty, q)$ and hence lies in the union. Conversely every $(- \infty, q)$ with $q \leq x$ is contained in $(- \infty, x)$ .

3.1L1step 2.1∎

Therefore [L1] gives $L (x) = (- \infty, x)$ for the left Kan extension value at every real $x$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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