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.
Kan Extensions Density and the Free Cocompletion — Examples
1 · Prerequisites
- Adjunctions Units and Counits
- Binary Operations, Monoids, Groups and Subgroups
- Cardinal Arithmetic, Cofinality and the Alephs
- Categories, Functors and Natural Transformations
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Free Groups and Presentations
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Kan Extensions Density and the Free Cocompletion
- Limits and Colimits
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Relations, Functions, and Quotients
- Set Theory Beyond Choice: Recorded, Not Proved Here
- Suprema and Infima
- The ZFC Axioms and the Basic Set Constructions
- Universal Properties, Representables and the Yoneda Lemma
2 · Summary
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A left Kan extension along a full subcategory inclusion of preorders
Example
Let be the full subcategory of the chain on the objects and , and let be the inclusion. Define by
with the unique map on the unique non-identity arrow.
Then the left Kan extension of along exists and is pointwise. It agrees with on and , and its value at the new object is again the singleton set .
Facts & Assumptions
Given: The preorder categories and the functor just described.
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).
The comma-category colimit formula computes the left Kan extension value at an object (Comma-category limit and colimit formulae compute Kan extensions).
A pointwise Kan extension along a fully faithful functor restricts back to the original functor by isomorphism (A pointwise Kan extension along a fully faithful functor genuinely extends the original functor, Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors).
Verification
The inclusion is fully faithful by [F1]. The comma category has two objects, namely the arrows and , and one non-identity morphism from the first to the second, corresponding to the inequality in .
The induced diagram is therefore just , whose colimit in is . By [L1], this is the left Kan extension value at .
On the objects and , the pointwise left Kan extension restricts back to by [L2]. Hence the left Kan extension along the full subcategory inclusion is the functor sending , , and .
A Kan extension computing the free-group functor
Example
Let be the one-object category, so . Let be the Yoneda embedding. Choose a free group on the one-element set , and let send the unique object to that group.
Then the left Kan extension is the free-group functor.
Facts & Assumptions
Given: The one-object category , the Yoneda embedding , and the functor whose value is a chosen free group on .
The free-cocompletion theorem makes left adjoint to (The presheaf category on a small category is the free cocompletion).
Choosing a free group on every set gives a free-group functor left adjoint to the underlying-set functor; at its adjunction bijection is naturally in (The free-group functor is left adjoint to the underlying-set functor).
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).
Groups and group homomorphisms form the locally small category , and has all small colimits (Groups and group homomorphisms form the large locally small category , Grp is complete and cocomplete).
Verification
By [F1], the functor has domain , and [F2] verifies the locally small and cocomplete target hypotheses of [L1]. Hence [L1] makes it left adjoint to the functor .
By [L2], the functor is naturally isomorphic to the underlying-set functor on groups. Therefore is a left adjoint to the underlying-set functor.
The published free-group functor is also a left adjoint to the underlying-set functor by [L2], so [L3] identifies with that free functor.
Induction and coinduction of permutation representations as Kan extensions
Example
Let be a subgroup inclusion, and view and 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 is then a permutation representation of .
The left Kan extension of along is the induced -set , and the right Kan extension is the coinduced -set .
Facts & Assumptions
Given: A subgroup inclusion and an -set , regarded as a functor .
A group may be regarded as a one-object category, and a subgroup inclusion is then a functor between such categories (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible, Covariant functor, identity functor, composite functor, and contravariant functor).
The comma-category colimit and limit formulae compute left and right Kan extensions (Comma-category limit and colimit formulae compute Kan extensions).
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
In the one-object setting, an object of is just an element . A morphism from to is an element with by the comma-category equation, equivalently . So the indexing category is the action groupoid for the right -action on , and the induced diagram on sends the arrow to the map on . By [F2], its colimit is the quotient of by , equivalently by , namely . Therefore [L1] identifies the induced representation with the left Kan extension.
Dually, an object of is again an element of , and a cone to a set is exactly a family of maps indexed by that is equivariant for the -action. By [F2], the limit is therefore the set of -equivariant maps , written . Hence [L1] identifies the coinduced representation with the right Kan extension.
The orbit-set and fixed-point constructions as Kan extensions
Example
Let be a group, view it as a one-object category, and let be the unique functor to the terminal category. A -action on a set is the same thing as a functor (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 along is the orbit set , while the right Kan extension is the fixed-point set .
Facts & Assumptions
Given: A group , a -set , and the unique functor .
Groups are one-object categories and -actions are functors to (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, Sets and functions form the large locally small category ).
The comma-category formulae compute left and right Kan extensions (Comma-category limit and colimit formulae compute Kan extensions).
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
For the unique object of , the comma category is just the one-object category again, by [F1] and [F2]. A cocone from the -action diagram to a set is exactly a function constant on -orbits, so its universal example is the quotient map . Therefore [L1] identifies the orbit set with the left Kan extension of along .
Dually, a cone from a set to the action diagram is exactly a function landing in the equalizer of all action maps, that is, in the fixed-point set . Hence [L1] identifies with the right Kan extension of along .
Density computed for a presheaf on a two-object discrete category
Example
Let be the discrete category on two objects and . Define a presheaf by
Then the category of elements of has three objects and no non-identity morphisms, and the density theorem identifies as the coproduct
in .
Facts & Assumptions
Given: The discrete two-object category and the presheaf above.
The category of elements has objects with ; because is discrete, it has no non-identity arrows between distinct such objects (The category of elements of a covariant functor or a presheaf).
The Yoneda embedding sends and to the representables and (The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding, Sets and functions form the large locally small category ).
The density theorem expresses as the colimit of the diagram indexed by whose values are the representables at those objects (Density theorem for a small category).
Verification
The category of elements of has the three objects , , and , and no non-identity morphisms, by [F1].
Therefore the density diagram of [L1] is the discrete three-object diagram with values , , and , by [F2]. Its colimit is the coproduct .
Applying [L1] to this presheaf gives exactly that coproduct as .
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 and a left Kan extension of a functor such that is empty while is not initial.
Facts & Assumptions
Given: The discrete category on two objects ; the category with objects and only the arrows and besides identities; the inclusion ; the category with objects , identities, and only the two non-identity arrows and ; the functor with and ; and the extension with , , , carrying the arrows of to and .
A left Kan extension is initial among pairs with (Left and right Kan extensions).
A pointwise left Kan extension value at is the colimit of the comma-category diagram on (Pointwise Kan extensions by the comma-category formula).
A fully faithful functor is bijective on each hom-set (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors).
An initial object must have a morphism to every object (Initial object, terminal object, and zero object).
Counterexample
The inclusion is fully faithful by [F3].
The pair with and is a left Kan extension of along . Indeed, if exists, then and , because and have no non-identity arrows out of them; and the arrows and force , the only object of with arrows to both and . So , and then is forced to be the identity on and , which leaves exactly one natural transformation . This is the universal property [F1].
But is empty, because there is no arrow from to and none from to in . If were pointwise, [F2] would make the colimit of the empty diagram and hence an initial object of . That is impossible by [F4], since there is no morphism . So this left Kan extension is not pointwise.
Therefore the claim is false: a fully faithful left Kan extension need not be pointwise.
A left Kan extension along the inclusion of the rationals in the reals
Example
View and as thin categories under their usual order, and let 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 by
with the structure maps the evident inclusions when .
Then the pointwise left Kan extension of along is the functor with
Facts & Assumptions
Given: The inclusion and the functor .
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).
The comma-category colimit formula computes the left Kan extension value at a real number (Comma-category limit and colimit formulae compute Kan extensions).
Between any two distinct reals there is a rational number (The rationals embed densely in the reals).
Verification
For a real , the comma category is the preorder of rationals . The induced diagram sends such a to and its colimit in is the union .
This union is exactly . If , [L2] gives a rational with , so and hence lies in the union. Conversely every with is contained in .
Therefore [L1] gives for the left Kan extension value at every real .
Sources
- E. Riehl, Category Theory in Context, 2nd ed., Proposition 6.5.11
- E. Riehl, Category Theory in Context, 2nd ed., Example 6.2.11
- E. Riehl, Category Theory in Context, 2nd ed., Example 6.2.14
- E. Riehl, Category Theory in Context, 2nd ed., Example 6.2.17
- E. Riehl, Category Theory in Context, 2nd ed., Example 6.2.10