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 be a map of bounded-below complexes, and let 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 over . Any two such maps differ by for maps commuting with . After any additive functor, comparisons induce the same maps on vertical-first spectral sequences from , and on horizontal-first spectral sequences from . 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 hold when the augmented source 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.
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).
Maps to an injective object extend across monomorphisms (Injective object).
The snake lemma controls kernels and cokernels in a diagram of short exact sequences (Snake lemma in an abelian category).
DC supplies countably many successive choices on a set (The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain).
Taking page homology gives the next page naturally (The next page is the homology of the current page).
Proof
Call a short exact sequence of horizontal complexes admissible if the induced sequences on boundaries, cycles and cohomology are also short exact. For such a monomorphism , the maps and are monic. For the latter assertion, apply the snake lemma to the exact boundary sequences inside the term sequences: an element of mapping into comes from , as a subobject identity. This argument uses kernels and images and holds in an arbitrary abelian category.
Regard as a resolution in horizontal complexes. Its successive image complexes fit into admissible sequences , with . 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 and , 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 .
Fix a horizontal row . Its split sequences decompose it as the locally finite sum of stalk complexes in degree and two-term disk complexes in degrees . At each degree there are only three summands. A cochain map is the same as a map . A cochain map , with in degrees , is the same as a map : the degree- component is that map composed with . Because each is injective, these maps extend across the monomorphisms in step 1.1. Assemble the extensions into a map . 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 has the extension property for admissible monomorphisms.
Extend across by step 2.1. After this extension, kills , so it descends to and extends across into . Continue: at stage , kills the preceding image because , hence descends and extends. Each extension is a horizontal cochain map. These choices yield , with , and therefore a bicomplex map over . DC applies to finite partial maps in the set of these Hom groups; supplied extensions give the same recursion without choice.
For two lifts, put . At vertical degree zero kills , so it factors through and extends to . Inductively, kills : substitution of the preceding homotopy equation and verifies this equality. It therefore descends to and extends to by step 2.1. Thus , with every a horizontal cochain map. The same countable-choice accounting applies.
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 maps. On horizontal cohomology, the same equation gives a homotopy for the induced vertical differential, so its cohomology maps coincide on horizontal-first . All subsequent maps agree by natural page transitions. The signed total homotopy is on bidegree : the horizontal mixed terms cancel since commutes with , and the vertical terms are . 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 are included by .
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
- Weibel, Exercises 5.7.2–3 and cohomology variant 5.7.9; completed comparison argument (standard reference, not scraped)