Chapter 10. The Derived Category
FC05 — Weibel, An Introduction to Homological Algebra.
This chapter contains 27 definitions, 11 theorems, 7 propositions, 8 lemmas, 18 corollaries, 20 examples, 13 constructions, 5 remarks, 5 conventions and 7 other statements.
Of the 121 statements checked against Lean, 24 are formalized somewhere and 97 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 97 | 80% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 24 | 20% | Mathlib states and proves it. |
| checked in total | 121 |
- Project-first search was performed at repository HEAD
f90173886bc881c2d43c0a7eb2d9fe7f110ac9a5. No project declaration owns a complete C10 source row under strict bundle semantics. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0 and directly project-compatible. The checked P interfaces cover the homotopy-category quotient and homology descent, mapping-cone and Verdier triangulated structures, categorical localization and fraction calculus, K-injective/K-projective Hom comparison, short-exact-sequence triangles, additive functors on homotopy categories, and generic localized shifted Hom. Every P target promoted in the C10 table was inspected at this exact revision. - Current Mathlib was refreshed on 2026-09-06 at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f, Apache-2.0, Lean 4.34.0-rc2. H addsMathlib/CategoryTheory/Functor/Derived/RightDerivedTriangulated.lean::Functor.isTriangulated_of_leftExtensionand its left-derived dual, but these are conditional generic criteria rather than an instantiation of Weibel’s total derived-functor bundles U055/U057. H still has no completed derived tensor/RHom, Grothendieck spectral sequence, derived sheaf direct-image/Leray, or stable-homotopy-spectrum package realizing the missing C10 bundles. - The bounded-derived support at P is asymmetric for the source’s bundled statements:
HomotopyCategory.PlusandDerivedCategory.Plusare developed explicitly, together with injective derivability andrightDerivedFunctorPlus, but the checked pin has no correspondingHomotopyCategory.Minus/DerivedCategory.MinusorBoundedchapter files. Therefore rows such as U004, U019, U040, U045, U050, and U062 that simultaneously assert the bounded, bounded-above, bounded-below, or both injective/projective halves are not partially credited. - P’s localization calculus has exact left/right fraction structures, equivalence relations, composition, map-equality criteria, and additive localization. However, U026 bundles the two-sided Ore and two-sided cancellation axioms as one multiplicative-system interface, while the checked API separates left and right calculus assumptions and does not package that whole source definition; U026 therefore remains unmatched. The local-smallness/filtered-colimit theorems U029–U032 likewise exceed the checked fraction infrastructure.
- P’s derived category gives exact K-injective and K-projective Hom-comparison interfaces (
CochainComplex.IsKInjective.Qh_map_bijectiveand the projective dual), so U049 is direct.ShortComplex.ShortExact.triangleOfSESwithtriangleOfSES_distinguisheddirectly owns U051. By contrast, the stronger bundled equivalence/existence statements U048/U050 and the zero-map criterion U052 are not inferred from adjacent localization machinery without a checked declaration of the whole source row. Mathlib/Algebra/Homology/Monoidal.leanandMathlib/Algebra/Homology/BifunctorHomotopy.leanprovide the ordinary total tensor/bifunctor and homotopy infrastructure, andMathlib/Algebra/Homology/HomotopyCategory/HomComplex.leanprovides the total Hom complex. These are not promoted for U068–U099 when the source row additionally asserts total-derived tensor/RHom, hypertor/hyperext recovery, change of rings, projection formula, derived composition, or spectral-sequence conclusions that the checked P/H API does not instantiate.- U079 is routed through
Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean::Localization.SmallShiftedHomandSmallShiftedHom.equiv: for arbitrary complexes this is exactly a small representative of the shifted Hom type in the localization, i.e. the source definition of hyperext. This is not conflated with the later object-levelCategoryTheory.Abelian.ExtAPI. LC=50500fadbbfa205092dd7fb07a59a05eea23ce66is the audited 2026-09-06 HEAD ofdagurtomas/LeanCondensed, Apache-2.0, Lean 4.32.0-rc1. ItsLeanCondensed/Mathlib/Algebra/Homology/DerivedCategory/TwoVariable.leancontains substantial two-variable K-projective/K-injective/K-flat derived-functor work, but the audited file still has fivesorryobligations, including a key enough-K-projectives equivalence. It is therefore incomplete reference evidence, not a route for the total-derived tensor/RHom rows.SP=3b078f5f1de251637decf04bd3fc8aa01930a6b3is the audited HEAD of the historical Apache-2.0 HLean repositorycmu-phil/Spectral. It contains prespectrum/spectrum, stable homotopy-group, suspension, and spectrification constructions inspectrum/basic.hleanandspectrum/spectrification.hlean, but the development contains unfinishedsorryproofs and does not supply the complete category/CW-localization/triangulation/HZ-module bundles U100–U121. No such row is upgraded from this partial historical development.- Indexed GitHub code search and open Mathlib PR search on 2026-09-06 found no completed Lean implementation closing the total-derived tensor/RHom or stable-spectrum gaps. TauCeti at its refreshed C09 baseline
T=0857cbca8b6a91dd22680eba45ecc284c14d8325likewise supplied no complete C10 row beyond the Mathlib interfaces already audited. Ndenotes dated 2026-09-06 negative evidence after project-first inspection, P, H/current Mathlib, TauCeti, LeanCondensed, the historical Spectral development, open Mathlib work, indexed GitHub search, and relevant external Lean repositories. A prerequisite, generic construction not instantiated to the source theorem, mathematically derivable consequence, incomplete development, differently scoped theorem, or proper subset of a bundled row is not credited as that row’s route.
Construction/comparison — two-stage construction of the derived category
For an abelian category A, first pass from Ch(A) to K(A) by identifying chain-homotopic maps, then localize K(A) by inverting quasi-isomorphisms to obtain D(A).
Formalized. Mathlib/Algebra/Homology/HomotopyCategory.lean::HomotopyCategory, HomotopyCategory.quotient; Mathlib/Algebra/Homology/DerivedCategory/Basic.lean::DerivedCategory, DerivedCategory.Qh — Pinned Mathlib implements the homotopy category as the quotient of complexes by chain homotopy and the derived category as the quasi-isomorphism localization of that homotopy category, matching the source two-stage construction.
Searched: P
Definition — homotopy category K(A)
K(A) has the same cochain complexes as Ch(A), with morphisms chain maps modulo chain homotopy; the quotient functor Ch(A)→K(A) is additive.
Formalized. Mathlib/Algebra/Homology/HomotopyCategory.lean::HomotopyCategory, HomotopyCategory.quotient, HomotopyCategory.eq_of_homotopy, HomotopyCategory.homotopyOfEq — Pinned Mathlib has the same complexes as objects, identifies quotient maps exactly by chain homotopy, and equips the quotient with its additive/preadditive structure, matching the source definition of K(A).
Searched: P
Construction — quotient subcategory associated to C⊂Ch(A)
For a full subcategory C of Ch(A), define the corresponding full subcategory of K(A) on the same complexes; its Hom sets are Hom_C/∼, and it is additive when C is closed under ⊕ and contains 0.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For a full subcategory C of Ch(A), define the corresponding full subcategory of K(A) on the same complexes; its Hom sets are Hom_C/∼, and it is additive when C is closed under ⊕ and contains 0. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Convention/notation — K^b(A), K^-(A), K^+(A)
Names the full homotopy subcategories of bounded, bounded-above, and bounded-below cochain complexes.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Names the full homotopy subcategories of bounded, bounded-above, and bounded-below cochain complexes. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Lemma 10.1.1
Cohomology of cochain complexes descends through chain homotopy to well-defined functors H^i:K(A)→A.
Formalized. Mathlib/Algebra/Homology/HomotopyCategory.lean::HomotopyCategory.homologyFunctor, HomotopyCategory.homologyFunctorFactors — The pinned homology functor is constructed by quotient-lifting ordinary complex homology through chain homotopy, exactly the source descent H^i:K(A)→A.
Searched: P
Proposition 10.1.2 (Universal property)
Any functor F:Ch(A)→D that sends chain-homotopy equivalences to isomorphisms factors uniquely through K(A).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Any functor F:Ch(A)→D that sends chain-homotopy equivalences to isomorphisms factors uniquely through K(A). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.1.3 (Triangles in K(A))
For u:A→B, the mapping-cone sequence defines a strict triangle; an exact triangle is a triangle isomorphic in K(A) to a strict triangle.
Formalized. Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean::HomotopyCategory.Pretriangulated.triangleh, mappingCone_triangleh_distinguished — Pinned Mathlib constructs the mapping-cone triangle in the homotopy category and proves it distinguished; distinguished triangles are closed under isomorphism, matching the strict/exact-triangle source interface.
Searched: P
Corollary 10.1.4
Every exact triangle A→B→C→A[-1] induces the displayed long exact cohomology sequence.
Formalized. Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean::Functor.homologySequenceδ, Functor.homologySequence_exact₁, Functor.homologySequence_exact₂, Functor.homologySequence_exact₃; Mathlib/Algebra/Homology/HomotopyCategory/HomologicalFunctor.lean::instance (n : ℤ) : (homologyFunctor C (ComplexShape.up ℤ) n).IsHomological — Pinned Mathlib makes homology on K(A) homological and supplies the connecting morphisms and exactness of the resulting bi-infinite homology sequence, exactly the source long exact sequence.
Searched: P
Example 10.1.5
The zero and identity endomorphisms of A give the basic exact triangles; cone(0)=A⊕A[-1], while cone(id_A) is zero in K(A).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: The zero and identity endomorphisms of A give the basic exact triangles; cone(0)=A⊕A[-1], while cone(id_A) is zero in K(A). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example 10.1.6 (Rotation)
Rotating an exact triangle produces exact triangles, with the standard sign on the translated map.
Formalized. Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean::HomotopyCategory.Pretriangulated.rotate_distinguished_triangle; Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean::Pretriangulated.rotate_distinguished_triangle — Pinned Mathlib proves the distinguished-triangle rotation axiom with the standard shifted/sign conventions used by the triangulated structure.
Searched: P
Remark 10.1.7
A short exact sequence of complexes need not itself extend to an exact triangle in K(A), although its long exact cohomology sequence is recovered from the mapping-cylinder triangle and quasi-isomorphisms.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A short exact sequence of complexes need not itself extend to an exact triangle in K(A), although its long exact cohomology sequence is recovered from the mapping-cylinder triangle and quasi-isomorphisms. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition — triangle in a category with translation
For a category K with automorphism T, a triangle on (A,B,C) is a triple A→B→C→T(A).
Formalized. Mathlib/CategoryTheory/Triangulated/Basic.lean::CategoryTheory.Pretriangulated.Triangle, Triangle.mk — Pinned Mathlib’s triangle is precisely a triple of maps X→Y→Z→X⟦1⟧ in a category with shift, matching the source definition up to the conventional choice of shift direction.
Searched: P
Definition — morphism of triangles
A morphism of triangles is a triple of maps making the four standard squares, including the translated square, commute.
Formalized. Mathlib/CategoryTheory/Triangulated/Basic.lean::CategoryTheory.Pretriangulated.TriangleMorphism, Triangle.homMk — Pinned Mathlib packages a morphism of triangles as three component maps satisfying the three structural commutative squares (with shift compatibility built into the final square), exactly the source interface.
Searched: P
Definition 10.2.1 (Verdier)
A triangulated category is an additive category with translation T and exact triangles satisfying TR1 (completion/isomorphism), TR2 (rotation), TR3 (morphisms), and TR4 (octahedral axiom).
Formalized. Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean::CategoryTheory.Pretriangulated; Mathlib/CategoryTheory/Triangulated/Triangulated.lean::CategoryTheory.IsTriangulated, CategoryTheory.Octahedron — Pinned Mathlib separates TR1–TR3 into Pretriangulated and the octahedral axiom into IsTriangulated; together these are the source Verdier triangulated-category structure.
Searched: P
Remark 10.2.2
Any exact triangle is determined up to isomorphism by any one of its maps; consequently the octahedral data are determined up to isomorphism by composable A→B→C.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Any exact triangle is determined up to isomorphism by any one of its maps; consequently the octahedral data are determined up to isomorphism by composable A→B→C. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Proposition 10.2.4
K(A) is a triangulated category with translation A↦A[-1] and the exact triangles of 10.1.3.
Formalized. Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean::instance : Pretriangulated (HomotopyCategory C (ComplexShape.up ℤ)); Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean::instance : IsTriangulated (HomotopyCategory C (ComplexShape.up ℤ)) — At the project pin the homotopy category of cochain complexes carries the mapping-cone pretriangulation and satisfies the octahedral axiom, exactly the source theorem that K(A) is triangulated.
Searched: P
Corollary 10.2.5
If a full subcategory C⊂Ch(A) is additive and closed under translation and mapping cones, its quotient subcategory of K(A) is triangulated; in particular K^b, K^-, K^+ are triangulated.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: If a full subcategory C⊂Ch(A) is additive and closed under translation and mapping cones, its quotient subcategory of K(A) is triangulated; in particular K^b, K^-, K^+ are triangulated. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.2.6
Defines a morphism of triangulated categories as an additive functor commuting with translation and preserving exact triangles; defines triangulated subcategories by full inclusion with inherited exact triangles.
Formalized. Mathlib/CategoryTheory/Triangulated/Functor.lean::CategoryTheory.Functor.IsTriangulated; Mathlib/CategoryTheory/Triangulated/Subcategory.lean::CategoryTheory.Triangulated.Subcategory — Pinned Mathlib formalizes functors preserving distinguished triangles and full subcategories with inherited triangulated structure, matching the two source definitions.
Searched: P
Example/comparison — standard triangulated subcategories
K^b(A), K^+(A), and K^-(A), and more generally quotients from Corollary 10.2.5, are triangulated subcategories of K(A).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: K^b(A), K^+(A), and K^-(A), and more generally quotients from Corollary 10.2.5, are triangulated subcategories of K(A). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.2.7
A covariant cohomological functor H:K→A is additive and sends each exact triangle to the associated long exact sequence H(T^i−); notation Hi(A)=H(TiA).
Formalized. Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean::CategoryTheory.Functor.IsHomological, Functor.homologySequenceδ, Functor.homologySequence_exact₁, Functor.homologySequence_exact₂, Functor.homologySequence_exact₃ — Mathlib uses the name IsHomological for the covariant convention used here; it is additive and sends distinguished triangles to exact long sequences with the shifted connecting maps, exactly the source cohomological-functor contract.
Searched: P
Example 10.2.8 (Hom)
For every X in a triangulated category K, Hom_K(X,−) is a cohomological functor to Ab.
Formalized. Mathlib/CategoryTheory/Triangulated/Yoneda.lean::instance (A : Cᵒᵖ) : (preadditiveCoyoneda.obj A).IsHomological, instance (B : C) : (preadditiveYoneda.obj B).IsHomological — Pinned Mathlib proves the additive representable and corepresentable Hom functors homological; the covariant Hom_K(X,-) instance is the source example.
Searched: P
Definition — derived category D(A)
D(A) is defined as Q^{-1}K(A), the localization of K(A) at all quasi-isomorphisms Q.
Formalized. Mathlib/Algebra/Homology/DerivedCategory/Basic.lean::CategoryTheory.DerivedCategory, DerivedCategory.Qh, instance : Qh.IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) — Pinned Mathlib defines D(A) by localizing the homotopy category at quasi-isomorphisms and registers the localization universal property, exactly the source definition.
Searched: P
Definition 10.3.1
A localization S^{-1}C is a category with q:C→S^{-1}C sending S to isomorphisms and universal for functors that invert S.
Formalized. Mathlib/CategoryTheory/Localization/Predicate.lean::CategoryTheory.Functor.IsLocalization; Mathlib/CategoryTheory/Localization/Basic.lean::CategoryTheory.Localization.lift, CategoryTheory.Localization.fac — Pinned Mathlib’s IsLocalization is the universal functorial inversion property: the localizer inverts the chosen class and every inverting functor factors through it, matching the source definition.
Searched: P
Examples 10.3.2
K(A) is the localization of Ch(A) at chain-homotopy equivalences; equivalently D(A) can be viewed as the localization of Ch(A) directly at quasi-isomorphisms.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: K(A) is the localization of Ch(A) at chain-homotopy equivalences; equivalently D(A) can be viewed as the localization of Ch(A) directly at quasi-isomorphisms. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example/comparison — Set-Theoretic Remark 10.3.3
Localizations exist automatically for small C or set-sized S, whereas localization at a proper class can require universe/set-theoretic control.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Localizations exist automatically for small C or set-sized S, whereas localization at a proper class can require universe/set-theoretic control. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.3.4
A multiplicative system S contains identities, is closed under composition, satisfies the two-sided Ore condition, and satisfies the stated two-sided cancellation condition.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A multiplicative system S contains identities, is closed under composition, satisfies the two-sided Ore condition, and satisfies the stated two-sided cancellation condition. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example/comparison — Prototype 10.3.5 (Localizations of rings)
A multiplicative subset of a commutative ring, or a central subset more generally, gives a multiplicative system in the one-object category; in the noncentral case this matches the denominator-set condition.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A multiplicative subset of a commutative ring, or a central subset more generally, gives a multiplicative system in the one-object category; in the noncentral case this matches the denominator-set condition. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Construction — left fractions and their equivalence
A left fraction X←X₁→Y with denominator in S represents a prospective localized morphism; equivalence is defined by a common refinement, yielding classes Hom_S(X,Y).
Formalized. Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean::CategoryTheory.MorphismProperty.LeftFraction, LeftFractionRel, equivalenceLeftFractionRel — Pinned Mathlib represents localized arrows by left fractions and quotients them by the common-refinement relation, exactly the source construction of Hom_S(X,Y).
Searched: P
Definition — Set-Theoretic Considerations 10.3.6
S is locally small on the left when each target X admits a set S_X cofinal, in the stated sense, among S-morphisms into X.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: S is locally small on the left when each target X admits a set S_X cofinal, in the stated sense, among S-morphisms into X. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Construction — HomS as a filtered colimit
Under local smallness, Hom_S(X,Y) is a set, realized as the colimit of Hom_C(−,Y) over a small filtered denominator category S_X.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Under local smallness, Hom_S(X,Y) is a set, realized as the colimit of Hom_C(−,Y) over a small filtered denominator category S_X. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Construction — composition of fractions
The Ore condition supplies common denominators, defining associative composition on equivalence classes of fractions with identity X=X=X; hence the localized category has the same objects as C.
Formalized. Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean::CategoryTheory.MorphismProperty.LeftFraction.comp, CategoryTheory.Localization.exists_leftFraction — Under the left calculus of fractions, pinned Mathlib supplies common-denominator representatives and composition of left fractions/classes, realizing the source localized-category composition.
Searched: P
Theorem — Gabriel–Zisman Theorem 10.3.7
For a locally small multiplicative system S, the fraction category S^{-1}C exists and satisfies the localization universal property; q sends f to the fraction with identity denominator.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For a locally small multiplicative system S, the fraction category S^{-1}C exists and satisfies the localization universal property; q sends f to the fraction with identity denominator. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.3.8
If S is locally small on the right, S^{-1}C may dually be constructed from right fractions t^{-1}g.
Formalized. Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean::CategoryTheory.MorphismProperty.RightFraction, CategoryTheory.Localization.exists_rightFraction — Pinned Mathlib contains the right-calculus dual of the left-fraction construction, matching the source right-fraction presentation.
Searched: P
Corollary 10.3.9
Parallel maps f,g:X→Y become equal in S^{-1}C exactly when they become equal after composition with a suitable denominator in S.
Formalized. Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean::CategoryTheory.MorphismProperty.map_eq_iff_postcomp, map_eq_iff_precomp — Pinned Mathlib characterizes equality after localization by equality after post- or precomposition with a denominator, exactly the source criterion (with both fraction orientations available).
Searched: P
Corollary 10.3.10
Hypothesis visible: C has a zero object and X is any object of C. The conclusion is missing after the colon in the frozen extraction; no conclusion is reconstructed here.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Hypothesis visible: C has a zero object and X is any object of C. The conclusion is missing after the colon in the frozen extraction; no conclusion is reconstructed here. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.3.11
If C is additive, then S^{-1}C is additive and the localization functor q is additive.
Formalized. Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean::CategoryTheory.Localization.preadditive, CategoryTheory.Localization.functor_additive — Pinned Mathlib constructs the preadditive structure on a localization satisfying a calculus of fractions and proves the localization functor additive, exactly the source additive-localization conclusion.
Searched: P
Definition 10.3.12 (Localizing subcategories)
For full B⊂C and multiplicative S with multiplicative restriction to B, B is localizing when S{-1}B→S{-1}C is fully faithful, identifying it with the full subcategory on B-objects.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For full B⊂C and multiplicative S with multiplicative restriction to B, B is localizing when S{-1}B→S{-1}C is fully faithful, identifying it with the full subcategory on B-objects. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Lemma 10.3.13
Characterizes localizing subcategories by equality of localized Hom colimits; gives left- and right-fraction sufficient cofinality criteria under corresponding local-smallness hypotheses.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Characterizes localizing subcategories by equality of localized Hom colimits; gives left- and right-fraction sufficient cofinality criteria under corresponding local-smallness hypotheses. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.3.14
If B is localizing and every C-object admits an S-map to an object of B, then S{-1}B≅S{-1}C; if S∩B consists of isomorphisms, then B itself is equivalent to S^{-1}C.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: If B is localizing and every C-object admits an S-map to an object of B, then S{-1}B≅S{-1}C; if S∩B consists of isomorphisms, then B itself is equivalent to S^{-1}C. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example 10.3.15
Assuming D(A) exists, K^b(A), K^+(A), K^-(A) are localizing for quasi-isomorphisms, and their localizations are the corresponding full derived subcategories D^b, D^+, D^-.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Assuming D(A) exists, K^b(A), K^+(A), K^-(A) are localizing for quasi-isomorphisms, and their localizations are the corresponding full derived subcategories D^b, D^+, D^-. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example 10.3.16
For a ring multiplicative system S, localizing mod-R at maps becoming isomorphisms after S^{-1}(−) yields a category equivalent to mod-S^{-1}R.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For a ring multiplicative system S, localizing mod-R at maps becoming isomorphisms after S^{-1}(−) yields a category equivalent to mod-S^{-1}R. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition/construction — multiplicative system arising from a cohomological functor
For cohomological H:K→A, let S be the maps inducing H^i-isomorphisms for all i; quasi-isomorphisms are the instance arising from H^0 on K(A).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For cohomological H:K→A, let S be the maps inducing H^i-isomorphisms for all i; quasi-isomorphisms are the instance arising from H^0 on K(A). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Proposition 10.4.1
If S arises from a cohomological functor, S is multiplicative; whenever S^{-1}K is formed it carries a triangulated structure for which K→S^{-1}K is a morphism of triangulated categories.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: If S arises from a cohomological functor, S is multiplicative; whenever S^{-1}K is formed it carries a triangulated structure for which K→S^{-1}K is a morphism of triangulated categories. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.4.2 (Universal property)
A morphism F:K→L of triangulated categories that inverts S factors uniquely through S^{-1}K, and the induced factor is again a morphism of triangulated categories.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A morphism F:K→L of triangulated categories that inverts S factors uniquely through S^{-1}K, and the induced factor is again a morphism of triangulated categories. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.4.3
D(A), D^b(A), D^+(A), and D^-(A) are triangulated categories in any universe in which they exist.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: D(A), D^b(A), D^+(A), and D^-(A) are triangulated categories in any universe in which they exist. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Proposition 10.4.4
D(A) exists and is triangulated for A=mod-R, Presheaves(X), or Sheaves(X), by local smallness of the quasi-isomorphism system.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: D(A) exists and is triangulated for A=mod-R, Presheaves(X), or Sheaves(X), by local smallness of the quasi-isomorphism system. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Remark 10.4.5 (Gabber)
The preceding existence argument extends to every well-powered abelian category satisfying AB5 and having a set of generators.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: The preceding existence argument extends to every well-powered abelian category satisfying AB5 and having a set of generators. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Lemma 10.4.6
If Y is a bounded-below cochain complex of injectives, every quasi-isomorphism t:Y→Z is a split injection in K(A).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: If Y is a bounded-below cochain complex of injectives, every quasi-isomorphism t:Y→Z is a split injection in K(A). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.4.7
For bounded-below injective I, Hom_D(X,I)≅Hom_K(X,I); dually, for bounded-above projective P, Hom_D(P,X)≅Hom_K(P,X).
Formalized. Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean::CochainComplex.IsKInjective.Qh_map_bijective; Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean::CochainComplex.IsKProjective.Qh_map_bijective — Pinned Mathlib proves that localization induces a bijection on Hom into K-injectives and out of K-projectives. Bounded-below injective and bounded-above projective complexes are the source special cases.
Searched: P
Theorem 10.4.8
If A has enough injectives, D^+(A) exists and is equivalent to K^+(I), bounded-below complexes of injectives; dually enough projectives gives D-(A)≅K-(P).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: If A has enough injectives, D^+(A) exists and is equivalent to K^+(I), bounded-below complexes of injectives; dually enough projectives gives D-(A)≅K-(P). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example 10.4.9
Every short exact sequence 0→A→B→C→0 of cochain complexes fits into an exact triangle in D(A), via the quasi-isomorphism cone(u)→C; this contrasts with 10.1.7 for K(A).
Formalized. Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean::CategoryTheory.ShortComplex.ShortExact.triangleOfSES, triangleOfSES_distinguished — Pinned Mathlib associates a distinguished triangle in the derived category to every short exact sequence of cochain complexes, exactly the source result.
Searched: P
Lemma/comparison — two zero criteria in D(A)
A complex X is isomorphic to 0 in D(A) iff X is exact; a chain map f:X→Y becomes zero in D(A) iff some quasi-isomorphism s:Y→Y′ makes sf null-homotopic.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A complex X is isomorphic to 0 in D(A) iff X is exact; a chain map f:X→Y becomes zero in D(A) iff some quasi-isomorphism s:Y→Y′ makes sf null-homotopic. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Construction — additive functors on homotopy categories
An additive F:A→B extends degreewise to Ch and K, commutes with translation and mapping cones, and hence gives a morphism K(A)→K(B) of triangulated categories.
Formalized. Mathlib/Algebra/Homology/HomotopyCategory.lean::CategoryTheory.Functor.mapHomotopyCategory; Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean::instance (G : C ⥤ D) [G.Additive] : (G.mapHomotopyCategory (ComplexShape.up ℤ)).IsTriangulated — Pinned Mathlib extends an additive functor degreewise to homotopy categories and proves the induced functor triangulated, matching the source mapping-cone/translation compatibility statement.
Searched: P
Convention/notation — localizing domain K and corresponding D
Fix K=K^+(A) or another localizing triangulated subcategory of K(A), and let D be the corresponding full subcategory of D(A); derived functors are formed on this pair.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Fix K=K^+(A) or another localizing triangulated subcategory of K(A), and let D be the corresponding full subcategory of D(A); derived functors are formed on this pair. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.5.1
A total right derived functor RF is a triangulated functor D→D(B) with ξ:qF⇒(RF)q universal among such natural transformations.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A total right derived functor RF is a triangulated functor D→D(B) with ξ:qF⇒(RF)q universal among such natural transformations. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Convention/notation — uniqueness and domain notation for RF
The universal property makes RF unique up to natural isomorphism and yields restriction transformations; notation records bounded/localizing domains such as R^bF, R^+F, and R_BF.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: The universal property makes RF unique up to natural isomorphism and yields restriction transformations; notation records bounded/localizing domains such as R^bF, R^+F, and R_BF. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition — total left derived functor
A total left derived functor LF has ξ:(LF)q⇒qF with the dual universal property; equivalently LF=R(Fop)op.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A total left derived functor LF has ξ:(LF)q⇒qF with the dual universal property; equivalently LF=R(Fop)op. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example/comparison — Exact Functors 10.5.2
An exact additive F:A→B preserves quasi-isomorphisms and descends to D(A)→D(B); in this sense F is both its own left and right derived functor.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: An exact additive F:A→B preserves quasi-isomorphisms and descends to D(A)→D(B); in this sense F is both its own left and right derived functor. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example 10.5.3
On bounded-below injective or bounded-above projective complexes, where the homotopy and derived categories agree, qFq^{-1} is simultaneously a left and right total derived functor.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: On bounded-below injective or bounded-above projective complexes, where the homotopy and derived categories agree, qFq^{-1} is simultaneously a left and right total derived functor. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.5.4
A complex X in the chosen K is F-acyclic when F(X) is acyclic, equivalently H^i(FX)=0 for all i.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A complex X in the chosen K is F-acyclic when F(X) is acyclic, equivalently H^i(FX)=0 for all i. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example 10.5.5 (F-acyclic complexes)
If every acyclic complex in K is F-acyclic, then F sends quasi-isomorphisms to quasi-isomorphisms and the localized functor Q^{-1}F is both the left and right derived functor.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: If every acyclic complex in K is F-acyclic, then F sends quasi-isomorphisms to quasi-isomorphisms and the localized functor Q^{-1}F is both the left and right derived functor. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Theorem — Existence Theorem 10.5.6
Enough injectives imply R^+F exists on D^+(A) and agrees with qF on bounded-below injective complexes; dually enough projectives imply L^-F exists on D^-(A) and agrees on projective complexes.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Enough injectives imply R^+F exists on D^+(A) and agrees with qF on bounded-below injective complexes; dually enough projectives imply L^-F exists on D^-(A) and agrees on projective complexes. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.5.7
For additive F between abelian categories, when enough injectives/projectives exist the hyper-derived functors are Hi(R+F(X)) and H{-i}(L-F(X)), respectively.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For additive F between abelian categories, when enough injectives/projectives exist the hyper-derived functors are Hi(R+F(X)) and H{-i}(L-F(X)), respectively. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Remark 10.5.8
Left/right exactness is unnecessary to define hyper-derived functors, but it is required on degree-zero objects to recover ordinary derived functors and degree-zero F.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Left/right exactness is unnecessary to define hyper-derived functors, but it is required on degree-zero objects to recover ordinary derived functors and degree-zero F. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Theorem — Generalized Existence Theorem 10.5.9
If K′⊂K is triangulated, every X∈K is quasi-isomorphic to an object of K′, and every exact complex in K′ is F-acyclic, then D′≅D and the derived functor computed on K′ is a right derived functor of F.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: If K′⊂K is triangulated, every X∈K is quasi-isomorphic to an object of K′, and every exact complex in K′ is F-acyclic, then D′≅D and the derived functor computed on K′ is a right derived functor of F. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.5.10
F has cohomological dimension n when R^iF=0 for i>n but R^nF≠0; dually, homological dimension n is defined using L_iF.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: F has cohomological dimension n when R^iF=0 for i>n but R^nF≠0; dually, homological dimension n is defined using L_iF. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.5.11
Finite cohomological dimension gives an unbounded RF on D(A) restricting to R^+F; finite homological dimension dually gives an unbounded LF restricting to L^-F.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Finite cohomological dimension gives an unbounded RF on D(A) restricting to R^+F; finite homological dimension dually gives an unbounded LF restricting to L^-F. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Construction — total tensor functor before deriving
For a fixed bounded-above right R-complex A, form F(B)=Tot^⊕(A⊗_R B); the existence theorem gives its left total derived functor on D^-.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For a fixed bounded-above right R-complex A, form F(B)=Tot^⊕(A⊗_R B); the existence theorem gives its left total derived functor on D^-. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.6.1
The total derived tensor product A⊗^L_R B is defined as the left derived functor of Tot^⊕(A⊗_R−), for bounded-above complexes in the stated module categories.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: The total derived tensor product A⊗^L_R B is defined as the left derived functor of Tot^⊕(A⊗_R−), for bounded-above complexes in the stated module categories. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Lemma 10.6.2
For bounded-above A,A′,B, a quasi-isomorphism A→A′ induces an isomorphism A⊗^L_R B→A′⊗^L_R B.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For bounded-above A,A′,B, a quasi-isomorphism A→A′ induces an isomorphism A⊗^L_R B→A′⊗^L_R B. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Theorem 10.6.3
Total tensor is a bifunctor D-(mod-R)×D-(R-mod)→D^-(Ab), and its degree −i cohomology is the hypertor group Tor_i^R(A,B).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Total tensor is a bifunctor D-(mod-R)×D-(R-mod)→D^-(Ab), and its degree −i cohomology is the hypertor group Tor_i^R(A,B). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.6.4
For modules A and B regarded in degree zero, H{-i}(A⊗L_R B) recovers the ordinary Tor_i^R(A,B).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For modules A and B regarded in degree zero, H{-i}(A⊗L_R B) recovers the ordinary Tor_i^R(A,B). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Remark 10.6.5
For sheaves of O_X-modules, enough flat objects suffice to construct the derived tensor product even when the category need not have enough projectives.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For sheaves of O_X-modules, enough flat objects suffice to construct the derived tensor product even when the category need not have enough projectives. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
10.6.6 (label type absent in extraction)
For f:R→S, Lf^=L(−⊗R S):D-(mod-R)→D-(mod-S); its cohomology gives Tor with S. Under finite flat dimension it extends unboundedly; restriction f** is exact and f_Lf^A≅A⊗^L_R S.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For f:R→S, Lf^=L(−⊗R S):D-(mod-R)→D-(mod-S); its cohomology gives Tor with S. Under finite flat dimension it extends unboundedly; restriction f** is exact and f_Lf^A≅A⊗^L_R S. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example/comparison — scheme variance comparison
For a morphism of ringed spaces, inverse image behaves like extension of scalars, while direct image generally requires a right-derived functor; the paragraph records the resulting f^/f_ variance convention.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For a morphism of ringed spaces, inverse image behaves like extension of scalars, while direct image generally requires a right-derived functor; the paragraph records the resulting f^/f_ variance convention. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Lemma 10.6.7
For a homomorphism of commutative rings f:R→S, derived extension of scalars is monoidal: Lf^*A⊗^L_S LfB≅Lf^(A⊗L_R B).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For a homomorphism of commutative rings f:R→S, derived extension of scalars is monoidal: Lf^*A⊗^L_S LfB≅Lf^(A⊗L_R B). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
10.6.8 (label type absent in extraction)
For a space X, writes D(X) for the derived category of sheaves; constructs R^+Γ and hypercohomology, and for f:X→Y constructs R^+f_*. Under noetherian finite-Krull-dimension hypotheses these extend to unbounded derived categories.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For a space X, writes D(X) for the derived category of sheaves; constructs R^+Γ and hypercohomology, and for f:X→Y constructs R^+f_*. Under noetherian finite-Krull-dimension hypotheses these extend to unbounded derived categories. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Construction — total Hom complex and its homotopy interpretation
For complexes A,B, the total cochain Hom complex satisfies H^n Hom•(A,B)≅Hom_K(A,TnB); total Hom is a bifunctor K(A)^op×K(A)→K(Ab).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For complexes A,B, the total cochain Hom complex satisfies H^n Hom•(A,B)≅Hom_K(A,TnB); total Hom is a bifunctor K(A)^op×K(A)→K(Ab). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.7.1
Hyperext is Extn(A,B)=Hom_D(A,TnB) for complexes in the derived category.
Formalized. Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean::CategoryTheory.Localization.SmallShiftedHom, CategoryTheory.Localization.SmallShiftedHom.equiv — For arbitrary complexes, pinned Mathlib’s localized shifted-Hom object is by definition the (small representative of the) morphism type from A to the shift of B in the localized category, exactly Weibel’s hyperext definition.
Searched: P
Construction — canonical Hom-to-hyperext comparison
Localization induces natural maps H^n Hom•(A,B)=Hom_K(A,TnB)→Hom_D(A,TnB)=Extn(A,B), and both sides are cohomological in the appropriate variables.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Localization induces natural maps H^n Hom•(A,B)=Hom_K(A,TnB)→Hom_D(A,TnB)=Extn(A,B), and both sides are cohomological in the appropriate variables. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.7.2
When A has enough injectives, RHom(A,B) is the right derived functor in the second variable of the total Hom complex, initially on the bounded-below derived category.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: When A has enough injectives, RHom(A,B) is the right derived functor in the second variable of the total Hom complex, initially on the bounded-below derived category. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Lemma 10.7.3
A quasi-isomorphism A→A′ induces an isomorphism RHom(A′,B)→RHom(A,B) in the first variable.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A quasi-isomorphism A→A′ induces an isomorphism RHom(A′,B)→RHom(A,B) in the first variable. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Theorem 10.7.4
Under enough injectives, or dually enough projectives, RHom is a bifunctor on the stated bounded derived categories, and Extn(A,B)≅Hn RHom(A,B).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Under enough injectives, or dually enough projectives, RHom is a bifunctor on the stated bounded derived categories, and Extn(A,B)≅Hn RHom(A,B). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.7.5
For objects A,B concentrated in degree zero, the hyperext groups agree with the ordinary Ext groups whenever the category has enough injectives or enough projectives.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For objects A,B concentrated in degree zero, the hyperext groups agree with the ordinary Ext groups whenever the category has enough injectives or enough projectives. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Convention/notation — R-linear refinement RHomR
For a commutative ring R, RHom_R(A,B) is regarded as an object of D(R), refining the underlying object in D(Ab).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For a commutative ring R, RHom_R(A,B) is regarded as an object of D(R), refining the underlying object in D(Ab). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Construction — change-of-rings map for RHom
For f:R→S, the universal property gives a natural map f_RHom_S(A,B)→RHom_R(f_A,f_*B).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For f:R→S, the universal property gives a natural map f_RHom_S(A,B)→RHom_R(f_A,f_*B). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Theorem 10.7.6
For commutative f:R→S, Lf^* is left adjoint to restriction f_* on the stated bounded derived categories; equivalently the derived Hom sets, and more strongly the RHom objects, satisfy the displayed adjunction isomorphism.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For commutative f:R→S, Lf^* is left adjoint to restriction f_* on the stated bounded derived categories; equivalently the derived Hom sets, and more strongly the RHom objects, satisfy the displayed adjunction isomorphism. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example/comparison — scheme comparison for derived Hom adjunction
For schemes the analogous RHom adjunction needs a localization argument and a finiteness restriction on the first argument; the source flags this as a limitation of the naive ring proof.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For schemes the analogous RHom adjunction needs a localization argument and a finiteness restriction on the first argument; the source flags this as a limitation of the naive ring proof. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example 10.8.1
For bounded-above complexes over composable rings, the two parenthesizations of a threefold derived tensor product are naturally isomorphic.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For bounded-above complexes over composable rings, the two parenthesizations of a threefold derived tensor product are naturally isomorphic. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Theorem — Composition Theorem 10.8.2
Given composable triangulated functors G,F and existing right derived functors, there is a canonical natural transformation R(FG)⇒RF∘RG; under the stated good-subcategory hypotheses it is an isomorphism.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Given composable triangulated functors G,F and existing right derived functors, there is a canonical natural transformation R(FG)⇒RF∘RG; under the stated good-subcategory hypotheses it is an isomorphism. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.8.3 (Grothendieck spectral sequences)
For left exact G:A→B and F:B→C with enough injectives and the usual acyclicity hypothesis, R+(FG)≅R+F∘R^+G and the Grothendieck spectral sequence follows; finite cohomological dimension gives the unbounded version.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For left exact G:A→B and F:B→C with enough injectives and the usual acyclicity hypothesis, R+(FG)≅R+F∘R^+G and the Grothendieck spectral sequence follows; finite cohomological dimension gives the unbounded version. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Convention/notation — dual composition theorem
Subsequent applications use without further comment the dual isomorphism LF∘LG≅L(FG) when the hypotheses of the Composition Theorem hold.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Subsequent applications use without further comment the dual isomorphism LF∘LG≅L(FG) when the hypotheses of the Composition Theorem hold. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
10.8.5 (label type absent in extraction)
For f:R→S, bounded-above right R-complex A, and left S-complex B, the Composition Theorem gives Lf^A⊗^L_S B≅A⊗^L_R f_B; after restriction this is the projection formula in D(R).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For f:R→S, bounded-above right R-complex A, and left S-complex B, the Composition Theorem gives Lf^A⊗^L_S B≅A⊗^L_R f_B; after restriction this is the projection formula in D(R). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
10.8.6 (label type absent in extraction)
For ring maps R→S→T, derived extension of scalars composes: (Lg)(Lf^)A≅L(gf)*A; this is the derived-category form underlying the indicated Tor spectral sequence.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For ring maps R→S→T, derived extension of scalars composes: (Lg)(Lf^)A≅L(gf)*A; this is the derived-category form underlying the indicated Tor spectral sequence. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Theorem 10.8.7
For commutative R and bounded-above B, −⊗^L_R B is left adjoint to RHom_R(B,−) on the stated bounded derived categories; the theorem records the RHom-level isomorphism and its unit and counit.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For commutative R and bounded-above B, −⊗^L_R B is left adjoint to RHom_R(B,−) on the stated bounded derived categories; the theorem records the RHom-level isomorphism and its unit and counit. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Construction/comparison — change-of-rings RHom composition
For f:R→S, because Hom_R(S,−) preserves injectives, RHom_S(A,RHom_R(S,B))≅RHom_R(f_*A,B); this is the derived form underlying the base-change-for-Ext spectral sequence.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For f:R→S, because Hom_R(S,−) preserves injectives, RHom_S(A,RHom_R(S,B))≅RHom_R(f_*A,B); this is the derived form underlying the base-change-for-Ext spectral sequence. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
10.8.8 (label type absent in extraction)
For f:X→Y, the Leray spectral sequence is promoted to RΓ(X,F)≅RΓ(Y,Rf_*F) on D^+(X), and on unbounded D(X) when the spaces satisfy the stated noetherian finite-Krull-dimension hypotheses.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For f:X→Y, the Leray spectral sequence is promoted to RΓ(X,F)≅RΓ(Y,Rf_*F) on D^+(X), and on unbounded D(X) when the spaces satisfy the stated noetherian finite-Krull-dimension hypotheses. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Lemma 10.8.9
For continuous X→Y→Z, direct image sheaves compose strictly: (gf)F=g(f_*F).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For continuous X→Y→Z, direct image sheaves compose strictly: (gf)F=g(f_*F). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.8.10
The preceding identity derives to R(gf)F≅Rg(Rf_*F) on D^+(X), and unboundedly under the stated noetherian finite-dimensional hypotheses.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: The preceding identity derives to R(gf)F≅Rg(Rf_*F) on D^+(X), and unboundedly under the stated noetherian finite-dimensional hypotheses. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.9.1
A spectrum E is a sequence of based spaces E_n with based homeomorphisms E_n≅ΩE_{n+1}; compatible level maps form the category S, with the one-point spectrum as zero object and levelwise products.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A spectrum E is a sequence of based spaces E_n with based homeomorphisms E_n≅ΩE_{n+1}; compatible level maps form the category S, with the one-point spectrum as zero object and levelwise products. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Construction — Looping and Delooping 10.9.2
Defines ΩE levelwise and Ω^{-1}E by reindexing E_{n+1}; Ω and Ω^{-1} are inverse automorphisms of S, with Ω^{-1} serving as translation in the stable category.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Defines ΩE levelwise and Ω^{-1}E by reindexing E_{n+1}; Ω and Ω^{-1} are inverse automorphisms of S, with Ω^{-1} serving as translation in the stable category. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example 10.9.3 (Sphere spectra)
Constructs the n-sphere spectrum S^n by stabilization (S^n)_p=colim_i Ω^i S^{n+p+i} and records ΩpSn=S^{n-p} for all integers n,p.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Constructs the n-sphere spectrum S^n by stabilization (S^n)_p=colim_i Ω^i S^{n+p+i} and records ΩpSn=S^{n-p} for all integers n,p. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.9.4 (The stable category)
Defines π_nE, weak homotopy equivalences of spectra as π_*-isomorphisms, and the stable homotopy/topological derived category D(S)=W̃^{-1}S.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Defines π_nE, weak homotopy equivalences of spectra as π_*-isomorphisms, and the stable homotopy/topological derived category D(S)=W̃^{-1}S. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.9.5
A prespectrum is a sequence D_n with structure maps SD_n→D_{n+1}, equivalently D_n→ΩD_{n+1}; defines functions of prespectra, the category P, the forgetful S→P, and CW prespectra.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A prespectrum is a sequence D_n with structure maps SD_n→D_{n+1}, equivalently D_n→ΩD_{n+1}; defines functions of prespectra, the category P, the forgetful S→P, and CW prespectra. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
10.9.6 (label type absent in extraction)
Defines spectrification Ω^∞:P→S on CW prespectra by (Ω^∞D)_n=colim_i Ω^iD_{n+i}, with structure maps induced by index shift.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Defines spectrification Ω^∞:P→S on CW prespectra by (Ω^∞D)_n=colim_i Ω^iD_{n+i}, with structure maps induced by index shift. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition — CW spectrum and SCW
A CW spectrum is a spectrum Ω^∞D for some CW prespectrum D; S_CW is the full subcategory of S on CW spectra.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A CW spectrum is a spectrum Ω^∞D for some CW prespectrum D; S_CW is the full subcategory of S on CW spectra. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example/comparison — Analogy 10.9.7
Compares prespectra/spectra with presheaves/sheaves: the source states Ω^∞ is left adjoint to the forgetful functor, paralleling sheafification; it uses this analogy to transport standard constructions from prespectra to spectra.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Compares prespectra/spectra with presheaves/sheaves: the source states Ω^∞ is left adjoint to the forgetful functor, paralleling sheafification; it uses this analogy to transport standard constructions from prespectra to spectra. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example 10.9.8 (Coproduct)
The wedge of prespectra is levelwise wedge; applying Ω^∞ gives the wedge/coproduct of spectra.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: The wedge of prespectra is levelwise wedge; applying Ω^∞ gives the wedge/coproduct of spectra. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Example 10.9.9 (Suspension)
Defines suspension SE by spectrifying the levelwise suspended prespectrum and records the natural weak equivalence Ω^{-1}E→SE.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Defines suspension SE by spectrifying the levelwise suspended prespectrum and records the natural weak equivalence Ω^{-1}E→SE. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition 10.9.10 (Homotopy category)
Defines the cylinder spectrum by spectrification, homotopy of spectrum maps through the cylinder, homotopy classes [E,F], the homotopy category K(S), and its CW full subcategory K(S_CW).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Defines the cylinder spectrum by spectrification, homotopy of spectrum maps through the cylinder, homotopy classes [E,F], the homotopy category K(S), and its CW full subcategory K(S_CW). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Proposition 10.9.11
K(S) is an additive category; each [E,F] is an abelian group and composition distributes over addition.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: K(S) is an additive category; each [E,F] is an abelian group and composition distributes over addition. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.9.12
The natural map E∨F→E×F is an isomorphism in K(S).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: The natural map E∨F→E×F is an isomorphism in K(S). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Proposition 10.9.13
Every spectrum E admits a natural weak homotopy equivalence C→E from a CW spectrum C; hence K(S_CW) is localizing in K(S).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Every spectrum E admits a natural weak homotopy equivalence C→E from a CW spectrum C; hence K(S_CW) is localizing in K(S). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Theorem — Whitehead’s Theorem 10.9.14
If C is a CW spectrum, every weak equivalence E→F induces [C,E]≅[C,F]; consequently every weak equivalence between CW spectra is a homotopy equivalence.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: If C is a CW spectrum, every weak equivalence E→F induces [C,E]≅[C,F]; consequently every weak equivalence between CW spectra is a homotopy equivalence. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Corollary 10.9.15
The stable homotopy category D(S) exists and is equivalent to the homotopy category K(S_CW) of CW spectra.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: The stable homotopy category D(S) exists and is equivalent to the homotopy category K(S_CW) of CW spectra. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition/construction — Mapping Cones 10.9.16
For u:E→F, spectrify the levelwise topological mapping cones to define cone(u); the resulting E→F→cone(u)→SE is the Puppe sequence, and a cofibration sequence is any triangle isomorphic to a Puppe sequence.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: For u:E→F, spectrify the levelwise topological mapping cones to define cone(u); the resulting E→F→cone(u)→SE is the Puppe sequence, and a cofibration sequence is any triangle isomorphic to a Puppe sequence. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Definition — homotopy-commutative diagram
A diagram of spectra is homotopy commutative when it commutes in K(S).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: A diagram of spectra is homotopy commutative when it commutes in K(S). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Proposition 10.9.17
Every homotopy-commutative square of spectra can be replaced by a diagram whose lower square commutes strictly, after replacing one spectrum by a mapping-cylinder homotopy equivalent spectrum.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Every homotopy-commutative square of spectra can be replaced by a diagram whose lower square commutes strictly, after replacing one spectrum by a mapping-cylinder homotopy equivalent spectrum. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Theorem 10.9.18
K(S_CW), with translation given by suspension/delooping and cofibration sequences as exact triangles, is a triangulated category.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: K(S_CW), with translation given by suspension/delooping and cofibration sequences as exact triangles, is a triangulated category. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Construction — Geometric Realization 10.9.19
Using Dold–Kan and good truncation, constructs a realization functor Ch(Ab)→S_CW that sends quasi-isomorphisms to weak equivalences and shifts to loopings, hence induces D(Ab)→D(S).
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: Using Dold–Kan and good truncation, constructs a realization functor Ch(Ab)→S_CW that sends quasi-isomorphisms to weak equivalences and shifts to loopings, hence induces D(Ab)→D(S). Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.
Vista 10.9.20
With HZ the realization of Z, the source records the equivalence of D(Ab) with the stable category of HZ-module spectra, carrying derived tensor product to the smash product over HZ.
Not formalized. none; partial adjacent homotopy, triangulated, localization, derived-functor, tensor/Hom, sheaf, or historical stable-spectrum infrastructure only — As of 2026-09-06, no checked A/P/H/external/open/indexed Lean declaration realizes the whole source bundle: With HZ the realization of Z, the source records the equivalence of D(Ab) with the stable category of HZ-module spectra, carrying derived tensor product to the smash product over HZ. Under strict bundle semantics, adjacent prerequisites, a generic construction not instantiated to the source theorem, a narrower hypothesis set, an incomplete development, or a proper subset does not own the row.