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.

Euler-Poincare for a finite complex

Example

Consider the split exact three-term complex $0 \to Z \overset{i}{\to} Z \oplus Z \overset{p}{\to} Z \to 0,$ with $i (a) = (a, 0)$ and $p (a, b) = b$ . Then $χ (C) = 1 - 2 + 1 = 0 = \sum_{n} (- 1)^{n} rank (H_{n} (C)) .$

Facts & Assumptions

Given: The split exact complex just displayed.

[L1]

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

[L2]

The Euler-Poincare formula holds for bounded complexes of finite-rank free abelian groups with finite-rank free homology (Euler-Poincare formula for finite free complexes).

Verification

technique · direct

1.1L1givenalgebra

The complex is split exact, hence acyclic, so every homology group is zero. Its chain groups have ranks $1$ , $2$ , and $1$ . Therefore $χ (C) = 1 - 2 + 1 = 0,$ while the alternating sum of homology ranks is also $0$ .

2.1L2step 1.1∎

This agrees with the theorem [L2], so the example is a direct Euler-Poincare computation in a finite free complex.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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

P. Hekmati, Homological Algebra, section 3.1 (standard reference, not scraped)