Chapter 5. Spectral Sequences

FC05 — Weibel, An Introduction to Homological Algebra.

This chapter contains 23 definitions, 7 theorems, 5 propositions, 4 lemmas, 7 corollaries, 7 examples, 10 constructions and 17 other statements.

Of the 80 statements checked against Lean, 7 are formalized somewhere and 73 are not.

Status	Statements	Share	What it means
not formalized	73	91%	A documented search found no Lean statement of it anywhere.
in Mathlib	4	5%	Mathlib states and proves it.
in another Lean project	2	2%	Some other Lean development has it; using it means porting that code.
in lean-categories	1	1%	This repository states and proves it.
checked in total	80

Which versions of Lean and Mathlib were searched

• Project-first search was performed at repo HEAD f90173886bc881c2d43c0a7eb2d9fe7f110ac9a5. The project has no spectral-sequence, filtered-complex, exact-couple, Cartan–Eilenberg, hyperhomology, or Grothendieck-spectral-sequence implementation. LeanCategories/Homological/DerivedDimension.lean::LeanCategories.Homological.IsAcyclicFor exactly owns U062: it is explicitly documented as Weibel Definition 5.8.2 and states vanishing of all positive right-derived functors. No other C05 row is credited project-first merely from adjacent generic homological imports.
• Pinned Mathlib is P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. P already contains Mathlib/Algebra/Homology/SpectralSequence/Basic.lean: CategoryTheory.SpectralSequence is a sequence of homological-complex pages with isomorphisms from page homology to the next page; SpectralSequence.Hom is a compatible family of page maps; pageHomologyNatIso packages the next-page naturality. This exactly owns U002. The cohomological specialization CohomologicalSpectralSequence/E₂CohomologicalSpectralSequence has differential bidegree (r,1-r) and owns U004. The positive declaration set was compile-probed successfully against the project pin.
• U005 (Weibel’s Mapping Lemma) is credited to P by a checked source-shaped assembly, not by name similarity. In /tmp/fc05-c05-map-lemma.lean, from [IsIso (f.hom r)], pinned ShortComplex homology functoriality makes homologyMap (f.hom r) an isomorphism; SpectralSequence.Hom.comm transports this through the page-homology isomorphisms; HomologicalComplex.isIso_of_components then makes the next page map an isomorphism. This compiled successfully against P and iterates page by page to all later pages.
• U061 is only the setup for the Grothendieck spectral sequence, not the theorem itself. P supplies abelian categories, enough injective resolutions, left exactness as preservation of finite limits, functor composition, and Functor.rightDerived, so this data row is mathlib. No spectral-sequence theorem is inferred from that setup.
• Current Mathlib was rechecked immediately before promotion at H=5aedf732b6987e8c26ab3c9ebc855314f82b045f. Targeted current-tree search found no generic convergence/abutment/E∞ interface, no filtered-chain-complex-to-spectral-sequence construction, no exact-couple owner, no multiplicative spectral sequence, no Cartan–Eilenberg resolutions/hyperderived functors, no Grothendieck spectral sequence, and no Leray–Serre/Wang/Gysin/Bockstein implementations. The only GroupCohomology occurrence of “Hochschild-Serre spectral sequence” is commentary indicating future/use-case direction, not a theorem owner.
• P/H do contain extensive SpectralObject machinery and construct E₂ homological/cohomological spectral sequences from spectral objects. This is not credited to filtered-complex, convergence, or double-complex rows unless a checked bridge with the source pages and abutment exists. Targeted search found no such bridge for U001 or U022–U050. In particular P’s bicomplex totalization is coproduct/direct-sum based and C01 already recorded the absence of product totalization, so C05 U045 cannot be upgraded by neighboring bicomplex infrastructure.
• Current/external search for “filtered complex spectral sequence”, Künneth spectral sequence, Cartan–Eilenberg resolution, hypertor, hypercohomology spectral sequence, Grothendieck spectral sequence, Leray–Serre, Bockstein spectral sequence, and Eilenberg–Moore spectral sequence found no acceptable Lean4 owner matching the relevant source rows. Searches were refreshed on 2026-09-06 rather than reused from earlier chapter audits.
• The one substantive external exact-couple development is the legacy HoTT/Lean repository cmu-phil/Spectral@3b078f5f1de251637decf04bd3fc8aa01930a6b3, rechecked at that HEAD immediately before promotion; the repository is Apache-2.0. algebra/exact_couple.hlean::exact_couple.exact_couple defines graded modules D,E, maps i,j,k, and exactness at each vertex, exactly U068. The same file’s derived_couple namespace defines d=j∘k, D'=im(i), E'=H(E,d), induced i',j',k', and proves the three exactness conditions, exactly U069. These are reference-port routes because the code is legacy .hlean/HoTT Lean and not directly importable into the current Mathlib project.
• The same legacy repository is not used as blanket coverage. It has a bespoke is_bounded/convergent_exact_couple framework and a convergent_spectral_sequence, but no checked morphism category for exact couples giving the whole U070 functorial proposition; its convergence hypotheses/abutment data are not Weibel’s bounded-below exact-couple theorem with target colim D, so U073–U075 remain unmatched. Its cohomology/gysin.hlean and cohomology/serre.hlean concern HoTT/generalized cohomology and do not realize the homological Leray–Serre/Wang/Gysin rows U016–U021.
• The source’s convergence terminology is not collapsed into Mathlib’s use of the word “convergent” in comments around certain spectral-object constructions. Under strict bundle semantics, a page construction does not satisfy U006–U013 without the source filtration/abutment/E∞ data, and an internal cycles/boundaries implementation does not satisfy U009 without the stated generic nested-subobject and limit construction.
• N denotes dated 2026-09-06 negative evidence after project-first inspection, P, H/current Mathlib, targeted open/current/indexed searches, and the legacy exact-couple repository above. A source row is not credited from adjacent spectral-object machinery, a topologically different generalized-cohomology theorem, or only part of a convergence/multiplicative/hyperderived bundle.

Construction — First pages of the double-complex spectral sequence

FC05-C05-U001 · §5.1 Introduction; pp. 120–121; L3646–3652 · after FC05-C01-U016, FC05-C01-U018, FC05-C01-U002 · not formalized

For a first-quadrant double complex E, set E¹_{pq}=H_q^v(E_{p,}) and E²_{pq}=H_p^h(E¹_{,q}); these are the first successive approximations to H_{p+q}(Tot E).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — P has bicomplexes, vertical/horizontal homology, total complexes, and generic spectral sequences, but no checked canonical double-complex spectral sequence whose first two pages are the stated iterated homologies and which abuts to total homology.

Definition 5.2.1 — Homology spectral sequence

FC05-C05-U002 · §5.2 Terminology; pp. 122–126; L3685–3697 · after FC05-C01-U013, FC05-C01-U014 · in Mathlib

