Alphabeta Math
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.

✓ 21 results · all verified · 12 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 9 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Kan Extensions Density and the Free Cocompletion

1 · Prerequisites

2 · Summary

This page uses the published language of functor categories, comma categories, adjunctions, Yoneda, and weighted limits to turn Kan extensions from a universal property into something computable. Restriction along K, representables, and categories of elements are the bridges: they let the same object be read as a local extension, a comma-category colimit or limit, and later as a coend or end.

It defines local, global, pointwise, and absolute Kan extensions; proves their uniqueness, the restriction adjunctions, the fully faithful extension theorem, and the coend/end formulas; then reinterprets limits, colimits, adjunctions, and evaluation as Kan extensions. From there it proves density for presheaves, identifies Yoneda as its own pointwise left Kan extension, derives the free-cocompletion theorem for presheaf categories, and closes with the codensity monad and its ultrafilter realization.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Left and right Kan extensions

Definition

Let C, D, and E be categories, let K:C→D be a functor, and let F:C→E be a functor (Covariant functor, identity functor, composite functor, and contravariant functor).

A left Kan extension of F along K is a functor L:D→E together with a natural transformation

η:F⇒LK

(Natural transformation and its components) such that for every functor M:D→E and every natural transformation α:F⇒MK, there exists a unique natural transformation α‾:L⇒M with

α=(α‾K)∘η.

Thus (L,η) is initial among pairs (M,α) with α:F⇒MK.

A right Kan extension of F along K is a functor R:D→E together with a natural transformation

ε:RK⇒F

such that for every functor M:D→E and every natural transformation β:MK⇒F, there exists a unique natural transformation β‾:M⇒R with

β=ε∘(β‾K).

Thus (R,ε) is terminal among pairs (M,β) with β:MK⇒F.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Mac Lane's warning about left and right Kan extensions

Remarks

Mac Lane warns in Chapter X.3 that some authors reverse the names. This library follows Left and right Kan extensions: a left Kan extension comes with a unit F⇒LK, and a right Kan extension comes with a counit RK⇒F.

Nothing mathematical changes with the vocabulary, but the directions of the two structure maps do. This page therefore keeps those arrows visible in every definition and theorem rather than writing only Lan⁡K and Ran⁡K.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Kan extensions are unique up to unique isomorphism

Statement

Let K:C→D and F:C→E be functors.

If (L,η) and (L′,η′) are left Kan extensions of F along K, then there is a unique natural isomorphism α:L⇒L′ such that

η′=(αK)∘η.

If (R,ε) and (R′,ε′) are right Kan extensions of F along K, then there is a unique natural isomorphism β:R⇒R′ such that

ε=ε′∘(βK).

So both left and right Kan extensions are unique up to unique compatible isomorphism.

Facts & Assumptions

Given: Functors K:C→D and F:C→E; left Kan extensions (L,η) and (L′,η′) of F along K; and right Kan extensions (R,ε) and (R′,ε′) of F along K.

[L1]

A left Kan extension (L,η) of F along K is initial among pairs (M,α) with α:F⇒MK, and a right Kan extension (R,ε) is terminal among pairs (M,β) with β:MK⇒F (Left and right Kan extensions).

Proof

technique · direct
1.1L1

Since (L,η) is a left Kan extension and η′:F⇒L′K is another such pair, [L1] gives a unique natural transformation α:L⇒L′ with η′=(αK)∘η; similarly [L1] gives a unique natural transformation α′:L′⇒L with η=(α′K)∘η′.

2.1L1step 1.1

By step 1.1, ((α′α)K)∘η=(α′K)∘η′=η, while (1LK)∘η=η trivially. So the uniqueness clause of [L1] forces α′α=1L; likewise αα′=1L′. Hence α is a natural isomorphism, and its compatibility with η was built in at step 1.1.

3.1L1step 2.1∎

The same argument with the terminal clause of [L1] gives unique β:R⇒R′ and β′:R′⇒R satisfying ε=ε′∘(βK) and ε′=ε∘(β′K), and uniqueness forces β′β=1R and ββ′=1R′. So right Kan extensions are unique up to unique compatible isomorphism as well.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Global Kan extensions as adjoints to restriction

Definition

Let K:C→D be a functor with C and D small, and let E be locally small (Small, locally small, and large categories, If C is small and D is locally small then [C,D] is locally small; if both are small it is small). Then the functor categories [C,E] and [D,E] are legitimate categories (Functor category [C,D]).

Precomposition with K defines the restriction functor

K∗:[D,E]⟶[C,E],H⟼HK.

A global left Kan extension along K is a functor

Lan⁡K:[C,E]⟶[D,E]

equipped with an adjunction Lan⁡K⊣K∗ in the sense of Adjunction by unit, counit, and the triangle identities.

Dually, a global right Kan extension along K is a functor

Ran⁡K:[C,E]⟶[D,E]

equipped with an adjunction K∗⊣Ran⁡K.

This is a functor-level notion. It differs from a local Kan extension of one functor F:C→E in Left and right Kan extensions: forming a global Kan extension requires data for every object of the functor category, not a silent class-indexed choice of one local extension for each F.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Lan is left adjoint to restriction, and restriction is left adjoint to Ran

Statement

Let K:C→D be a functor with C and D small and E locally small, so that the restriction functor

K∗:[D,E]⟶[C,E]

is defined (Global Kan extensions as adjoints to restriction).

Assume that for every functor F:C→E a local left Kan extension of F along K is supplied, and for every such F a local right Kan extension of F along K is supplied.

Then the object assignments F↦Lan⁡KF and F↦Ran⁡KF admit unique functor structures for which

Lan⁡K⊣K∗⊣Ran⁡K.

No class-indexed choice is made inside the proof: the local Kan extensions are part of the data.

Facts & Assumptions

Given: The functor K:C→D with C,D small and E locally small; the restriction functor K∗; and supplied local left and right Kan extensions for every F:C→E.

[F1]

A local left Kan extension of F along K is a pair (L,η) initial among natural transformations F⇒MK, and a local right Kan extension is a pair (R,ε) terminal among natural transformations MK⇒F (Left and right Kan extensions).

[L1]

Chosen universal arrows from each object to a functor assemble uniquely into a left adjoint (Chosen objectwise universal arrows assemble uniquely into a left adjoint).

[L2]

