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: objectwise projective-resolution choices uniquely determine a resolution functor
Statement
False. Once one projective resolution has been chosen for each object in a category with enough projectives, those objectwise choices uniquely determine comparison maps and hence a projective-resolution functor.
Facts & Assumptions
Given: The category of abelian groups and the standard projective resolution of .
Enough projectives gives projective resolutions only after choosing successive projective epimorphisms for each fixed object (A chosen chain of projective epimorphisms gives a projective resolution).
Finite-rank free modules are projective without any infinite choice (Free modules are projective, with the exact choice boundary).
Refutation
The proof of [L1] is objectwise: it chooses terms and differentials but supplies no unique lift of a morphism between resolved objects.
The exact row is a projective resolution by [L2]. On two copies of it, multiplication by in both degrees and multiplication by in both degrees are distinct chain maps lifting the identity of : both commute with multiplication by , and . Thus the chosen objectwise resolution does not uniquely determine the map assigned to the identity morphism.
Therefore objectwise resolution choices do not uniquely determine comparison maps or a resolution functor; additional coherent choices or a separate functorial construction are required.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
8 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 (standard reference, not scraped)
- Romyar Sharifi, Homological Algebra (standard reference, not scraped)
- The Stacks Project, Section 12.28: Projectives (standard reference, not scraped)