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.
FALSE: A reflective inclusion creates colimits
Statement
False claim. The inclusion of every reflective full subcategory creates all small colimits.
Facts & Assumptions
Given: The inclusion of the full subcategory whose only object is a fixed singleton .
A full subcategory is reflective when its inclusion has a left adjoint (Reflective full subcategory and reflector).
Ordinary creation of a colimit requires every target colimiting cocone to be isomorphic to the image of a source colimiting cocone (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).
The empty colimit is an initial object (Limits of empty diagrams are terminal objects, and colimits of empty diagrams are initial objects).
For locally small categories, an adjunction determines hom-set bijections natural in both variables, and conversely every such natural family of bijections determines a unique unit and counit satisfying the triangle identities, hence a unique adjunction structure (Under local smallness, transposition gives the natural hom-set bijection, and conversely).
Refutation
The constant functor at is left adjoint to , since the unique maps give hom-set bijections natural in ; by the converse clause of [L4] these determine a unit and counit satisfying the triangle identities, hence an adjunction . Thus is a reflective inclusion by [L1].
The empty diagram in has colimit , whereas the empty diagram in has colimit , by [L3]. Since , the ambient colimiting cocone is not isomorphic to the image of any cocone with an apex in .
This violates the creation requirement [L2], so a reflective inclusion need not create colimits.
Depends on
- Reflective full subcategory and reflector
- Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors
- Limits of empty diagrams are terminal objects, and colimits of empty diagrams are initial objects
- Under local smallness, transposition gives the natural hom-set bijection, and conversely
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 28 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- E. Riehl, Category Theory in Context, corollary 4.5.15 (standard reference, not scraped)