LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-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.

The highest positive homology of a depth-bounded finite complex has positive depth

Statement

Assume the Axiom of Choice. Let $(R, m)$ be a Noetherian local ring and $F_{∙} : 0 \to F_{e} \to F_{e - 1} \to \dots \to F_{0}$ a complex of finite $R$ -modules with ${depth}_{R} F_{j} \geq j$ for every $j$ . If $i > 0$ is the largest index with $H_{i} (F_{∙}) \neq 0$ , then ${depth}_{R} H_{i} (F_{∙}) \geq 1$ . In particular a nonzero finite-length module cannot be the highest positive homology of such a complex.

Facts & Assumptions

Given: The local ring, finite complex, depth bounds, and largest positive homology index.

[F1]

For a short exact sequence $0 \to A \to B \to C \to 0$ of finite modules over a Noetherian local ring, the depth lemma gives $depth C \geq \min (depth A - 1, depth B)$ and $depth A \geq \min (depth B, depth C + 1)$ (The three Depth Lemma inequalities).

[F2]

The zero module has infinite depth. Every nonzero finite-length module has depth zero, since its maximal ideal has a nonzero annihilated element (Depth with respect to an ideal).

Proof

technique · move downward through the exact top of the complex using the depth lemma, then compare boundaries, cycles, and homology at index $i$

1.1F1

Write $B_{j} = im (F_{j + 1} \to F_{j})$ and $Z_{j} = \ker (F_{j} \to F_{j - 1})$ , with $B_{e} = 0$ . All are finite because $R$ is Noetherian. Since $i$ is the highest nonexact positive index, $Z_{j} = B_{j}$ for every $j > i$ . The exact top provides short sequences $0 \to B_{j} \to F_{j} \to B_{j - 1} \to 0$ for $j = e, e - 1, \dots, i + 1$ , where $B_{e} = 0$ .

2.1F1F2step 1.1

If $i = e$ , then $B_{i} = B_{e} = 0$ has infinite depth, so $depth B_{i} \geq i + 1$ directly. Suppose $i < e$ . The top sequence of step 1.1 gives $B_{e - 1} ≅ F_{e}$ , of depth at least $e$ . Descend along the remaining sequences: if $depth B_{j} \geq j + 1$ , [F1] applied to $0 \to B_{j} \to F_{j} \to B_{j - 1} \to 0$ gives $depth B_{j - 1} \geq \min (j, depth F_{j}) \geq j$ . Thus also in this case $depth B_{i} \geq i + 1$ .

3.1F1F2step 2.1

The exact sequence $0 \to Z_{i} \to F_{i} \to B_{i - 1} \to 0$ and [F1] give $depth Z_{i} \geq \min (depth F_{i}, depth B_{i - 1} + 1) \geq 1$ , since $i > 0$ and every finite module has nonnegative depth (with infinite depth for zero). The sequence $0 \to B_{i} \to Z_{i} \to H_{i} \to 0$ and [F1], together with step 2.1, give $depth H_{i} \geq \min (depth B_{i} - 1, depth Z_{i}) \geq 1$ .

4.1F1F2step 3.1∎

A nonzero finite-length module has depth zero by [F2], so it cannot equal $H_{i}$ . AC enters through the published depth lemma; no further infinite choice is needed.

Depends on

Used by

Expected ranks and determinantal regular sequences force a free complex to be exact Lemma

Dependency tree · two levels

8 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, Algebra, Lemma 10.102.8 (tag 00N0), acyclicity lemma (standard reference, not scraped)