In an abelian category A, a homology spectral sequence from E^a is a family E^r_{pq} with d^r:Er_{pq}→E^r_{p-r,q+r-1}, (d^r)2=0, and specified isomorphisms E^{r+1}{pq}≅H(E^r,dr){pq}; morphisms commute with d and induce the next-page maps.

Formalized. Mathlib/Algebra/Homology/SpectralSequence/Basic.lean::CategoryTheory.SpectralSequence; SpectralSequence.Hom; pageHomologyNatIso — Pinned Mathlib defines pages as homological complexes, next-page homology isomorphisms, and morphisms commuting with those isomorphisms, exactly the source abstract spectral-sequence data.

Searched: P

Example 5.2.2 — First-quadrant spectral sequence

FC05-C05-U003 · §5.2 Terminology; pp. 122–126; L3699 · after FC05-C05-U002 · not formalized

A homology spectral sequence is first quadrant when E^r_{pq}=0 unless p,q≥0. Then each fixed spot stabilizes for large r; its stable value is denoted E^∞_{pq}.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — P has first-quadrant spectral-sequence shapes, but no generic stabilization/E∞ object or theorem that every fixed first-quadrant spot stabilizes; the whole row is therefore not represented.

Dual Definition 5.2.3 — Cohomology spectral sequence

FC05-C05-U004 · §5.2 Terminology; pp. 122–126; L3701–3709 · after FC05-C05-U002, FC05-C01-U005 · in Mathlib

A cohomology spectral sequence has d_r^{pq}:E_r{pq}→E_r^{p+r,q-r+1}, hence raises total degree by one, and E_{r+1} is the homology of E_r; equivalently E_r^{pq}=Er_{-p,-q} for a homology spectral sequence.

Formalized. CategoryTheory.CohomologicalSpectralSequence; E₂CohomologicalSpectralSequence; ComplexShape.up' — The pinned specialization has differential bidegree (r,1-r), i.e. raises total cohomological degree by one, with next page given by homology.

Searched: P

Mapping Lemma 5.2.4

FC05-C05-U005 · §5.2 Terminology; pp. 122–126; L3711 · after FC05-C05-U002, FC05-C05-U004 · in Mathlib

A morphism of spectral sequences that is an isomorphism in every bidegree on one page r is an isomorphism on every later page s≥r.

Formalized. SpectralSequence.Hom.comm; ShortComplex.isIso_homologyMap_of_isIso; HomologicalComplex.isIso_of_components — If a page map is an isomorphism, its homology map is an isomorphism; compatibility with the next-page isomorphisms makes every component on the next page an isomorphism, hence the next page map is an isomorphism. The one-step source-shaped assembly compiled against P and iterates to all later pages.

Searched: P

Definition 5.2.5 — Bounded spectral sequence and convergence

FC05-C05-U006 · §5.2 Terminology; pp. 122–126; L3713–3731 · after FC05-C05-U002, FC05-C05-U004 · not formalized

Degree-bounded means finitely many nonzero E^a_{pq} in each total degree, hence every spot stabilizes. Such a spectral sequence converges to H_* when H_n has a finite filtration with E^∞{pq}≅F_pH{p+q}/F_{p-1}H_{p+q}; dually for cohomology.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — P/H define page-by-page spectral sequences but no boundedness/convergence/abutment structure identifying E∞ with graded pieces of a filtered target.

Example 5.2.6 — First-quadrant filtrations and edge maps

FC05-C05-U007 · §5.2 Terminology; pp. 122–126; L3733–3745 · after FC05-C05-U003, FC05-C05-U006 · not formalized

For a first-quadrant spectral sequence converging to H_*, H_n has filtration 0=F_{-1}⊂…⊂F_n=H_n; the y-axis gives F_0 and the x-axis gives H_n/F_{n-1}, producing the standard edge homomorphisms. The cohomological version is dual.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — Edge homomorphisms here depend on the missing convergence filtration/abutment layer; no checked P/H/external owner packages the first-quadrant edge-map statement.

Definition 5.2.7 — Collapse of a spectral sequence

FC05-C05-U008 · §5.2 Terminology; pp. 122–126; L3747 · after FC05-C05-U002, FC05-C05-U006 · not formalized

A spectral sequence collapses at E^r when E^r has exactly one nonzero row or column; if it converges, the unique E^r_{pq} of total degree n identifies with H_n.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — P has finite-row spectral-sequence shapes but no source collapse predicate together with convergence-to-abutment identification of the unique term.

Construction 5.2.8 — E^∞ via nested cycles and boundaries

FC05-C05-U009 · §5.2 Terminology; pp. 122–126; L3763–3777 · after FC05-C05-U002, FC05-C03-U045 · not formalized

For each bidegree there are nested subobjects B^r⊂B{r+1}⊂Z^{r+1}⊂Zr of E^a with E^r≅Zr/B^r. Define B^∞=∪_rB^r, Z^∞=∩_rZ^r and E^∞=Z∞/B^∞ when these exist; in bounded sequences they equal the stable page.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — The spectral-object implementation has internal cycle/boundary constructions, but no checked generic source interface for nested B^r,Z^r, unions/intersections, and E∞=Z∞/B∞ for an arbitrary spectral sequence.

Definition 5.2.9 — Bounded-below spectral sequence

FC05-C05-U010 · §5.2 Terminology; pp. 122–126; L3781–3783 · after FC05-C05-U002 · not formalized

A homology spectral sequence is bounded below when, in every total degree n, E^a_{pq}=0 for all sufficiently small p; dually, a cohomology spectral sequence is bounded below when the terms of degree n vanish for sufficiently large p.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked P/H declaration defines Weibel’s total-degree bounded-below predicate for a spectral sequence.

Definition 5.2.10 — Regular spectral sequence

FC05-C05-U011 · §5.2 Terminology; pp. 122–126; L3785 · after FC05-C05-U002, FC05-C05-U009 · not formalized

A spectral sequence is regular when for each (p,q) the outgoing differentials are zero for all sufficiently large r; equivalently Z^∞{pq}=Z^r{pq} eventually.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked P/H declaration defines regularity as eventual vanishing of outgoing differentials or the equivalent eventual-cycle condition.

Definition 5.2.11 — Weak convergence, abutment, and convergence

FC05-C05-U012 · §5.2 Terminology; pp. 122–126; L3787–3799 · after FC05-C05-U009, FC05-C05-U011, FC05-C02-U063 · not formalized

Weak convergence to H_* means a filtration F_pH_n with E^∞{pq}≅F_pH{p+q}/F_{p-1}H_{p+q}. It approaches H_* if the filtration is exhaustive and Hausdorff, and converges if additionally the spectral sequence is regular and H_n≅lim H_n/F_pH_n; bounded-below approach already implies convergence.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — P/H have no weak-convergence/approach/completeness package or inverse-limit target condition matching the source definition.

