Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-13
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.

Hypercohomology edge maps are canonical

Statement

In the setting and comparison-data conventions of the two hypercohomology spectral sequences, suppose Kq=0 for q<b and nb. Write RnF(K) for the relative target. The first sequence has canonical edge maps Hn(FK)RnF(K)ker(RnbF(Kb)RnbF(Kb+1)). The second has canonical edge maps RnbF(HbK)RnF(K)F(HnK). They are the augmentation, inclusion and projection maps described in the proof, after the indicated degree translation. No map is asserted to split, be monic, or be epic beyond the associated filtration maps.

Facts & Assumptions

Given: F,K,I,b,n as in the statement, with the comparison qualifications of the two spectral-sequence theorems.

[F1]

The first sequence has E1p,q=RqF(Kp), support q0, pb, and differentials of bidegree (r,1r) (First hypercohomology spectral sequence).

[F2]

The second sequence has E2p,q=RpF(HqK) with the filtration by resolution degree (Second hypercohomology spectral sequence).

[F3]

A cohomological edge is the extremal graded inclusion or quotient followed by the finite transition maps (Edge homomorphisms of a first quadrant spectral sequence).

Proof

1.1

Let hp:Ip,Ip+1, be the horizontal Cartan–Eilenberg map. Compatibility with the augmentations says that hp lifts dKp, so its map on vertical cohomology is the relative derived map RqF(dKp). Since d1 is induced by this horizontal map, d1=RqF(dK). For q=0, left exactness identifies F(Kp) with ker(F(Ip,0)F(Ip,1)), and this identification carries d1 to F(dK). The augmentations therefore give a cochain map FKTot(FI). On a degree-n cycle its image lies in the extremal column n and has no positive-resolution component. In the column filtration this is exactly the representative of the bottom-row edge from E2n,0=Hn(FK), with the finite transition quotients killing precisely the later boundaries. Thus the induced cohomology map is that edge.

F1F3
1.2

In the second sequence, Bb,p=0 and therefore Hb,p=Zb,pIb,p. Inclusion of these horizontal cycles gives a cochain map from their vertical resolution after F, placed starting in total degree b, into the total complex. Its cohomology map is RnbF(HbK)RnF(K), using the constant sign (1)b on the vertical differential. These are the bottom-row representatives for the resolution-degree filtration, so this is its lower edge.

F2F3
2.1

Projection of the total complex onto column b gives a cochain map to that column with its signed differential and original degree placement. The total cocycle equation in column b+1 says the horizontal image of the projected vertical class is zero. By the d1 calculation in step 1.1, the cohomology map therefore lands in ker(RnbF(Kb)RnbF(Kb+1)), which is the left-axis E2 term because there is no preceding column. Projection is the quotient by the first positive translated filtration piece, so F3 identifies it with the other first-sequence edge.

F1F3step 1.1
3.1

Projection onto resolution degree zero sends a total cocycle to a horizontal cohomology class in F(Hn,0). Its induced vertical differential is zero by the next component of the total cocycle equation. Left exactness identifies this kernel with F(HnK), since Hn, resolves HnK. Total boundaries give zero under this map. It is the filtration quotient at resolution degree zero and hence the upper edge. The same equations are morphism equalities on cycle and boundary subobjects, so they do not require selected representatives in an abelian category. For n=b both filtrations have one piece and the arrows agree with the bottom augmentation identification; zero targets cause no exception.

F2F3step 1.2

Depends on

Used by

Dependency tree · two levels

9 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