A left adjoint to a functor is supplied exactly by chosen initial objects in its comma categories, and dually a right adjoint is supplied exactly by chosen terminal objects (A left adjoint exists exactly when chosen initial objects are supplied in every comma category).

Proof

technique · direct
1.1F1

By [F1], each supplied local left Kan extension of a functor F:C→E is exactly a universal arrow from the object F of [C,E] to the restriction functor K∗, while each supplied local right Kan extension is exactly a terminal object of the corresponding comma category for K∗.

2.1L1step 1.1

Applying [L1] to the supplied universal arrows of step 1.1 gives a unique functor structure on F↦Lan⁡KF for which the displayed unit transformations are natural, and with that structure Lan⁡K⊣K∗.

3.1L2step 1.1step 2.1∎

Applying the dual clause of [L2] to the supplied terminal objects of step 1.1 gives a unique functor structure on F↦Ran⁡KF with K∗⊣Ran⁡K. Hence Lan⁡K⊣K∗⊣Ran⁡K.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Comma-category limit and colimit formulae compute Kan extensions

Statement

Let K:C→D and F:C→E be functors, and fix d∈D.

For the comma category (K↓d), let

πd:(K↓d)⟶C⟶E

be the diagram sending (c,u:Kc→d) to F(c).

If πd has a colimit cocone λ(c,u):F(c)→Ld, then Ld has the objectwise universal property of the left Kan extension value at d: for every functor M:D→E and natural transformation α:F⇒MK, there is a unique morphism α‾d:Ld→M(d) with

α‾d∘λ(c,u)=M(u)∘αc.

Dually, if the diagram

σd:(d↓K)⟶C⟶E

has a limit cone ρ(c,u):Rd→F(c), then Rd has the objectwise universal property of the right Kan extension value at d: for every functor M:D→E and natural transformation β:MK⇒F, there is a unique morphism β‾d:M(d)→Rd with

ρ(c,u)∘β‾d=βc∘M(u).

If such colimits, respectively limits, are supplied for every d, then their values and the uniquely forced arrow maps assemble into a functor Lan⁡KF, respectively Ran⁡KF. The left unit component ηc:F(c)→Lan⁡KF(Kc) is the leg at (c,1Kc), and the right counit component εc:Ran⁡KF(Kc)→F(c) is the leg at (c,1Kc).

Facts & Assumptions

Given: Functors K:C→D and F:C→E; an object d of D; the comma categories (K↓d) and (d↓K); and the diagrams πd and σd described in the Statement.

[F1]

The objects of (K↓d) are pairs (c,u:Kc→d) and the objects of (d↓K) are pairs (c,u:d→Kc), with the usual commuting-arrow morphisms (Comma category, slice category, and coslice category).

[F2]

A colimit is an initial cocone and a limit is a terminal cone: morphisms out of a colimit, and into a limit, are uniquely determined by their composites with the structure maps (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties, Constant diagrams, cones, cocones, and their morphisms).

[F3]

A left Kan extension (L,η) of F along K is initial among pairs (M,α) with α:F⇒MK, and a right Kan extension (R,ε) is terminal among pairs (M,β) with β:MK⇒F (Left and right Kan extensions).

Proof

technique · direct
1.1F1F2F3

Let α:F⇒MK. For each object (c,u:Kc→d) of (K↓d), the morphism M(u)∘αc:F(c)→M(d) is natural in (c,u) because α is natural, so it is a cocone under πd. By [F2] there is a unique morphism α‾d:Ld→M(d) with α‾dλ(c,u)=M(u)αc for every (c,u). This is exactly the left objectwise universal property at d.

1.2F1F2F3

Let β:MK⇒F. For each object (c,u:d→Kc) of (d↓K), the morphism βc∘M(u):M(d)→F(c) is natural in (c,u), hence a cone over σd. By [F2] there is a unique morphism β‾d:M(d)→Rd with ρ(c,u)β‾d=βcM(u) for every (c,u). This is exactly the right objectwise universal property at d.

2.1F1F2step 1.1step 1.2∎

Suppose the colimits are supplied for all d. For v:d→d′, the family λ(c,vu):F(c)→Ld′ is a cocone under πd, so [F2] gives a unique morphism Lan⁡KF(v):Ld→Ld′ with Lan⁡KF(v)λ(c,u)=λ(c,vu); uniqueness makes identities and composition hold, so the values assemble into a functor, and the leg at (c,1Kc) is the unit component ηc. The same argument with the cones of step 1.2 assembles the supplied limits into Ran⁡KF, with counit component εc the leg at (c,1Kc).

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Pointwise Kan extensions by the comma-category formula

Definition

Let K:C→D and F:C→E be functors.

Suppose (L,η) is a left Kan extension of F along K (Left and right Kan extensions). It is pointwise when, for every object d of D, the value L(d) is computed by the comma-category colimit of Comma-category limit and colimit formulae compute Kan extensions: the family of morphisms

L(u)∘ηc:F(c)⟶L(d)

indexed by the objects (c,u:Kc→d) of (K↓d) (Comma category, slice category, and coslice category) is a colimit cocone of the diagram (K↓d)→C→E. In particular, at d=Kc and u=1Kc this leg is ηc.

Suppose instead that (R,ε) is a right Kan extension of F along K. It is pointwise when, for every object d of D, the value R(d) is computed by the comma-category limit formula: the family

εc∘R(u):R(d)⟶F(c)

indexed by the objects (c,u:d→Kc) of (d↓K) is a limit cone of the diagram (d↓K)→C→E. In particular, at d=Kc and u=1Kc this leg is εc.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Pointwise Kan extensions exist under smallness and completeness hypotheses

Statement

Let K:C→D and F:C→E be functors.

If C is small, D locally small, and E cocomplete, then for every d∈D the comma category (K↓d) is small and the pointwise left Kan extension value at d exists.

If C is small, D locally small, and E complete, then for every d∈D the comma category (d↓K) is small and the pointwise right Kan extension value at d exists.

These are objectwise existence statements. A global functor Lan⁡KF or Ran⁡KF is obtained only when the corresponding colimits or limits are supplied, with chosen universal cones, for every d.

Facts & Assumptions

Given: Functors K:C→D and F:C→E with C small and D locally small.

[F1]

A category is small when its objects and morphisms form sets, and locally small when every hom-collection is a set (Small, locally small, and large categories).

[F2]

A category is cocomplete when it has all small colimits and complete when it has all small limits (Finite, small, and large limits and colimits; complete and cocomplete categories).

[L1]

