Alphabeta Math
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.

33 results · all verified · 24 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 9 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Derived Functors

1 · Prerequisites

2 · Summary

This page builds derived functors only relative to displayed projective or injective resolution data. The object definitions, map definitions, functoriality, and change-of-data isomorphisms are kept separate, so the phrase "well defined" does not hide any missing choice, comparison, or naturality step.

The second half of the page records the main usable consequences that do belong at this stage: degree-zero recovery, vanishing on projectives or injectives, acyclic-resolution computation, the exact-functor and finite-biproduct corollaries, and the variance bridge to the opposite category. The long exact sequence and universality structure remain deferred to the next page.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Supplied projective resolution data

Definition

Let A be an abelian category, and let D be a class of objects of A.

A supplied projective resolution datum on D assigns to each AD a specific projective resolution P(A)A in the sense of Projective resolutions in an abelian category.

This is extra structure on the chosen domain of objects. It records displayed resolutions objectwise; it does not assert that such a choice exists canonically for all objects of A.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Supplied injective resolution data

Definition

Let A be an abelian category, and let D be a class of objects of A.

A supplied injective resolution datum on D assigns to each AD a specific injective resolution AI(A) in the sense of Injective resolutions in an abelian category.

Again this is part of the input data. It keeps the chosen coaugmented resolutions visible rather than hiding a global selection claim in the background.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Left derived objects relative to supplied projective resolution data

Definition

Let P be a supplied projective resolution datum on a class D of objects in an abelian category A, and let F:AB be an additive functor to an abelian category B.

For AD and nZ, the nth left derived object of F relative to P at A is LnPF(A):=Hn ⁣(F(P(A)del)), where P(A)del is the deleted resolution from Deleted resolutions.

No exactness hypothesis on F is needed for this definition. The datum P supplies the chosen resolution whose image under F is being measured by homology.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Right derived objects relative to supplied injective resolution data

Definition

Let I be a supplied injective resolution datum on a class D of objects in an abelian category A, and let F:AB be an additive functor to an abelian category B.

For AD and nZ, the nth right derived object of F relative to I at A is RInF(A):=Hn ⁣(F(I(A)del)), where I(A)del is the deleted injective resolution from Deleted resolutions.

The superscript records the supplied injective datum. This page keeps that data visible instead of suppressing it into an unstated global choice.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

Negative derived degrees vanish for one-sided resolutions

Statement

Let P and I be supplied projective and injective resolution data, and let F be an additive functor.

If n<0, then for every object A in the common domain, LnPF(A)=0andRInF(A)=0.

Facts & Assumptions

Given: An object A and an integer n<0.

[L1]

The object LnPF(A) is the homology of the deleted projective resolution F(P(A)del) in degree n (Left derived objects relative to supplied projective resolution data).

[L2]

The object RInF(A) is the cohomology of the deleted injective resolution F(I(A)del) in degree n (Right derived objects relative to supplied injective resolution data).

Proof

technique · direct
1.1

By [L1], the complex computing LnPF(A) is zero in every negative degree, because a deleted projective resolution is supported only in nonnegative homological degrees. Therefore both its degree-n cycle object and its degree-n boundary object are zero, so LnPF(A)=0.

L1givenalgebra
1.2

By [L2], the cochain complex computing RInF(A) is zero in every negative cohomological degree, because a deleted injective resolution begins in degree 0. Hence its degree-n cocycle and coboundary objects are zero, so RInF(A)=0.

L2givenalgebra
2.1

Steps 1.1 and 1.2 prove the claimed vanishing for both one-sided derived constructions.

step 1.1step 1.2
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A morphism has a comparison lift between the supplied projective resolutions

Statement

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum on a class D in an abelian category. For every morphism u:AB with A,BD, there exists an augmentation-preserving chain map u~:P(A)P(B) lifting u.

Facts & Assumptions

Given: A morphism u:AB with A,BD.

[L1]

The datum P supplies specific projective resolutions P(A)A and P(B)B (Supplied projective resolution data).

[L2]

Assuming Dependent Choice, projective comparison maps exist for any morphism between resolved objects (Projective comparison maps exist).

Proof

technique · direct
1.1

By [L1], the objects A and B come with chosen projective resolutions.

L1given
2.1

Apply [L2] to u:AB and the chosen resolutions from step 1.1. This yields an augmentation-preserving chain map u~:P(A)P(B) lifting u.

L2step 1.1construct
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The induced homology map is independent of the chosen comparison lift

Statement

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum and F:AB an additive functor. If u:AB is a morphism and u~,u^:P(A)P(B) are two comparison lifts of u, then for every nZ the induced maps on homology Hn ⁣(F(u~)),Hn ⁣(F(u^)):LnPF(A)LnPF(B) are equal.

Facts & Assumptions

Given: A morphism u:AB and two comparison lifts u~,u^ of u.

[L1]

Two comparison maps lifting the same morphism are chain-homotopic (Projective comparison maps are unique up to chain homotopy).

[L2]

A chain homotopy is given by equations of the form fngn=dn+1sn+sn1dn (A chain homotopy).

[L3]

Additive functors preserve sums and zero morphisms (Additive functor, An additive functor preserves zero morphisms).

[L4]

Chain-homotopic maps induce the same map on homology (Chain-homotopic maps induce the same map on homology).

[L5]

The objects LnPF(A) and LnPF(B) are the homology objects of the deleted resolutions after applying F (Left derived objects relative to supplied projective resolution data).

Proof

technique · direct
1.1

By [L1], the two lifts u~ and u^ are chain-homotopic. Let s be such a homotopy.

L1givenconstruct
2.1

The equations in [L2] become F(u~n)F(u^n)=F(dn+1)F(sn)+F(sn1)F(dn) after applying F, because [L3] lets F preserve sums and zero morphisms. Hence F(s) is a chain homotopy from F(u~) to F(u^).

L2L3step 1.1algebra
3.1

By [L4], chain-homotopic maps induce the same map on homology. Using [L5] to identify those homology objects with the displayed left derived objects gives Hn ⁣(F(u~))=Hn ⁣(F(u^)) for every n.

L4L5step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The left derived map relative to supplied resolution data

Definition

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum on a class D in an abelian category A, let F:AB be an additive functor to an abelian category B, let A,BD, and let nZ. For a morphism u:AB, choose any comparison lift u~:P(A)P(B).

The left derived map of u in degree n relative to P is the induced map on homology LnPF(u):=Hn ⁣(F(u~)):LnPF(A)LnPF(B).

By A morphism has a comparison lift between the supplied projective resolutions such a lift exists, and by The induced homology map is independent of the chosen comparison lift the result does not depend on which lift was chosen.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Left derived maps preserve identities

Statement

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum on a class D and F:AB an additive functor between abelian categories. For every object AD and every nZ, LnPF(1A)=1LnPF(A).

Facts & Assumptions

Given: An object AD and an integer n.

[L1]

The map LnPF(1A) is defined from any comparison lift of the identity on the chosen resolution of A (The left derived map relative to supplied resolution data).

[L2]

Any comparison map lifting 1A is homotopic to the identity chain map (Comparison of the identity is homotopic to the identity).

[L3]

Homology sends the identity chain map to the identity and respects composition (Homology respects identities and composition).

Proof

technique · direct
1.1

Let 1~ be any comparison lift of 1A used in [L1]. By [L2], 1~ is homotopic to the identity chain map on the chosen projective resolution of A.

L1L2given
2.1

Applying F preserves that homotopy relation as in the construction of the left derived map, so the induced map on homology agrees with the map from the identity chain map. By [L3], that latter map is 1LnPF(A). Therefore LnPF(1A)=1LnPF(A).

