ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-30

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 chain map computed on cycles, boundaries, and homology

Example

Let $C_{∙}$ be the two-term complex $0 \to Z \overset{\times 2}{\to} Z \to 0,$ and let $D_{∙}$ be $0 \to Z \overset{\times 4}{\to} Z \to 0.$ The maps $f_{1} = 1_{Z}$ and $f_{0} = \times 2$ define a chain map $f : C \to D$ . It induces the zero map on $H_{1}$ and the inclusion $Z / 2 Z \to Z / 4 Z, \overset{ˉ}{x} \mapsto \overline{2 x},$ on $H_{0}$ .

Facts & Assumptions

Given: The complexes $C_{∙}, D_{∙}$ and the family $f_{1} = 1_{Z}$ , $f_{0} = \times 2$ .

[L1]

$A b$ is an abelian category (Abelian groups form an abelian category).

[L2]

A chain map induces a well-defined homology map (A chain map induces a well-defined map on homology).

Verification

technique · direct

1.1L1givenalgebra

The chain condition holds because $(\times 4) \circ 1_{Z} = (\times 2) \circ (\times 2)$ . Also $Z_{1} (C) = Z_{1} (D) = 0$ , $B_{0} (C) = 2 Z$ , and $B_{0} (D) = 4 Z$ . Hence $H_{1} (C) = H_{1} (D) = 0$ , $H_{0} (C) ≅ Z / 2 Z$ , and $H_{0} (D) ≅ Z / 4 Z$ .

2.1L2step 1.1∎

By [L2], the induced homology map comes from the degree- $0$ map $f_{0} = \times 2$ on cycles. It sends the boundary subgroup $2 Z$ into $4 Z$ , so on quotients it is $\overset{ˉ}{x} ⟼ \overline{2 x} .$ In degree $1$ the homology groups are zero, so the induced map there is zero.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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)