PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04

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.

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 : A \to B$ 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) \to T_{∙} (A)$ lifting $1_{A}$ . Then:

$θ_{P, P} = 1_{L_{n}^{P} F}$ for every $n$ .
$θ_{Q, R} \circ θ_{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 $1_{A}$ , so [L2] makes it homotopic to the identity chain map. By [L3], the induced homology map is therefore the identity on $L_{n}^{P} F (A)$ .

L1L2L3given

1.2

For the triple $(P, Q, R)$ , the chain map defining $θ_{Q, R} (A) \circ θ_{P, Q} (A)$ is the composite of two comparison maps $P_{∙} (A) \to Q_{∙} (A) \to R_{∙} (A)$ lifting $1_{A}$ . The chain map defining $θ_{P, R} (A)$ is another comparison map lifting $1_{A}$ . By [L2] they are homotopic, so [L3] gives equality of the induced homology maps: $θ_{Q, R} (A) \circ θ_{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∎

Depends on

Used by

Derived functors are well defined relative to supplied resolution data Remark

Dependency tree · two levels

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