L3step 1.1algebra
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Left derived maps preserve composition

Statement

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum on a class D and F:AB an additive functor between abelian categories. For composable morphisms AuBvC with A,B,CD and every nZ, LnPF(vu)=LnPF(v)LnPF(u).

Facts & Assumptions

Given: Composable morphisms AuBvC with A,B,CD and an integer n.

[L1]

Each derived map is induced from a comparison lift on the supplied resolutions (The left derived map relative to supplied resolution data).

[L2]

A comparison lift of a composite is homotopic to the composite of comparison lifts (Comparison maps respect composition up to homotopy).

[L3]

Chain-homotopic maps induce the same homology map (Chain-homotopic maps induce the same map on homology).

[L4]

Homology respects composition (Homology respects identities and composition).

Proof

technique · direct
1.1

Choose comparison lifts u~ of u, v~ of v, and vu~ of vu as in [L1]. By [L2], vu~ is homotopic to v~u~.

L1L2givenconstruct
2.1

After applying F, [L3] makes the induced homology map of F(vu~) equal to that of F(v~u~). By [L4], the latter equals the composite of the maps induced by F(u~) and F(v~). Translating back through [L1] gives LnPF(vu)=LnPF(v)LnPF(u).

L1L3L4step 1.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Left derived functors relative to supplied data are additive functors

Statement

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum and F:AB an additive functor between abelian categories. For every nZ, the assignments ALnPF(A),uLnPF(u) define an additive functor on the domain of P.

Facts & Assumptions

Given: An integer n.

[L1]

Left derived maps preserve identities (Left derived maps preserve identities).

[L2]

Left derived maps preserve composition (Left derived maps preserve composition).

[L3]

The category of complexes in an additive category is additive, so comparison lifts can be added degreewise (The category of complexes in an additive category is additive).

[L4]

Two comparison lifts of the same morphism are chain-homotopic (Projective comparison maps are unique up to chain homotopy).

[L5]

Applying F degreewise preserves chain maps, and homology is an additive functor on complexes (An additive functor applies degreewise to complexes and chain maps, Homology is an additive functor).

[L6]

Chain-homotopic maps induce the same map on homology (Chain-homotopic maps induce the same map on homology).

[L7]

An additive functor is a functor that is additive on each hom-group (Additive functor).

Proof

technique · direct
1.1

By [L1] and [L2], the assignments ALnPF(A) and uLnPF(u) already form a functor.

L1L2
1.2

Let u,v:AB. Choose comparison lifts u~ and v~. By [L3], their degreewise sum u~+v~ is again a chain map, and it lifts u+v because augmentations are additive. Thus it is a comparison lift of u+v.

L3givenconstruct
2.1

By definition of the derived map and [L5], LnPF(u+v)=Hn ⁣(F(u~+v~))=Hn ⁣(F(u~))+Hn ⁣(F(v~)). If a different comparison lift of u+v were chosen, [L4] and [L6] would give the same homology map. Hence LnPF(u+v)=LnPF(u)+LnPF(v).

L4L5L6step 1.2algebra
3.1

Step 1.1 gives functoriality, and step 2.1 gives additivity on each hom-group. Therefore [L7] identifies LnPF as an additive functor.

L7step 1.1step 2.1
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A morphism has a comparison extension between the supplied injective resolutions

Statement

Assume the Axiom of Dependent Choice.

Let I be a supplied injective resolution datum on a class D in an abelian category. For every morphism u:AB with A,BD, there exists a coaugmentation-preserving cochain map u~:I(A)I(B) extending u.

Facts & Assumptions

Given: A morphism u:AB with A,BD.

[L1]

The datum I supplies specific injective resolutions AI(A) and BI(B) (Supplied injective resolution data).

[L2]

Assuming Dependent Choice, injective comparison maps exist for morphisms between chosen injective resolutions (Injective comparison maps exist).

Proof

technique · direct
1.1

By [L1], the objects A and B come with chosen injective resolutions.

L1given
2.1

Apply [L2] to u:AB and the resolutions from step 1.1. The resulting coaugmentation-preserving cochain map u~:I(A)I(B) is the required comparison extension.

L2step 1.1construct
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The induced cohomology map is independent of the chosen injective comparison extension

Statement

Assume the Axiom of Dependent Choice.

Let I be a supplied injective resolution datum and F:AB an additive functor. If u:AB is a morphism and u~,u^:I(A)I(B) are two injective comparison extensions of u, then for every nZ the induced maps on cohomology Hn ⁣(F(u~)),Hn ⁣(F(u^)):RInF(A)RInF(B) are equal.

Facts & Assumptions

Given: A morphism u:AB and two comparison extensions u~,u^ of u.

[L1]

Two injective comparison maps extending the same morphism are cochain-homotopic (Injective comparison maps are unique up to cochain homotopy).

[L2]

A cochain complex is read as a reindexed chain complex by reversing the grading sign (Cochain complex in an abelian category).

[L3]

A chain homotopy is an equation of the form fngn=dn+1sn+sn1dn (A chain homotopy).

[L4]

Additive functors preserve sums and zero morphisms (Additive functor, An additive functor preserves zero morphisms).

[L5]

Chain-homotopic maps induce the same map on homology (Chain-homotopic maps induce the same map on homology).

[L6]

The objects RInF(A) and RInF(B) are the cohomology objects of the deleted injective resolutions after applying F (Right derived objects relative to supplied injective resolution data).

Proof

technique · direct
1.1

By [L1], the two comparison extensions are cochain-homotopic. Using [L2], read that cochain homotopy as a chain homotopy after reindexing the complexes.

L1L2givenconstruct
2.1

Applying F to the homotopy equations from [L3] preserves their sum-and- zero form by [L4]. Hence the two reindexed chain maps F(u~) and F(u^) remain chain-homotopic.

L3L4step 1.1algebra
3.1

By [L5], these two maps induce the same homology map on the reindexed complexes. Translating back through [L2] and [L6], that is exactly equality of the induced maps on cohomology RInF(A)RInF(B).

L2L5L6step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The right derived map relative to supplied resolution data

Definition

Assume the Axiom of Dependent Choice.

Let I be a supplied injective resolution datum on a class D in an abelian category A, let F:AB be an additive functor to an abelian category B, let A,BD, and let nZ. For a morphism u:AB, choose any injective comparison extension u~:I(A)I(B).

The right derived map of u in degree n relative to I is the induced map on cohomology RInF(u):=Hn ⁣(F(u~)):RInF(A)RInF(B).

Existence of u~ comes from A morphism has a comparison extension between the supplied injective resolutions, and independence of the chosen extension comes from The induced cohomology map is independent of the chosen injective comparison extension.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Right derived functors relative to supplied data are additive functors

Statement

Assume the Axiom of Dependent Choice.

Let I be a supplied injective resolution datum and F:AB an additive functor between abelian categories. For every nZ, the assignments ARInF(A),uRInF(u) define an additive functor on the domain of I.

Facts & Assumptions

Given: An integer n.

[L1]

Right derived maps are defined from injective comparison extensions (The right derived map relative to supplied resolution data).

[L2]

The cochain comparison-extension construction is available for every morphism, and its induced cohomology map is independent of the chosen extension (A morphism has a comparison extension between the supplied injective resolutions, The induced cohomology map is independent of the chosen injective comparison extension).

[L3]

A cochain complex may be reindexed as a chain complex (Cochain complex in an abelian category).

[L4]

The category of complexes in an additive category is additive, and additive functors apply degreewise to chain maps (The category of complexes in an additive category is additive, An additive functor applies degreewise to complexes and chain maps).

[L5]

