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: Every reflective subcategory is closed under ambient colimits
Statement
False claim. If a full subcategory is reflective, then the colimit in the ambient category of every diagram valued in the subcategory again lies in the subcategory.
Facts & Assumptions
Given: 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).
The colimit of the empty diagram 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 with value is left adjoint to the inclusion: both and are singletons, naturally in . By the converse clause of [L3] that natural family of bijections determines a unit and counit satisfying the triangle identities, hence an adjunction , and [L1] then makes reflective.
In , the object is initial and is therefore the empty colimit. In the empty colimit is by [L2], and is not an object of .
Thus an ambient colimit of a diagram valued in a reflective subcategory need not remain in that subcategory, refuting the claim.
Depends on
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: 21 results over 8 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)