Comparison Theorem 5.2.12

FC05-C05-U013 · §5.2 Terminology; pp. 122–126; L3801 · after FC05-C05-U005, FC05-C05-U012 · not formalized

For convergent spectral sequences E,E’ with compatible h:H_*→H’_* and f:E→E’, if f is an isomorphism on one page (hence on E^∞), then h is an isomorphism.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — The comparison theorem depends on the absent convergence/filtered-abutment infrastructure; the pagewise mapping lemma U005 alone does not identify the target map.

Construction 5.2.13 — Multiplicative spectral sequence

FC05-C05-U014 · §5.2 Terminology; pp. 122–126; L3813–3825 · after FC05-C05-U002 · not formalized

A bigraded product on E^a satisfying the graded Leibniz rule for d^a descends to every later page, yielding a multiplicative spectral sequence.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked P/H/current/external implementation equips spectral-sequence pages with products satisfying the graded Leibniz rule and descends them page by page.

Definition 5.3.1 — Serre fibration

FC05-C05-U015 · §5.3 The Leray-Serre Spectral Sequence; pp. 127–130; L3831–3843 · not formalized

A based sequence F→E→B is a Serre fibration when F is the fiber over the basepoint and π:E→B has the homotopy-lifting property for every finite polyhedron P and homotopy P×I→B; the section assumes B simply connected.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — Mathlib has homotopy lifting for covering maps but no Serre-fibration predicate with lifting against finite polyhedra matching the source definition.

Theorem 5.3.2 — Leray–Serre spectral sequence

FC05-C05-U016 · §5.3 The Leray-Serre Spectral Sequence; pp. 127–130; L3845–3873 · after FC05-C05-U015, FC05-C05-U003, FC05-C05-U006, FC05-C01-U008 · not formalized

For a Serre fibration F→E→B with B simply connected, there is a first-quadrant homology spectral sequence E²_{pq}=H_p(B;H_q(F))⇒H_{p+q}(E). Its edge maps are induced by F→E and E→B (under the stated connectivity hypothesis on F for the latter).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked P/H/current/external Leray–Serre homology spectral sequence with the source E² page, convergence, and edge maps was found. The legacy cmu-phil/Spectral code concerns a HoTT/generalized-cohomology Serre construction and does not realize this row.

Application 5.3.3 — Low-degree exact sequence of a fibration

FC05-C05-U017 · §5.3 The Leray-Serre Spectral Sequence; pp. 127–130; L3875–3889 · after FC05-C05-U016, FC05-C05-U007 · not formalized

The lower-left corner of the Leray–Serre sequence gives an exact homology sequence through H_2(F), H_2(E), H_2(B), H_1(F), H_1(E), with d²:H_2(B)→H_1(F); the preceding term records the first obstruction to a homology LES for a fibration.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked low-degree homology exact sequence extracted from a Leray–Serre spectral sequence was found.

Application 5.3.4 — Loop-space fibration

FC05-C05-U018 · §5.3 The Leray-Serre Spectral Sequence; pp. 127–130; L3891–3897 · after FC05-C05-U015, FC05-C05-U016 · not formalized

For ΩB→PB→B with PB contractible and π_1(B)=0, the Leray–Serre sequence yields H_1(ΩB)≅H_2(B) and the displayed exact sequence H_4(B)→H_2(B)⊗H_2(B)→H_2(ΩB)→H_3(B)→0.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked loop-path fibration spectral-sequence calculation with the displayed H₂/H₃/H₄ exact sequence was found.

Application 5.3.5 — Wang sequence

FC05-C05-U019 · §5.3 The Leray-Serre Spectral Sequence; pp. 127–130; L3905–3911 · after FC05-C05-U016 · not formalized

For a fibration F→E→S^n with n≠0,1, only the p=0,n columns survive on E², giving the Wang long exact sequence …→H_q(F)→H_q(E)→H_{q-n}(F)→^{dn}H_{q-1}(F)→…; in particular H_q(F)≅H_q(E) for 0≤q≤n−2.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Wang sequence for a fibration over a sphere was found in P/H/current/external Lean.

Example 5.3.6 — Homology of SO(3) from the fibration over S²

FC05-C05-U020 · §5.3 The Leray-Serre Spectral Sequence; pp. 127–130; L3927–3939 · after FC05-C05-U019 · not formalized

Applying the Wang sequence to S¹→SO(3)→S² and using π_1SO(3)=Z/2 gives H_3(SO(3))≅Z, H_1(SO(3))≅Z/2, and H_2(SO(3))=0 (the extraction’s apparent Z is an OCR error contradicted by exactness).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked source calculation of H_*(SO(3)) from the circle fibration over S² was found.

Application 5.3.7 — Gysin sequence

FC05-C05-U021 · §5.3 The Leray-Serre Spectral Sequence; pp. 127–130; L3941–3947 · after FC05-C05-U016 · not formalized

For a sphere fibration S^n→E→B with B simply connected and n≠0, the two-row Leray–Serre sequence yields the Gysin long exact sequence …→H_{p-n}(B)→H_p(E)→H_p(B)→^{d{n+1}}H_{p-n-1}(B)→…; hence H_p(E)≅H_p(B) for p<n.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked homological Gysin sequence for a sphere fibration matching the source row was found. The legacy HoTT repository contains a cohomological generalized-cohomology Gysin construction, not this whole statement.

Definition — Filtration of a chain complex

FC05-C05-U022 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L3959 · after FC05-C01-U002, FC05-C01-U011 · not formalized

A filtration F on C is an increasing family of chain subcomplexes …⊂F_{p-1}C⊂F_pC⊂… .

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked P/H structure packages an increasing filtration by chain subcomplexes of a homological complex in the source form.

Definition — Exhaustive filtration

FC05-C05-U023 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L3961 · after FC05-C05-U022 · not formalized

A filtration F on C is exhaustive when C=∪_pF_pC; replacing C by ∪F_pC does not change the associated spectral sequence.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — The source exhaustive-union predicate depends on the missing filtered-complex owner; no checked declaration packages it.

Construction Theorem 5.4.1 — Spectral sequence of a filtered complex

FC05-C05-U024 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L3963–3965 · after FC05-C05-U022, FC05-C05-U002 · not formalized

A filtration F on a chain complex C canonically yields a spectral sequence with E^0_{pq}=F_pC_{p+q}/F_{p-1}C_{p+q} and E^{1_{pq}=H_{p+q}(E}0_{p,*}).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked construction turns an arbitrary filtered chain complex into the stated E⁰/E¹ spectral sequence. Mathlib’s spectral-object machinery is not connected to a filtered complex by such an owner.