Two injective comparison extensions of the same morphism are cochain-homotopic, and after reindexing chain-homotopic maps induce the same map on homology (Injective comparison maps are unique up to cochain homotopy, Chain-homotopic maps induce the same map on homology).

[L6]

An additive functor is a functor that is additive on each hom-group (Additive functor).

Proof

technique · direct
1.1

Identity and composition are proved exactly as on the projective side: choose comparison extensions for the relevant morphisms, compare the extension of a composite or identity with the obvious chain-level candidate, and use [L5] after reindexing by [L3]. Therefore the assignments in [L1] form a functor.

L1L2L3L5givenalgebra
1.2

Let u,v:AB. Choose comparison extensions u~ and v~. By [L4], their degreewise sum is a cochain map and extends u+v, so it is a comparison extension of u+v.

L2L4construct
2.1

Reindexing by [L3], applying F degreewise by [L4], and using homotopy invariance from [L5], the induced cohomology map of u~+v~ equals the sum of the induced cohomology maps of u~ and v~. Hence RInF(u+v)=RInF(u)+RInF(v).

L3L4L5step 1.2algebra
3.1

Steps 1.1 and 2.1 give the functoriality and hom-group additivity required by [L6]. Therefore RInF is an additive functor.

L6step 1.1step 2.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A natural transformation induces natural transformations of left derived functors

Statement

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum, let F,G:AB be additive functors between abelian categories, and let α:FG be a natural transformation. Then for every nZ the maps LnP(α)A:=Hn ⁣(αP(A)del):LnPF(A)LnPG(A) define a natural transformation LnP(α):LnPFLnPG.

Facts & Assumptions

Given: An integer n.

[L1]

A natural transformation is a family of components satisfying the naturality equation on every morphism (Natural transformation and its components).

[L2]

Additive functors apply degreewise to complexes and chain maps (An additive functor applies degreewise to complexes and chain maps).

[L3]

Every chain map induces a well-defined map on homology (A chain map induces a well-defined map on homology).

[L4]

The left derived maps are the homology maps induced from comparison lifts (The left derived map relative to supplied resolution data).

[L5]

The source and target assignments are already functors (Left derived functors relative to supplied data are additive functors).

Proof

technique · direct
1.1

For each object A, the components αPk(A) form a chain map αP(A)del:F(P(A)del)G(P(A)del), because [L1] makes them commute with each differential of the chosen deleted resolution.

L1L2givenalgebra
2.1

By [L3], step 1.1 induces a morphism LnP(α)A:LnPF(A)LnPG(A) for each A.

L3step 1.1construct
3.1

Let u:AB, and choose a comparison lift u~:P(A)P(B). Naturality in [L1] gives G(u~k)αPk(A)=αPk(B)F(u~k) for every degree k, so the square of chain maps commutes. Passing to homology and using [L4] gives LnPG(u)LnP(α)A=LnP(α)BLnPF(u). Thus the components from step 2.1 are natural.

L1L4L5step 2.1algebra
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A natural transformation induces natural transformations of right derived functors

Statement

Assume the Axiom of Dependent Choice.

Let I be a supplied injective resolution datum, let F,G:AB be additive functors, and let α:FG be a natural transformation. Then for every nZ the maps RIn(α)A:=Hn ⁣(αI(A)del):RInF(A)RInG(A) define a natural transformation RIn(α):RInFRInG.

Facts & Assumptions

Given: An integer n.

[L1]

A natural transformation is objectwise and satisfies the naturality equation on every morphism (Natural transformation and its components).

[L2]

A cochain complex is read as a reindexed chain complex (Cochain complex in an abelian category).

[L3]

Additive functors apply degreewise to chain maps, and every chain map induces a homology map (An additive functor applies degreewise to complexes and chain maps, A chain map induces a well-defined map on homology).

[L4]

Right derived maps are induced by comparison extensions on the chosen injective resolutions (The right derived map relative to supplied resolution data).

[L5]

The source and target assignments are already functors (Right derived functors relative to supplied data are additive functors).

Proof

technique · direct
1.1

For each object A, the components αIk(A) commute with the cochain differentials by [L1], so they form a cochain map F(I(A)del)G(I(A)del). Reindexing by [L2] turns this into a chain map.

L1L2givenalgebra
2.1

By [L3], step 1.1 induces a map on homology of the reindexed complexes, hence on cohomology: RIn(α)A:RInF(A)RInG(A).

L2L3step 1.1construct
3.1

Let u:AB, and choose a comparison extension u~:I(A)I(B). Naturality in [L1] gives degreewise commutative squares with the maps αIk(A) and αIk(B). Passing to cohomology and translating through [L4] gives RInG(u)RIn(α)A=RIn(α)BRInF(u). Thus the components from step 2.1 are natural.

L1L4L5step 2.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Objectwise comparison of two projective resolution data induces an isomorphism on derived objects

Statement

Assume the Axiom of Dependent Choice.

Let P and Q be supplied projective resolution data on the same domain, and let F:AB be an additive functor between abelian categories. For every object A in the common domain and every nZ, there is an isomorphism θP,Q(A):LnPF(A)  LnQF(A) induced by a comparison map between the chosen resolutions of A.

Facts & Assumptions

Given: An object A in the common domain and an integer n.

[L1]

The data P and Q supply specific projective resolutions of A (Supplied projective resolution data).

[L2]

Any two projective resolutions of the same object are homotopy equivalent over that object (Projective resolutions of the same object are homotopy equivalent over that object).

[L3]

Chain-homotopic maps induce the same homology map, and homology respects composition (Chain-homotopic maps induce the same map on homology, Homology respects identities and composition).

[L4]

The derived objects are the homology objects of the chosen deleted resolutions after applying F (Left derived objects relative to supplied projective resolution data).

Proof

technique · direct
1.1

By [L1] and [L2], there exist comparison maps c:P(A)Q(A) and d:Q(A)P(A) whose composites are homotopic to the identity chain maps on the two resolutions.

L1L2givenconstruct
2.1

Apply F degreewise and pass to homology. By [L3], the induced maps Hn(F(c)) and Hn(F(d)) are inverse because their composites equal the homology maps of chain maps homotopic to the identities. Using [L4], this yields the claimed isomorphism θP,Q(A):LnPF(A)LnQF(A).

L3L4step 1.1
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The change-of-projective-resolution isomorphisms are natural

Statement

Assume the Axiom of Dependent Choice.

With the notation of Objectwise comparison of two projective resolution data induces an isomorphism on derived objects, the isomorphisms θP,Q(A) are natural in A.

Facts & Assumptions

Given: A morphism u:AB and an integer n.

[L1]

The supplied projective data admit comparison lifts of u on both sides (A morphism has a comparison lift between the supplied projective resolutions).

[L2]

The objectwise comparison maps induce isomorphisms on derived objects (Objectwise comparison of two projective resolution data induces an isomorphism on derived objects).

[L3]

Two projective comparison maps lifting the same morphism are chain-homotopic, and chain-homotopic maps induce the same homology map (Projective comparison maps are unique up to chain homotopy, Chain-homotopic maps induce the same map on homology).

Proof

technique · direct
1.1

Choose objectwise comparison maps cA:P(A)Q(A) and cB:P(B)Q(B) that define the isomorphisms in [L2], and choose comparison lifts u~P:P(A)P(B) and u~Q:Q(A)Q(B) from [L1].

L1L2givenconstruct
2.1

Both composites cBu~P and u~QcA are comparison maps from P(A) to Q(B) lifting the same morphism u, so [L3] makes them chain-homotopic. Passing to homology gives θP,Q(B)LnPF(u)=LnQF(u)θP,Q(A). Therefore the family θP,Q(A) is natural.

L2L3step 1.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Two supplied projective resolution data define naturally isomorphic left derived functors

Statement

