LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-27

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.

Lifting a morphism from an exact complex into an injective resolution

Statement

Assume the Axiom of Dependent Choice. Let $0 \to A \overset{η}{\to} J^{0} \overset{d^{0}}{\to} J^{1} \overset{d^{1}}{\to} \dots$ be a coaugmented cochain complex in an abelian category that is exact at every displayed term, and let $0 \to B \overset{η^{'}}{\to} I^{0} \overset{δ^{0}}{\to} I^{1} \overset{δ^{1}}{\to} \dots$ be a coaugmented cochain complex whose terms $I^{n}$ are all injective (Injective object, Cochain complex in an abelian category).

Then for every morphism $u : A \to B$ there is a coaugmentation-preserving cochain map $φ^{∙} : J^{∙} \to I^{∙}$ , that is $φ^{0} \circ η = η^{'} \circ u$ and $δ^{n} \circ φ^{n} = φ^{n + 1} \circ d^{n}$ for all $n \geq 0$ (Chain map, A graded morphism of chain complexes); and any two such cochain maps are cochain-homotopic (A chain homotopy).

Facts & Assumptions

[F1]

An object $I$ is injective when every morphism $M \to I$ out of a subobject extends over the inclusion $M ↣ E$ (Injective object).

[F2]

In an abelian category, the canonical map $coim (d) = coker (\ker d) \to im (d)$ is an isomorphism. Consequently, if $g$ vanishes on $\ker d$ , the cokernel universal property factors $g$ uniquely through $coim (d)$ and hence through $im (d)$ (Abelian category).

[F3]

A cochain map is a family of morphisms commuting with the differentials, and a cochain homotopy $s : f ≃ g$ satisfies $f^{n} - g^{n} = δ^{n - 1} s^{n} + s^{n + 1} d^{n}$ in the cochain indexing (Chain map, A chain homotopy, Cochain complex in an abelian category).

[F4]

In ZF, AC implies DC (AC implies DC implies countable choice).

Proof

Given: The Axiom of Dependent Choice, the two coaugmented complexes, and a morphism $u : A \to B$ .

1.1

By exactness at $A$ the map $η : A \to J^{0}$ has zero kernel, so it is a monomorphism; the composite $η^{'} \circ u : A \to I^{0}$ is a morphism out of that subobject into the injective object $I^{0}$ , so by [F1] there is $φ^{0} : J^{0} \to I^{0}$ with $φ^{0} \circ η = η^{'} \circ u$ . This starts a recursion in degree $0$ .

F1construct

2.1

Suppose $φ^{n} : J^{n} \to I^{n}$ has been constructed with $δ^{n - 1} φ^{n - 1} = φ^{n} d^{n - 1}$ for $n \geq 1$ (for $n = 0$ take the coaugmentation identity of step 1.1). The composite $g : = δ^{n} \circ φ^{n} : J^{n} \to I^{n + 1}$ kills the kernel of $d^{n}$ , which by exactness at $J^{n}$ is the image of $d^{n - 1}$ ; hence $g$ factors as $J^{n} ↠ im (d^{n}) \overset{\overset{ˉ}{g}}{\to} I^{n + 1}$ through the image of $d^{n}$ by [F2]. By exactness at $J^{n + 1}$ the image of $d^{n}$ is the kernel of $d^{n + 1}$ , so the inclusion $im (d^{n}) ↣ J^{n + 1}$ is a monomorphism; since $I^{n + 1}$ is injective, [F1] extends $\overset{ˉ}{g}$ to $φ^{n + 1} : J^{n + 1} \to I^{n + 1}$ , and $φ^{n + 1} \circ d^{n} = g = δ^{n} \circ φ^{n}$ because both sides agree on the quotient $J^{n} ↠ im (d^{n})$ . [F1, F2, step 1.1, construct]

F1F2construct

3.1

By step 2.1 one may choose an extension $φ^{n + 1}$ for every $n \geq 0$ ; the recursion produces a coaugmentation-preserving cochain map $φ^{∙}$ , since the identities of step 1.1 and step 2.1 are exactly $φ^{0} η = η^{'} u$ and $δ^{n} φ^{n} = φ^{n + 1} d^{n}$ . The construction makes one choice of extension in each degree $n \in N$ , and the assumed DC, also implied by AC via [F4], ensures that an infinite sequence of nonempty choices of this recursive shape exists; hence the lift exists. [F3, F4, step 2.1]

F3F4

4.1

For the uniqueness, let $φ^{∙}, ψ^{∙} : J^{∙} \to I^{∙}$ be coaugmentation-preserving cochain maps and put $h^{n} : = φ^{n} - ψ^{n}$ , so that $h$ is a cochain map with $h^{0} \circ η = 0$ . I claim inductively that there are morphisms $s^{n} : J^{n} \to I^{n - 1}$ for $n \geq 1$ , with $s^{n} = 0$ for $n \leq 0$ , satisfying $h^{n} = δ^{n - 1} s^{n} + s^{n + 1} d^{n}$ : for $n = 0$ this says $h^{0} = s^{1} d^{0}$ , and since $h^{0}$ kills the kernel of $d^{0}$ (which equals the image of $η$ ) it factors through the image of $d^{0}$ by [F2], and that factorization extends to $J^{1} \to I^{0}$ by injectivity of $I^{0}$ [F1]; given $s^{n}$ , one computes that $h^{n} - δ^{n - 1} s^{n}$ kills the image of $d^{n - 1}$ (using the displayed identity in degree $n - 1$ and the cochain identity for $h$ ), hence factors through the image of $d^{n}$ , and again [F1] extends it over the inclusion $im (d^{n}) ↣ J^{n + 1}$ , giving $s^{n + 1}$ . [F1, F2, F3, step 3.1]

F1F2F3

5.1

The homotopy identities produced in step 4.1 require one choice in each degree, which the assumed DC provides; the sequence $s^{n}$ is a cochain homotopy from $φ^{∙}$ to $ψ^{∙}$ in the sense of [F3], so any two coaugmentation-preserving lifts are cochain-homotopic. [F3, F4, step 4.1] ∎

F3F4∎

Depends on

Used by

Dependency tree · two levels

24 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

The Stacks Project, Derived Categories, Section 13.18: Injective resolutions (tags 013P, 013R) (standard reference, not scraped)