Definition 5.4.2 — Bounded filtration

FC05-C05-U025 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L3967 · after FC05-C05-U022, FC05-C05-U006 · not formalized

F is bounded when for each degree n there are s<t with F_sC_n=0 and F_tC_n=C_n; its associated spectral sequence is bounded.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked bounded-filtration predicate and theorem that its associated spectral sequence is bounded was found.

Definitions — Bounded-below and bounded-above filtrations

FC05-C05-U026 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L3969 · after FC05-C05-U022, FC05-C05-U010 · not formalized

F is bounded below if each C_n has F_sC_n=0 for some s, and bounded above if each C_n has F_tC_n=C_n for some t. Bounded below induces a bounded-below spectral sequence; bounded above implies exhaustiveness.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked bounded-below/above filtered-complex predicates with the stated spectral-sequence/exhaustiveness consequences were found.

Example 5.4.3 — Canonically bounded filtration

FC05-C05-U027 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L3971–3973 · after FC05-C05-U022, FC05-C05-U003, FC05-C05-U025, FC05-C05-U016 · not formalized

A filtration is canonically bounded when F_{-1}C=0 and F_nC_n=C_n. Its spectral sequence is first quadrant and converges to H_*(C); the Leray–Serre sequence arises this way from singular chains on E.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked canonical-bounded filtration construction or theorem recovering Leray–Serre from singular chains was found.

Definition 5.4.4 — Hausdorff filtration

FC05-C05-U028 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L3975 · after FC05-C05-U022 · not formalized

A filtration is Hausdorff when ∩_pF_pC=0; C and the Hausdorff quotient C/(∩F_pC) have the same associated spectral sequence.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Hausdorff filtered-complex predicate with invariance under quotient by the intersection was found.

Definitions — Complete filtration and completion

FC05-C05-U029 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L3977 · after FC05-C05-U022, FC05-C05-U028, FC05-C02-U063 · not formalized

The completion of a filtered complex is Ĉ=lim_p C/F_pC; the filtration is complete when C→Ĉ is an isomorphism. Complete implies Hausdorff, and bounded-below filtrations are complete.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — P has inverse limits and completion infrastructure elsewhere, but no filtered-complex completion lim C/F_pC with the source completeness/Hausdorff/bounded-below theorem bundle.

Addendum 5.4.5 — Completion preserves the spectral sequence

FC05-C05-U030 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L3979 · after FC05-C05-U024, FC05-C05-U029 · not formalized

The filtered complexes C and its completion Ĉ have naturally isomorphic associated spectral sequences on every page.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked theorem states that completion of a filtered complex preserves every page of its associated spectral sequence.

Construction 5.4.6 — Explicit Z^r, B^r, E^r of a filtered complex

FC05-C05-U031 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L3981–4001 · after FC05-C05-U024, FC05-C05-U022 · not formalized

For A_p^r={c∈F_pC : dc∈F_{p-r}C}, define Z_p^r and B_p^r as their images in E_p^0 and E_p^r=Z_pr/B_p^r; d on C induces d_p^r:E_pr→E_{p-r}^r, producing the spectral sequence of 5.4.1.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked explicit A_p^r,Z_p^r,B_p^r,E_p^r construction for a filtered complex was found.

Lemma 5.4.7 — Successive Z/B quotients

FC05-C05-U032 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L4003–4007 · after FC05-C05-U031 · not formalized

The differential induces isomorphisms Z_p^r/Z_p{r+1}≅B_{p-r}^{{r+1}/B_{p-r}}r, which identifies E^{r+1} with the homology of E^r in Construction 5.4.6.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — Without U031’s filtered construction, the successive cycle/boundary quotient isomorphism and next-page identification are not formalized in the source form.

Construction 5.4.8 — Multiplicative filtration

FC05-C05-U033 · §5.4 Spectral Sequence of a Filtration; pp. 131–134; L4039–4045 · after FC05-C05-U031, FC05-C05-U014, FC05-C04-U071 · not formalized

If C is a DG-algebra and F is multiplicative, the associated spectral sequence is multiplicative; when it weakly converges to H_(C), E^∞ is the associated graded algebra of H_(C) for the induced multiplicative filtration.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked multiplicative filtered-DG-algebra spectral sequence with associated-graded abutment exists; P also lacks the C04 DG-algebra bundle required by the row.

Classical Convergence Theorem 5.5.1

FC05-C05-U034 · §5.5 Convergence; pp. 135–140; L4069–4079 · after FC05-C05-U024, FC05-C05-U025, FC05-C05-U026, FC05-C05-U012 · not formalized

For the spectral sequence of a filtered complex: a bounded filtration yields a bounded sequence converging to H_(C); a bounded-below exhaustive filtration yields a bounded-below sequence converging to H_(C). The convergence is natural for filtered chain maps.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked classical convergence theorem for bounded or bounded-below exhaustive filtered complexes, including naturality, was found.

Example 5.5.2 — First-quadrant convergence

FC05-C05-U035 · §5.5 Convergence; pp. 135–140; L4081 · after FC05-C05-U027, FC05-C05-U034, FC05-C05-U007 · not formalized

For a canonically bounded filtration, the associated first-quadrant spectral sequence converges to H_(C); the y-axis and x-axis E^∞ terms are respectively controlled by H_(F_0C) and the top quotient complex C_n/F_{n-1}C_n.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked first-quadrant filtered-complex convergence/edge-term example was found.

Corollary 5.5.3 — Edge terms as image and quotient

FC05-C05-U036 · §5.5 Convergence; pp. 135–140; L4083 · after FC05-C05-U035, FC05-C01-U022 · not formalized

For a canonically bounded filtration, E^∞{0q}=im(H_q(F_0C)→H_q(C)) and E^∞{p0}=im(H_p(C)→H_p(C/F_{p-1}C))≅H_p(C)/F_{p-1}H_p(C).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked theorem identifies the two E∞ edge terms with the displayed image and quotient of homology.

Example 5.5.4 — Weak convergence without convergence

FC05-C05-U037 · §5.5 Convergence; pp. 135–140; L4095 · after FC05-C05-U029, FC05-C05-U012, FC05-C05-U030 · not formalized

For C=(0→Z→^3 Z→0) with F_pC=2^pC, the spectral sequence collapses to zero at E¹ and weakly converges to H_(C), but the induced homology filtration is not Hausdorff; it converges instead to H_(Ĉ)=0.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked formalization of Weibel’s 3-map/2^p weak-but-not-strong convergence counterexample was found.

Theorem 5.5.5 — Eilenberg–Moore filtration sequence

FC05-C05-U038 · §5.5 Convergence; pp. 135–140; L4097–4107 · after FC05-C05-U029, FC05-C03-U054 · not formalized

If C is complete, the Milnor sequence for the tower C/F_pC identifies lim¹H_{n+1}(C/F_pC) with ∩_pF_pH_n(C), and identifies lim H_n(C/F_pC) with the Hausdorff completion H_n(C)/(∩F_pH_n(C)).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — P contains inverse-limit and lim¹ ingredients, but no checked Eilenberg–Moore filtered-complex exact sequence identifying the homology-filtration intersection and completion as stated.

Corollary 5.5.6 — Weak convergence and completion

FC05-C05-U039 · §5.5 Convergence; pp. 135–140; L4117–4119 · after FC05-C05-U038, FC05-C05-U012, FC05-C05-U030 · not formalized

If the spectral sequence of a complete filtered complex weakly converges, then H_(C)≅H_(Ĉ).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked weak-convergence/completion corollary for complete filtered complexes was found.

Lemma 5.5.7 — The actual E^∞ subquotient for Hausdorff exhaustive filtrations

FC05-C05-U040 · §5.5 Convergence; pp. 135–140; L4121–4129 · after FC05-C05-U028, FC05-C05-U023, FC05-C05-U031 · not formalized

For a Hausdorff exhaustive filtration, A^∞{pq}=ker(d:F_pC_n→F_pC{n-1}); the subquotient e^{∞{pq}=η_p(A^∞{pq})/B}∞{pq} is naturally F_pH_n(C)/F{p-1}H_n(C).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked theorem realizes the actual E∞ subquotient e∞ of a Hausdorff exhaustive filtered complex and identifies it with the associated graded homology filtration.

Corollary 5.5.8 — Boardman criterion

FC05-C05-U041 · §5.5 Convergence; pp. 135–140; L4139–4145 · after FC05-C05-U040, FC05-C03-U046 · not formalized

For Q_p=lim¹_r A^r_{pq}, there is an exact sequence 0→e^∞{pq}→E^∞{pq}→Q_{p-1}→Q_p→lim¹_r Z^r_{pq}→0. For Hausdorff exhaustive F, weak convergence to H_*(C) is equivalent to injectivity of every Q_{p-1}→Q_p.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Boardman six-term lim¹ exact sequence or its weak-convergence criterion was found.

Proposition 5.5.9 — Boardman vanishing of the inverse limit of Qp

FC05-C05-U042 · §5.5 Convergence; pp. 135–140; L4165 · after FC05-C05-U041, FC05-C05-U029, FC05-C03-U052, FC05-C03-U053 · not formalized

If the filtration on C_n is complete and Q_p=lim¹_r A^r_{p,n-p}, then lim_p Q_p=0.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Boardman theorem proving lim_p Q_p=0 under completeness was found.

Complete Convergence Theorem 5.5.10

FC05-C05-U043 · §5.5 Convergence; pp. 135–140; L4197–4203 · after FC05-C05-U042, FC05-C05-U041, FC05-C05-U011, FC05-C05-U029, FC05-C05-U038 · not formalized

If F is complete and exhaustive and the associated spectral sequence is regular, then it weakly converges to H_(C). If in addition the spectral sequence is bounded above, it converges to H_(C).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked complete-convergence theorem under complete/exhaustive/regular hypotheses was found.

Eilenberg–Moore Comparison Theorem 5.5.11

FC05-C05-U044 · §5.5 Convergence; pp. 135–140; L4227 · after FC05-C05-U043, FC05-C05-U005 · not formalized

Let f:B→C be a filtered map of module complexes, with B,C complete and exhaustive. If f induces an isomorphism E^{r_{pq}(B)→E}r_{pq}(C) for every p,q on some fixed page r, then f induces an isomorphism on homology.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Eilenberg–Moore comparison theorem for complete exhaustive filtered complexes was found.

Definition 5.6.1 — Column filtration of a double complex

FC05-C05-U045 · §5.6 Spectral Sequences of a Double Complex; pp. 141–144; L4235–4267 · after FC05-C01-U016, FC05-C01-U018, FC05-C05-U024, FC05-C05-U034, FC05-C05-U043 · not formalized

Filtering Tot(C) by columns gives a spectral sequence with ^IE0_{pq}=C_{pq}, ^IE1_{pq}=H_q^v(C_{p,*}), and ^{IE²_{pq}=H_p}hH_q^v(C). For first-quadrant C it converges to H_{p+q}(Tot C); the appropriate direct-sum/product totalization is required in other quadrants.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — P has bicomplexes and direct-sum totalization, but no checked column-filtration spectral-sequence construction with the stated E⁰/E¹/E² pages and convergence; product totalization is also absent.

Definition 5.6.2 — Row filtration of a double complex

FC05-C05-U046 · §5.6 Spectral Sequences of a Double Complex; pp. 141–144; L4269–4283 · after FC05-C05-U045, FC05-C01-U016 · not formalized

Filtering Tot(C) by rows gives ^IIE0_{pq}=C_{qp}, ^IIE1_{pq}=H_q^h(C_{*,p}), and ^{IIE²_{pq}=H_p}vH_q^h(C), with convergence behavior dual to the column filtration.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked row-filtration spectral-sequence construction for bicomplexes was found.

Application 5.6.3 — Spectral-sequence proof that Tor is balanced

FC05-C05-U047 · §5.6 Spectral Sequences of a Double Complex; pp. 141–144; L4285–4297 · after FC05-C05-U045, FC05-C05-U046, FC05-C02-U075, FC05-C05-U008 · not formalized

For projective resolutions P→A and Q→B, the two spectral sequences of P⊗Q each collapse, identifying H_*(Tot(P⊗Q)) with the two possible derived tensor computations; hence they give the same Tor groups.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — Pinned Tor explicitly lacks the two-variable balancing theorem (already recorded in FC05 C03), and no spectral-sequence proof via a projective-resolution bicomplex is formalized.

Theorem 5.6.4 — Künneth spectral sequence

FC05-C05-U048 · §5.6 Spectral Sequences of a Double Complex; pp. 141–144; L4299–4303 · after FC05-C05-U045, FC05-C05-U046, FC05-C03-U009, FC05-C02-U056, FC05-C03-U018 · not formalized

If P is a bounded-below complex of flat right R-modules and M a left R-module, there is a boundedly convergent right-half-plane spectral sequence E²_{pq}=Tor_p^R(H_q(P),M)⇒H_{p+q}(P⊗_RM).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Künneth spectral sequence Tor_p(H_q(P),M) ⇒ H_{p+q}(P⊗M) exists in the source generality.

Construction 5.6.5 — Künneth formula by collapse

FC05-C05-U049 · §5.6 Spectral Sequences of a Double Complex; pp. 141–144; L4317–4327 · after FC05-C05-U048, FC05-C05-U008, FC05-C03-U060 · not formalized

