Chapter 2. Derived Functors
FC05 — Weibel, An Introduction to Homological Algebra.
This chapter contains 18 definitions, 5 theorems, 4 propositions, 7 lemmas, 7 corollaries, 8 examples, 6 constructions and 27 other statements.
Of the 82 statements checked against Lean, 48 are formalized somewhere and 34 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 46 | 56% | Mathlib states and proves it. |
| not formalized | 34 | 41% | A documented search found no Lean statement of it anywhere. |
| in lean-categories | 1 | 1% | This repository states and proves it. |
| in another Lean project | 1 | 1% | Some other Lean development has it; using it means porting that code. |
| checked in total | 82 |
- Project-first search was performed at repo HEAD
f901738.LeanCategories/Homological/DerivedDimension.leanowns the source-facing higher-left-derived vanishing predicateLeanCategories.Homological.IsCoacyclicFor; this is the canonical project route for U041. Other C02 project homological files reexport or specialize Mathlib owners rather than replacing them. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. P directly supplies categorical projectives/injectives, enough-projective/enough-injective structures, projective and injective resolutions and comparison homotopies, generic left/right derived functors, intrinsic derived-category Ext and both resolution computations, adjunction/exactness machinery, sheaf stalk/skyscraper and (co)image functors, arbitrary (co)limits in abelian categories from products/coproducts, filtered categories, ModuleCat filtered colimits, AB5, and the Hom-complex/homotopy-category cohomology theorem. - Two source-shaped infrastructure assertions were compile-checked against P: abelian sheaves on a topological space infer
EnoughInjectivesthrough Mathlib’s Grothendieck-category machinery, and an abelian category with arbitrary coproducts (respectively products) infers all small colimits (respectively limits). These justify U036/U061/U063 without weakening their existence claims. - The source is explicitly written for an arbitrary associative ring with right and left modules. Mathlib’s standard
TensorProductand the monoidal/closed structure onModuleCat Rstill require a commutative scalar ring;TensorProduct.liftAddHomitself notes that the first action should be a right action but is currently represented using commutativity. Therefore the noncommutative tensor-Hom, tensor, Tor, tensor-complex, and Tor-balancing rows U031 and U054-U057/U074-U075 are not credited from commutative-base Mathlib. - Current Mathlib was rechecked at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f. Searches at H did not add a δ-functor abstraction, Horseshoe lemma, generic syzygy owner, noncommutative module tensor/Tor, Tor balancing, Acyclic Assembly Lemma, balanced-multivariable-functor definitions, or the derived direct-sum/filtered-colimit preservation theorems left unmatched here. - Open Mathlib PR search on 2026-09-06 for δ-functors, Horseshoe, Tor balancing, homology/colimit, and sheaf enough-injectives found no applicable open PR. Thus no C02 route is attributed to an open Mathlib PR.
leanprover-community/lean-liquid@087fffad55dc1dd8d54ab35c9816926a45b8c0fdwas rechecked at its current HEAD. Its legacy Lean 3src/for_mathlib/universal_delta_functor/basic.leanimplements a covariant cohomological δ-functor category, morphisms, universality, effaceability, anduniversal_of_effaceable, but the repository has no LICENSE/COPYING file, uses Lean 3.48 with Mathlib5947fb69058f2fa5ac8a4476182707a52f5cf2be, and does not directly implement the homological dual/source left-derived package. It is therefore evidence of prior Lean work but not an acceptablereference-portunder this mapping contract.- U071 has one exact revision-specific external owner:
TauCetiProject/TauCeti@a8e6879667d6e38093b899315881b4f7b8e4b55a, Apache-2.0, Leanv4.34.0-rc2, Mathlib5fcc6656b48daf74b23607447c65ea30934f1b8f.TauCeti/Algebra/Homology/ShortComplex/Colimit.lean::HomologicalComplex.preservesHomologyOfShapeproves that homology preserves any exact colimit shape. Specializing to a filtered shape in an AB5 category is exactly U071, so the row is a revision-specificreference-port, never pinned Mathlib. - Pinned
CategoryTheory/Monoidal/Tor.leanexplicitly records that the two Tor variable constructions are expected to be isomorphic but that this balancing has not been proved there. This is positive evidence for the strict negatives U057/U075 rather than grounds to count them as Mathlib coverage. - The older definition-only Weibel catalogue is not route authority. Its generic
Torand “balanced functor” hints lose the source’s noncommutative right/left-module generality and do not provide Weibel’s balanced-functor predicates; the Sweep-II rows here use the stricter checked interfaces instead. Ndenotes dated 2026-09-06 negative evidence after project-first inspection, P, H/current Mathlib, open-PR search where relevant, and targeted external Lean search. Adjacent primitives, commutative-only implementations of arbitrary-ring rows, or one component of a bundled source statement are not credited under strict bundle semantics.
Definition 2.1.1 — Homological and cohomological δ-functors
A graded family of additive functors with natural connecting maps satisfying long-exactness and naturality; negative degrees are set to zero.
Not formalized. partial: pinned long-exact homology sequences and connecting-map naturality — P/H have the ingredients for individual long exact sequences but no homological/cohomological δ-functor structure with graded functors and connecting natural transformations.
Searched: N
Example 2.1.2 — Homology and cohomology δ-functors
Homology on nonnegative chain complexes is homological; cohomology on nonnegative cochain complexes is cohomological.
Not formalized. partial: HomologicalComplex.HomologySequence — Homology/cohomology and their long exact sequences are pinned, but they are not bundled as objects of a δ-functor theory because U001 is absent.
Searched: N
Example 2.1.3 — p-torsion δ-functor
For abelian groups, T_0(A)=A/pA, T_1(A)={a:pa=0}, higher T_n=0; Snake Lemma supplies the connecting maps.
Not formalized. partial: ZMod; torsion submodules; snake lemma — The underlying quotient and p-torsion constructions exist, but no checked owner packages them with the source connecting maps as a δ-functor.
Searched: N
Generalization — r-torsion δ-functor over a ring
For r∈R, the functors M/rM and {m:rm=0} extend the p-torsion construction to R-modules.
Not formalized. partial: quotient modules; torsion-by-element APIs — P/H have the two module constructions but no checked δ-functor bundle for arbitrary r.
Searched: N
Vista/comparison — Preview identification with Tor
Records that the r-torsion δ-functor will be identified with Tor_*^R(R/r,-).
Not formalized. partial: commutative-base CategoryTheory.Tor — The source is over an arbitrary associative ring and identifies the r-torsion δ-functor with noncommutative Tor. Mathlib’s standard Tor specialization is built from the commutative-base monoidal module category, and no exact noncommutative owner was found.
Searched: N
Definition 2.1.4 — Morphisms and universal δ-functors
A morphism of δ-functors is degreewise natural and commutes with connecting maps; universality is unique extension from degree zero.
Not formalized. partial: natural transformations and connecting-map naturality — No P/H δ-functor category provides degreewise morphisms commuting with connecting maps or the source universal-extension predicate.
Searched: N
Example 2.1.5 — Homology/cohomology are universal δ-functors
Records the later result that the standard homology and cohomology δ-functors are universal.
Not formalized. partial: pinned homology/cohomology functors — The source universality statement depends on the absent δ-functor abstraction. The only external implementation checked is unlicensed legacy Lean 3 and is not an acceptable route.
Searched: N
Terminology — Satellite functors
When a functor extends to a universal δ-functor, the higher functors are called its left/right satellites.
Not formalized. partial: leftDerived; rightDerived — Mathlib has derived functors but no source satellite definition as the higher terms of a universal δ-functor.
Searched: N
Definition — Projective object
P is projective when maps P→C lift across every epimorphism B→C.
Formalized. CategoryTheory.Projective — Pinned Projective is the categorical lifting property against epimorphisms.
Proposition 2.2.1 — Projective modules are direct summands of free modules
An R-module is projective iff it is a direct summand of a free R-module.
Formalized. Module.Projective; direct-summand-of-free characterization in Algebra/Module/Projective.lean — Pinned module projectivity is equivalent to being a direct summand of a free module.
Example 2.2.2 — Nonfree projective modules
Gives nonfree projectives from product rings and tangent-bundle-type modules over coordinate rings.
Not formalized. partial: projective modules over product rings; vector-bundle/projective-module infrastructure — No checked P/H/current/external declaration realizes both source example families, in particular the tangent-bundle coordinate-ring example.
Searched: N
Definition — Enough projectives
An abelian category has enough projectives if every object receives an epimorphism from a projective object.
Formalized. EnoughProjectives; ModuleCat.enoughProjectives — The pinned predicate is exactly that every object admits an epimorphism from a projective object; module categories have the instance.
Lemma 2.2.3 — Projectivity detected by Hom exactness
M is projective iff Hom_A(M,-) is exact.
Formalized. projective exactness APIs in CategoryTheory/Preadditive/Projective/Basic.lean — Pinned projective-object APIs characterize projectivity by exactness/surjectivity of representable Hom.
Definition — Complex of projectives
A chain complex is a complex of projectives when every component is projective.
Formalized. ∀ n, Projective (K.X n); CochainComplex.isKProjective_of_projective — The source condition is represented directly by the degreewise Projective instances; bounded degreewise-projective complexes are promoted to K-projective complexes.
Definition 2.2.4 — Left and projective resolutions
A left resolution P→M is an exact augmented nonnegative complex; it is projective when each P_i is projective.
Formalized. ProjectiveResolution; HasProjectiveResolutions — Pinned projective resolutions are exact augmented nonnegative complexes with projective terms.
Lemma 2.2.5 — Existence of projective resolutions
Every module, and every object in an abelian category with enough projectives, has a projective resolution.
Formalized. HasProjectiveResolutions; EnoughProjectives.hasProjectiveResolutions — Enough projectives canonically supplies projective resolutions; module categories satisfy the hypotheses.
Comparison Theorem 2.2.6 — Maps lift to projective resolutions uniquely up to homotopy
A map M→N lifts from a projective resolution of M to any resolution of N; any two lifts are chain homotopic.
Formalized. ProjectiveResolution.lift; liftHomotopy; homotopyEquiv — Maps lift to projective resolutions and any two lifts are homotopic; projective resolutions are homotopy equivalent.
Porism 2.2.7 — Comparison theorem for projective complexes
The source need only be a complex of projectives with appropriate augmentation; the same existence/uniqueness-up-to-homotopy argument applies.
Formalized. CochainComplex.IsKProjective; isKProjective_of_projective; K-projective orthogonality — Pinned K-projective theory generalizes the porism: bounded complexes of projectives have maps into acyclic targets null-homotopic, which supplies the comparison existence/uniqueness mechanism beyond chosen resolutions.
Horseshoe Lemma 2.2.8 — Compatible projective resolutions for a short exact sequence
For 0→M′→M→M″→0 and projective resolutions of the ends, constructs P_n=P′_n⊕P″_n resolving M in a short exact sequence of complexes.
Not formalized. partial: projective resolutions; biproducts; short exact complexes — No Horseshoe construction or source-shaped compatible middle resolution was found in P/H/current Mathlib, open PRs, or targeted external Lean search.
Searched: N
Definition — Injective object
I is injective when maps A→I extend across every monomorphism A→B.
Formalized. CategoryTheory.Injective — Pinned Injective is exactly extension of maps across monomorphisms.
Definition — Enough injectives
An abelian category has enough injectives if every object embeds in an injective object; products of injectives are injective when products exist.
Formalized. EnoughInjectives; Injective (∏ᶜ c) instance — The pinned predicate is enough injectives, and arbitrary existing products of injectives are injective.
Baer’s Criterion 2.3.1 — Injectivity criterion for modules
A right R-module E is injective iff every map J→E from a right ideal J⊂R extends to R.
Formalized. Module.Baer; Module.Baer.iff_injective — Pinned Baer criterion is exactly extension from right ideals and is equivalent to module injectivity.
Corollary 2.3.2 — Injective modules over a PID are divisible
For R=Z or a PID, an R-module is injective iff it is divisible.
Not formalized. partial: Module.Baer; Module.Baer.of_divisible for ℤ — P proves the divisible-implies-injective construction for abelian groups and has generic Baer criterion, but no checked theorem/assembly covers the full source statement for arbitrary PIDs in both directions.
Searched: N
Example 2.3.3 — Injective divisible abelian groups
Q and Prüfer p-groups are injective; Q/Z is injective and decomposes into its p-primary Prüfer groups.
Not formalized. partial: AddCircle; Prüfer-subgroup infrastructure; divisible abelian groups — No checked P/H/current/external declaration packages Q, all Prüfer p-groups, and the decomposition of Q/Z into its p-primary Prüfer groups as the full source example.
Searched: N
Construction — Canonical map into a product of Q/Z
For an abelian group A, constructs the evaluation map A→∏_{Hom(A,Q/Z)}Q/Z; the subsequent exercise supplies the injectivity proof.
Formalized. Algebra/Category/Grp/EnoughInjectives.lean evaluation embedding into products of AddCircle (1 : ℚ) — Mathlib’s enough-injectives proof for abelian groups uses precisely the character/evaluation embedding into a product of copies of Q/Z.
Duality/lemma 2.3.4 — Injectives and projectives in the opposite category
I is injective in A iff it is projective in A^op, equivalently Hom_A(-,I) is exact.
Formalized. injective/projective opposite instances; representable-Hom exactness APIs — Pinned duality identifies injectives in A with projectives in Aᵒᵖ and gives exactness of Hom(-,I).
Definition 2.3.5 — Right and injective resolutions
A right resolution M→I^• is an exact augmented nonnegative cochain complex; it is injective if every I^i is injective.
Formalized. InjectiveResolution; HasInjectiveResolutions — Pinned injective resolutions are exact augmented nonnegative cochain resolutions with injective terms.
Lemma 2.3.6 — Existence of injective resolutions
If an abelian category has enough injectives, every object has an injective resolution.
Formalized. EnoughInjectives.hasInjectiveResolutions — Enough injectives supplies injective resolutions.
Comparison Theorem 2.3.7 — Maps lift to injective resolutions uniquely up to cochain homotopy
Dual comparison theorem for a resolution of the source and injective resolution of the target.
Formalized. InjectiveResolution.desc; descHomotopy; homotopyEquiv — The pinned dual comparison theorem gives lifts/descents uniquely up to cochain homotopy.
Construction/convention — Right R-action on HomAb(B,A)
For a left R-module B, Hom_Ab(B,A) becomes a right R-module by (fr)(b)=f(rb).
Not formalized. partial: coextendScalars contains the special coinduced action on Hom_Ab(R,-) — No checked generic owner equips Hom_Ab(B,A) with the source right R-action for an arbitrary left R-module B over a noncommutative ring.
Searched: N
Lemma 2.3.8 — Tensor–Hom adjunction over Ab
For right R-module M and abelian group A, Hom_Ab(M⊗_R B,A)≅Hom_R(M,Hom_Ab(B,A)) naturally.
Not formalized. partial: TensorProduct.liftAddHom explicitly notes the first action should be a right action but currently assumes a commutative scalar ring — Weibel uses a right R-module tensored with a left R-module for arbitrary associative R. P/H tensor products still require a commutative scalar ring, so the source adjunction is not represented at full generality.
Searched: N
Definition 2.3.9 — Adjoint functors
L:A→B and R:B→A are adjoint when Hom_B(LA,B)≅Hom_A(A,RB) naturally in both variables; L is left adjoint and R right adjoint.
Formalized. Adjunction; Adjunction.mkOfHomEquiv — Pinned adjunctions are exactly natural Hom equivalences with left/right adjoints.
Proposition 2.3.10 — Adjoints preserve injectives/projectives under exactness
A right adjoint to an exact functor preserves injectives; dually a left adjoint to an exact functor preserves projectives.
Formalized. PreservesProjectiveObjects.of_adjunction; PreservesInjectiveObjects.of_adjunction — An adjoint preserves projectives/injectives when the opposite adjoint is exact in the required direction, matching the source proposition.
Corollary 2.3.11 — Coinduced injective R-modules
If I is injective in Ab, Hom_Ab(R,I) is injective as an R-module.
Formalized. ModuleCat.coextendScalars; restrictCoextendScalarsAdj; ModuleCat.enoughInjectives — For ℤ → R, the right adjoint has carrier Hom_ℤ(R,I) with the coinduced R-action; exact restriction of scalars makes it preserve injectives.
Example 2.3.12 — Stalk and skyscraper constructions for sheaves
Defines the stalk F_x as a direct limit and the skyscraper sheaf x_*A; records the injective-sheaf strategy.
Formalized. topological stalkFunctor; skyscraperSheafFunctor; stalk-skyscraper adjunction — Pinned sheaf APIs define stalks as filtered colimits, skyscraper sheaves, and their adjunction, exactly the source ingredients.
Construction — Embedding a sheaf into a product of skyscraper sheaves
Uses stalk maps to form F→∏*x x**(I_x), with injective stalk targets, yielding enough injectives for sheaves in the main text.
Formalized. Grothendieck-category EnoughInjectives for abelian sheaves; stalk/skyscraper adjunction; products of injectives — Compile-checked at P: abelian sheaves have EnoughInjectives. The source stalk/skyscraper and product ingredients are separately pinned, so the stated embedding strategy is realizable without a new primitive.
Example 2.3.13 — Product functors k in functor categories
Assuming A is complete and has enough injectives, the example states the goal that A^I has enough injectives and constructs the additive functors k_*A(i)=∏_{Hom_I(i,k)}A. The adjunction and injective-embedding proof are assigned to Exercise 2.3.7 and are not promoted here.
Not formalized. partial: evaluationRightAdjoint has value ∏_{Hom(i,k)} A exactly as Weibel’s k_*A — P constructs the source k_* functor and its adjunction, but no checked P/H/current/external theorem supplies the full enough-injectives conclusion for A^I under exactly the source assumptions.
Searched: N
Construction — Left derived functors
For right exact F:A→B with enough projectives, choose P→A and define L_iF(A)=H_i(F(P)); L_0F(A)≅F(A).
Formalized. Functor.leftDerived; ProjectiveResolution.isoLeftDerivedObj — Pinned left derived functors are computed from projective resolutions and degree zero identifies with the original right-exact functor.
Lemma 2.4.1 — Independence of projective resolution
L_iF(A) is well defined up to canonical natural isomorphism, using comparison maps and chain-homotopy invariance.
Formalized. ProjectiveResolution.isoLeftDerivedObj; naturality lemmas — The pinned canonical isomorphism computes left derived objects from any projective resolution and is natural.
Corollary 2.4.2 — Higher left derived functors vanish on projectives
If A is projective then L_iF(A)=0 for i≠0.
Formalized. Functor.isZero_leftDerived_obj_projective — Higher left-derived functors vanish on projective objects.
Definition 2.4.3 — F-acyclic objects and resolutions
Q is F-acyclic when higher L_iF(Q) vanish; an F-acyclic resolution has F-acyclic terms.
Formalized. LeanCategories.Homological.IsCoacyclicFor — The project defines exactly vanishing of all positive left-derived functors. The source F-acyclic-resolution condition is the pointwise use of this predicate on resolution terms.
Lemma 2.4.4 — Functorial map on left derived functors
Any f:A′→A induces L_iF(f):L_iF(A′)→L_iF(A), independent of the chosen comparison lift.
Formalized. Functor.leftDerived; projective-resolution naturality — The derived object map is canonical and independent of comparison-lift choices.
Result (label absent in extraction) — LiF is an additive functor
The main-text proof verifies identity/composition and additivity for the maps L_iF(f). The expected 2.4.5 label/statement is absent from the extraction.
Formalized. additive instance for Functor.leftDerived — Pinned left-derived functors are additive functors, covering the source missing-label result.
Theorem 2.4.6 — Left derived functors form a homological δ-functor
Horseshoe resolutions turn a short exact sequence into a degreewise split exact sequence after F, giving the natural long exact derived-functor sequence.
Not formalized. partial: derived functors plus long-exact homology sequences — P/H do not bundle the left-derived family and connecting maps as a homological δ-functor; the source proof also depends on the absent Horseshoe row.
Searched: N
Definition/terminology — Syzygy
In an exact partial projective resolution, the terminal kernel M_m is called the m-th syzygy of A.
Not formalized. partial: kernels in projective resolutions — Pinned Mathlib can form the terminal kernel but exports no source-level syzygy definition/owner.
Searched: N
Theorem 2.4.7 — Universality of left derived functors
If A has enough projectives and F is right exact, L_*F is a universal homological δ-functor.
Not formalized. partial: Functor.leftDerived — No P/H universal-δ-functor abstraction exists. The external lean-liquid implementation is unlicensed legacy Lean 3 and therefore is not an acceptable reference route.
Searched: N
Construction 2.5.1 — Right derived functors
For left exact F with enough injectives, define RiF(A)=Hi(F(I^•)); identifies R^iF with the opposite-category left derived functors, with universality and acyclic-resolution consequences.
Not formalized. partial: Functor.rightDerived; injective-resolution computation — The construction and opposite-category comparison are pinned, but the source row also includes δ-functor universality and acyclic-resolution consequences. With universality absent, strict whole-row semantics leave this bundle unmatched.
Searched: N
Definition 2.5.2 — Ext functors
Ext_Ri(A,B)=Ri Hom_R(A,-)(B); in degree zero this is Hom_R(A,B).
Formalized. Abelian.Ext; Ext.addEquiv₀; enough-injectives/projectives computation APIs — Intrinsic derived-category Ext has degree-zero Hom and works in arbitrary abelian categories, including ModuleCat R for noncommutative R.
Construction — Right derived functors of contravariant left exact functors
Treat a contravariant F:A→B as covariant on A^op; if A has enough projectives, compute R^*F(A) from a projective resolution of A.
Formalized. ProjectiveResolution.extEquivCohomologyClass; opposite/projective Ext APIs — Pinned projective-resolution Ext computes the contravariant derived functor in the first variable.
Example 2.5.3 — Two-variable Ext preview
For fixed B, derived Hom_R(-,B) is previewed as naturally isomorphic to Ext_R^*(A,B) derived in the second variable.
Formalized. ProjectiveResolution.extEquivCohomologyClass; InjectiveResolution.extEquivCohomologyClass; intrinsic Abelian.Ext — Both projective- and injective-resolution constructions map naturally to the same intrinsic Ext groups, giving the source two-variable balance.
Application 2.5.4 — Sheaf cohomology as derived global sections
For X, Γ(F)=F(X) is left exact and Hi(X,F)=RiΓ(F).
Formalized. Sheaf.Γ; Functor.rightDerived; EnoughInjectives for abelian sheaves; Sheaf.H.equiv₀ — The source definition is directly represented as the right derived functors of the pinned global-sections functor; abelian sheaves have injective resolutions.
Theorem 2.6.1 — Adjoints and one-sided exactness
For additive L⊣R between abelian categories, L is right exact and R is left exact.
Formalized. adjunction preservation of finite colimits/limits; RightExactFunctor; LeftExactFunctor — Left adjoints preserve finite colimits and are right exact; right adjoints preserve finite limits and are left exact.
Reusable comparison — Derived functors of adjoints
Left adjoints admit left derived functors when the source has enough projectives; right adjoints admit right derived functors when the target has enough injectives.
Formalized. Functor.leftDerived; Functor.rightDerived; adjunction exactness — Once the relevant category has projective/injective resolutions, the pinned generic derived-functor constructors apply to the one-sided exact adjoints.
Application 2.6.2 — Tensor is a left adjoint and right exact
For a left R-module B, -⊗_R B is left adjoint to Hom_Ab(B,-), and similarly for bimodule targets; hence tensor is right exact.
Not formalized. partial: commutative-base ModuleCat monoidal closed structure — The source tensor adjunction is for right/left modules over arbitrary associative R. Mathlib’s standard module tensor/closed structure still requires CommRing R.
Searched: N
Proposition 2.6.3 — Bimodule tensor–Hom adjunction
For an R–S bimodule B and right S-module C, Hom_S(B,C) is a right R-module and Hom_S(A⊗_R B,C)≅Hom_R(A,Hom_S(B,C)).
Not formalized. partial: change-of-rings adjunctions; commutative-base tensor — No checked P/H/current/external owner realizes the full R-S bimodule tensor-Hom adjunction for arbitrary associative rings.
Searched: N
Definition 2.6.4 — Tor functors
Tor_n^R(A,B)=L_n(-⊗_R B)(A); Tor_0=A⊗B, computed by projective resolutions, with projective vanishing and bimodule-valued refinement.
Not formalized. partial: CategoryTheory.Tor on monoidal abelian categories; commutative ModuleCat specialization — Weibel’s Tor is for arbitrary associative R using right/left modules. P/H have no corresponding noncommutative tensor category, so the source construction is not covered at full generality.
Searched: N
Reusable comparison — Tor in the two variables
For an R–S bimodule, Tor inherits the S-module structure; deriving A⊗_R- in the other variable is previewed to give the same groups.
Not formalized. partial: CategoryTheory.Tor and Tor' — The pinned Tor file explicitly notes that the two variable constructions are expected to be isomorphic but that the balanced-functor theorem is not proved; the source also has noncommutative bimodule generality.
Searched: N
Application 2.6.5 — Sheafification–inclusion adjunction
The inclusion of sheaves into presheaves is the right adjoint of sheafification, explaining left exactness of inclusion; sheafification is in fact exact.
Formalized. sheafificationAdjunction; finite-limit preservation of sheafification — Pinned sheafification is left adjoint to inclusion; inclusion is left exact and sheafification preserves finite limits as well as colimits, hence is exact for abelian coefficients.
Application 2.6.6 — Direct/inverse image sheaves and higher direct images
Defines f_F(V)=F(f^{-1}V), inverse image by sheafifying a colimit presheaf, and names R^if_ the higher direct-image functors; no exercise-only adjunction claim is promoted.
Formalized. topological Sheaf.pushforward; Sheaf.pullback; sheaf pushforward/pullback adjunction; Functor.rightDerived — Pinned sheaf functors have the source formulas/adjunction. Applying the generic right-derived constructor to pushforward gives the named higher direct images once injective resolutions are available.
Application 2.6.7 — Diagonal functor and colimits
Defines Δ:A→A^I and colim_I F by the universal natural transformation F→Δ(colim F).
Formalized. Functor.const; colim; const-colim adjunction/universal cocones — The diagonal functor and colimit universal natural transformation are canonical pinned limit-category constructions.
Proposition 2.6.8 — Arbitrary sums characterize cocompleteness in an abelian category
An abelian category has all set-indexed direct sums iff it has all small colimits; constructs colim as a cokernel of maps between direct sums.
Formalized. has_colimits_of_hasCoequalizers_and_coproducts; abelian coequalizers; HasCoproducts — Compile-checked at P: an abelian category with arbitrary coproducts infers all small colimits; the converse is immediate.
Reusable examples/comparison — Cocomplete abelian categories
Ab, module, presheaf, and sheaf categories are cocomplete; infinite sheaf coproducts require sheafification; finite abelian groups are not cocomplete.
Not formalized. partial: cocompleteness of Ab, ModuleCat, presheaves, and sheaves — The positive examples are pinned, but no checked whole bundle includes the source noncocompleteness example for finite abelian groups together with the sheaf-coproduct comparison.
Searched: N
Variation 2.6.9 — Limits and completeness
Defines limits dually; lim is right adjoint to Δ and left exact; existence of all products characterizes completeness for abelian categories.
Formalized. products/equalizers to limits; lim; const-limit adjunction — Compile-checked at P: an abelian category with arbitrary products infers all small limits; lim is right adjoint to the diagonal and therefore left exact.
Adjoints and Limits Theorem 2.6.10 — Left adjoints preserve colimits; right adjoints preserve limits
For arbitrary categories, L⊣R carries existing colimits through L and existing limits through R.
Formalized. Adjunction.leftAdjoint_preservesColimits; rightAdjoint_preservesLimits — Pinned adjunction theory gives the full source theorem for arbitrary categories.
Corollary 2.6.11 — Derived left adjoints commute with direct sums
In a cocomplete abelian category with enough projectives, L_F(⊕A_i)≅⊕L_F(A_i) for a left adjoint F.
Not formalized. partial: left adjoints preserve coproducts; projective-resolution left derived functors — No checked P/H/current/open/external theorem proves the source natural isomorphism for all left-derived degrees under the stated hypotheses.
Searched: N
Corollary 2.6.12 — Tor commutes with direct sums
Tor_(A,⊕B_i)≅⊕Tor_(A,B_i).
Not formalized. partial: commutative-base Tor — Besides the noncommutative Tor gap, no checked owner gives the source arbitrary-direct-sum preservation theorem.
Searched: N
Definition 2.6.13 — Filtered categories, filtered colimits, directed systems
Defines filtered categories by common successors/equalizers of parallel arrows; filtered posets are directed and their colimits are direct limits.
Formalized. IsFiltered; IsFilteredOrEmpty; filtered colimit APIs — Pinned filtered categories use common cocones and equalizers of parallel arrows; filtered preorders are directed and their colimits are direct limits.
Lemma 2.6.14 — Element description of filtered module colimits
Every colimit element comes from one stage; an element from A_i dies iff it dies after some transition A_i→A_j.
Formalized. ModuleCat.FilteredColimits; Types.FilteredColimit.Rel; quotient model — Pinned module filtered colimits are explicit quotients of the disjoint union of stages, with the source representative and eventual-equality relation.
Theorem 2.6.15 — Filtered colimits of modules are exact
For filtered I, colim:(mod-R)^I→mod-R preserves monomorphisms as well as cokernels, hence is exact.
Formalized. ModuleCat.instAB5; HasExactColimitsOfShape for filtered shapes — Module categories over arbitrary rings satisfy AB5, hence filtered colimits are exact.
Definition — Grothendieck axiom AB5
An abelian category satisfies AB5 when it is cocomplete and filtered colimits are exact; module categories satisfy AB5.
Formalized. AB5; AB5OfSize; ModuleCat.instAB5 — Mathlib’s AB5 class is exactness of filtered colimits; combined with the pinned cocompleteness of module categories it realizes the source convention and example.
Reusable comparison — Homology commutes with filtered colimits under AB5
In module categories and analogous AB5 settings, exactness of filtered colimits lets homology commute with them.
Formalized. TauCetiProject/TauCeti@a8e6879667d6e38093b899315881b4f7b8e4b55a::TauCeti/Algebra/Homology/ShortComplex/Colimit.lean::HomologicalComplex.preservesHomologyOfShape — At current TauCeti HEAD the theorem says homology preserves any exact colimit shape. Under AB5 and a filtered indexing category this is exactly the source comparison. Repository is Apache-2.0, Lean v4.34.0-rc2, Mathlib 5fcc6656b48daf74b23607447c65ea30934f1b8f.
Searched: E
Corollary 2.6.16 — Derived left adjoints commute with filtered colimits
Under enough projectives and AB5, L_F(colim A_i)≅colim L_F(A_i) for filtered diagrams and left adjoint F.
Not formalized. partial: U071 reference theorem; left adjoints preserve colimits — No checked P/H/current/open/external theorem assembles the source left-derived filtered-colimit isomorphism under the stated hypotheses.
Searched: N
Corollary 2.6.17 — Tor commutes with filtered colimits
For filtered B:I→R-mod, Tor_(A,colim B_i)≅colim Tor_(A,B_i).
Not formalized. partial: filtered colimits exact; commutative-base Tor — The source uses arbitrary-ring Tor and a derived preservation result; neither the required noncommutative Tor owner nor the exact preservation theorem was found.
Searched: N
Tensor Product of Complexes 2.7.1 — Tensor product double and total complexes
For right-module complex P and left-module complex Q, defines P⊗_R Q with sign-trick vertical differential and its Tot^⊕ tensor product complex.
Not formalized. partial: commutative-base Algebra/Homology/Monoidal.lean — Pinned tensor complexes totalize degreewise tensor products only in the commutative-base monoidal module category; Weibel’s right/left arbitrary-ring tensor double complex is not represented.
Searched: N
Comparison/result (label absent in extraction) — Balancing Tor via a double complex
For projective resolutions P→A and Q→B, Tot(P⊗Q) maps by quasi-isomorphisms to A⊗Q and P⊗B, yielding the natural balancing isomorphism between the two left-derived tensor functors. The expected 2.7.2 label is absent.
Not formalized. partial: Tor; Tor' — Pinned Mathlib explicitly lacks the balancing isomorphism, and the source noncommutative double-complex proof has no checked external owner.
Searched: N
Acyclic Assembly Lemma 2.7.3 — Acyclicity criteria for total complexes
Exact rows/columns plus upper/right half-plane boundedness imply acyclicity of the appropriate product or direct-sum totalization; diagonal-bounded refinements are noted.
Not formalized. partial: direct-sum totalization; exactness/acyclicity APIs — No checked P/H/current/external theorem gives the source row/column exactness criteria for both product and direct-sum totalizations with the stated half-plane/diagonal hypotheses.
Searched: N
Hom Cochain Complex 2.7.4 — Hom double complex and product totalization
Defines Hom(P,I) with signed vertical differential and Tot^Π as the total Hom cochain complex; records convention dependence.
Formalized. HomComplex.Cochain; HomComplex.Cochain.d; product/dependent-function carrier — Pinned Hom-complex code uses the product over source degrees and the signed differential, exactly the source total Hom cochain complex.
Morphisms and Hom 2.7.5 — Cohomology of total Hom as homotopy classes
An n-cycle in Hom(C,D) is a chain map C→D[-n], boundaries are null-homotopic maps, so H^n Hom(C,D) is the group of chain-homotopy classes.
Formalized. HomComplex.CohomologyClass.equivHom — Pinned cohomology classes of the Hom complex are naturally equivalent to shifted morphisms in the homotopy category, i.e. chain-homotopy classes.
Theorem 2.7.6 — Balancing Ext
For all R-modules A,B, deriving Hom_R(A,-) in B or Hom_R(-,B) contravariantly in A gives naturally isomorphic Ext_R^n(A,B).
Formalized. intrinsic Abelian.Ext; projective/injective resolution extEquivCohomologyClass — The two resolution computations are naturally identified with the same intrinsic Ext group for arbitrary abelian categories.
Definition 2.7.7 — Right balanced multivariable functor
A left exact multivariable functor is right balanced when inserting an injective covariant argument or projective contravariant argument makes the remaining-variable functors exact.
Not formalized. partial: exact-functor and projective/injective APIs — No P/H/current/external declaration defines Weibel’s right-balanced multivariable functor predicate.
Searched: N
Definition/comparison — Left balanced functor
Dually defines left balanced right-exact functors; A⊗B is the prototype and its left derived functors in different variables are isomorphic.
Not formalized. partial: commutative-base tensor and Tor — No source balanced-functor abstraction is pinned, and the tensor prototype again requires arbitrary right/left module tensoring not available in Mathlib’s commutative-base monoidal module category.
Searched: N
Application 2.7.8 — External product for Tor
For commutative R, constructs Tor_i(A,B)⊗Tor_j(A′,B′)→Tor_{i+j}(A⊗A′,B⊗B′) using projective resolutions, comparison maps, and tensor products of cycles.
Not formalized. partial: commutative Tor and complex tensor APIs — No checked P/H/current/open/external Lean theorem constructs the source external product on Tor groups.
Searched: N