Assume the Axiom of Dependent Choice.

Let P and Q be supplied projective resolution data on the same domain, and let F:AB be an additive functor. For every nZ, the additive functors LnPF and LnQF are naturally isomorphic.

Facts & Assumptions

Given: An integer n.

[L1]

Both constructions define additive functors (Left derived functors relative to supplied data are additive functors).

[L2]

For each object, objectwise comparison of the two chosen resolutions induces an isomorphism on derived objects (Objectwise comparison of two projective resolution data induces an isomorphism on derived objects).

[L3]

Those isomorphisms are natural in the object (The change-of-projective-resolution isomorphisms are natural).

Proof

technique · direct
1.1

By [L2], each object A carries an isomorphism θP,Q(A):LnPF(A)LnQF(A).

L2given
2.1

By [L3], the family from step 1.1 is natural. Together with [L1], this is exactly a natural isomorphism of additive functors LnPFLnQF.

L1L3step 1.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

Change-of-projective-resolution isomorphisms satisfy identity and cocycle laws

Statement

Assume the Axiom of Dependent Choice.

Let P,Q,R be supplied projective resolution data on the same domain, and let F:AB be an additive functor between abelian categories. For each ordered pair (S,T) among these data, let θS,T be the change-of-data natural isomorphism whose component at an object A is induced by any comparison map S(A)T(A) lifting 1A. Then:

  1. θP,P=1LnPF for every n.
  2. θQ,RθP,Q=θP,R for every n.

Facts & Assumptions

Given: An object A in the common domain and an integer n.

[L1]

A comparison map between two supplied projective resolutions of A induces the isomorphism θS,T(A), and these objectwise isomorphisms are natural in A (Objectwise comparison of two projective resolution data induces an isomorphism on derived objects, The change-of-projective-resolution isomorphisms are natural).

[L2]

Two projective comparison maps lifting the same morphism are chain-homotopic (Projective comparison maps are unique up to chain homotopy).

[L3]

Chain-homotopic maps induce the same homology map, and homology respects composition (Chain-homotopic maps induce the same map on homology, Homology respects identities and composition).

Proof

technique · direct
1.1

For the pair (P,P), one valid comparison map is the identity chain map on P(A). Any comparison map used to define θP,P(A) also lifts 1A, so [L2] makes it homotopic to the identity chain map. By [L3], the induced homology map is therefore the identity on LnPF(A).

L1L2L3given
1.2

For the triple (P,Q,R), the chain map defining θQ,R(A)θP,Q(A) is the composite of two comparison maps P(A)Q(A)R(A) lifting 1A. The chain map defining θP,R(A) is another comparison map lifting 1A. By [L2] they are homotopic, so [L3] gives equality of the induced homology maps: θQ,R(A)θP,Q(A)=θP,R(A).

L1L2L3algebra
2.1

Since A was arbitrary, steps 1.1 and 1.2 prove the identity and cocycle laws for the natural isomorphisms.

step 1.1step 1.2
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

Two supplied injective resolution data define naturally isomorphic right derived functors

Statement

Assume the Axiom of Dependent Choice.

Let I and J be supplied injective resolution data on the same domain, and let F:AB be an additive functor. For every nZ, the additive functors RInF and RJnF are naturally isomorphic.

Facts & Assumptions

Given: A morphism u:AB and an integer n.

[L1]

The two constructions define additive functors (Right derived functors relative to supplied data are additive functors).

[L2]

The chosen injective resolutions of a fixed object are homotopy equivalent under that object (Injective resolutions of the same object are homotopy equivalent under that object).

[L3]

Two injective comparison maps extending the same morphism are cochain-homotopic (Injective comparison maps are unique up to cochain homotopy).

[L4]

A cochain complex is read as a reindexed chain complex, and chain-homotopy invariance together with homology's compatibility with composition survives that reindexing (Cochain complex in an abelian category, Chain-homotopic maps induce the same map on homology, Homology respects identities and composition).

[L5]

Comparison extensions exist for morphisms on the supplied injective data (A morphism has a comparison extension between the supplied injective resolutions).

Proof

technique · direct
1.1

Fix an object A. By [L2], there are comparison maps cA:I(A)J(A) and dA:J(A)I(A) whose composites are cochain- homotopic to the identities. Using [L4], these induce inverse isomorphisms θI,J(A):RInF(A)RJnF(A).

L2L4givenconstruct
2.1

For a morphism u:AB, choose comparison extensions u~I:I(A)I(B) and u~J:J(A)J(B) from [L5]. Both composites cBu~I and u~JcA extend u, so [L3] makes them cochain-homotopic. By [L4], their induced cohomology maps agree, which is exactly the naturality square θI,J(B)RInF(u)=RJnF(u)θI,J(A).

L3L4L5step 1.1algebra
3.1

Steps 1.1 and 2.1 produce a natural isomorphism RInFRJnF, and [L1] records that both sides are additive functors.

L1step 1.1step 2.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

Change-of-injective-resolution isomorphisms satisfy identity and cocycle laws

Statement

Assume the Axiom of Dependent Choice.

Let I,J,K be supplied injective resolution data on the same domain, and let F:AB be an additive functor between abelian categories. For each ordered pair (S,T) among these data, let θS,T be the change-of-data natural isomorphism whose component at an object A is induced by any comparison extension S(A)T(A) of 1A. Then:

  1. θI,I=1RInF for every n.
  2. θJ,KθI,J=θI,K for every n.

Facts & Assumptions

Given: An object A in the common domain and an integer n.

[L1]

The chosen injective resolutions of the same object are homotopy equivalent under that object (Injective resolutions of the same object are homotopy equivalent under that object).

[L2]

Two injective comparison maps extending the same morphism are cochain-homotopic (Injective comparison maps are unique up to cochain homotopy).

[L3]

Reindexing turns cochain homotopies into chain homotopies, and homology then respects both homotopy and composition (Cochain complex in an abelian category, Chain-homotopic maps induce the same map on homology, Homology respects identities and composition).

[L4]

Comparison extensions exist for morphisms between objects in the domain of each supplied injective datum (A morphism has a comparison extension between the supplied injective resolutions).

Proof

technique · direct
1.1

For any ordered pair (S,T), [L1] gives comparison extensions cA:S(A)T(A) and dA:T(A)S(A) of 1A. Their composites extend 1A, so [L2] and [L3] show that the induced cohomology maps are inverse. Any other choice of cA extends the same identity and hence induces the same map. For a morphism u:AB, choose within-data comparison extensions using [L4]. The two composites from S(A) to T(B) both extend u, so [L2] and [L3] give the naturality square. Thus the displayed construction specifies a well-defined natural isomorphism θS,T.

L1L2L3L4givenconstruct
2.1

For the pair (I,I), the identity cochain map on I(A) is a comparison extension of 1A. Any comparison extension used in step 1.1 to define θI,I(A) extends the same identity morphism, so [L2] makes it cochain-homotopic to the identity. By [L3], the induced map on cohomology is therefore the identity on RInF(A).

L2L3step 1.1
2.2

For the triple (I,J,K), the cochain map defining θJ,K(A)θI,J(A) is the composite of two comparison extensions of 1A, while the map defining θI,K(A) is another comparison extension of 1A. By [L2] these are cochain-homotopic, so [L3] gives θJ,K(A)θI,J(A)=θI,K(A).

L2L3step 1.1algebra
3.1

Since A was arbitrary, steps 2.1 and 2.2 prove the identity and cocycle laws for the natural isomorphisms constructed in step 1.1.

step 1.1step 2.1step 2.2
RemarkRemark: Literature-sourcedProof: Not applicableaudited 2026-09-04Open item page →

Derived functors are well defined relative to supplied resolution data

