LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01

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.

Extending a partial comparison map by one degree

Statement

Let $u : A \to B$ be a morphism, and let $P_{∙} \to A$ and $Q_{∙} \to B$ be projective resolutions. Suppose morphisms $f_{0}, \dots, f_{n}$ have already been chosen so that the augmentation condition holds and the chain-map squares commute through degree $n$ . Then there exists $f_{n + 1} : P_{n + 1} \to Q_{n + 1}$ making the next square commute as well.

Facts & Assumptions

Given: Projective resolutions $P_{∙} \to A$ and $Q_{∙} \to B$ , a morphism $u : A \to B$ , and a partial comparison map through degree $n$ .

[L1]

A projective resolution is exact, so at degree $n$ its cycle object is the image of the next differential (Projective resolutions in an abelian category).

[L2]

The $n$ th cycle object is the kernel of the degree- $n$ differential (Cycle and boundary subobjects of a complex).

[L3]

Projective objects lift across epimorphisms (Projective object).

Proof

technique · direct

1.1L1L2givenalgebra

If $n = 0$ , the augmentation identity gives $ε_{Q} f_{0} d_{1}^{P} = u ε_{P} d_{1}^{P} = 0,$ so $f_{0} d_{1}^{P}$ lands in $\ker (ε_{Q}) = Z_{0} (Q)$ . If $n > 0$ , the previous squares commute and $d_{n}^{Q} f_{n} d_{n + 1}^{P} = f_{n - 1} d_{n}^{P} d_{n + 1}^{P} = 0,$ so again $f_{n} d_{n + 1}^{P}$ lands in $Z_{n} (Q) = \ker (d_{n}^{Q})$ by [L2]. Exactness of $Q_{∙}$ at degree $n$ makes the canonical map $Q_{n + 1} ↠ Z_{n} (Q)$ epic by [L1].

2.1L3step 1.1construct∎

The object $P_{n + 1}$ is projective, so [L3] lifts $f_{n} d_{n + 1}^{P} : P_{n + 1} \to Z_{n} (Q)$ across the epimorphism $Q_{n + 1} ↠ Z_{n} (Q)$ . Writing the lift as $f_{n + 1}$ gives $d_{n + 1}^{Q} f_{n + 1} = f_{n} d_{n + 1}^{P},$ so the partial comparison map extends by one degree.

Extending a partial comparison map by one degree

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources