TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)

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 first quadrant filtered complex spectral sequence converges to filtered homology

Statement

An exhaustive first-quadrant filtered chain complex in an abelian category, with finite filtration on each chain object, has a pointwise stationary spectral sequence strongly converging to its homology with the induced finite image filtration. No uniform bound over all chain degrees is required. In the normalized case $F_{- 1} C = 0$ and $F_{n} C_{n} = C_{n}$ , one has $F_{- 1} H_{n} (C) = 0$ and $F_{n} H_{n} (C) = H_{n} (C)$ .

Facts & Assumptions

[F1]

Bounded filtered complex spectral sequence abuts to filtered homology proves pointwise stabilization, natural actual-cycle graded identifications and finiteness of the homology image filtration for a degreewise finite filtration.

[F2]

Induced filtration on homology defines that filtration as the image of $H_{n} (F_{p} C) \to H_{n} (C)$ .

[F3]

Strong convergence of a spectral sequence requires the weak identifications, two-sided regularity, exhaustiveness, separatedness and completeness; it specifies the inverse-system orientation and proves the constant-tail limit description.

Proof

Given: Such a filtered complex $(C, d, F)$ . Fix a degree $n$ .

1.1

Choose finite endpoints $a_{j}, b_{j}$ in each of the three degrees $j = n - 1, n, n + 1$ . The hypothesis of [F1] holds degreewise. Its proof identifies the stationary page with the quotient of $F_{p} C_{n} \cap \ker d_{n}$ by $(F_{p - 1} C_{n} \cap \ker d_{n}) + (F_{p} C_{n} \cap im d_{n + 1})$ : the lower endpoint in degree $n - 1$ makes approximate cycles actual cycles, and the upper endpoint in degree $n + 1$ includes all actual boundaries. Thus its graded isomorphisms have exactly the actual-cycle meaning required for weak convergence, and are natural in filtered chain maps. The same theorem gives eventual vanishing of both incident differentials, hence two-sided regularity.

F1F3

1.2

The image filtration satisfies $F_{p} H_{n} (C) = 0$ for $p \leq a_{n}$ , since there are no degree- $n$ cycles in $F_{p} C$ . It satisfies $F_{p} H_{n} (C) = H_{n} (C)$ for $p \geq b_{n}$ , since every cycle of $C_{n}$ is then a cycle in $F_{p} C$ . Images, not the possibly larger domain homology groups, are being used. The filtration is therefore finite, and its meet is zero and its join is $H_{n} (C)$ . This proves separatedness and exhaustiveness, including when $H_{n} (C) = 0$ .

F1F2

2.1

For $p \leq a_{n}$ the quotients $H_{n} (C) / F_{p} H_{n} (C)$ are canonically $H_{n} (C)$ and their transitions are identities. A compatible cone into the full inverse system is uniquely determined by its component at $a_{n}$ : compatibility fixes every smaller-index component and every larger-index component is its quotient. Consequently $H_{n} (C)$ with the quotient maps satisfies the limit universal property, and the canonical completion map is an isomorphism. All the conditions in [F3] now hold. No general existence of infinite limits or choice of a family of representatives is required.

F3step 1.1step 1.2

3.1

Under the normalized hypotheses, the zero subcomplex $F_{- 1} C$ has zero homology, giving $F_{- 1} H_{n} (C) = 0$ . Every degree- $n$ cycle lies in $F_{n} C_{n} = C_{n}$ , so the inclusion $F_{n} C \to C$ is surjective on degree- $n$ homology, giving the other endpoint. The statements also hold for zero chain degrees, repeated filtration terms and the boundary axis of the first quadrant. The proof above fixed $n$ and used finitely many integer bounds, so it introduces no uniform-degree bound or AC assumption.

F2step 1.2∎

Source notes

Stacks, Lemma 12.24.11, with increasing homological indices. The local bounded supplier gives the full numerator proof; the constant-tail argument supplies completeness in the stated strong-convergence convention.

Depends on

Strong convergence of a spectral sequence

Used by

Quasi isomorphism criterion from a filtered map Corollary

Dependency tree · two levels

4 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

Weibel, An Introduction to Homological Algebra, Chapter 5 (standard reference, not scraped)
The Stacks Project, Homological Algebra (standard reference, not scraped)