Assume the Axiom of Dependent Choice. Derived functors are well defined here in a specific seven-part sense, and each part is now on the page rather than being collapsed into one slogan:

  1. supplied resolutions give the object assignments;
  2. comparison maps or extensions exist for each morphism (A morphism has a comparison lift between the supplied projective resolutions, A morphism has a comparison extension between the supplied injective resolutions);
  3. the induced map is independent of the chosen lift (The induced homology map is independent of the chosen comparison lift, The induced cohomology map is independent of the chosen injective comparison extension);
  4. those maps preserve identities (Left derived functors relative to supplied data are additive functors, Right derived functors relative to supplied data are additive functors);
  5. those maps preserve composition (Left derived functors relative to supplied data are additive functors, Right derived functors relative to supplied data are additive functors);
  6. changing the supplied data yields a natural isomorphism (Two supplied projective resolution data define naturally isomorphic left derived functors, Two supplied injective resolution data define naturally isomorphic right derived functors); and
  7. those change-of-data isomorphisms satisfy identity and cocycle laws (Change-of-projective-resolution isomorphisms satisfy identity and cocycle laws, Change-of-injective-resolution isomorphisms satisfy identity and cocycle laws).

What this remark does not claim is a global theorem saying that enough projectives or enough injectives canonically choose one resolution for every object. The present conclusions are relative to displayed supplied data, and two different data are compared by natural isomorphism rather than by an unstated class-sized choice.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The zero-th left derived functor of a right exact functor recovers the functor

Statement

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum on a class D, and let F:AB be an additive right exact functor between abelian categories. Then for every AD there is a canonical isomorphism L0PF(A)  F(A), natural in A.

Facts & Assumptions

Given: An object AD.

[L1]

The chosen projective resolution of A is an exact augmented complex P1(A)P0(A)A0 (Projective resolutions in an abelian category).

[L2]

The zeroth homology of the deleted complex is the cokernel of the boundary map into degree 0 (Homology object of a chain complex).

[L3]

Right exactness means that F preserves the cokernel appearing at the end of the displayed augmented resolution (Left exact and right exact functors).

[L4]

The assignments AL0PF(A) are already functorial (Left derived functors relative to supplied data are additive functors).

Proof

technique · direct
1.1

By [L1], the morphism P1(A)P0(A)A0 is exact. Applying F and using [L3] gives an exact sequence F(P1(A))F(P0(A))F(A)0. Hence F(A) is the cokernel of F(P1(A))F(P0(A)).

L1L3givenalgebra
2.1

By [L2], that same cokernel is exactly H0(F(P(A)del))=L0PF(A). Therefore there is a canonical isomorphism L0PF(A)F(A).

L2step 1.1
3.1

The construction in steps 1.1 and 2.1 is functorial in A, and [L4] already supplies the functoriality of L0PF. Thus the isomorphism is natural in A.

L4step 2.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The zero-th right derived functor of a left exact functor recovers the functor

Statement

Assume the Axiom of Dependent Choice.

Let I be a supplied injective resolution datum on a class D, and let F:AB be an additive left exact functor between abelian categories. Then for every AD there is a canonical isomorphism RI0F(A)  F(A), natural in A.

Facts & Assumptions

Given: An object AD.

[L1]

The chosen injective resolution of A is an exact coaugmented complex 0AI0(A)I1(A) (Injective resolutions in an abelian category).

[L2]

The zeroth cohomology object is the quotient of the kernel of d0:F(I0(A))F(I1(A)) by the zero-th coboundary, which is 0 (Cohomology object of a cochain complex).

[L3]

Left exactness means that F preserves the kernel at the beginning of the displayed injective resolution (Left exact and right exact functors).

[L4]

The assignments ARI0F(A) are already functorial (Right derived functors relative to supplied data are additive functors).

Proof

technique · direct
1.1

By [L1], the morphism 0AI0(A)I1(A) is exact. Applying F and using [L3] gives an exact sequence 0F(A)F(I0(A))F(I1(A)). Therefore F(A)=ker(F(I0(A))F(I1(A))).

L1L3givenalgebra
2.1

By [L2], the zeroth cohomology of F(I(A)del) is that kernel, because the zero-th coboundary object is 0. Hence RI0F(A)=H0(F(I(A)del))F(A).

L2step 1.1
3.1

Step 2.1 is natural in A, and [L4] records the functoriality of RI0F. Therefore the displayed isomorphism is natural.

L4step 2.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Positive left derived functors vanish on projective objects

Statement

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum on a class D and F:AB an additive functor between abelian categories. If QD is a projective object, then for every n>0, LnPF(Q)=0.

Facts & Assumptions

Given: A projective object QD and an integer n>0.

[L1]

Every projective object admits a length-zero projective resolution (A projective object has a length-zero projective resolution).

[L2]

Changing the supplied projective resolution datum changes the derived objects only by natural isomorphism (Two supplied projective resolution data define naturally isomorphic left derived functors).

[L3]

The left derived object is the homology of the deleted chosen resolution (Left derived objects relative to supplied projective resolution data).

Proof

technique · direct
1.1

By [L1], the object Q has a projective resolution concentrated in degree 0. Its deleted complex therefore has only one nonzero term, namely Q in degree 0.

L1givenconstruct
2.1

Let P be the supplied projective resolution datum on the same domain as P that agrees with P away from Q and assigns the length-zero resolution from step 1.1 to Q. By [L2], the derived object computed from P is isomorphic to the one computed from P. By [L3], the deleted resolution in P(Q) is the one-term complex from step 1.1, whose homology is zero in every positive degree. Hence LnPF(Q)=0 for n>0.

L2L3step 1.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

Positive right derived functors vanish on injective objects

Statement

Assume the Axiom of Dependent Choice.

Let I be a supplied injective resolution datum on a class D and F:AB an additive functor between abelian categories. If JD is an injective object, then for every n>0, RInF(J)=0.

Facts & Assumptions

Given: An injective object JD and an integer n>0.

[L1]

An injective resolution is a coaugmented exact complex of injectives (Injective resolutions in an abelian category).

[L2]

The object J is injective (Injective object).

[L3]

Changing the supplied injective resolution datum changes the derived objects only by natural isomorphism (Two supplied injective resolution data define naturally isomorphic right derived functors).

[L4]

The right derived object is the cohomology of the deleted chosen resolution after applying F (Right derived objects relative to supplied injective resolution data).

Proof

technique · direct
1.1

The coaugmented complex 0J1JJ00 is exact and all its terms are injective by [L2], so [L1] makes it an injective resolution of J. After applying F, its deleted cochain complex has only one nonzero term, namely F(J) in degree 0.

L1L2L4givenconstruct
2.1

Let I be the supplied injective resolution datum on the same domain as I that agrees with I away from J and assigns the trivial injective resolution from step 1.1 to J. By [L3], the right derived object computed from I is isomorphic to the one computed from I. By [L4], the complex computing RInF(J) is the one-term complex from step 1.1, whose cohomology is zero in every positive degree. Hence RInF(J)=0 for n>0.

L3L4step 1.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

An acyclic object for a left exact functor

Definition

Let I be a supplied injective resolution datum on a class D, and let F:AB be an additive left exact functor between abelian categories.

An object AD is F-acyclic if RInF(A)=0for every n>0.

If J is another supplied injective resolution datum on the same domain and one assumes the Axiom of Dependent Choice, then Two supplied injective resolution data define naturally isomorphic right derived functors gives natural isomorphisms RInF(A)RJnF(A) for every n. Under that additional hypothesis, this vanishing condition is independent of the chosen supplied injective datum.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

An acyclic object for a right exact functor

Definition

