TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

A bounded below complex of injectives is homotopically injective

Statement

A bounded-below cochain complex $I$ of injective objects is K-injective. Assume dependent choice for the countable successive homotopy extensions, or supply those extensions as data.

Facts & Assumptions

Given: A bounded-below cochain complex $I$ of injective objects is K-injective. Assume dependent choice for the countable successive homotopy extensions, or supply those extensions as data.

[F1]

An injective object extends maps from a subobject to the ambient object (Injective object).

[F2]

K-injectivity is vanishing of Hom from every acyclic complex into every shift of the target (Homotopically injective bounded below complex).

[F3]

DC supplies a sequence extending successive choices on a nonempty set (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

Proof

1.1

Let $A$ be acyclic and $f : A \to I$ a chain map. Choose $a$ with $I^{n} = 0$ for $n < a$ and set $h^{n} : A^{n} \to I^{n - 1}$ equal to zero for $n \leq a$ . The equation $f^{n} = d_{I} h^{n} + h^{n + 1} d_{A}$ holds below $a$ . In particular it is valid for zero complexes.

givenalgebra

2.1

If the equation holds below $n$ , then $u^{n} = f^{n} - d_{I}^{n - 1} h^{n}$ vanishes on $im d_{A}^{n - 1}$ by the chain-map identity. Since $A$ is acyclic this image equals $\ker d_{A}^{n}$ , so $u^{n}$ factors through $im d_{A}^{n} ↪ A^{n + 1}$ . Injectivity of $I^{n}$ extends it to $h^{n + 1} : A^{n + 1} \to I^{n}$ . This establishes the equation in degree $n$ .

F1step 1.1algebra

3.1

Apply DC to the set of finite partial homotopies with the entire extension relation, or take the supplied successive extensions. The resulting homotopy makes $f$ zero in $K$ . Apply the same argument to every shift $I [r]$ , which remains bounded below and termwise injective. This is the K-injective condition.

F2F3step 2.1∎

Depends on

Used by

Ext is hom in the derived category Theorem
Injective complexes model the bounded below derived category Theorem

Dependency tree · two levels

10 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

13.18.3–13.18.8; W 10.4.8 for the equivalence (standard reference, not scraped)