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.
Edge homomorphisms of a first quadrant spectral sequence
Definition
Let a homological spectral sequence be first quadrant from page s≥2, with finite abutment data as in Abutment to a filtered object, normalized by and for n≥0. By Degree reasons force stabilization in a bounded region the axis terms stabilize. The edge maps are the composites The first surjection is obtained by composing the finitely many transition quotient maps on the vertical axis: every outgoing differential there lands at negative first coordinate. On the horizontal axis, every incoming source has second coordinate , so the transitions identify successive kernels as subobjects; their composite gives the second inclusion. Further stationary transitions do not change these maps.
For cohomological first-quadrant indexing, normalize and . The analogous arrows are through , and through . Neither the first whole-target map is necessarily epic nor the second monic: for example, in an abelian category with a supplied nonzero object , with page terms fixed equal to at (0,1) and (1,0), zero elsewhere and zero differentials, the abutment filtered by its first summand has edges the summand inclusion and the other summand projection. These respectively miss the second summand and kill the first.
Source notes
Weibel, Example 5.2.6 p.124. The whole-target epic/monic claims in Sharifi Remark 4.1.16 are not used.
Depends on
Used by
- Serre edge homomorphisms and transgression Definition
- Spectral-sequence computation record Definition
- Edge maps from a first quadrant spectral sequence Example
- Edge homomorphisms are natural Lemma
- Hypercohomology edge maps are canonical Proposition
- Acyclic assembly lemma for a first quadrant double complex Theorem
- Five term exact sequence of a first quadrant cohomological spectral sequence Theorem
- Five term exact sequence of a first quadrant homological spectral sequence Theorem
- Gysin sequence from a sphere-fiber Serre spectral sequence Theorem
- Wang sequence for a fibration over the circle Theorem
Dependency tree · two levels
5 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
- Charles A. Weibel, An Introduction to Homological Algebra, Chapter 5 (standard reference, not scraped)
- Romyar Sharifi, Homological Algebra (standard reference, not scraped)