Alphabeta Math
PropositionStatement: 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.

A map of exact couples induces a map of spectral sequences

Statement

A morphism of graded exact couples induces a morphism of their derived exact couples and therefore a morphism of their spectral sequences, preserving every bidegree and page transition. This construction respects identities and composition.

Facts & Assumptions

[F1]

Exact couple defines bidegree-zero pairs (u,v) commuting with i,j,k. Derived exact couple gives D′=im⁡i, E′=H(E,jk) and the formulas i′(a)=ia, j′(ix)=[jx], k′[e]=ke.

[F2]

An exact couple generates a spectral sequence iterates this derivation with its specified homology transitions.

[F3]

Morphism of spectral sequences requires differential and homology-transition commutation.

[F4]

Spectral sequence subquotient and local lifting calculus permits local epic lifts, image restrictions and unique quotient descent.

Proof

Given: A map (u,v):(D,E,i,j,k)→(D~,E~,i~,j~,k~) of page-r exact couples. Tildes denote the target structure throughout.

1.1F1F4

Since ui=i~u, the component of u at (p,q) sends Dp,q′=im⁡ip−1,q+1 into D~p,q′, giving a restriction u′. Also vjk=j~uk=j~k~v, so v commutes with the page differential, sends cycles to cycles and boundaries to boundaries, and induces v′:Ep,q′→E~p,q′. Both maps preserve the bidegree.

2.1F1F4step 1.1

For a∈Dp,q′, the equality u′i′a=u(ia)=i~(ua)=i~′u′a proves the derived i square. Locally write a=ix, where x has bidegree (p−1,q+1). Then v′j′a=[vjx]=[j~ux]=j~′(i~ux)=j~′u′a, at bidegree (p−r,q+r). The formula is independent of the local lift by the already defined derived maps, and equality descends by epic cancellation. For a cycle e∈Ep,q, u′k′[e]=uke=k~ve=k~′v′[e], with target D~p−1,q′. Quotient descent proves this last equality on all of E′. These are every derived-couple commutation square with its required degrees.

3.1F2F3F4step 1.1step 2.1∎

Repeat steps 1.1–2.1 at each derived couple. On its E terms the next map is precisely the map induced on homology by the current v map. Thus the maps commute with every differential and with each transition in [F2], as required by [F3]. Image restrictions of identity maps are identities; quotient maps induced by identities are identities. Restrictions and quotient descents of a composite agree with composites of the restrictions and descents by their uniqueness. This proves identity and composition compatibility at every finite stage. Zero images, zero homology quotients and the initial r=1 case all use the same formulas; the latter sends the derived j to degree (−1,1) as required. No global lifts or AC are used.

Remarks

The three squares below display the derived-couple compatibility proved in step 2.1. Nodes denote indexed families, not direct sums: the horizontal maps have bidegrees (1,−1), (−r,r) and (−1,0), respectively, while all vertical maps have bidegree (0,0). Thus each square is read componentwise with the indicated shift in its right-hand column.

D0D0D0E0E0D0eD0eD0eD0eE0eE0eD0i0u0u0j0u0v0k0v0u0ei0ej0ek0

At every page s, let vs:Es→E~s be the induced map. Since it commutes with the differentials, its homology map fits into the transition square below, where the horizontal arrows are the specified homology-to-next-page isomorphisms. This is the repeated quotient descent in step 3.1; neither diagram replaces the proof.

H(Es;ds)Es+1H(eEs;eds)eEs+1®sH(vs)vs+1e®s

Depends on

Used by

Dependency tree · two levels

14 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