Alphabeta Math
Session-authored (Fable 5 assisted)
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.

7 results · all verified · 3 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 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Kan Extensions Density and the Free Cocompletion — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-26Open item page →

A left Kan extension along a full subcategory inclusion of preorders

Example

Let A be the full subcategory of the chain 0<1<2 on the objects 0 and 1, and let i:AB be the inclusion. Define F:ASet by

F(0)=,F(1)={},

with the unique map {} on the unique non-identity arrow.

Then the left Kan extension of F along i exists and is pointwise. It agrees with F on 0 and 1, and its value at the new object 2 is again the singleton set {}.

Facts & Assumptions

Given: The preorder categories AB and the functor F just described.

[F1]

A preorder may be read as a category with one arrow precisely when the order relation holds, and monotone maps are the functors between them (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 an object (Comma-category limit and colimit formulae compute Kan extensions).

Verification

technique · direct
1.1

The inclusion i is fully faithful by [F1]. The comma category (i2) has two objects, namely the arrows 02 and 12, and one non-identity morphism from the first to the second, corresponding to the inequality 01 in A.

F1
1.2

The induced diagram (i2)AFSet is therefore just {}, whose colimit in Set is {}. By [L1], this is the left Kan extension value at 2.

L1
2.1

On the objects 0 and 1, the pointwise left Kan extension restricts back to F by [L2]. Hence the left Kan extension along the full subcategory inclusion is the functor sending 0, 1{}, and 2{}.

L2step 1.2
ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-26 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A Kan extension computing the free-group functor

Example

Let 1 be the one-object category, so [1op,Set]Set. Let y:1Set be the Yoneda embedding. Choose a free group F({}) on the one-element set {}, and let F:1Grp send the unique object to that group.

Then the left Kan extension LanyF:SetGrp is the free-group functor.

Facts & Assumptions

Given: The one-object category 1, the Yoneda embedding y, and the functor whose value is a chosen free group on {}.

[L1]

The free-cocompletion theorem makes LanyF left adjoint to Grp(F,) (The presheaf category on a small category is the free cocompletion).

[L2]

Choosing a free group on every set gives a free-group functor left adjoint to the underlying-set functor; at {} its adjunction bijection is Grp(F({}),G)U(G) naturally in G (The free-group functor is left adjoint to the underlying-set functor).

[L3]

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

[F2]

Groups and group homomorphisms form the locally small category Grp, and Grp has all small colimits (Groups and group homomorphisms form the large locally small category Grp, Grp is complete and cocomplete).

Verification

technique · direct
1.1

By [F1], the functor LanyF has domain Set, and [F2] verifies the locally small and cocomplete target hypotheses of [L1]. Hence [L1] makes it left adjoint to the functor GGrp(F({}),G).

F1F2L1
2.1

By [L2], the functor GGrp(F({}),G) is naturally isomorphic to the underlying-set functor on groups. Therefore LanyF is a left adjoint to the underlying-set functor.

L2step 1.1
3.1

The published free-group functor is also a left adjoint to the underlying-set functor by [L2], so [L3] identifies LanyF with that free functor.

L2L3step 2.1
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Induction and coinduction of permutation representations as Kan extensions

Example

Let i:HG be a subgroup inclusion, and view H and G as one-object categories (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible). A functor X:HSet is then a permutation representation of H.

The left Kan extension of X along i is the induced G-set G×HX, and the right Kan extension is the coinduced G-set MapH(G,X).

Facts & Assumptions

Given: A subgroup inclusion i:HG and an H-set X, regarded as a functor X:HSet.

[L1]

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

[F2]

Every small Set-valued diagram has a colimit given by the quotient of its tagged union by the relations generated by its structure maps, and a limit given by its set of compatible tuples (Set has all small colimits, realized as a quotient of a set-indexed disjoint union, Set has all small limits, realized as compatible tuples in a set-indexed product).

Verification

technique · direct
1.1

In the one-object setting, an object of (i) is just an element gG. A morphism from g to g is an element hH with g=gi(h) by the comma-category equation, equivalently g=gi(h1). So the indexing category is the action groupoid for the right H-action on G, and the induced diagram on Set sends the arrow ggi(k) to the map xk1x on X. By [F2], its colimit is the quotient of G×X by (g,x)(gi(k),k1x), equivalently by (gi(h),x)(g,hx), namely G×HX. Therefore [L1] identifies the induced representation with the left Kan extension.

F1F2L1
2.1

Dually, an object of (i) is again an element of G, and a cone to a set Y is exactly a family of maps indexed by G that is equivariant for the H-action. By [F2], the limit is therefore the set of H-equivariant maps GX, written MapH(G,X). Hence [L1] identifies the coinduced representation with the right Kan extension.

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

The orbit-set and fixed-point constructions as Kan extensions

Example

Let G be a group, view it as a one-object category, and let !:G1 be the unique functor to the terminal category. A G-action on a set X is the same thing as a functor X:GSet (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible, Left group actions, transitive actions, and faithful actions).

Then the left Kan extension of X along ! is the orbit set X/G, while the right Kan extension is the fixed-point set XG.

Facts & Assumptions

Given: A group G, a G-set X, and the unique functor !:G1.

[L1]

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

[F2]

The one-object category of a group is connected, hence equivalent to the automorphism groupoid of its sole object (Under the Axiom of Choice, a connected small groupoid is equivalent to the automorphism group of any one of its objects).

Verification

technique · direct
1.1

For the unique object of 1, the comma category (!) is just the one-object category G again, by [F1] and [F2]. A cocone from the G-action diagram X:GSet to a set Y is exactly a function q:XY constant on G-orbits, so its universal example is the quotient map XX/G. Therefore [L1] identifies the orbit set with the left Kan extension of X along !.

F1F2L1
2.1

Dually, a cone from a set Y to the action diagram is exactly a function YX landing in the equalizer of all action maps, that is, in the fixed-point set XG. Hence [L1] identifies XG with the right Kan extension of X along !.

F1L1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Density computed for a presheaf on a two-object discrete category

Example

Let C be the discrete category on two objects 0 and 1. Define a presheaf P:CopSet by

P(0)={x},P(1)={y,z}.

Then the category of elements of P has three objects and no non-identity morphisms, and the density theorem identifies P as the coproduct

Py(0)y(1)y(1)

in [Cop,Set].

Facts & Assumptions

Given: The discrete two-object category C and the presheaf P above.

[F1]

The category of elements has objects (c,u) with uP(c); because C is discrete, it has no non-identity arrows between distinct such objects (The category of elements of a covariant functor or a presheaf).

[L1]

The density theorem expresses P as the colimit of the diagram indexed by P whose values are the representables at those objects (Density theorem for a small category).

Verification

technique · direct
1.1

The category of elements of P has the three objects (0,x), (1,y), and (1,z), and no non-identity morphisms, by [F1].

F1
2.1

Therefore the density diagram of [L1] is the discrete three-object diagram with values y(0), y(1), and y(1), by [F2]. Its colimit is the coproduct y(0)y(1)y(1).

F2L1step 1.1
3.1

Applying [L1] to this presheaf gives exactly that coproduct as P.

L1step 2.1
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

A fully faithful left Kan extension that is not pointwise

Statement refuted

That a left Kan extension along a fully faithful functor is automatically pointwise.

The witness is a fully faithful inclusion K:AD and a left Kan extension (L,η) of a functor F:AE such that (Km) is empty while L(m) is not initial.

Facts & Assumptions

Given: The discrete category A on two objects ,r; the category D with objects ,m,r and only the arrows m and mr besides identities; the inclusion K:AD; the category E with objects a,b,c,d, identities, and only the two non-identity arrows ca and cb; the functor F with F()=a and F(r)=b; and the extension L with L()=a, L(r)=b, L(m)=c, carrying the arrows of D to ca and cb.

[F1]

A left Kan extension is initial among pairs (M,α) with α:FMK (Left and right Kan extensions).

[F2]

A pointwise left Kan extension value at m is the colimit of the comma-category diagram on (Km) (Pointwise Kan extensions by the comma-category formula).

[F4]

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

Counterexample

technique · direct
1.1

The inclusion K is fully faithful by [F3].

F3given
2.1

The pair (L,η) with η=1a and ηr=1b is a left Kan extension of F along K. Indeed, if α:FMK exists, then M()=a and M(r)=b, because a and b have no non-identity arrows out of them; and the arrows m and mr force M(m)=c, the only object of E with arrows to both a and b. So M=L, and then α is forced to be the identity on and r, which leaves exactly one natural transformation LM. This is the universal property [F1].

F1step 1.1
3.1

But (Km) is empty, because there is no arrow from to m and none from r to m in D. If (L,η) were pointwise, [F2] would make L(m)=c the colimit of the empty diagram and hence an initial object of E. That is impossible by [F4], since there is no morphism cd. So this left Kan extension is not pointwise.

F2F4step 2.1assume-hyp
4.1

Therefore the claim is false: a fully faithful left Kan extension need not be pointwise.

step 3.1
ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-26 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

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:QR 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:QSet by

F(q)=(,q)R,

with the structure maps the evident inclusions when qq.

Then the pointwise left Kan extension of F along i is the functor L:RSet with

L(x)=(,x)R.

Facts & Assumptions

Given: The inclusion i:QR and the functor F(q)=(,q).

[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.1

For a real x, the comma category (ix) is the preorder of rationals qx. The induced diagram sends such a q to (,q) and its colimit in Set is the union qx, qQ(,q).

F1L1
2.1

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

L2step 1.1
3.1

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

L1step 2.1

Sources