For each object d, the comma-category colimit over (K↓d) computes the pointwise left Kan extension value, and the comma-category limit over (d↓K) computes the pointwise right Kan extension value (Comma-category limit and colimit formulae compute Kan extensions, Pointwise Kan extensions by the comma-category formula).

Proof

technique · direct
1.1F1

Because C is small and D is locally small, the objects of (K↓d) form a set: they are pairs (c,u) with c∈C and u∈D(Kc,d), and both pieces are set-sized by [F1]. Its morphisms are arrows of C satisfying one extra equation, so they also form a set. The same argument applies to (d↓K). Thus both comma categories are small.

2.1F2L1step 1.1

If E is cocomplete, then every small diagram in E has a colimit by [F2], so the diagram from (K↓d) into E has a colimit for each d; by [L1] that colimit is the pointwise left Kan extension value at d. Dually, if E is complete, then every diagram from (d↓K) into E has a limit, and [L1] makes it the pointwise right Kan extension value at d.

3.1L1step 2.1∎

The values obtained in step 2.1 exist objectwise. A global pointwise Kan extension functor requires, in addition, that these colimits or limits and their universal cones be supplied for every d, because that is the data used in [L1] to assemble the arrow maps of Lan⁡KF or Ran⁡KF.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Pointwise Kan extensions as those preserved by representables

Definition

Let K:C→D and F:C→E be functors, with D and E locally small (Small, locally small, and large categories).

Suppose (R,ε) is a right Kan extension of F along K (Left and right Kan extensions). It is pointwise when, for every object e of E, the covariant representable functor

E(e,−):E→Set

(The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category) sends (R,ε) to a right Kan extension of E(e,F−) along K.

Suppose (L,η) is a left Kan extension of F along K. It is pointwise when, after passage to opposite categories (Opposite category Cop), the corresponding right Kan extension in Eop is preserved by every covariant representable of Eop, equivalently by every contravariant representable

E(−,e):Eop→Set.

So the phrase "preserved by representables" is not one definition but two variance-specific ones: covariant representables for right Kan extensions, and contravariant representables after passing to opposites for left Kan extensions.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

The comma-category and representable-preservation notions of pointwise Kan extension agree

Statement

Let K:C→D and F:C→E be functors, with C small and D,E locally small (Small, locally small, and large categories).

For a right Kan extension of F along K, the two definitions

  1. pointwise by the comma-category limit formula, and
  2. pointwise by preservation by all representables,

are equivalent (Pointwise Kan extensions by the comma-category formula, Pointwise Kan extensions as those preserved by representables).

By passage to opposite categories, the same equivalence holds for left Kan extensions.

Facts & Assumptions

Given: Functors K:C→D and F:C→E with C small and D,E locally small, and a right Kan extension (R,ε) of F along K.

[F1]

A right Kan extension is pointwise by the comma-category formula when, for every d, the canonical cone with vertex R(d) and legs εc∘R(u) indexed by (c,u:d→Kc) is a limit cone; it is pointwise by representable preservation when every covariant representable E(e,−) carries it to a right Kan extension in Set (Pointwise Kan extensions by the comma-category formula, Pointwise Kan extensions as those preserved by representables).

[L1]

The comma-category formulas compute pointwise Kan extension values (Comma-category limit and colimit formulae compute Kan extensions).

[L2]

Every covariantly representable functor to Set preserves all existing small limits (Every covariantly representable functor to Set preserves all existing small limits).

[F2]

