TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31

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.

Shift is an additive autoequivalence of the complex and homotopy categories

Statement

Let $A$ be an abelian category. For each integer $k$ , shift defines an additive autoequivalence $[k] : Ch (A) \to Ch (A)$ and descends to an additive autoequivalence $[k] : K (A) \to K (A) .$ Its inverse is the shift $[- k]$ .

Facts & Assumptions

Given: An abelian category $A$ and an integer $k$ .

[L1]

The shift of a complex is again a chain complex (The shift of a chain complex, The shifted differential squares to zero).

[L2]

Shifted chain maps and shifted homotopies are defined degreewise, with the sign $(- 1)^{k}$ on shifted homotopies (Shifted chain maps and shifted chain homotopies).

[L3]

Morphisms in $K (A)$ are homotopy classes (The homotopy category of chain complexes).

[L4]

Because $A$ is abelian and hence additive, $K (A)$ is additive (The homotopy category is additive).

Proof

technique · direct

1.1

By [L1] and [L2], sending $C$ to $C [k]$ and $f$ to $f [k]$ defines a functor on $Ch (A)$ . The formulas are degreewise, so $[k]$ preserves zero maps and sums, and applying $[- k]$ returns the original complex and map on the nose. Hence $[k]$ is an additive autoequivalence of $Ch (A)$ .

L1L2givenalgebra

2.1

If $f ≃ g$ , then [L2] gives $f [k] ≃ g [k]$ , so [L3] lets the same formula descend to homotopy classes. Since step 1.1 already gives the inverse $[- k]$ and [L4] provides the additive structure on the quotient, $[k]$ is also an additive autoequivalence of $K (A)$ .

L2L3L4step 1.1algebra∎

Depends on

Used by

Shift preserves homotopy equivalences, contractibility, and quasi-isomorphisms Proposition

Dependency tree · two levels

13 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, Chapter 1 of An Introduction to Homological Algebra (standard reference, not scraped)
The Stacks Project, Section 12.14: Homotopy and the shift functor (standard reference, not scraped)