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: enough projectives imply a canonical resolution for every object
Statement
If an abelian category has enough projectives, then that property uniquely determines a projective resolution for every object.
Facts & Assumptions
Given: The category of abelian groups, which has enough projectives, and the object .
A supplied projective resolution datum is extra objectwise structure, not an existence theorem of its own (Supplied projective resolution data).
Even chosen objectwise projective resolutions do not uniquely determine comparison maps, and hence do not by themselves determine a resolution functor (FALSE: objectwise projective-resolution choices uniquely determine a resolution functor).
The iterated free resolution is a special canonical construction in module categories, not a general consequence of enough projectives (The iterated free-module resolution is canonical in ZF).
Refutation
One projective resolution of is Adding the contractible projective complex in degrees and gives a different projective resolution where the augmentation is reduction modulo on the first summand. Both displayed augmented complexes are exact, but they are not the same resolution.
Thus even in a category with enough projectives the property alone does not uniquely determine a resolution of a fixed object. Moreover, [L2] shows that arbitrary objectwise choices still do not uniquely determine the comparison maps of a resolution functor. The special construction in [L3] uses the extra underlying-set structure of a module category, while [L1] records that a general supplied datum is additional structure. Therefore the displayed claim is false.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Charles A. Weibel, An Introduction to Homological Algebra, Chapter 2 `Derived Functors` (standard reference, not scraped)