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

Cartan–Eilenberg comparisons preserve both filtrations

Statement

Let f:KL be a map of bounded-below complexes, and let I,J be supplied Cartan–Eilenberg injective resolutions, in the commuting convention. Assume DC or supply the countable splittings and extensions used below. There is a bicomplex map a:IJ over f. Any two such maps a,a differ by vJs+svI for maps sp,q:Ip,qJp,q1 commuting with h. After any additive functor, comparisons induce the same maps on vertical-first spectral sequences from E1, and on horizontal-first spectral sequences from E2. Identity lifts and composites therefore give canonical resolution-independent spectral sequences from these respective pages.

More generally, the existence and uniqueness of a lift into J hold when the augmented source KI is exact on terms, horizontal boundaries, cycles and cohomology, even if its objects are not injective. The spectral-sequence comparison conclusions hold whenever its filtered totals have the stated pages. Only the target rows need the injective split Cartan–Eilenberg condition.

Facts & Assumptions

Given: The bounded-below data and the DC or supplied-extension qualification above.

[F1]

Cartan–Eilenberg columns resolve terms, cycles, boundaries and cohomology, and the two horizontal short exact sequences split degreewise (Cartan-Eilenberg injective resolution of a bounded-below complex).

[F2]

Maps to an injective object extend across monomorphisms (Injective object).

[F3]

The snake lemma controls kernels and cokernels in a diagram of short exact sequences (Snake lemma in an abelian category).

[F5]

Taking page homology gives the next page naturally (The next page is the homology of the current page).

Proof

1.1

Call a short exact sequence 0XYZ0 of horizontal complexes admissible if the induced sequences on boundaries, cycles and cohomology are also short exact. For such a monomorphism XY, the maps XpYp and Xp/BpXYp/BpY are monic. For the latter assertion, apply the snake lemma to the exact boundary sequences inside the term sequences: an element of Xp mapping into BpY comes from BpX, as a subobject identity. This argument uses kernels and images and holds in an arbitrary abelian category.

F3
1.2

Regard 0KI,0I,1 as a resolution in horizontal complexes. Its successive image complexes CIq fit into admissible sequences 0CIqI,qCIq+10, with CI0=K. To check this assertion, use vertical exactness separately on terms, boundaries, cycles and cohomology in F1, or the explicit exactness assumption for the more general source. No source injectivity or splitting is used in this step. In the diagrams for 0BZH0 and 0ZIB[1]0, the snake lemma identifies the induced cokernels with the next cycle, boundary and cohomology objects. This proves the same assertions for every successive image by induction. The analogous statement holds for J.

F1F3
2.1

Fix a horizontal row J,q. Its split sequences decompose it as the locally finite sum of stalk complexes Hp,q in degree p and two-term disk complexes Bp+1,q1Bp+1,q in degrees p,p+1. At each degree there are only three summands. A cochain map XSp(E) is the same as a map Xp/BpXE. A cochain map XDp(E), with Dp(E) in degrees p,p+1, is the same as a map Xp+1E: the degree-p component is that map composed with dXp. Because each E is injective, these maps extend across the monomorphisms in step 1.1. Assemble the extensions into a map YJ,q. Countably many splittings and extensions are sufficient; take them as supplied or apply DC to finite partial selections in the fixed Hom sets. Thus every row J,q has the extension property for admissible monomorphisms.

F1F2F4step 1.1
3.1

Extend KfLJ,0 across KI,0 by step 2.1. After this extension, vJa0 kills K, so it descends to CI1 and extends across CI1I,1 into J,1. Continue: at stage q, vJaq1 kills the preceding image because vJ2=0, hence descends and extends. Each extension is a horizontal cochain map. These choices yield aq, with vJaq1=aqvI, and therefore a bicomplex map over f. DC applies to finite partial maps in the set of these Hom groups; supplied extensions give the same recursion without choice.

F4step 2.1step 1.2
4.1

For two lifts, put s0=0. At vertical degree zero a0a0 kills K, so it factors through CI1 and extends to s1:I,1J,0. Inductively, aqaqvJsq kills imvIq1: substitution of the preceding homotopy equation and vJ2=0 verifies this equality. It therefore descends to CIq+1 and extends to sq+1 by step 2.1. Thus aa=vJs+svI, with every sq a horizontal cochain map. The same countable-choice accounting applies.

F4step 2.1step 1.2step 3.1
5.1

After an additive functor the equation of step 4.1 remains a vertical homotopy, so the induced maps on vertical cohomology coincide. These are the vertical-first E1 maps. On horizontal cohomology, the same equation gives a homotopy for the induced vertical differential, so its cohomology maps coincide on horizontal-first E2. All subsequent maps agree by natural page transitions. The signed total homotopy is (1)ps on bidegree (p,q): the horizontal mixed terms cancel since s commutes with h, and the vertical terms are vs+sv. It preserves the horizontal-degree filtration and lowers the resolution-degree filtration by one, consistently with the respective starting pages. Applying the result to lifts of identities and composites proves the stated canonicity. Zero rows, zero maps and bottom resolution degree q=0 are included by s0=0.

F5step 3.1step 4.1

Depends on

Used by

Dependency tree · two levels

28 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