Let P be a supplied projective resolution datum on a class D, and let F:AB be an additive right exact functor between abelian categories.

An object AD is F-acyclic if LnPF(A)=0for every n>0.

If Q is another supplied projective resolution datum on the same domain and one assumes the Axiom of Dependent Choice, then Two supplied projective resolution data define naturally isomorphic left derived functors gives natural isomorphisms LnPF(A)LnQF(A) for every n. Under that additional hypothesis, this vanishing condition is independent of the chosen supplied projective datum.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

An F-acyclic resolution

Definition

Let F be an additive functor between abelian categories.

  1. If F is left exact and I is a supplied injective resolution datum on a class D, an F-acyclic resolution of A relative to I is a coaugmented exact complex 0AJ0J1 such that every Jq lies in D and is F-acyclic in the sense of An acyclic object for a left exact functor.
  2. If F is right exact and P is a supplied projective resolution datum on a class D, an F-acyclic resolution of A relative to P is an augmented exact complex P1P0A0 such that every Pq lies in D and is F-acyclic in the sense of An acyclic object for a right exact functor.

Thus the phrase keeps both the resolution orientation and the chosen supplied datum visible.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The acyclic-resolution theorem for right derived functors

Statement

Assume the Axiom of Dependent Choice.

Let I be a supplied injective resolution datum on a class D, let F:AB be an additive left exact functor, and let 0AJ0J1J2 be an F-acyclic resolution of A relative to I. Assume moreover that AD and that, for Z0:=A and 0ZqJqZq+10(q0), each Zq lies in D. Then for every n0 there is a canonical isomorphism RInF(A)  Hn(F(Jdel)).

Facts & Assumptions

Given: An F-acyclic resolution 0AJ0J1 of A relative to I, the associated objects ZqD, and an integer n0.

[L1]

An F-acyclic resolution is an exact coaugmented complex whose terms are F-acyclic objects (An F-acyclic resolution, An acyclic object for a left exact functor).

[L2]

The zero-th right derived functor of a left exact functor recovers the functor (The zero-th right derived functor of a left exact functor recovers the functor).

[L3]

Change of supplied injective resolution data produces natural isomorphisms of right derived functors (Two supplied injective resolution data define naturally isomorphic right derived functors).

[L4]

Passing to the opposite abelian category and applying the projective horseshoe lemma produces injective resolutions of a short exact sequence in a degreewise split short exact sequence of cochain complexes (The opposite of an abelian category is abelian, The horseshoe lemma for projective resolutions).

[L5]

A short exact sequence of cochain complexes yields a long exact sequence in cohomology (The long exact sequence in cohomology).

[L6]

An additive functor preserves finite biproducts (An additive functor preserves finite biproducts), and therefore preserves split short exact sequences.

Proof

technique · direct
1.1

By exactness in [L1], let Z0=A and for each q0 let Zq+1 fit into a short exact sequence 0ZqJqZq+10. Every Jq is F-acyclic by [L1].

L1givenconstruct
2.1

Apply [L4] to each short exact sequence from step 1.1 using the supplied injective resolutions of Zq and Zq+1, which exist by the domain hypothesis in the statement. The result is a degreewise split short exact sequence of injective resolutions. By [L6], applying F preserves its degreewise exactness, so [L5] gives a long exact cohomology sequence. The middle injective resolution supplied by the horseshoe construction may differ from the one fixed for Jq, but [L3] identifies their right derived objects. Its higher cohomology therefore vanishes because Jq is F-acyclic. Using [L2] for degree 0, we obtain exact sequences 0F(Zq)F(Jq)F(Zq+1)RI1F(Zq)0 and isomorphisms RIm+1F(Zq)RImF(Zq+1)(m>0).

L2L3L4L5L6step 1.1algebra
3.1

Repeatedly applying the isomorphisms from step 2.1 gives RInF(A)=RInF(Z0)RI1F(Zn1)(n>0).

step 2.1algebra
4.1

For n>0, the exact sequence 0F(Zn)F(Jn)F(Zn+1) from step 2.1 shows that the nth cohomology of F(Jdel) is the cokernel of F(Jn1)F(Zn). The same step identifies that cokernel with RI1F(Zn1), so step 3.1 gives Hn(F(Jdel))RInF(A).

step 2.1step 3.1algebra
5.1

For n=0, step 2.1 with q=0 gives 0F(A)F(J0)F(Z1) exact, so H0(F(Jdel))F(A). By [L2], F(A)RI0F(A). Together with step 4.1, this proves the theorem for all n0.

L2step 2.1step 4.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The acyclic-resolution theorem for left derived functors

Statement

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum on a class D, let F:AB be an additive right exact functor, and let Q2Q1Q0A0 be an F-acyclic resolution of A relative to P. Assume moreover that AD and that, for Z0:=A and 0Zq+1QqZq0(q0), each Zq lies in D. Then for every n0 there is a canonical isomorphism LnPF(A)  Hn(F(Qdel)).

Facts & Assumptions

Given: An F-acyclic resolution Q1Q0A0 of A relative to P, the associated objects ZqD, and an integer n0.

[L1]

An F-acyclic resolution is an exact augmented complex whose terms are F-acyclic objects (An F-acyclic resolution, An acyclic object for a right exact functor).

[L2]

The zero-th left derived functor of a right exact functor recovers the functor (The zero-th left derived functor of a right exact functor recovers the functor).

[L3]

Change of supplied projective resolution data produces canonical natural isomorphisms of left derived functors (Two supplied projective resolution data define naturally isomorphic left derived functors).

[L4]

Projective resolutions of a short exact sequence can be arranged into a short exact sequence of chain complexes by the projective horseshoe lemma (The horseshoe lemma for projective resolutions).

[L5]

A short exact sequence of chain complexes yields a long exact sequence in homology (The long exact sequence in homology).

Proof

technique · direct
1.1

By exactness in [L1], let Z0=A and for each q0 let Zq+1 fit into a short exact sequence 0Zq+1QqZq0. Every Qq is F-acyclic by [L1].

L1givenconstruct
2.1

Apply [L4] to each short exact sequence from step 1.1 using the supplied projective resolutions of Zq+1 and Zq, which exist by the domain hypothesis in the statement. The middle projective resolution from horseshoe need not be the supplied one for Qq, but [L3] identifies the resulting left derived objects. After applying F and [L5], the higher homology of the middle term vanishes because Qq is F-acyclic, while [L2] identifies the degree-zero term. Thus we obtain exact sequences 0L1PF(Zq)F(Zq+1)F(Qq)F(Zq)0 and isomorphisms LmPF(Zq+1)Lm+1PF(Zq)(m>0).

L2L3L4L5step 1.1algebra
3.1

Repeatedly applying the isomorphisms from step 2.1 gives LnPF(A)=LnPF(Z0)L1PF(Zn1)(n>0).

step 2.1algebra
4.1

For n>0, the exact sequence F(Zn+1)F(Qn)F(Zn)0 from step 2.1 shows that the quotient of F(Qn) by boundaries is F(Zn), and the same step identifies the kernel of F(Zn)F(Qn1) with L1PF(Zn1). Therefore Hn(F(Qdel))L1PF(Zn1)LnPF(A).

step 2.1step 3.1algebra
5.1

For n=0, right exactness gives F(Q1)F(Q0)F(A)0, so H0(F(Qdel))F(A). By [L2], F(A)L0PF(A). Together with step 4.1, this proves the theorem for all n0.

L2step 2.1step 4.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Adapted classes compute derived functors

Statement