If the boundaries d(P) (hence cycles) are flat, each H_q(P) has flat dimension at most one; the Künneth spectral sequence has only columns p=0,1, collapses at E², and yields the Künneth short exact sequence of 3.6.1.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked collapse argument from the missing Künneth spectral sequence to the source Künneth short exact sequence was found.

Theorem 5.6.6 — Base-change spectral sequence for Tor

FC05-C05-U050 · §5.6 Spectral Sequences of a Double Complex; pp. 141–144; L4331–4337 · after FC05-C05-U045, FC05-C05-U046, FC05-C02-U056, FC05-C02-U015 · not formalized

For a ring map R→S, A∈mod-R and B∈S-mod, there is a first-quadrant spectral sequence E²_{pq}=Tor_p^S(Tor_qR(A,S),B)⇒Tor_{p+q}^R(A,B).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Tor base-change spectral sequence for a ring map was found.

Definition 5.7.1 — Left Cartan–Eilenberg resolution

FC05-C05-U051 · §5.7 Hyperhomology; pp. 145–149; L4371–4380 · after FC05-C01-U016, FC05-C02-U009, FC05-C02-U015, FC05-C01-U002 · not formalized

For an abelian category A with enough projectives, a left Cartan–Eilenberg resolution of a chain complex A_* is an upper-half-plane double complex P of projectives with augmentation P_{0}→A_ such that the induced boundary and homology complexes resolve B_p(A) and H_p(A) projectively (and P_{p,*}=0 when A_p=0).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Cartan–Eilenberg resolution structure for chain complexes was found in P/H/current/external Lean.

Lemma 5.7.2 — Existence of Cartan–Eilenberg resolutions

FC05-C05-U052 · §5.7 Hyperhomology; pp. 145–149; L4390 · after FC05-C05-U051, FC05-C02-U019 · not formalized

Every chain complex in an abelian category with enough projectives has a Cartan–Eilenberg resolution, constructed from projective resolutions of boundaries and homology using the Horseshoe Lemma twice.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked existence theorem for Cartan–Eilenberg resolutions was found.

Definition 5.7.3 — Chain homotopy of double-complex maps

FC05-C05-U053 · §5.7 Hyperhomology; pp. 145–149; L4420–4430 · after FC05-C01-U016, FC05-C01-U035 · not formalized

A homotopy f⇒g of double-complex maps consists of horizontal and vertical degree-raising maps s^h,sv satisfying g−f=(d^hsh+s^hdh)+(d^vsv+s^vdv) and the mixed anticommutation identities; Tot(s^h+sv) is an ordinary chain homotopy.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — P has bicomplexes and ordinary chain homotopy, but no checked double-complex homotopy with separate horizontal/vertical homotopies and mixed identities whose totalization is the stated homotopy.

Definition 5.7.4 — Left hyper-derived functors

FC05-C05-U054 · §5.7 Hyperhomology; pp. 145–149; L4438–4442 · after FC05-C05-U051, FC05-C05-U053, FC05-C02-U038, FC05-C01-U019 · not formalized

For right exact F:A→B with A having enough projectives and P→A a Cartan–Eilenberg resolution, define 𝕃_iF(A)=H_i(Tot^⊕F(P)); comparison/homotopy makes this independent of P and functorial on complexes (subject to totalization existence).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked left hyper-derived-functor construction via Cartan–Eilenberg resolutions and direct-sum totalization was found.

Lemma 5.7.5 — Long exact sequence for hyper-derived functors

FC05-C05-U055 · §5.7 Hyperhomology; pp. 145–149; L4452–4456 · after FC05-C05-U054, FC05-C01-U022 · not formalized

A short exact sequence 0→A→B→C→0 of bounded-below complexes induces the natural long exact sequence …→𝕃_{i+1}F(C)→𝕃_iF(A)→𝕃_iF(B)→𝕃_iF(C)→… .

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked long exact sequence for the source hyper-derived functors was found.

Proposition 5.7.6 — Hyperhomology spectral sequences

FC05-C05-U056 · §5.7 Hyperhomology; pp. 145–149; L4460–4470 · after FC05-C05-U054, FC05-C05-U045, FC05-C05-U046, FC05-C02-U038 · not formalized

For a chain complex A, ^IIE²_{pq}=(L_pF)(H_q(A))⇒𝕃_{p+q}F(A) always; if A is bounded below, also ^IE²_{pq}=H_p(L_qF(A))⇒𝕃_{p+q}F(A).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked pair of hyperhomology spectral sequences from a Cartan–Eilenberg resolution was found.

Corollary 5.7.7 — Exactness, quasi-isomorphism invariance, and acyclic computation

FC05-C05-U057 · §5.7 Hyperhomology; pp. 145–149; L4474–4487 · after FC05-C05-U056, FC05-C01-U004, FC05-C02-U041 · not formalized

Hyper-derived functors vanish on exact complexes and send quasi-isomorphisms to isomorphisms. If A is bounded below and each A_p is F-acyclic, then 𝕃_pF(A)=H_p(F(A)).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked exact-complex vanishing/quasi-isomorphism invariance/F-acyclic computation theorem for the source hyper-derived functors was found.

Application 5.7.8 — Hypertor

FC05-C05-U058 · §5.7 Hyperhomology; pp. 145–149; L4489–4507 · after FC05-C05-U054, FC05-C02-U056, FC05-C05-U056, FC05-C05-U057, FC05-C02-U080 · not formalized

For a chain complex A of right R-modules and left R-module B, define Tor_i^R(A_,B)=𝕃_i(-⊗RB)(A**). This extends ordinary Tor, is computed by A⊗B for bounded-below flat A, and carries the two spectral sequences of 5.7.6; for two complexes use Cartan–Eilenberg resolutions in both variables.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked hypertor construction for complexes with the source spectral sequences and flat-complex computation was found.

Construction 5.7.9 — Right Cartan–Eilenberg resolutions and right hyper-derived functors

FC05-C05-U059 · §5.7 Hyperhomology; pp. 145–149; L4527–4531 · after FC05-C05-U051, FC05-C02-U027, FC05-C02-U047, FC05-C01-U019 · not formalized

Dually, in an abelian category with enough injectives, a cochain complex A^* admits an upper-half-plane Cartan–Eilenberg resolution A→I. For left exact F define 𝕽^iF(A)=Hi(Tot^ΠF(I)); this is functorial where the product totalization exists and has the dual hypercohomology spectral sequences.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked right Cartan–Eilenberg resolution/product-totalization hyper-derived-functor construction was found; product totalization was already absent in C01.

Application 5.7.10 — Hypercohomology of a complex of sheaves

FC05-C05-U060 · §5.7 Hyperhomology; pp. 145–149; L4533 · after FC05-C05-U059, FC05-C02-U051 · not formalized

