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 for and . Write for the relative target. The first sequence has canonical edge maps The second has canonical edge maps 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: as in the statement, with the comparison qualifications of the two spectral-sequence theorems.
The first sequence has , support , , and differentials of bidegree (First hypercohomology spectral sequence).
The second sequence has with the filtration by resolution degree (Second hypercohomology spectral sequence).
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
Let be the horizontal Cartan–Eilenberg map. Compatibility with the augmentations says that lifts , so its map on vertical cohomology is the relative derived map . Since is induced by this horizontal map, . For , left exactness identifies with , and this identification carries to . The augmentations therefore give a cochain map . On a degree- cycle its image lies in the extremal column and has no positive-resolution component. In the column filtration this is exactly the representative of the bottom-row edge from , with the finite transition quotients killing precisely the later boundaries. Thus the induced cohomology map is that edge.
In the second sequence, and therefore . Inclusion of these horizontal cycles gives a cochain map from their vertical resolution after , placed starting in total degree , into the total complex. Its cohomology map is , using the constant sign on the vertical differential. These are the bottom-row representatives for the resolution-degree filtration, so this is its lower edge.
Projection of the total complex onto column gives a cochain map to that column with its signed differential and original degree placement. The total cocycle equation in column says the horizontal image of the projected vertical class is zero. By the calculation in step 1.1, the cohomology map therefore lands in , which is the left-axis 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.
Projection onto resolution degree zero sends a total cocycle to a horizontal cohomology class in . Its induced vertical differential is zero by the next component of the total cocycle equation. Left exactness identifies this kernel with , since resolves . 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 both filtrations have one piece and the arrows agree with the bottom augmentation identification; zero targets cause no exception.
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
- Weibel, Section 5.7 (standard reference, not scraped)