Assume the Axiom of Dependent Choice.

  1. Let I be a supplied injective resolution datum on a class D, and let F be an additive left exact functor. Suppose CD is made of F-acyclic objects, is closed under cokernels of monomorphisms between objects of C, and every object of D admits a monomorphism into an object of C. Then any coaugmented resolution of an object AD obtained by iterating monomorphisms ZqCq,CqC,Zq+1:=coker(ZqCq)D, computes RInF(A).
  2. Dually, let P be a supplied projective resolution datum on a class D, let F be additive and right exact, and suppose CD is made of F-acyclic objects, is closed under kernels of epimorphisms between objects of C, and every object of D admits an epimorphism from an object of C. Then any augmented resolution of an object AD obtained by iterating epimorphisms CqZq,CqC,Zq+1:=ker(CqZq)D, computes LnPF(A).

Facts & Assumptions

Given: One of the two clause-wise hypotheses from the statement.

[L1]

Once the relevant supplied datum is fixed, an F-acyclic resolution is exactly a resolution whose terms are F-acyclic and whose orientation matches the side being derived (An F-acyclic resolution).

[L2]

Such resolutions compute right derived functors (The acyclic-resolution theorem for right derived functors).

[L3]

Such resolutions compute left derived functors (The acyclic-resolution theorem for left derived functors).

Proof

technique · direct
1.1

In the left exact case, start with Z0=A. By hypothesis, every object of D admits a monomorphism into an object of C, so we may choose monomorphisms ZqCq with CqC and define Zq+1 to be the cokernel, still in D. This produces an exact coaugmented resolution by objects of C. Because every object of C is F-acyclic, [L1] identifies the result as an F-acyclic resolution relative to I.

L1givenconstruct
1.2

The right exact case is dual: start with Z0=A, repeatedly choose epimorphisms CqZq with CqC, and define Zq+1 to be the kernel, still in D. The resulting exact augmented resolution has all terms in C, hence is an F-acyclic resolution relative to P by [L1].

L1givenconstruct
2.1

Apply [L2] to the resolution from step 1.1 and [L3] to the resolution from step 1.2. This proves both clauses.

L2L3step 1.1step 1.2
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

An exact functor has vanishing positive derived functors

Statement

Let P be a supplied projective resolution datum on a class DP, let I be a supplied injective resolution datum on a class DI, and let F:AB be an exact functor between abelian categories. Then for every ADP and every n>0, LnPF(A)=0, and for every BDI and every n>0, RInF(B)=0.

Facts & Assumptions

Given: An integer n>0, an object ADP, and an object BDI.

[L1]

The left and right derived objects are the homology or cohomology of the deleted chosen resolutions after applying F (Left derived objects relative to supplied projective resolution data, Right derived objects relative to supplied injective resolution data).

[L2]

Exact functors commute with homology of chain complexes (An exact functor commutes with homology).

[L3]

Exactness means that F is exact on both the projective and injective resolution complexes (Exact functor between abelian categories).

Proof

technique · direct
1.1

The deleted projective resolution of A is exact in every positive degree. By [L3], applying F preserves that exactness, so the resulting chain complex has zero homology in every positive degree. Using [L1], this says LnPF(A)=0 for n>0.

L1L3givenalgebra
1.2

Read the deleted injective resolution of B as a reindexed chain complex. It is exact in every positive cohomological degree, and [L3] preserves that exactness after applying F. By [L2], the resulting homology, hence cohomology, is zero in every positive degree. Therefore RInF(B)=0 for n>0.

L1L2L3algebra
2.1

Steps 1.1 and 1.2 prove the claimed vanishing on both sides.

step 1.1step 1.2
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Derived functors commute with finite biproducts

Statement

Assume the Axiom of Dependent Choice.

Let P be a supplied projective resolution datum on a class DP, let I be a supplied injective resolution datum on a class DI, and let F:AB be an additive functor between abelian categories. For every nZ, the additive functor LnPF preserves finite biproducts that exist in the domain of P, and the additive functor RInF preserves finite biproducts that exist in the domain of I.

Facts & Assumptions

Given: A finite biproduct in one of the two relevant supplied-data domains.

[L1]

The left derived functor LnPF is additive (Left derived functors relative to supplied data are additive functors).

[L2]

The right derived functor RInF is additive (Right derived functors relative to supplied data are additive functors).

[L3]

Any additive functor preserves finite biproducts (An additive functor preserves finite biproducts).

Proof

technique · direct
1.1

Apply [L3] to the additive functor LnPF from [L1]. This gives preservation of finite biproducts on the left-derived side.

L1L3
1.2

Apply [L3] to the additive functor RInF from [L2]. This gives preservation of finite biproducts on the right-derived side.

L2L3
2.1

Therefore both derived constructions commute with finite biproducts.

step 1.1step 1.2
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Contravariant derived functors are derived on the opposite category

Statement

Let G:AB be a contravariant additive functor between abelian categories, regarded as a covariant functor G:AopB. If P is a supplied projective resolution datum on a class D in A, then reversing arrows turns it into a supplied injective resolution datum Pop on the same class in Aop, and for every AD, RPopnG(A)=Hn ⁣(G(P(A)del)). Thus contravariant derived functors are computed on the opposite category.

Facts & Assumptions

Given: A contravariant additive functor G, a supplied projective datum P on D, and an object AD.

[L1]
[L2]

If A is abelian then Aop is abelian (The opposite of an abelian category is abelian).

[L3]

Projective objects are defined by lifting against epimorphisms, while injective objects are defined dually by extension across monomorphisms (Projective object, Injective object).

[L4]

Right derived objects are defined from supplied injective resolution data (Right derived objects relative to supplied injective resolution data).

Proof

technique · direct
1.1

By [L1] and [L2], G may be treated as a covariant additive functor on the abelian category Aop.

L1L2given
1.2

A projective resolution in A becomes, after reversing arrows, a coaugmented exact complex in Aop. Because [L3] exchanges the lifting and extension conditions under passage to the opposite category, each projective term becomes injective there. Hence the supplied datum P becomes an injective resolution datum Pop on D in Aop.

L2L3construct
2.1

Applying [L4] to the covariant functor G:AopB and the injective datum Pop gives RPopnG(A)=Hn(G(P(A)del)). This is exactly the correct opposite-category formulation of deriving the original contravariant functor.

L1L4step 1.2
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A bifunctor can be derived in either variable when the relevant resolution data are supplied

Statement

Let A,C,D be abelian categories, and let B:Aop×CD be additive in each variable. Let P be supplied projective resolution data on a class DA of objects of A, and let I be supplied injective resolution data on a class DC of objects of C. Then:

  1. for each fixed ADA, the covariant functor B(A,) has right derived objects at every CDC, RIn(B(A,))(C);
  2. for each fixed CDC, the contravariant functor B(,C) is derived at every ADA on Aop using the projective datum on A.

These are the two candidate one-variable derived constructions. No equality between them is asserted here.

Facts & Assumptions

Given: Abelian categories A,C,D, the displayed bifunctor B, and the supplied data P on DA and I on DC.

[L1]

Right derived objects are defined for covariant functors from supplied injective resolution data (Right derived objects relative to supplied injective resolution data).

[L2]

Left derived objects are defined for covariant functors from supplied projective resolution data (Left derived objects relative to supplied projective resolution data).

[L3]

Contravariant functors are derived on the opposite category (Contravariant derived functors are derived on the opposite category).

Proof

technique · direct
1.1

Fix ADA. Then B(A,):CD is a covariant additive functor between abelian categories, so [L1] gives the right derived objects RIn(B(A,))(C) for each CDC.

L1givenconstruct
1.2

Fix CDC. Then B(,C) is contravariant and additive in the A-variable. By [L3], it is derived at each ADA on Aop using P, equivalently the corresponding injective datum Pop on Aop.

L2L3construct
2.1