For a space X and cochain complex of sheaves F^{, define 𝕳i(X,F)=𝕽}iΓ(F^). It extends sheaf cohomology; for bounded-below injective complexes it is H^iΓ(F), and there is a spectral sequence E_2^{pq}=Hp(X,H^q(F))⇒𝕳^{p+q}(X,F).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — Mathlib formalizes ordinary sheaf cohomology, but no checked hypercohomology of a complex of sheaves or the stated hypercohomology spectral sequence was found.

Construction 5.8.1 — Cohomological setup for composed derived functors

FC05-C05-U061 · §5.8 Grothendieck Spectral Sequences; pp. 150–152; L4539–4543 · after FC05-C01-U013, FC05-C02-U021, FC05-C01-U058, FC05-C02-U047 · in Mathlib

Fix abelian categories A,B,C with A and B having enough injectives, and left exact functors G:A→B and F:B→C; the target is to compare R^(F∘G) with R^F and R^*G.

Formalized. CategoryTheory.Abelian; HasInjectiveResolutions; CategoryTheory.leftExactFunctor; CategoryTheory.Functor.rightDerived — Pinned Mathlib has the abelian/enough-injectives setting, left-exact functor property, composites, and right-derived functors appearing in the source setup; this row introduces data rather than the spectral-sequence theorem.

Searched: P

Definition 5.8.2 — F-acyclic object for right derived functors

FC05-C05-U062 · §5.8 Grothendieck Spectral Sequences; pp. 150–152; L4545 · after FC05-C05-U061, FC05-C02-U047 · in lean-categories

For a left exact F:B→C, an object B of B is F-acyclic when R^iF(B)=0 for all i≠0.

Formalized. LeanCategories/Homological/DerivedDimension.lean::LeanCategories.Homological.IsAcyclicFor — The project definition is explicitly Weibel 5.8.2: all positive right-derived functors vanish on the object.

Searched: repo HEAD

Theorem 5.8.3 — Grothendieck spectral sequence

FC05-C05-U063 · §5.8 Grothendieck Spectral Sequences; pp. 150–152; L4547–4565 · after FC05-C05-U061, FC05-C05-U062, FC05-C05-U059, FC05-C05-U004 · not formalized

In the setup 5.8.1, if G sends injectives of A to F-acyclic objects of B, then for each A there is a convergent first-quadrant cohomology spectral sequence E_2^{pq}=(RpF)(R^qG)(A)⇒R{p+q}(FG)(A), with the stated edge maps and five-term exact sequence.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Grothendieck spectral sequence R^pF(R^qG A) ⇒ R^{p+q}(FG)A, edge maps, or five-term exact sequence exists in P/H/current/external Lean.

Corollary 5.8.4 — Homological Grothendieck spectral sequence

FC05-C05-U064 · §5.8 Grothendieck Spectral Sequences; pp. 150–152; L4587–4597 · after FC05-C05-U063, FC05-C02-U012, FC05-C02-U038 · not formalized

Dually, if A,B have enough projectives, G:A→B and F:B→C are right exact, and G sends projectives to F-acyclic objects, then E²_{pq}=(L_pF)(L_qG)(A)⇒L_{p+q}(FG)(A), with the corresponding low-degree exact sequence.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked homological/left-derived Grothendieck spectral sequence was found.

Applications 5.8.5 — Base-change spectral sequences as Grothendieck sequences

FC05-C05-U065 · §5.8 Grothendieck Spectral Sequences; pp. 150–152; L4601–4607 · after FC05-C05-U063, FC05-C05-U064, FC05-C05-U050 · not formalized

The Tor and Ext base-change spectral sequences are instances of the Grothendieck spectral sequence for the appropriate tensor/Hom composites associated to a ring map R→S.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked formalization realizes the Tor/Ext base-change spectral sequences as Grothendieck spectral sequences.

Theorem 5.8.6 — Leray spectral sequence for sheaf cohomology

FC05-C05-U066 · §5.8 Grothendieck Spectral Sequences; pp. 150–152; L4609–4625 · after FC05-C05-U063, FC05-C02-U059, FC05-C02-U051 · not formalized

For a continuous f:X→Y and sheaf F on X, f_* is left exact and preserves injectives; the Grothendieck spectral sequence for Γ_Y∘f_=Γ_X is E_2^{pq}=Hp(Y;R^qf_F)⇒H^{p+q}(X;F).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Leray spectral sequence for sheaf cohomology was found; P has direct images and sheaf cohomology but not this derived-composite spectral sequence.

Proposition 5.8.7 — Derived limits of a double tower

FC05-C05-U067 · §5.8 Grothendieck Spectral Sequences; pp. 150–152; L4627–4635 · after FC05-C05-U063, FC05-C03-U043, FC05-C03-U046, FC05-C03-U049 · not formalized

For a double tower A:I×I→Ab, lim_{I×I}=lim_i lim_j. The Grothendieck spectral sequence for these two inverse limits yields the stated short exact description of R¹lim, R²lim≅lim_i¹(lim_j¹A_{ij}), and R^nlim=0 for n≥3.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — P has inverse limits and derived-limit material, but without a Grothendieck spectral sequence no checked double-tower computation gives the stated R¹lim, R²lim, and higher vanishing bundle.

Definition — Exact couple

FC05-C05-U068 · §5.9 Exact Couples; pp. 153–159; L4649–4655 · after FC05-C01-U014, FC05-C02-U070 · in another Lean project

An exact couple is a pair (D,E) with maps i:D→D, j:D→E, k:E→D forming an exact triangle (kernel=image at each vertex), in modules or more generally an AB5 abelian category.

Formalized. cmu-phil/Spectral@3b078f5f1de251637decf04bd3fc8aa01930a6b3::algebra/exact_couple.hlean::exact_couple.exact_couple — The Apache-2.0 legacy Lean/HoTT development defines graded modules D,E with maps i,j,k and exactness at all three vertices, exactly the source exact-couple structure. It is not Mathlib-compatible and is preserved only as a revision-specific port source.

Searched: E

Definition 5.9.1 — Derived couple

FC05-C05-U069 · §5.9 Exact Couples; pp. 153–159; L4657–4679 · after FC05-C05-U068, FC05-C01-U002 · in another Lean project

For an exact couple, d=jk on E satisfies d²=0. The derived couple has D’=i(D), E’=H(E,d), with the induced maps i’,j’,k’; iterating gives D^r=irD and E^r=H(E{r-1}).

Formalized. cmu-phil/Spectral@3b078f5f1de251637decf04bd3fc8aa01930a6b3::algebra/exact_couple.hlean::exact_couple.derived_couple; derived_couple.d; D'; E'; i'; j'; k' — The same Apache-2.0 legacy Lean/HoTT file constructs d=jk, D'=im(i), E'=H(E,d), the induced maps, and proves the three exactness conditions, matching Weibel’s derived couple.

