TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-09-24

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.

Chain-homotopic maps induce the same map on homology

Statement

If $f, g : C_{∙} \to D_{∙}$ are chain-homotopic chain maps, then for every $n \in Z$ , $H_{n} (f) = H_{n} (g) : H_{n} (C) \to H_{n} (D) .$

Facts & Assumptions

Given: A chain homotopy $s : f ≃ g$ and an integer $n$ .

[L1]

A chain homotopy satisfies $f_{n} - g_{n} = d_{n + 1}^{D} s_{n} + s_{n - 1} d_{n}^{C}$ (A chain homotopy).

[L2]

The cycle inclusion $k_{C} : Z_{n} (C) \to C_{n}$ is the kernel of $d_{n}^{C}$ , hence $d_{n}^{C} k_{C} = 0$ . The boundary inclusion $B_{n} (D) \to D_{n}$ is the image of $d_{n + 1}^{D}$ (Cycle and boundary subobjects of a complex).

[L3]

The boundary inclusion factors through the cycle inclusion $k_{D} : Z_{n} (D) \to D_{n}$ . Thus there are arrows $e_{D} : D_{n + 1} \to B_{n} (D)$ and $β_{D} : B_{n} (D) \to Z_{n} (D)$ with $d_{n + 1}^{D} = k_{D} β_{D} e_{D}$ (The boundary subobject factors through the cycle subobject).

[L4]

The homology quotients $q_{C} : Z_{n} (C) \to H_{n} (C)$ and $q_{D} : Z_{n} (D) \to H_{n} (D)$ are cokernels of the respective boundary-to-cycle maps; in particular $q_{D} β_{D} = 0$ (Homology object of a chain complex).

[L5]

For a chain map $u : C_{∙} \to D_{∙}$ , its cycle map satisfies $k_{D} Z_{n} (u) = u_{n} k_{C}$ (A chain map carries cycles to cycles and boundaries to boundaries), and its induced homology map is characterized by $H_{n} (u) q_{C} = q_{D} Z_{n} (u)$ (A chain map induces a well-defined map on homology).

[L6]

A cokernel is a coequalizer and therefore an epimorphism: two arrows agreeing after precomposition with $q_{C}$ are equal (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

Proof

technique · direct

1.1L1L2L3L5givenalgebra

Restrict the homotopy identity [L1] along $k_{C}$ . Since $d_{n}^{C} k_{C} = 0$ by [L2], $(f_{n} - g_{n}) k_{C} = d_{n + 1}^{D} s_{n} k_{C} = k_{D} β_{D} e_{D} s_{n} k_{C} .$ By [L5], the left side is $k_{D} (Z_{n} (f) - Z_{n} (g))$ . The kernel inclusion $k_{D}$ is monic, so $Z_{n} (f) - Z_{n} (g) = β_{D} e_{D} s_{n} k_{C} .$

2.1L4L5L6step 1.1algebra∎

Apply $q_{D}$ to the equality in step 1.1. Since $q_{D} β_{D} = 0$ by [L4], $q_{D} (Z_{n} (f) - Z_{n} (g)) = 0.$ By [L5], this is $(H_{n} (f) - H_{n} (g)) q_{C} = 0$ . The cokernel map $q_{C}$ is epic by [L6], so $H_{n} (f) = H_{n} (g)$ for every $n$ .

Depends on

Used by

Dependency tree · two levels

16 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)
Joseph J. Rotman, An Introduction to Homological Algebra, 2nd ed. (standard reference, not scraped)