Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass
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 row filtration spectral sequence of a first quadrant double complex

Statement

For a first-quadrant homological double complex C, the row filtration of T=Tot⁡(C) has a spectral sequence with Ep,q1=Hqh(C∗,p),d1 induced by v,Ep,q2=Hpv(Hqh(C)). The differential on page r has bidegree (−r,r−1), and the stationary page identifies canonically with Ep,q∞≅FprowHp+q(T)/Fp−1rowHp+q(T),FprowHn(T)=im⁡(Hn(FprowT)→Hn(T)). This target filtration is finite in each total degree. Horizontal homology is taken first; the spectral first coordinate is the original vertical index.

Facts & Assumptions

[F1]

Row and column filtrations of a first quadrant double complex gives the finite row cutoff and associated graded Cq,p with differential h.

[F2]

The next page is the homology of the current page gives the natural page transition H(Er,dr)≅Er+1.

[F3]

The filtered differential induces d r on the r page gives bidegree (−r,r−1) and the local rule [x]↦[dx].

[F4]

Spectral sequence subquotient and local lifting calculus licenses local representatives after epic pullback and descent of maps preserving numerator and denominator.

[F5]

Bounded filtered complex spectral sequence abuts to filtered homology proves natural abutment for degreewise finite filtrations; Induced filtration on homology specifies the image filtration.

Proof

Given: C as stated, with hv+vh=0 and h2=v2=0.

1.1F1given

The row-p quotient of total degree p+q is Cq,p. The arrow h stays in this row and v enters the preceding row, which is zero in the quotient. Thus Ep,q0=Cq,p and d0=h. This remains valid when either index is negative, as the component is then zero.

2.1F2F3F4step 1.1given

Taking homology gives Ep,q1=Hqh(C∗,p). A horizontal cycle x has total differential dx=vx, so the page-one rule gives d1[x]=[vx]. This is a well-defined horizontal homology class: h(vx)=−v(hx)=0, and if x changes by hy then vx changes by vhy=−hvy, a horizontal boundary. In an abelian category these calculations mean preservation of kernel and image subobjects; they may be checked after epic pullback and descend uniquely. No global representatives are selected.

3.1F2F3step 2.1given

Since v2=0, the induced page-one arrows square to zero, and their homology is precisely Hpv(Hqh(C)). The next-page isomorphism therefore gives the displayed E2. Both E0 and all later subquotients vanish off the first quadrant. The differential bidegrees are those of the filtered construction, (−r,r−1), with no extra sign in d1 because h+v was already the total differential.

4.1F1F5step 3.1∎

In degree n≥0, F−1rowTn=0 and FnrowTn=Tn; negative degrees are zero. Thus the bounded-filtration theorem applies degree by degree to this spectral sequence and identifies its stationary page with the associated graded of the displayed image filtration. That filtration is zero at p=−1 and all of Hn(T) at p=n for n≥0. For n=0 there is only one possible quotient, and for the zero complex all pages and quotients are zero. The argument uses no infinite exactness or AC.

Remarks

In this low-degree part of the first-quadrant grid, the original horizontal index increases to the right and the original vertical index increases upward. Every square anticommutes: hv=−vh; the squares are not asserted to commute.

C0;2C1;2C2;2C0;1C1;1C2;1C0;0C1;0C2;0vhvhvvhvhvhh

The grid continues upward and to the right; components with a negative index are zero. The cutoff F1rowT retains rows 0 and 1, and its quotient by F0rowT retains only row 1. More generally the row-p quotient has Ep,q0=Cq,p and differential h. Taking horizontal homology turns the downward arrows into the following part of the page-one chain, for any fixed q≥0:

E12;q=Hhq(C¤;2)E11;q=Hhq(C¤;1)E10;q=Hhq(C¤;0)d1=v¤d1=v¤

Here v∗[x]=[vx], with no additional sign because the total differential is h+v. Thus d1 has bidegree (−1,0) in spectral coordinates, and the chain continues upward, and its homology at index p is Ep,q2=Hpv(Hqh(C)). These diagrams illustrate the filtration and page calculation; the proof above is independent of them.

Depends on

Used by

Dependency tree · two levels

24 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