Alphabeta Math
TheoremStatement: AI-adaptedProof: 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.

The presheaf category on a small category is the free cocompletion

Statement

Let C be small, let y:C→[Cop,Set] be the Yoneda embedding, let E be locally small and cocomplete, and let F:C→E be a functor.

For each presheaf P, choose a colimit in E of the canonical density diagram

∫P⟶C⟶FE.

These chosen colimits assemble into a functor

Lan⁡yF:[Cop,Set]⟶E,

and this functor is left adjoint to

E(F−,−):E⟶[Cop,Set].

Conversely, if L:[Cop,Set]→E is any left adjoint, then with F:=Ly one has

L≅Lan⁡yF,andright adjoint⁡(L)≅E(F−,−).

More generally, every functor L:[Cop,Set]→E that preserves all small colimits satisfies L≅Lan⁡y(Ly). Every natural transformation between two functors on C extends uniquely to a natural transformation between their small-colimit-preserving extensions.

So [Cop,Set] is the free cocompletion of C under small colimits, with the chosen-colimit clause made explicit in the data.

Facts & Assumptions

Given: A small category C, the Yoneda embedding y, a locally small cocomplete category E, and a functor F:C→E.

[L1]

The identity functor on the presheaf category is the pointwise left Kan extension of y along y (The Yoneda embedding is its own pointwise left Kan extension).

[L2]

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

[L3]

For presheaves P,Q, cocones from the canonical density diagram of P to Q are exactly natural transformations P⇒Q (Density theorem for a small category).

[L4]

Natural transformations y(c)⇒H are naturally in bijection with elements of H(c) (For a presheaf P, Nat⁡(C(−,a),P)≅P(a) naturally in a and P).

[L5]

Two left adjoints to the same functor are uniquely naturally isomorphic in a way compatible with the adjunction data (Adjoints are unique up to a unique natural isomorphism compatible with the adjunction data).

[L6]

The comma-category colimit formula computes the pointwise left Kan extension value at each target object (Comma-category limit and colimit formulae compute Kan extensions).

[L7]

For small C, the Yoneda functor y:C→[Cop,Set] is fully faithful (The Yoneda functor is fully faithful, and it is a full embedding when its object map is injective).

[L8]

Every left adjoint preserves all colimits that exist (Left adjoints preserve every colimit that exists).

Proof

technique · direct
1.1L1L2L4L6L7

Fix a presheaf P. Under the Yoneda bijection [L4], an object of the comma category (y↓P) is exactly a pair (c,x) with x∈P(c), and the comma-category morphism condition says that a map (c,x)→(d,y) is precisely an arrow f:c→d with x=P(f)(y), exactly as in the category of elements (The category of elements of a covariant functor or a presheaf, The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding). So (y↓P) is canonically ∫P, the same indexing category that appears in the self-Kan presentation [L1], and the displayed diagram ∫P→C→FE is the comma-category diagram used by [L6]. Therefore its chosen colimit is the pointwise left Kan extension value of F along y at P. Because these colimits and their universal cocones are supplied for every P, [L6] assembles them into a functor Lan⁡yF:[Cop,Set]→E. By [L7] the functor y is fully faithful, so [L2] shows that this pointwise extension restricts along y to F up to the canonical isomorphism.

2.1L3L4step 1.1

Let e∈E, and define the presheaf Qe:=E(F−,e) on C. A morphism Lan⁡yF(P)→e is, by the chosen colimit universal property, exactly a cocone from the diagram ∫P→C→FE to the constant diagram at e. By [L4], giving such a cocone is equivalently giving, for each object (c,x) of ∫P, an element of Qe(c) natural in morphisms of ∫P, that is, a cocone from the canonical density diagram of P to Qe. By [L3], these cocones are exactly natural transformations P⇒Qe=P⇒E(F−,e). Hence E(Lan⁡yF(P),e)≅[Cop,Set](P,E(F−,−)) naturally in P and e, so Lan⁡yF⊣E(F−,−).

2.2L3step 1.1

Now let L:[Cop,Set]→E preserve all small colimits and put F:=Ly. By [L3], every presheaf P is the colimit of its canonical density diagram of representables. Applying L preserves that colimit, so L(P) is the colimit of the diagram (c,x)↦Ly(c)=F(c). By step 1.1 this is exactly Lan⁡yF(P), naturally in P. Hence L≅Lan⁡y(Ly).

3.1L8step 2.1

Since Lan⁡yF is a left adjoint by step 2.1, [L8] shows that it preserves all small colimits.

3.2L4L5step 2.1

Conversely, let L⊣H with domain the presheaf category, and put F:=Ly. For any e∈E and c∈C, adjunction and [L4] give H(e)(c)≅[Cop,Set](y(c),H(e))≅E(Ly(c),e)=E(F(c),e), naturally in c and e. So H≅E(F−,−), and step 2.1 shows Lan⁡yF is another left adjoint to the same right adjoint. Therefore [L5] gives L≅Lan⁡yF.

4.1L3step 3.1step 2.2∎

Given τ:F⇒F′, its components induce a morphism between the two chosen density colimits at every presheaf, and the colimit universal properties make these morphisms natural. Conversely, any natural transformation between small-colimit-preserving extensions is determined at P by its components on the representables in the canonical density colimit of [L3]. Therefore extension of τ is unique, which completes the free-cocompletion universal property.

Depends on

Used by

Dependency tree · two levels

34 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