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.
Collapsed vector-space spectral sequences split noncanonically
Statement
Assume AC. A collapsed first-quadrant spectral sequence of -vector spaces with finite abutment filtrations gives, degree by degree, an isomorphism of the target with the direct sum of its terms on that diagonal, respecting the filtration. Such a splitting exists but cannot in general be chosen naturally in filtered data. If the finitely many graded pieces in a fixed degree are finite-dimensional, existence in that degree needs only finite choice and is valid in ZF.
Facts & Assumptions
Given: The stated finite filtered abutment over a field .
A finite filtration with projective quotients splits by lifting their identity maps across the quotient maps (Collapse with projective associated graded pieces splits the finite filtration noncanonically).
Under AC, every vector space is projective, using a basis (Modules over a field are projective, flat, and injective).
AC permits choices from arbitrary families of nonempty sets (The Axiom of Choice).
Proof
Convergence identifies each graded quotient with the corresponding stationary page term. Under AC, F2 makes each such quotient projective. Apply F1 to the finite filtration; a decreasing filtration is first read in reverse order. The resulting isomorphism is the asserted direct sum, with partial sums in the filtration order. Zero quotients use the zero section. If the whole target is zero, its empty nonzero sum is zero; if only one quotient is nonzero, the normalized endpoints identify it with the target canonically.
In the finite-dimensional branch, choose a finite basis of each quotient in the fixed degree and choose a lift of each basis vector to the preceding extension. Linear extension is a section: composing with the quotient sends every basis vector to itself. There are only finitely many such bases and lifts, so finite induction supplies them in ZF. The same successive direct-sum construction as F1 therefore works without AC in that degree. This does not assert a simultaneous choice of splittings across an arbitrary family of degrees or spectral sequences.
For nonnaturality take with . The quotient has basis and any linear section sends it to for some . The filtration-preserving automorphism , induces the identity on both graded pieces but moves every such section, since . These filtered data occur as a collapsed first-quadrant cohomological sequence: put in cochain degree one, differential zero, with . The two associated graded entries at and remain unchanged on every page. A natural splitting would have to commute with , contradicting the calculation. Thus even finite-dimensional collapse gives no general natural splitting.
Depends on
Used by
Dependency tree · two levels
12 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.2 (standard reference, not scraped)