Searched: E

Proposition 5.9.2 — Spectral sequence from a bigraded exact couple

FC05-C05-U070 · §5.9 Exact Couples; pp. 153–159; L4699 · after FC05-C05-U069, FC05-C05-U002 · not formalized

If i,k,j have bidegrees (1,−1), (−1,0), and (−a,a), repeated derivation gives a homology spectral sequence starting at E^a with d^r of bidegree (−r,r−1). Morphisms of exact couples induce morphisms of spectral sequences.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — The legacy exact-couple development iterates derived couples, but it does not package morphisms of exact couples inducing morphisms of spectral sequences as required by the whole source proposition; P/H have no exact-couple owner.

Example 5.9.3 — Exact couple of a filtered complex

FC05-C05-U071 · §5.9 Exact Couples; pp. 153–159; L4701–4717 · after FC05-C05-U068, FC05-C05-U022, FC05-C01-U022 · not formalized

For a filtered chain complex C, the short exact sequences 0→F_{p-1}C→F_pC→F_pC/F_{p-1}C→0 give an exact couple with D^1_{pq}=H_{p+q}(F_pC) and E^1_{pq}=H_{p+q}(F_pC/F_{p-1}C).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked construction of the exact couple attached to a filtered complex was found.

Theorem 5.9.4 — Exact-couple and filtered-complex constructions agree

FC05-C05-U072 · §5.9 Exact Couples; pp. 153–159; L4719 · after FC05-C05-U071, FC05-C05-U024, FC05-C05-U031 · not formalized

For any filtered chain complex, the spectral sequence starting at E¹ from the exact couple 5.9.3 is naturally isomorphic to the spectral sequence of §5.4 starting at E⁰; both have the same subquotients Z_p^r/B_pr and differentials induced by d_C.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked theorem compares the exact-couple and filtered-complex spectral-sequence constructions; neither filtered construction is present.

Definition 5.9.5 — Convergence data of an exact couple

FC05-C05-U073 · §5.9 Exact Couples; pp. 153–159; L4727–4733 · after FC05-C05-U070, FC05-C02-U060 · not formalized

For a suitably bigraded exact couple, let H_n=colim_p D_{p,n-p} along i and F_pH_n be the image of the corresponding D-term. This is exhaustive and the associated E^∞ maps to gr_FH; weak convergence is characterized by Z^∞=k{-1}(0)=j(D).

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — The legacy repository has a separate bounded/convergent exact-couple framework, but not Weibel’s source convergence data with abutment colim D and the stated Z∞=k⁻¹(0)=j(D) criterion.

Definition — Bounded-below exact couple

FC05-C05-U074 · §5.9 Exact Couples; pp. 153–159; L4749 · after FC05-C05-U073 · not formalized

An exact couple is bounded below when for each total degree n there is f(n) with D_{pq}=0 whenever p<f(n); then the associated spectral sequence is bounded below.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked declaration matches Weibel’s total-degree bounded-below exact-couple predicate.

Classical Convergence Theorem 5.9.7

FC05-C05-U075 · §5.9 Exact Couples; pp. 153–159; L4751–4757 · after FC05-C05-U074, FC05-C05-U073 · not formalized

A bounded-below exact couple has a bounded-below spectral sequence converging to H_*=colim D. If in each total degree some D_{p,n-p}→H_n is an isomorphism, the spectral sequence is bounded and convergent.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — The legacy HoTT development proves convergence under its stronger bespoke is_bounded/convergent_exact_couple data, not the source theorem for every bounded-below exact couple with abutment colim D; no exact whole-row owner was found.

Application 5.9.8 — Exact couple from Tor of an exact complex

FC05-C05-U076 · §5.9 Exact Couples; pp. 153–159; L4761–4779 · after FC05-C05-U068, FC05-C02-U056, FC05-C01-U022, FC05-C05-U058 · not formalized

For an exact complex C of left R-modules with cycles Z_p and a right module M, the long exact Tor sequences of 0→Z_p→C_p→Z_{p-1}→0 form an exact couple with E^0_{pq}=Tor_q(M,C_p) and E^1_{pq}=H_p(Tor_q(M,C_*)). If C is bounded below, the associated hyperhomology sequence converges to zero.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked exact couple formed from the long exact Tor sequences of an exact complex, nor its zero-abutment hyperhomology convergence, was found.

Construction 5.9.9 — Bockstein spectral sequence

FC05-C05-U077 · §5.9 Exact Couples; pp. 153–159; L4781–4804 · after FC05-C05-U068, FC05-C05-U070 · not formalized

Fix a prime ℓ. Any long exact sequence …→E_{n+1}→H_n→^ℓH_n→E_n→… forms an exact couple whose associated spectral sequence starts at E^0=E; standard examples come from mod-ℓ homology, homotopy, group homology, or C/ℓC.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked Bockstein exact couple/spectral sequence with the source examples was found.

Proposition 5.9.10 — Bockstein pages and E^∞

FC05-C05-U078 · §5.9 Exact Couples; pp. 153–159; L4806–4816 · after FC05-C05-U077 · not formalized

For the Bockstein exact couple, each E_n^r fits into the stated exact sequence between a quotient of H_n and the ℓ^r-divisible ℓ-torsion in H_{n-1}; at E^∞ this becomes 0→H_n/(ℓH_n+T_n)→E_n^∞→Q_{n-1}→0, with T_n the ℓ-primary torsion and Q_n the infinitely ℓ-divisible part.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked description of Bockstein pages and E∞ in terms of ℓ-primary torsion/divisibility was found.

Corollary 5.9.11 — Bockstein convergence for finitely generated H

FC05-C05-U079 · §5.9 Exact Couples; pp. 153–159; L4832–4836 · after FC05-C05-U078 · not formalized

If every H_n is finitely generated and d_n=dim_Q(H_n⊗Q), then the Bockstein sequence stabilizes and E_n^{∞≅(Z/ℓ)}{d_n}.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked finite-generation stabilization theorem computing Bockstein E∞ as (ℤ/ℓ)^d was found.

Corollary 5.9.12 — Reading ℓ-primary summands from Bockstein survival

FC05-C05-U080 · §5.9 Exact Couples; pp. 153–159; L4838–4842 · after FC05-C05-U078, FC05-C05-U079 · not formalized

Classes surviving to E^r but not E^{r+1} detect exponent-ℓ classes in H_{n-1} divisible by ℓ^r but not ℓ^{r+1}; if j(y) dies precisely on page r, then y generates a direct summand Z/ℓ^r of H_n.

Not formalized. partial: adjacent spectral-sequence/homological infrastructure — No checked theorem reads exact ℓ-primary cyclic summands from Bockstein page survival/death as in the source corollary.