Steps 1.1 and 1.2 give the two candidate one-variable derived constructions. Since no comparison map between them has yet been supplied, no balance conclusion follows here.

step 1.1step 1.2
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A balanced derived bifunctor

Definition

Assume the Axiom of Dependent Choice. Let A,C,D be abelian categories, let B:Aop×CD be additive in each variable, let P be supplied projective resolution data on a class DA in A, and let I be supplied injective resolution data on a class DC in C. Assume moreover that for each fixed ADA the covariant functor B(A,):CD is left exact, and that for each fixed CDC the functor B(,C):AopD is left exact.

A balanced derived bifunctor relative to (P,I) on DAop×DC consists of the two candidate one-variable right-derived constructions from A bifunctor can be derived in either variable when the relevant resolution data are supplied together with, for every n0, a natural isomorphism RIn(B(A,))(C)RPopn(B(,C))(A) natural in ADA and CDC. These isomorphisms must satisfy:

  1. in degree 0, when the two candidates are identified with B(A,C) by The zero-th right derived functor of a left exact functor recovers the functor on C and on Aop, the balance isomorphism becomes the identity of B(A,C);
  2. the isomorphisms are natural in both variables in the sense of Natural transformation and its components.

This is a definition relative to the displayed supplied data P and I; it does not impose an unquantified condition involving alternative data. The definition records extra comparison data, while the previous proposition only constructs the two candidates.

5 · Examples, counterexamples and false statements

False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

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 Z/2Z.

[L1]

A supplied projective resolution datum is extra objectwise structure, not an existence theorem of its own (Supplied projective resolution data).

[L2]

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).

[L3]

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

technique · direct
1.1

One projective resolution of Z/2 is 0Z2ZZ/20. Adding the contractible projective complex 0Z1Z0 in degrees 1 and 0 gives a different projective resolution 0ZZdiag(2,1)ZZZ/20, where the augmentation is reduction modulo 2 on the first summand. Both displayed augmented complexes are exact, but they are not the same resolution.

givenconstructalgebra
2.1

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.

L1L2L3step 1.1
False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

FALSE: the definition of a derived map may depend on the chosen comparison lift

Statement

Assume the Axiom of Dependent Choice.

The definition of a derived map may depend on which comparison lift or comparison extension is chosen.

Facts & Assumptions

Given: The Axiom of Dependent Choice and a morphism between objects with supplied resolutions.

[L1]

Left derived maps are defined from comparison lifts (The left derived map relative to supplied resolution data).

[L2]

Right derived maps are defined from comparison extensions (The right derived map relative to supplied resolution data).

[L3]

The induced homology map is independent of the chosen projective comparison lift (The induced homology map is independent of the chosen comparison lift).

[L4]

The induced cohomology map is independent of the chosen injective comparison extension (The induced cohomology map is independent of the chosen injective comparison extension).

Refutation

technique · direct
1.1

On the projective side, [L1] defines the derived map from a comparison lift, and [L3] proves that any two such lifts induce the same homology map.

L1L3given
2.1

On the injective side, [L2] defines the derived map from a comparison extension, and [L4] proves that any two such extensions induce the same cohomology map. Therefore the displayed claim is false on both sides.

L2L4step 1.1
False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

FALSE: every additive functor has L_0 naturally isomorphic to itself

Statement

Every additive functor F has L0F naturally isomorphic to F.

Facts & Assumptions

Given: The additive functor F(M)=HomZ(Z/2Z,M) on abelian groups, and supplied projective resolution data P on a class containing Z/2Z that assigns it the standard resolution below.

[L1]

If F is right exact, the zero-th left derived functor recovers F naturally (The zero-th left derived functor of a right exact functor recovers the functor).

[L2]

Left derived objects are computed from the homology of an applied deleted projective resolution (Left derived objects relative to supplied projective resolution data).

[L3]

Additivity means preservation of sums on hom-groups (Additive functor).

Refutation

technique · direct
1.1

The functor F is additive by [L3], but it is enough to compute its value on the standard projective resolution 0Z×2ZZ/2Z0. Applying F to the deleted resolution gives 0HomZ(Z/2,Z)×2HomZ(Z/2,Z)0, and both displayed Hom groups are 0.

L2L3givenalgebra
2.1

Therefore L0PF(Z/2)=0, while F(Z/2)=HomZ(Z/2,Z/2)0. So L0PF is not naturally isomorphic to F for this supplied datum and additive functor. Thus additivity alone does not guarantee recovery; [L1] records right exactness as a sufficient hypothesis, and the displayed claim is false.

L1step 1.1
False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

FALSE: derived functors in two variables are automatically balanced

Statement

Whenever a bifunctor can be derived in each variable, the two derived constructions are automatically balanced.

Facts & Assumptions

Given: The Axiom of Dependent Choice, a field k, the ring R=k[ε]/(ε2), the abelian categories A=Vectkfd and C=R-Modfd, and the bifunctor B(A,C):=AkHomR(k,C) to Vectkfd.

[L1]

With supplied projective and injective data, one may derive an additive bifunctor in either variable and thereby obtain two candidate constructions (A bifunctor can be derived in either variable when the relevant resolution data are supplied).

[L2]

A balanced derived bifunctor relative to the supplied data requires extra natural isomorphisms, natural in both variables and normalized by the degree-zero identifications (A balanced derived bifunctor).

Refutation

technique · direct
1.1

The functor AA is exact on finite-dimensional vector spaces, CHomR(k,C) is left exact, and tensoring over k is exact. Hence B is additive and left exact in each variable in the sense required by [L1]. Give kA its length-zero projective resolution. The first-variable right-derived object at (k,k) is then zero in every positive degree.

L1givenconstructalgebra
1.2

The R-module R is injective: the coefficient-of-ε functional identifies R with Homk(R,k) as an R-module, and HomR(,Homk(R,k))Homk(,k) is exact. Thus 0k1εRεRεR is an injective resolution of k: at every copy of R, both the image and kernel of multiplication by ε are the ideal (ε).

givenconstructalgebra
2.1

Applying B(k,)=HomR(k,) to the deleted resolution in step 1.2 gives a cochain complex with one copy of k in every degree and zero differentials, since multiplication by ε annihilates HomR(k,R)(ε). Consequently the second-variable right-derived object in degree 1 is k, whereas the first-variable object from step 1.1 is 0. They cannot be isomorphic, so the balance data required by [L2] do not exist and the displayed automatic-balance claim is false.

L1L2step 1.1step 1.2algebra
False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

FALSE: an acyclic resolution is the same thing as an injective resolution

Statement

An acyclic resolution is the same thing as an injective resolution.

Facts & Assumptions

Given: The identity functor on abelian groups, a supplied projective resolution datum P on a class containing the free abelian groups, and the standard free resolution 0Z×2ZZ/2Z0.

[L1]

An F-acyclic resolution only requires a correctly oriented exact resolution by F-acyclic objects (An F-acyclic resolution).

[L2]

Exact functors have vanishing positive derived functors on every object, so every object is acyclic for the identity functor (An exact functor has vanishing positive derived functors).

[L3]

Injective objects are characterized by an extension property across monomorphisms (Injective object).

Refutation

technique · direct
1.1

The identity functor is exact, so [L2] makes every object in the domain of P Id-acyclic. The terms of the displayed free resolution are free abelian groups, hence lie in that domain. Therefore [L1] identifies the displayed free resolution of Z/2 as an Id-acyclic resolution relative to P.

L1L2given
2.1

The term Z in that resolution is not injective: the inclusion 2ZZ and the map 2nn into Z admit no extension ZZ. Thus [L3] fails. So an F-acyclic resolution need not be an injective resolution, and the displayed claim is false.

L3step 1.1algebra

Sources