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.
Applying F gives a termwise G-acyclic complex
Statement
Let and be additive left-exact functors and suppose that sends injectives to -acyclic objects, relative to supplied resolution data. For a supplied injective resolution , the complex is bounded below and termwise -acyclic, with . It need not be a resolution of .
Facts & Assumptions
Given: These functors, acyclicity hypothesis and supplied injective resolution.
A resolution has injective terms in nonnegative degrees (Injective resolutions in an abelian category).
-acyclicity is vanishing of positive right derived objects (G-acyclic object for a left-exact functor).
Relative right derived objects are (Right derived objects relative to supplied injective resolution data).
Supplied projective and injective models of Ext have quasi-isomorphic Hom complexes (Projective and injective constructions of Ext agree for supplied resolutions).
Proof
Each is injective, so the hypothesis gives for . Additivity makes a cochain complex, zero in negative degrees. Its cohomology is precisely by definition. In degree zero left exactness identifies its kernel with ; positive exactness would additionally require every positive to vanish.
For a witness take , the identity of abelian groups and , with a supplied injective resolution of . Identity is exact, so all its positive derived objects vanish. The projective resolution has rank-one free, hence projective, terms: a map from lifts across an epimorphism by lifting the image of . Applying gives in degrees zero and one. Its degree-one cohomology is . F4 identifies this with . Thus is not a resolution of , even though every one of its terms is -acyclic. This witness is relative to supplied data and uses no choice of an infinite family of lifts.
Depends on
Used by
Dependency tree · two levels
20 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
- Stacks Project, Tags 015H and 015M (standard reference, not scraped)