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.
Multiplicative filtered cochains induce products on every spectral-sequence page
Statement
Let be a commutative unital ring and let be an associative unital differential graded -algebra: has degree and for homogeneous . Suppose has a decreasing filtration by subcomplexes, indexed by all integers, such that Then every page of its cohomological spectral sequence has natural products making it a unital associative bigraded algebra, and The specified comparison is an isomorphism of bigraded algebras. If is graded-commutative, every page is graded-commutative with the total-degree sign.
If the filtration is degreewise finite, so that the filtered-complex construction converges to the decreasing image filtration then the stable product is exactly the associated-graded abutment product: corresponds to multiplication All assertions are choice-free.
Facts & Assumptions
Given: the DGA, its multiplicative decreasing filtration, homogeneous inputs, and the displayed Leibniz rule.
R cycles and r boundaries of an increasingly filtered complex and R page of the spectral sequence of a filtered complex give the exact , , , and page quotients. The filtered differential induces d r on the r page identifies with the original differential on representatives.
Spectral sequence subquotient and local lifting calculus permits numerator and denominator containments to be checked after local lifts and descends the resulting bilinear maps uniquely to quotients.
The next page is the homology of the current page gives the specified natural comparison and its lower-filtration correction of a page-cycle representative.
The cohomological filtered complex construction fixes the cohomological reindexing and gives the finite-filtration stable-page identification with the decreasing image filtration.
Proof
Reindex by and as in [F4]. Multiplication sends into , and its Leibniz sign is . Fix , , and . Then and , so Thus . For , multiplication sends times to , since either lower-filtration change lowers the product filtration by one.
Let . Then and so , the first target denominator summand. The same calculation with the factors reversed puts in that summand whenever .
Let . The Leibniz formula gives Here : its differential lies in because lies there and lies in . Also , since it lies in and its differential, up to sign, is . Thus belongs to the sum of the two target summands. Symmetrically, for , with and . Hence a change by either differential-boundary summand also changes the product by a target -boundary.
Steps 2.1 and 2.2 show separately that multiplication kills the source denominator in either variable after passage to the target quotient. Bilinearity handles simultaneous changes. Quotient descent in [F2] therefore gives a unique page product for every ; the calculation in Step 1.1 gives the associated-graded product. Associativity and the unit descend from . If in , the same representative equality gives graded commutativity on every page. A filtration-preserving DGA map sends to the product of the two image representatives and preserves every and ; uniqueness in [F2] therefore makes these page products natural for filtered DGA maps.
By [F1], the page differential is induced by . Therefore the calculation of Step 1.1 descends verbatim: Under , , the parity of is the parity of , and the target bidegrees translate to and . This is the asserted cohomological derivation rule, including .
Assume the filtration is degreewise finite and fix . For beyond both relevant filtration endpoints, [F1] reduces the stable numerator to and its denominator to Sending an actual cycle to its class in identifies this quotient, in both directions, with , which is the stable identification in [F4]. If and are actual filtered cycles, their product is the actual cycle , lies in , and represents both their page product from Step 3.1 and the product of their image-filtration classes. Lower-filtered cycles and actual boundaries give exactly the lower associated-graded ambiguity by Steps 2.1 and 2.2. Translating back to the decreasing filtration proves the displayed product is precisely the associated-graded abutment product.
The comparison in [F3] is multiplicative. For , a -cycle represented by already lies in , and the comparison sends it to the same representative; hence it sends the product class to . For , if page-cycle representatives require the lower-filtration corrections and from [F3], Step 1.1 puts their product in . Moreover so it represents the same product class. It is therefore a permitted correction for , and the representative rule in [F3] sends the product of the two homology classes to the product of their images. Independence follows from [F3]'s kernel calculation, not from a chosen correction. Thus is an algebra isomorphism.
If , the coefficient ring is zero, or either input is zero, every map is the unique zero map. The unit calculation includes one factor equal to , and and are covered separately in Steps 1.1 and 5.1. Repeated filtration terms, a zero differential, and representatives already in lower filtration satisfy the same containments. Step 2.2 checks both differential-boundary variables and Step 4.2 checks both finite filtration endpoints and both directions of the stable quotient identification. Every correction and calculation concerns finitely many supplied elements, so no choice principle is used. There is no iff assertion.
Depends on
- R cycles and r boundaries of an increasingly filtered complex
- R page of the spectral sequence of a filtered complex
- The filtered differential induces d r on the r page
- Spectral sequence subquotient and local lifting calculus
- The cohomological filtered complex construction
- The next page is the homology of the current page
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
20 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
- Miller, MIT 18.906 notes, Lecture 29 (standard reference, not scraped)
- Hatcher, Algebraic Topology, Chapter 5, Multiplicative Structure (standard reference, not scraped)