For fixed e∈E, the functor E(e,−):E→Set is covariantly representable (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[L3]

For a locally small category, evaluation at the identity gives a bijection Nat⁡(D(d,−),H)≅H(d) for every Set-valued functor H (Evaluation at the identity gives Nat⁡(C(a,−),F)≅F(a) and proves that the natural-transformation collection is a set).

Proof

technique · direct
1.1F1F2L1L2

Suppose (R,ε) is pointwise by the comma-category formula. Then for each d the value R(d) is the limit of the diagram on (d↓K) by [F1]. Because C is small and D locally small, this comma category is small, so [L2] applies to every representable [F2]: E(e,R(d)) is the limit in Set of the Set-valued diagram obtained by applying E(e,−) to that cone. By [L1], this says E(e,−) carries (R,ε) to a right Kan extension of E(e,F−) along K. So the comma-category notion implies the representable-preservation notion.

1.2F1F2algebra

Conversely, suppose every representable E(e,−) carries (R,ε) to a right Kan extension. Fix d∈D and e∈E. A cone from e to the diagram on (d↓K) is equivalently a natural transformation D(d,K−)⇒E(e,F−):C→Set, because its component at c assigns to each u:d→Kc the corresponding leg e→F(c).

2.1L3F1step 1.2

The preserved right Kan universal property gives a bijection from the natural transformations in step 1.2 to Nat⁡(D(d,−),E(e,R−)). By [L3], evaluation at 1d identifies the latter set with E(e,R(d)). Under these two bijections a morphism h:e→R(d) is sent to the canonical cone with legs εc∘R(u)∘h, so the correspondence is natural in e. Hence the canonical cone with vertex R(d) represents the cone functor and is a limit cone.

3.1F1step 2.1∎

Since d was arbitrary, (R,ε) is pointwise by the comma-category formula. The left-handed equivalence is the same argument in opposite categories, exactly as encoded in the left definition of [F1].

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-26Open item page →

Absolute Kan extension

Definition

Let (L,η) be a left Kan extension of F:C→E along K:C→D (Left and right Kan extensions). It is absolute when for every functor H:E→Z (Covariant functor, identity functor, composite functor, and contravariant functor), the pair (HL,Hη) is again a left Kan extension of HF along K.

Dually, a right Kan extension (R,ε) of F along K is absolute when for every functor H:E→Z, the pair (HR,Hε) is again a right Kan extension of HF along K.

Pointwise asks for preservation only by representables of the codomain; absolute asks for preservation by every functor out of the codomain and is therefore the stronger condition.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

Left adjoints preserve left Kan extensions

Statement

Let K:C→D and F:C→E be functors, and let (L,η) be a left Kan extension of F along K.

If S:E→Z is left adjoint to R:Z→E, 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 S⊣R with unit and counit.

[L1]

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

[F2]

Under an adjunction S⊣R, the right adjunct of u:SX→Y is u♭=R(u)∘ηX, and the left adjunct of v:X→RY is v♯=εY∘S(v) (Adjuncts and transposition under an adjunction).

Proof

technique · direct
1.1F2L1

Let α:SF⇒MK be any natural transformation. By [F2], each component αc:S(Fc)→M(Kc) has a right adjunct αc♭:Fc→R(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 τ:L⇒RM with α♭=(τK)∘η.

2.1F2L1step 1.1∎

Let σ:SL⇒M be the left adjunct of τ. Then (σK)∘Sη has right adjunct (τK)∘η=α♭, so by uniqueness of adjuncts it equals α. If σ′:SL⇒M 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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

A pointwise Kan extension along a fully faithful functor genuinely extends the original functor

Statement

Let K:C→D be fully faithful.

If (L,η) is a pointwise left Kan extension of F:C→E along K, then for every object c of C the unit component

ηc:F(c)⟶L(Kc)

is an isomorphism.

If (R,ε) is a pointwise right Kan extension of F along K, then for every object c the counit component

εc:R(Kc)⟶F(c)

is an isomorphism.

So a pointwise Kan extension along a fully faithful functor really does restrict back to the original functor.

Facts & Assumptions

Given: A fully faithful functor K:C→D; a pointwise left Kan extension (L,η) of F along K; and a pointwise right Kan extension (R,ε) of F along K.

[F1]

A functor is fully faithful when every map C(c,c′)→D(Kc,Kc′) is bijective (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors).

[F2]

The objects of (K↓Kc) are arrows u:Kc′→Kc, and the objects of (Kc↓K) are arrows u:Kc→Kc′ (Comma category, slice category, and coslice category).

[L1]

A pointwise left Kan extension value is the colimit of the diagram over (K↓Kc), with leg at (c,1Kc) equal to ηc; dually, a pointwise right Kan extension value is the limit over (Kc↓K), with leg at (c,1Kc) equal to εc (Pointwise Kan extensions by the comma-category formula).

[F3]

A colimit over a category with a terminal object is the value at that object, and dually a limit over a category with an initial object is the value there, by the universal property of colimits and limits (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

Proof

technique · direct
1.1F1F2

In (K↓Kc) the object (c,1Kc) is terminal: for any object (c′,u:Kc′→Kc), full faithfulness [F1] gives a unique arrow a:c′→c with K(a)=u, and that arrow is exactly the unique morphism (c′,u)→(c,1Kc) in the comma category [F2]. Dually, in (Kc↓K) the object (c,1Kc) is initial, by the same full-faithfulness argument.

2.1F3L1step 1.1

By [F3], the colimit of the diagram over (K↓Kc) is the value of the diagram at its terminal object (c,1Kc), namely F(c), and the colimit leg there is an isomorphism. Since [L1] identifies L(Kc) with that colimit and ηc with that leg, ηc is an isomorphism. The dual statement for εc follows from the initial object in (Kc↓K) and the limit clause of [F3].

3.1step 2.1∎

Therefore both the left and right pointwise Kan extensions along a fully faithful functor restrict back to the original functor by isomorphism on every object of the image.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

Kan extensions as coends and ends

Statement

Let K:C→D and F:C→E be functors, with C small and D locally small (Small, locally small, and large categories).

Suppose functorial choices of the required copowers and powers are supplied, with their universal bijections natural in both index variables, and suppose the resulting coends and ends in E exist. Then for each object d of D:

  1. the pointwise left Kan extension value of F along K at d is Lan⁡KF(d)  ≅  ∫cD(Kc,d)⋅F(c),
  2. the pointwise right Kan extension value of F along K at d is Ran⁡KF(d)  ≅  ∫cF(c)D(d,Kc).

So pointwise Kan extensions are the coend and end formulas suggested by the hom-weights.

Facts & Assumptions

Given: Functors K:C→D and F:C→E with C small and D locally small, functorial choices of the required powers and copowers, and the resulting ends and coends in E.

[F1]

A weighted colimit W⋆F represents natural transformations W⇒E(F−,m), while a weighted limit {W,F} represents natural transformations W⇒E(m,F−) (Set-weighted limits and colimits).

[L1]

Given functorial choices of powers or copowers whose universal bijections are natural in both index variables, a weighted limit is the corresponding end of powers and a weighted colimit is the corresponding coend of copowers (A weighted limit is an end of powers and a weighted colimit a coend of copowers, The power and the copower of an object by a set).

[F2]

For fixed d, the assignment c↦D(Kc,d) is a presheaf on C, while c↦D(d,Kc) is a covariant functor on C; both are obtained by composing K with the corresponding hom-functor of D (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[L2]

The comma-category formulas compute the pointwise left and right Kan extension values (Comma-category limit and colimit formulae compute Kan extensions, Pointwise Kan extensions by the comma-category formula).

Proof

technique · direct
1.1F1F2L1L2

Fix d∈D. By [L1], the coend ∫cD(Kc,d)⋅F(c) is the weighted colimit of F by the presheaf c↦D(Kc,d). By [F1], for every m∈E morphisms from this object to m are in natural bijection with natural transformations D(K−,d)⇒E(F−,m). Unwinding the two functors, such a natural transformation is exactly a family of maps F(c)→m indexed by arrows u:Kc→d, natural in morphisms of (K↓d); that is precisely a cocone under the comma-category diagram at d. Therefore the coend has the same objectwise universal property as the pointwise left Kan extension value at d, so [L2] identifies them.

1.2F1F2L1L2

Again fix d. By [L1], the end ∫cF(c)D(d,Kc) is the weighted limit of F by the copresheaf c↦D(d,Kc). By [F1], for every m∈E morphisms from m to this object are in natural bijection with natural transformations D(d,K−)⇒E(m,F−). Unwinding these data gives exactly a cone over the diagram on (d↓K) with vertex m. So this end has the same objectwise universal property as the pointwise right Kan extension value at d, and [L2] identifies them.

2.1step 1.1step 1.2∎

Since the argument is objectwise in d, the displayed coend and end formulas compute the values of the pointwise Kan extensions at every object of D.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

Limits and colimits are Kan extensions along the functor to the terminal category

Statement

Let C be a category, let 1 be the terminal category, and let !:C→1 be the unique functor.

For a diagram F:C→E:

  1. a colimit of F is a left Kan extension of F along !;
  2. a limit of F is a right Kan extension of F along !.

So the ordinary universal properties of limits and colimits are the Kan extension universal properties for the unique map to the terminal category.

Facts & Assumptions

Given: A diagram F:C→E and the unique functor !:C→1.

[L1]

The comma-category formulas compute left and right Kan extensions (Comma-category limit and colimit formulae compute Kan extensions).

[F2]

The terminal category has one object and only its identity morphism (Initial object, terminal object, and zero object).

[F3]

The comma categories (!↓∗) and (∗↓!) are formed as in Comma category, slice category, and coslice category.

Proof

technique · direct
1.1F2F3

Let ∗ be the unique object of 1. An object of (!↓∗) is an object c of C together with the unique arrow ! c→∗, and a morphism is exactly a morphism of C; so (!↓∗) is canonically just C. The same argument shows (∗↓!) is also canonically C.

2.1F1L1step 1.1

Under the identification of step 1.1, the comma-category colimit formula of [L1] says that a left Kan extension value at ∗ is an initial cocone under the original diagram F. By [F1], that is exactly a colimit of F.

3.1F1L1step 1.1∎

Under the same identification, the comma-category limit formula of [L1] says that a right Kan extension value at ∗ is a terminal cone over F. By [F1], that is exactly a limit of F.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Adjunctions as absolute Kan extensions, with the preserved converse

Statement

Let F:C→D and G:D→C be functors.

If F⊣G with unit η:1C⇒GF and counit ε:FG⇒1D, then:

  1. (G,η) is a left Kan extension of 1C along F, and it is absolute;
  2. (F,ε) is a right Kan extension of 1D along G, and it is absolute.

Conversely, if (G,η) is a left Kan extension of 1C along F and is preserved by F, then F⊣G. Dually, if (F,ε) is a right Kan extension of 1D along G and is preserved by G, then F⊣G.

The preservation clause in the converse is load-bearing.

Facts & Assumptions

Given: Functors F:C→D and G:D→C.

[F1]

An adjunction F⊣G consists of a unit η:1C⇒GF and a counit ε:FG⇒1D satisfying εF∘Fη=1F and Gε∘ηG=1G (Adjunction by unit, counit, and the triangle identities).

[F2]

A left Kan extension of 1C along F is initial among natural transformations 1C⇒HF, and a right Kan extension of 1D along G is terminal among natural transformations HG⇒1D (Left and right Kan extensions).

[F3]

An absolute Kan extension is one preserved by every functor out of its codomain (Absolute Kan extension, Covariant functor, identity functor, composite functor, and contravariant functor).

Proof

technique · direct
1.1F1F2

Assume F⊣G with unit η and counit ε. Let H:D→C and α:1C⇒HF be given. Define α‾d:=H(εd)∘αGd:Gd→Hd. Naturality of α at ηc:c→GFc and the triangle identity εFc∘F(ηc)=1Fc give (α‾F)∘η=α. If γ:G⇒H also satisfies (γF)∘η=α, then for each d naturality of γ at εd:FGd→d and the triangle identity G(εd)∘ηGd=1Gd force γd=H(εd)∘αGd=α‾d. So (G,η) is a left Kan extension of 1C along F. Dually, for H:C→D and β:HG⇒1D, the formula β‾c:=βFc∘H(ηc):Hc→Fc gives the unique factorization ε∘(β‾G)=β, so (F,ε) is a right Kan extension of 1D along G.

2.1F1F3step 1.1

The same formulas prove absoluteness. Let S:C→Z and α:S⇒HF with H:D→Z. Then α‾d:=H(εd)∘αGd:SGd→Hd gives the unique factorization (α‾F)∘Sη=α, so (SG,Sη) is a left Kan extension of S along F. Thus (G,η) is absolute by [F3]. The right-handed argument is dual.

3.1F1F2step 2.1∎

Conversely, suppose (G,η) is a left Kan extension of 1C along F and is preserved by F. Applying the preserved Kan-extension property to the identity transformation 1F:F⇒F yields a unique natural transformation ε:FG⇒1D with εF∘Fη=1F, the first triangle identity. To obtain the second, note that both 1G and Gε∘ηG are natural transformations G⇒G whose composites with η agree: componentwise, naturality of η at ηc and the first triangle identity give G(εFc)∘ηGFc∘ηc=G(εFc∘Fηc)∘ηc=ηc. By the uniqueness clause in the left Kan universal property, Gε∘ηG=1G. Hence F⊣G by [F1]. The right-handed converse is dual.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Evaluation is the limit over the coslice category

Statement

Let F:C→E be a functor and let c be an object of C. Then the diagram

c/C⟶C⟶FE

has a limit, and that limit is F(c).

The proof is direct: the identity arrow 1c:c→c is initial in the coslice category, so no product or equalizer computation is needed.

Facts & Assumptions

Given: A functor F:C→E and an object c of C.

[F1]

The coslice category c/C has objects arrows u:c→d, and a morphism from u:c→d to u′:c→d′ is an arrow a:d→d′ with a∘u=u′ (Comma category, slice category, and coslice category).

[L1]

The comma-category formulas compute right Kan extensions (Comma-category limit and colimit formulae compute Kan extensions).

Proof

technique · direct
1.1F1L1

Specialize the right-Kan part of [L1] to K=1C. Then the indexing category (c↓1C) is exactly the coslice category c/C of [F1].

2.1F1F2step 1.1∎

The object (c,1c) is initial in c/C: for any object u:c→d, the required morphism from (c,1c) to u is u itself, and it is unique because its defining equation is a∘1c=u. Therefore the image of (c,1c) under the diagram is a limit object. That image is F(c), and its limiting cone has components F(u):F(c)→F(d). By [F2], this says precisely that F(c) is the limit of the diagram on c/C.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Evaluation is the colimit over the slice category

Statement

Let F:C→E be a functor and let c be an object of C. Then the diagram

C/c⟶C⟶FE

has a colimit, and that colimit is F(c).

The proof is again direct: the identity arrow 1c:c→c is terminal in the slice category.

Facts & Assumptions

Given: A functor F:C→E and an object c of C.

[F1]

The slice category C/c has objects arrows u:d→c, and a morphism from u:d→c to u′:d′→c is an arrow a:d→d′ with u′∘a=u (Comma category, slice category, and coslice category).

[L1]

The comma-category formulas compute left Kan extensions (Comma-category limit and colimit formulae compute Kan extensions).

Proof

technique · direct
1.1F1L1

Specialize the left-Kan part of [L1] to K=1C. Then the indexing category (1C↓c) is exactly the slice category C/c of [F1].

2.1F1F2step 1.1∎

The object (c,1c) is terminal in C/c: for any object u:d→c, the required morphism from u to (c,1c) is u itself, and it is unique because its defining equation is 1c∘a=u. Therefore the image of (c,1c) under the diagram is a colimit object. That image is F(c), and its colimiting cocone has components F(u):F(d)→F(c). By [F2], this says precisely that F(c) is the colimit of the diagram on C/c.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Density theorem for a small category

Statement

Let C be small and let P:Cop→Set be a presheaf. Let

DP:∫P⟶[Cop,Set]

be the diagram sending an object (c,x) of the category of elements of P to the representable presheaf y(c) (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).

Then P is a colimit of DP. Equivalently, for every presheaf Q, cocones from DP to Q are in bijection with natural transformations P⇒Q.

Facts & Assumptions

Given: A small category C, a presheaf P:Cop→Set, and the Yoneda embedding y.

[F1]

The category of elements ∫P has objects (c,x) with x∈P(c), and a morphism (c,x)→(d,y) is an arrow f:c→d with x=P(f)(y) (The category of elements of a covariant functor or a presheaf).

[L1]

For a presheaf Q, natural transformations y(c)=C(−,c)⇒Q are in bijection with elements of Q(c), naturally in both variables (For a presheaf P, Nat⁡(C(−,a),P)≅P(a) naturally in a and P).

Proof

technique · direct
1.1F1F2L1

For each object (c,x) of ∫P, [L1] gives a natural transformation λ(c,x):y(c)⇒P corresponding to the element x∈P(c). If f:(c,x)→(d,y) in ∫P, then x=P(f)(y) by [F1], so naturality in [L1] gives λ(c,x)=λ(d,y)∘y(f). Therefore the family λ(c,x) is a cocone from DP to P.

1.2F1L1

Let Q be any presheaf. By [L1], giving a cocone from DP to Q is exactly giving, for each object (c,x) of ∫P, an element qc,x∈Q(c) such that whenever f:(c,x)→(d,y) in ∫P, one has qc,x=Q(f)(qd,y). But this is precisely the naturality condition for the assignment τc(x):=qc,x to define a natural transformation τ:P⇒Q. Thus cocones from DP to Q are exactly natural transformations P⇒Q.

2.1step 1.1step 1.2∎

Under the bijection of step 1.2, the canonical cocone of step 1.1 corresponds to the identity transformation 1P. Hence that cocone is universal, and P is the colimit of DP.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

The Yoneda embedding is its own pointwise left Kan extension

Statement

Let C be small, and let y:C→[Cop,Set] be the Yoneda embedding. Then the identity functor on [Cop,Set], together with the identity natural transformation on y, is a pointwise left Kan extension of y along y.

Equivalently, for every presheaf P, the comma-category colimit computing Lan⁡yy at P is just P itself.

Facts & Assumptions

Given: A small category C, its Yoneda embedding y, and a presheaf P on C.

[L1]

The density theorem expresses P as the colimit of the diagram ∫P→[Cop,Set] sending (c,x) to y(c) (Density theorem for a small category).

[F1]

Evaluation at the identity gives a natural bijection between morphisms y(c)⇒P and elements x∈P(c); under this bijection the comma category (y↓P) is the category of elements of P (For a presheaf P, Nat⁡(C(−,a),P)≅P(a) naturally in a and P, 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).

[F2]

A pointwise left Kan extension at P is computed by the colimit over (y↓P) (Pointwise Kan extensions by the comma-category formula).

[L2]

If comma-category colimits and their universal cocones are supplied at every target object, they assemble uniquely into a left Kan extension functor, with unit given by the identity-indexed legs (Comma-category limit and colimit formulae compute Kan extensions).

Proof

technique · direct
1.1F1L1

By [F1], the comma category (y↓P) is canonically the category of elements used in [L1], and under that identification its canonical diagram sends an object (c,x) to the representable presheaf y(c).

2.1F2step 1.1L1

The colimit given by [L1] is therefore exactly the comma-category colimit required by [F2] to compute the pointwise left Kan extension of y along itself at P. That colimit object is P.

3.1L1step 2.1

For a natural transformation θ:P⇒Q, the uniquely forced arrow between the two canonical density colimits is θ itself, because its composites with all Yoneda legs are the legs indexed by the elements θc(x). Thus the assembled arrow maps are those of the identity functor, and the identity-indexed unit legs are identities.

4.1L2F2step 2.1step 3.1∎

Since these canonical colimits are supplied for every presheaf, [L2] assembles them into a left Kan extension; steps 2.1 and 3.1 identify it with the identity functor and the identity transformation on y. By [F2] it is pointwise.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Dense subcategory

Definition

Let i:A→C be a fully faithful functor with A small and C locally small (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors, Small, locally small, and large categories). The functor i is dense when the identity functor 1C:C→C is a pointwise left Kan extension of i along i in the sense of Pointwise Kan extensions by the comma-category formula.

Equivalently, for each object c of C, the canonical diagram indexed by the category of elements of the presheaf C(i−,c) (The category of elements of a covariant functor or a presheaf) has colimit c. The model case is the Yoneda embedding: it is fully faithful by The Yoneda functor is fully faithful, and it is a full embedding when its object map is injective and satisfies the pointwise self-extension property by The Yoneda embedding is its own pointwise left Kan extension.

When A is identified with a full subcategory of C and i is the inclusion, one also says that A is a dense subcategory of C.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

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.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Codensity monad

Definition

Let G:B→C be a functor, and suppose a right Kan extension of G along itself is supplied:

ε:TG⇒G

with T:C→C (Left and right Kan extensions, Natural transformation and its components).

The codensity monad of G is the triple (T,η,μ) on C, where the underlying endofunctor is T, the unit η:1C⇒T is the unique natural transformation with

1G=ε∘(ηG),

and the multiplication μ:T2⇒T is the unique natural transformation with

ε∘(μG)=ε∘(Tε).

The theorem The codensity construction satisfies the monad laws ↗ proves that these data satisfy the axioms of Monad on a category.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

The codensity construction satisfies the monad laws

Statement

Let G:B→C be a functor, and suppose its codensity monad (T,η,μ) is supplied as in Codensity monad from a right Kan extension ε:TG⇒G of G along itself.

Then (T,η,μ) is a monad on C (Monad on a category): the two unit laws and the associativity law all hold.

Facts & Assumptions

Given: A right Kan extension ε:TG⇒G of G along itself, and the induced natural transformations η:1C⇒T and μ:T2⇒T.

[F1]

In the codensity construction, 1G=ε∘(ηG) and ε∘(μG)=ε∘(Tε) (Codensity monad).

[F2]

A right Kan extension (T,ε) is terminal among natural transformations SG⇒G (Left and right Kan extensions).

[F3]

A monad is an endofunctor with unit and multiplication satisfying μ∘Tη=1T=μ∘ηT and μ∘Tμ=μ∘μT (Monad on a category).

Proof

technique · direct
1.1F1

The codensity unit η is defined by the identity on G: by [F1], 1G=ε∘(ηG).

2.1F1step 1.1

The codensity multiplication μ is defined by pasting the counit with itself: by [F1], ε∘(μG)=ε∘(Tε).

3.1F1F2step 2.1

To prove the unit laws, compare natural transformations T⇒T after whiskering with G and composing with ε, which [F2] makes a uniqueness test: ε∘((μ∘Tη)G)=ε∘(μG)∘T(ηG)=ε∘Tε∘T(ηG)=ε by [F1], so μ∘Tη=1T; likewise ε∘((μ∘ηT)G)=ε∘(μG)∘ηTG=ε∘Tε∘ηTG=ε∘(ηG)∘ε=ε, where the third equality is naturality of η at ε, so μ∘ηT=1T.

4.1F1F2F3step 3.1∎

For associativity, both composites μ∘Tμ and μ∘μT are natural transformations T3⇒T. After whiskering with G and composing with ε, the left composite gives ε∘((μ∘Tμ)G)=ε∘(μG)∘T(μG)=ε∘Tε∘T2ε by [F1], while the right composite gives ε∘((μ∘μT)G)=ε∘(μG)∘μTG=ε∘Tε∘μTG=ε∘(μG)∘T2ε=ε∘Tε∘T2ε, where the third equality is naturality of μ at ε and the last uses [F1] again. By the uniqueness clause [F2], the two composites are equal. Thus μ∘Tμ=μ∘μT. Together with step 3.1, this is exactly the monad law package [F3].

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

The codensity monad of the small skeleton of finite sets is the ultrafilter monad

Statement

Let FinOrd be the full subcategory of Set on the standard finite ordinals [n]={0,…,n−1}, and let J:FinOrd↪Set be the inclusion functor.

Then the codensity monad of J exists and is naturally isomorphic to the ultrafilter monad β of The ultrafilter endofunctor with principal unit and flattening multiplication. Concretely, for a set X the codensity value consists of coherent finite-valued choice operators

αf∈[n](f:X→[n])

satisfying αh∘f=h(αf) for every map h:[n]→[m], and these operators are in natural bijection with the ultrafilters on X.

Under this bijection, the codensity unit and multiplication agree with the principal unit and flattening multiplication of the ultrafilter monad.

Facts & Assumptions

Given: The inclusion J:FinOrd↪Set, with FinOrd the full subcategory on the standard finite ordinals.

[L1]

Because FinOrd is small and Set is locally small and has all small limits, the pointwise right Kan extension of J along itself exists; at a set X, the comma-category formula identifies its value with the limit of the diagram (X↓J)→FinOrd→Set (Sets and functions form the large locally small category Set, Pointwise Kan extensions exist under smallness and completeness hypotheses, Set has all small limits, realized as compatible tuples in a set-indexed product, Comma-category limit and colimit formulae compute Kan extensions).

[L2]

A proper filter is an ultrafilter if and only if for each A⊆X exactly one of A and X∖A lies in it; moreover, if a finite union lies in an ultrafilter then one member of that union lies in the ultrafilter (Ultrafilter, Filter on a set, Characterisation of ultrafilters: every set or its complement, Ultrafilters are prime: a union in U has a member in U).

[L3]

The codensity construction gives a monad (Codensity monad, The codensity construction satisfies the monad laws).

Proof

technique · direct
1.1L1

By [L1], an element of Ran⁡JJ(X) is exactly a cone over the diagram (X↓J)→FinOrd→Set. Since an object of (X↓J) is a map f:X→[n], such a cone is exactly a family of chosen elements αf∈[n], one for each f:X→[n], satisfying the compatibility condition αh∘f=h(αf) for every map h:[n]→[m].

2.1L2step 1.1

Given such a coherent family α, define Uα:={A⊆X:αχA=1}, where χA:X→[2] is the characteristic function of A. Let !:X→[1] be the unique map, and let c0,c1:[1]→[2] be the constant maps with values 0 and 1. Since χ∅=c0∘! and χX=c1∘!, coherence gives αχ∅=0 and αχX=1, so ∅∉Uα and X∈Uα. If τ:[2]→[2] swaps 0 and 1, then χX∖A=τ∘χA, so exactly one of A and X∖A lies in Uα for every A⊆X. If A,B∈Uα, define g:X→[4] by g(x)=2χA(x)+χB(x), let p,q:[4]→[2] recover the first and second bits, and let m:[4]→[2] send only 3 to 1. Then p∘g=χA, q∘g=χB, and m∘g=χA∩B, so coherence gives p(αg)=q(αg)=1 and hence αχA∩B=m(αg)=1. Thus A∩B∈Uα. Finally, if A∈Uα, A⊆B, and B∉Uα, then X∖B∈Uα, so A∩(X∖B)=∅ lies in Uα, contradicting ∅∉Uα. Therefore Uα is a filter deciding every subset, hence an ultrafilter by [L2].

2.2L2

Conversely, let U be an ultrafilter on X. For each map f:X→[n], the fibres f−1(i) form a finite partition of X, so [L2] gives a unique index αfU∈[n] with f−1(αfU)∈U. If h:[n]→[m], then f−1(αfU)⊆(h∘f)−1(h(αfU)), so upward closure of the ultrafilter puts (h∘f)−1(h(αfU)) into U; uniqueness of the selected partition cell therefore gives αh∘fU=h(αfU). Thus αU is a coherent family of the kind described in step 1.1.

3.1step 2.1step 2.2

The two constructions are inverse. Starting from α, let χi:[n]→[2] be the characteristic function of {i}. Then for any f:X→[n] and any i∈[n], one has f−1(i)∈Uα exactly when αχi∘f=1, which by coherence is exactly when χi(αf)=1, that is, when i=αf; so the ultrafilter Uα selects precisely the fibre of αf, and step 2.2 recovers αf. Starting from an ultrafilter U, the definition of UαU says A∈UαU exactly when the fibre A is the cell selected by U in the partition {A,X∖A}, which is exactly the condition A∈U. Hence Ran⁡JJ(X)≅βX naturally in X.

4.1L3step 3.1

For x∈X, the family αfx:=f(x) is coherent, and the assignment x↦αx is natural in X. On a finite ordinal [n] and an element i∈[n], the counit of the right Kan extension evaluates αi at the identity map of [n], so it returns i; the defining equation 1J=ε∘(ηJ) in [L3] therefore forces the codensity unit to be x↦αx. Under step 3.1 this corresponds to the principal ultrafilter at x, since A∈Uαx exactly when χA(x)=1.

5.1L3L4step 2.2step 3.1∎

Now let W be an ultrafilter on βX, and let Ω be its coherent family from step 2.2. For each f:X→[n], define f^:βX→[n] by sending U to the unique index i with f−1(i)∈U; step 2.2 guarantees that this is well-defined. For the flattened ultrafilter of [L4], one has f−1(i)∈μX(W) if and only if f^−1(i)∈W, so the coherent family attached to μX(W) by step 2.2 takes the value Ωf^ at f. But Ωf^ is exactly the finite-set value produced by Tε in the defining equation ε∘(μJ)=ε∘(Tε) of [L3]. Hence the codensity multiplication is identified with ultrafilter flattening. Therefore step 3.1 matches both the codensity unit and multiplication with the principal unit and flattening multiplication of [L4], so the codensity monad of J is the ultrafilter monad.

5 · Examples, counterexamples and false statements

False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

FALSE: every Kan extension is pointwise

Statement refuted

That every left or right Kan extension is pointwise.

The witness below is a left Kan extension along a fully faithful functor which is not pointwise.

Facts & Assumptions

Given: The discrete category A on two objects ℓ,r; the category D with objects ℓ,m,r and only the two non-identity arrows m→ℓ and m→r; the fully faithful inclusion K:A↪D; the category E with objects a,b,c,d, identities, and only the two non-identity arrows c→a and c→b; the functor F:A→E with F(ℓ)=a and F(r)=b; and the extension L:D→E with L(ℓ)=a, L(r)=b, L(m)=c, and the two displayed arrows.

[F1]

A fully faithful functor is one that is bijective on each hom-set (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors).

[F2]

A left Kan extension is initial among pairs (M,α) with α:F⇒MK, while pointwise left Kan extensions are computed by the comma-category formula (Left and right Kan extensions, Pointwise Kan extensions by the comma-category formula, The comma-category and representable-preservation notions of pointwise Kan extension agree).

[F3]

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

[F4]

An initial object must admit a morphism to every object (Initial object, terminal object, and zero object).

Refutation

technique · direct
1.1F1F2given

The inclusion K is fully faithful by [F1], and the pair (L,η) with ηℓ=1a and ηr=1b is a left Kan extension of F along K: if α:F⇒MK exists, then necessarily M(ℓ)=a and M(r)=b, since a has no non-identity arrow out of it and neither does b; and because M must carry the arrows m→ℓ and m→r to arrows into a and b, necessarily M(m)=c, the only object of E with arrows to both. Thus M=L and α is forced to be the identity on ℓ and r, so there is exactly one natural transformation L⇒M.

2.1F2F4step 1.1assume-hyp

But (K↓m) is empty: there is no arrow ℓ→m and no arrow r→m in D. If (L,η) were pointwise, [F2] would make L(m)=c the colimit of the empty diagram, hence an initial object of E. This is impossible by [F4], since there is no morphism c→d. Therefore (L,η) is a left Kan extension which is not pointwise.

3.1F3step 2.1∎

So the claim that every Kan extension is pointwise is false. The pointwise hypothesis in [F3] is genuinely needed.

False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

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.

False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

FALSE: the free-cocompletion theorem holds for an arbitrary large locally small source category with no change in meaning

Statement refuted

That the statement of The presheaf category on a small category is the free cocompletion remains true with no change in meaning when the source category C is merely locally small and may be large.

Under this library's formation rules the smallness hypothesis is not cosmetic: without it, the presheaf category is not a category object on disk, and the Yoneda functor is not a functor into one.

Facts & Assumptions

Given: The large locally small category Set.

[L1]

The free-cocompletion theorem is stated for a small source category (The presheaf category on a small category is the free cocompletion).

[F1]

A functor category [C,D] is formed only when the source C is small; for an arbitrary large locally small C, the notation is only metatheoretic shorthand (The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding, If C is small and D is locally small then [C,D] is locally small; if both are small it is small).

[F2]

A category may be locally small without being small (Small, locally small, and large categories).

Refutation

technique · direct
1.1F2given

The category Set is locally small and large, so it satisfies the weakened hypothesis of the false claim by [F2].

1.2L1F1

But [F1] says that for such a large source the notation [Setop,Set] is not formed as a category in this library, and [L1] is a theorem about that presheaf category and the Yoneda functor landing in it. So the unchanged large-source sentence is not even a legal instance of the theorem on disk.

2.1step 1.1step 1.2∎

Therefore the false claim fails under the house schema: the smallness hypothesis in [L1] is mathematically active here, not removable decoration.

False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

FALSE: the Yoneda embedding preserves colimits

Statement refuted

That the Yoneda embedding y:C→[Cop,Set] (The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding) preserves colimits in general.

The true statement already on disk is the limit half: For a small category, the Yoneda functor preserves and reflects all existing small limits.

Facts & Assumptions

Given: The terminal category 1 with unique object ∗.

[F1]

In the terminal category, the unique object is in particular initial (Initial object, terminal object, and zero object).

[F3]

The Yoneda embedding sends ∗ to the representable presheaf 1(−,∗) (The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding).

Refutation

technique · direct
1.1F1assume-hyp

By [F1], the object ∗ is a colimit of the empty diagram in 1. If the Yoneda embedding preserved colimits, then y(∗) would be an initial object of the presheaf category on 1.

1.2F2F3

But by [F3], the presheaf y(∗) takes the value 1(∗,∗), which is the singleton set {1∗}. By [F2], an initial presheaf has value ∅ at ∗. Therefore y(∗) is not initial.

2.1step 1.1step 1.2∎

So the Yoneda embedding does not preserve colimits in general. The published limit-preservation theorem is not contradicted, because it is about limits, not colimits.

Sources