Chapter 1. Chain Complexes
FC05 — Weibel, An Introduction to Homological Algebra.
This chapter contains 19 definitions, 2 theorems, 3 propositions, 5 lemmas, 3 corollaries, 5 examples, 11 constructions, 1 remark and 19 other statements.
Of the 68 statements checked against Lean, 43 are formalized somewhere and 25 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 43 | 63% | Mathlib states and proves it. |
| not formalized | 25 | 37% | A documented search found no Lean statement of it anywhere. |
| checked in total | 68 |
- Project-first search was performed at repo HEAD
f901738(subsequently unchanged during this chapter audit).LeanCategories/Homological.leanreexports the canonical Mathlib homological stack andLeanCategories/Homological/Extensions.leanowns later extension material; no C01 source unit has a distinct project-owned implementation, so C01 has noproject-existingroute. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. P directly supplies homological/cohomological complexes, quasi-isomorphisms, support/truncation and shift machinery, exactness, snake/homology sequences, homotopies, mapping cones, Freyd–Mitchell, abelian full/functor categories, sheaves/sheafification, exact functors, and additive Yoneda. Source-shaped assemblies for U041 (QuasiIso φ ↔︎ (mappingCone φ).Acyclic) and U063 (all representable-Hom exactness tests imply exactness) were independently compiled against P. - Current Mathlib was rechecked at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f. Targeted current-source searches found no product totalization, algebraic mapping cylinder of a map, weakly-effaceable functor quotient, exponential-sequence sheaf counterexample, or packagedS ⥤ Llong-exact-sequence functor. Current additions therefore do not change the negative routes recorded here. - The older definition-only Weibel catalogue is not treated as route authority. In particular, its mapping-cylinder entry points to
HomologicalComplex.cylinder, which is a cylinder of a complex rather than Weibel’s cylinder of a map, and its split-complex entry conflates the weaker equationd=dsdwith a chain contractionds+sd=id; both overmatches are rejected here. - External search rechecked
deancureton/sphere-six-complex@895c0a0661501581c34d42fea3c553d4f0ee43b1(Apache-2.0, Leanv4.34.0-rc1, Mathlib fork revision97d303eb50436be7c4bac4388bdb49459ae9140b). It defines the canonical simplicial-to-singular chain map and the proposition that it is a quasi-isomorphism, but its proof files only reduce the assertion to additional cover-small quasi-isomorphism hypotheses and then special boundary-seven hypotheses; it does not prove the general triangulation/simplicial-realization comparison needed for U008. It is therefore negative evidence, not a reference port. - External effaceability search rechecked
leanprover-community/lean-liquid@087fffad55dc1dd8d54ab35c9816926a45b8c0fd. Itsuniversal_delta_functor/basic.leandefines effaceability of δ-functors for the universal-δ-functor theorem, not Weibel’s weakly-effaceable contravariant functors,W(M), or the localizing quotient of U064–U067. It is not a route for those rows. - External Yoneda search rechecked
mattrobball/BridgelandStability@b858822408838e40cf5077aea233dc1dc660c461; its exactness argument invokes Mathlib’sFunctor.reflects_exact_of_faithfulandpreadditiveYoneda, confirming the pinned owner rather than supplying a separate implementation. - Targeted GitHub Lean searches for map-level algebraic mapping cylinders, product totalizations, weakly-effaceable functors, bundled homology-sequence functors, and the source split-complex/counterexample interfaces returned no exact implementation.
Nis dated 2026-09-06 negative evidence after project, P, H/current, and these external searches. - Strict bundle semantics are used throughout: an adjacent theorem, a predicate without a proof, a stronger-but-different condition, or only part of a source comparison bundle does not receive a positive route.
Definition/convention — Exactness for module sequences
Fix an associative ring R; mod-R denotes right R-modules. A sequence A→B→C is exact at B when ker(g)=im(f).
Formalized. ShortComplex.moduleCat_exact_iff_range_eq_ker; LinearMap.exact_iff — For module maps, categorical exactness is equivalent to equality of range and kernel, exactly the source convention.
Definition 1.1.1 — Chain complex; cycles, boundaries, homology
A chain complex has d_n:C_n→C_{n-1} with d²=0; Z_n=ker d_n, B_n=im d_{n+1}, H_n=Z_n/B_n.
Formalized. HomologicalComplex; ChainComplex; HomologicalComplex.cycles; opcycles; homology — The differential-square-zero object, cycles/boundaries model, and homology quotient are all canonical pinned APIs.
Construction/category — Category Ch(mod-R) and chain maps
Chain maps are degreewise maps commuting with differentials; composition is degreewise, giving Ch(mod-R).
Formalized. HomologicalComplex; category instance; HomologicalComplex.Hom — Morphisms are degreewise maps commuting with differentials and compose degreewise.
Definition 1.1.2 — Quasi-isomorphism
A chain map is a quasi-isomorphism when it induces isomorphisms on every homology group.
Formalized. QuasiIso; HomologicalComplex.quasiIso_iff — QuasiIso is exactly isomorphism on every homology object.
Definition/convention — Cochain complexes and cohomology
Reindex C^n=C_{-n}; define cocycles, coboundaries, H^n, cochain maps, and quasi-isomorphisms dually.
Formalized. CochainComplex; HomologicalComplex.homology — The pinned upward complex convention supplies cochain complexes, maps, cohomology, and quasi-isomorphisms.
Definition/convention — Bounded complexes and standard subcategories
Defines bounded, bounded above/below, amplitude [a,b], and Ch_b, Ch_-, Ch_+, Ch_{≥0}; gives cochain analogues.
Formalized. HomologicalComplex.IsStrictlySupported; CochainComplex.IsStrictlyGE; IsStrictlyLE; ObjectProperty.FullSubcategory — Strict support on intervals/half-lines gives bounded, bounded-above/below, and amplitude subcategories; the same machinery applies after chain/cochain reindexing.
Application 1.1.3 — Simplicial homology
For a geometric simplicial complex, the alternating face map gives a simplicial chain complex; its homology is simplicial homology.
Not formalized. partial: AbstractSimplicialComplex; AlgebraicTopology.alternatingFaceMapComplex; simplicial-set homology — P/H formalize abstract/geometric simplicial complexes and simplicial-set chain homology separately, but no checked bridge sends a geometric simplicial complex to the source chain complex/homology. Targeted external search was negative.
Searched: N
Application 1.1.4 — Singular homology
The free module on singular k-simplices with alternating face differential gives S_(X); H_n(X;R)=H_n(S_(X)), with simplicial-to-singular quasi-isomorphism for triangulated X.
Not formalized. partial: singularChainComplexFunctor; simplicial-set homology; sSetTopAdj.unit — P/H have both theories but no theorem that a triangulation induces the source simplicial-to-singular quasi-isomorphism. deancureton/sphere-six-complex@895c0a0661501581c34d42fea3c553d4f0ee43b1 defines the desired comparison predicate and reduces special cases to extra cover-small quasi-isomorphism hypotheses; it does not prove the general theorem.
Searched: N
Definitions — Ab-categories and additive functors
An Ab-category has abelian-group Hom sets and bilinear composition; an additive functor preserves addition on Hom groups.
Formalized. Preadditive; Functor.Additive — Hom groups with bilinear composition and addition-preserving functors are the pinned categorical interfaces.
Definition/construction — Additive category; zero object, products and coproducts
An additive category is an Ab-category with finite products and coproducts; in Ch these are degreewise, hence Ch is additive.
Formalized. Preadditive; HasZeroObject; finite (co)products/biproducts; HomologicalComplex additive instances — Pinned additive-category infrastructure supplies zero objects and finite biproducts; chain-complex limits/colimits are degreewise.
Definitions/constructions — Subcomplexes, quotient complexes, degreewise kernels/cokernels
A subcomplex is degreewise stable under d; quotient differentials descend, and kernels/cokernels of chain maps are formed degreewise.
Formalized. HomologicalComplexLimits; kernels/cokernels in HomologicalComplex — Kernels and cokernels of complex maps are created degreewise; quotient complexes are the corresponding cokernels.
Definition 1.2.1 — Categorical kernel, cokernel, monic and epic
Defines kernels and cokernels by universal properties in an additive category; monic/epi mean zero kernel/cokernel.
Formalized. Limits.kernel; Limits.cokernel; Mono; Epi; abelian kernel/cokernel APIs — The universal constructions and their mono/epi characterizations are canonical.
Definition 1.2.2 — Abelian category and image factorization
An abelian category is additive, has kernels/cokernels, and every mono/epi is a kernel/cokernel; im(f)=ker(coker f), yielding epi–mono factorization.
Formalized. CategoryTheory.Abelian; Abelian.image; Abelian.coimageImageComparison — Pinned abelian categories have kernels/cokernels and canonical epi–mono image factorization.
Definitions/conventions — Exact sequences and complexes in an abelian category
Exactness is defined by im=ker; defines abelian subcategory and extends chain complexes, maps, and homology to any abelian category A.
Formalized. ShortComplex.Exact; ComposableArrows.Exact; HomologicalComplex — Exactness is the categorical image=kernel condition and extends uniformly to complexes in any abelian category.
Theorem 1.2.3 — Ch(A) is abelian
For abelian A, Ch(A) is abelian; a chain map is monic or epic exactly when each component is.
Formalized. HomologicalComplexAbelian; componentwise mono/epi instances — For abelian A, the homological-complex category is abelian and monic/epic maps are detected degreewise.
Example 1.2.4 — Double complexes
A bicomplex C_{p,q} has horizontal/vertical differentials squaring to zero and anticommuting; rows/columns are complexes; bounded and first-quadrant variants are named.
Not formalized. partial: HomologicalComplex₂ in HomologicalBicomplex.lean — P/H use the iterated-complex convention in which the two differentials commute before totalization signs are inserted. No checked owner represents Weibel’s raw anticommuting bicomplex data as stated.
Searched: N
Sign Trick 1.2.5 — Double complexes as complexes of complexes
Replacing d^v on column p by (-1)^p d^v turns vertical maps into chain maps and identifies double complexes with Ch(Ch).
Not formalized. partial: HomologicalComplex₂; ComplexShape.ε₁; ComplexShape.ε₂; HomologicalComplex₂.total — Pinned totalization implements the standard signs after choosing the commuting iterated-complex convention, but no checked declaration gives the source equivalence obtained by replacing the vertical differential by (-1)^p dᵛ.
Searched: N
Total Complexes 1.2.6 — Direct-sum and product totalizations
Defines Tot^⊕ and Tot^Π on diagonals with differential dh+dv; for bounded diagonals they coincide; existence is tied to coproducts/products.
Not formalized. partial: HomologicalComplex₂.total (coproduct/direct-sum totalization) — P/H provide the direct-sum/coproduct total complex with standard signs. No product totalization or theorem identifying the two on bounded diagonals was found in P/H/current/external Lean.
Searched: N
Definitions — Complete and cocomplete abelian categories
Names abelian categories with all products complete and with all coproducts cocomplete, controlling existence of the two totalizations.
Formalized. Limits.HasProducts; Limits.HasCoproducts; HasLimits; HasColimits — The source completeness/cocompleteness conditions are exactly existence of all products/coproducts (equivalently the corresponding limits/colimits in this additive setting).
Truncations 1.2.7 — Good and brutal truncations
Defines τ_{≥n}, τ_{<n} preserving homology in their ranges, and brutal truncations σ obtained by replacing boundary/cycle terms by C_n.
Formalized. HomologicalComplex.truncGE; truncLE; stupidTrunc; support lemmas — Pinned canonical truncations preserve the intended homology ranges; stupidTrunc is the brutal truncation.
Translation 1.2.8 — Translation/shift of complexes
Defines C[p]n=C{n+p} with differential (-1)^p d, H_n(C[p])=H_{n+p}(C), and translation as a functor on maps.
Formalized. homological-complex shift functors; HomologicalComplex.shiftFunctor infrastructure — Pinned shifts implement translated complexes with the standard differential sign and shift homology accordingly.
Theorem 1.3.1 — Long exact homology/cohomology sequence
A short exact sequence of chain complexes has natural connecting maps and a long exact homology sequence; dually for cochain complexes.
Formalized. HomologicalComplex.HomologySequence; ShortComplex.ShortExact; HomologySequence.exact — A short exact sequence of complexes gets connecting morphisms and the natural long exact homology sequence in an arbitrary abelian category; cohomology is the upward-indexed specialization.
Snake Lemma 1.3.2 — Snake lemma kernel–cokernel sequence
A commutative two-row diagram of modules with exact rows yields the standard exact sequence from kernels through cokernels, with endpoint extensions under mono/epi hypotheses.
Formalized. ShortComplex.SnakeInput; ShortComplex.SnakeInput.snake_lemma — Pinned snake-lemma infrastructure yields the kernel-to-cokernel exact sequence with endpoint refinements.
Reusable comparison — Snake lemma in arbitrary abelian categories
By Freyd–Mitchell embedding, the module-form Snake Lemma applies in every abelian category.
Formalized. Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean — The pinned snake lemma is already formulated for arbitrary abelian categories, stronger than routing through Freyd–Mitchell.
Construction — Connecting homomorphism for Theorem 1.3.1
Constructs δ:H_n(C)→H_{n-1}(A) by passing the short exact sequence through cycles/boundaries and the Snake Lemma.
Formalized. HomologicalComplex.HomologySequence.δ; mapSnakeInput; snake input construction — The connecting morphism is constructed from the snake diagram on cycles/boundaries, exactly the source construction.
Addendum 1.3.3 — Element formula for connecting homomorphism
For modules, lift a cycle c to b, write db=f(a), and δ([c])=[a].
Formalized. HomologicalComplex.HomologySequence.δ_eq; ConcreteCategory.δ_apply; δ_apply' — Pinned concrete-category lemmas implement the lift–differentiate–lift–homology-class formula.
Construction — Categories of short and long exact sequences
Defines the category S of short exact sequences and L of long exact sequences with commutative-diagram morphisms.
Not formalized. partial: ShortComplex; ComposableArrows; ShortComplex.Exact; ComposableArrows.Exact — P/H represent individual short and long exact sequences, but no checked construction packages Weibel’s categories S and L of such sequences and their diagram morphisms.
Searched: N
Proposition 1.3.4 — Functoriality of the long exact sequence
The long exact sequence construction is a functor S→L; connecting maps are natural in morphisms of short exact sequences.
Not formalized. partial: HomologySequence.δ_naturality; homology-sequence exactness — Pinned Mathlib proves naturality of the connecting maps and exactness, but no checked S ⥤ L long-exact-sequence functor was found in P/H/current/external Lean.
Searched: N
Remark 1.3.5 — Exact-triangle notation
Packages a short exact sequence and its connecting morphisms as the mnemonic exact triangle A→B→C→A[-1].
Formalized. DerivedCategory.triangleOfSES; triangleOfSESδ; triangleOfSES_distinguished — Pinned derived-category APIs attach the canonical distinguished triangle to a short exact sequence with the connecting map and shift, formalizing the source exact-triangle mnemonic.
Construction/comparison — Splitting a vector-space complex
Over a field, chosen complements to boundaries/cycles give maps s_n with d=d s d and decompose the complex into homology plus contractible pieces.
Not formalized. partial: homotopy/splitting APIs; semisimplicity of vector spaces — No checked P/H/current/external declaration chooses complements and decomposes every vector-space complex into homology plus contractible summands as in the source construction.
Searched: N
Definition 1.4.1 — Split and split exact complexes
A complex is split if maps s_n satisfy d=d s d; it is split exact if additionally ds+sd=id.
Not formalized. partial: Homotopy (𝟙 C) 0 realizes the split-exact condition — Pinned chain contraction gives ds+sd=id, but Weibel’s weaker split condition d=dsd is a separate part of the row and has no checked owner. The older definition catalogue over-identified both with contractibility.
Searched: N
Example 1.4.2 — Acyclic complex that is not split exact
The periodic Z/4 complex with differential multiplication by 2 is exact but not split exact.
Not formalized. partial: ZMod 4; homological-complex exactness/homotopy APIs — No checked P/H/current/external declaration packages the periodic multiplication-by-two complex over ℤ/4 and proves exact but not split-exact.
Searched: N
Construction — Maps of the form ds+sd
Given graded maps s:C_n→D_{n+1}, the expression f=ds+sd is automatically a chain map.
Formalized. HomologicalComplex.nullHomotopicMap; nullHomotopicMap' — Given the degree-one homotopy data, Mathlib constructs ds+sd as a chain map automatically.
Definition 1.4.3 — Null homotopy and chain contraction
A chain map f is null homotopic if f=ds+sd; a null homotopy of id_C is a chain contraction.
Formalized. HomologicalComplex.Homotopy; nullHomotopy; nullHomotopy' — A null homotopy is exactly a homotopy to zero; applying it to the identity is the source chain contraction.
Definition 1.4.4 — Chain homotopy and chain-homotopy equivalence
f and g are chain homotopic when f-g is null homotopic; C and D are chain-homotopy equivalent if maps both ways compose homotopically to identities.
Formalized. HomologicalComplex.Homotopy; Homotopy.equivSubZero; HomotopyEquiv — Pinned structures encode homotopic maps and two-sided homotopy equivalences with the source equations.
Reusable comparison — Topological homotopy induces chain homotopy
A homotopy of continuous maps induces a chain homotopy on singular chain complexes; homotopy-equivalent spaces give chain-homotopy-equivalent singular complexes.
Formalized. TopCat.Homotopy.singularChainComplexFunctorObjMap — A topological homotopy directly induces a homotopy of the singular-chain maps, hence homotopy-equivalent spaces give homotopy-equivalent singular complexes.
Lemma 1.4.5 — Homotopy invariance of homology
Null-homotopic maps induce zero on homology; chain-homotopic maps induce the same homology map.
Formalized. HomologicalComplex.Homotopy.homologyMap_eq; HomotopyEquiv.toHomologyIso — Homotopic maps induce equal homology maps; a homotopy equivalence induces homology isomorphisms.
Construction 1.5.1 — Mapping cone
For f:B→C, cone(f)n=B{n-1}⊕C_n with the standard signed differential; gives the cochain analogue as well.
Formalized. CochainComplex.mappingCone; HomologicalComplex.homotopyCofiber; mappingCone.inr; mappingCone.fst — Pinned homotopy-cofiber/mapping-cone objects have the standard biproduct components and signed differential.
Construction 1.5.2 — Cone short exact sequence and long exact sequence
There is 0→C→cone(f)→B[-1]→0, hence a long exact sequence linking H(B), H(C), and H(cone(f)).
Formalized. CochainComplex.mappingCone.triangle; DerivedCategory.mappingCone_triangle_distinguished; homological-functor exact sequence — Mathlib packages the source cone short-exact-sequence consequence as the equivalent distinguished mapping-cone triangle; applying homology yields the standard long exact sequence.
Lemma 1.5.3 — Cone connecting map equals f
Under the cone long exact sequence, the connecting map H_n(B)→H_n(C) is the map induced by f.
Formalized. CochainComplex.mappingCone.triangle; homology sequence of a distinguished triangle — The first morphism of the mapping-cone triangle is the original map, so the corresponding long-exact-sequence map is exactly f_*, matching the source identification.
Corollary 1.5.4 — Quasi-isomorphisms detected by cones
f is a quasi-isomorphism iff cone(f) is exact.
Formalized. DerivedCategory.isIso_Q_map_iff_quasiIso; DerivedCategory.mappingCone_triangle_distinguished; Triangle.isZero₃_iff_isIso₁ — Compile-checked against P: these APIs assemble to QuasiIso φ ↔︎ (CochainComplex.mappingCone φ).Acyclic.
Reusable comparison — Topological mapping cone versus algebraic cone
For an inclusion A⊂X, the singular complex of the topological mapping cone is quasi-isomorphic to the algebraic mapping cone of S(A)→S(X).
Not formalized. partial: topological mapping cones; singular chains; algebraic mappingCone — P/H/current/external search found no checked quasi-isomorphism comparing singular chains on a topological mapping cone of an inclusion with the algebraic mapping cone.
Searched: N
Construction 1.5.5 [OCR joined as 1.5.5A] — Mapping cylinder
Defines cyl(f) for a chain map f:B→C, with its signed differential and natural embedded copies of B and C.
Not formalized. partial: HomologicalComplex.cylinder is a cylinder of an object, not Weibel’s cylinder of a map — No map-level algebraic mapping-cylinder construction was found in P/H/current/external Lean. The older definition catalogue’s HomologicalComplex.cylinder route is a type mismatch.
Searched: N
Lemma 1.5.6 — C→cyl(f) is a quasi-isomorphism
The canonical inclusion of C as the (0,0,c) subcomplex of cyl(f) is a quasi-isomorphism.
Not formalized. partial: homotopy-cofiber cylinder-of-object API — Because the source map-cylinder object is absent, no checked owner proves the canonical C → cyl(f) quasi-isomorphism.
Searched: N
Reusable comparison — Topological mapping cylinder
Singular chains on a topological mapping cylinder compare naturally with the algebraic mapping cylinder construction.
Not formalized. partial: topological mapping-cylinder developments exist externally — No checked Lean theorem compares singular chains on the topological mapping cylinder with Weibel’s algebraic map-cylinder construction.
Searched: N
Construction — Mapping-cylinder short exact sequences
For f in a short exact sequence, constructs the associated cylinder objects and the comparison diagram of short exact sequences.
Not formalized. partial: short-exact and cone APIs — No checked source-level mapping-cylinder object or its short exact sequences were found.
Searched: N
Lemma 1.5.7 — Exact commutative cylinder diagram
The mapping-cylinder comparison diagram has exact rows and commutes.
Not formalized. partial: short-exact diagram APIs — No checked P/H/current/external declaration realizes the exact commutative mapping-cylinder diagram of Lemma 1.5.7.
Searched: N
Construction/comparison 1.5.8 — Replace a short exact sequence by cone/cylinder data
For 0→B→C→D→0, the natural cone-to-D map is a quasi-isomorphism, comparing the standard long exact sequence with cone/cylinder sequences.
Not formalized. partial: CochainComplex.mappingCone.quasiIso_descShortComplex; DerivedCategory.triangleOfSES — Pinned Mathlib has the cone-to-third-object quasi-isomorphism for a short exact sequence, but the source row also compares through the missing map-cylinder data; strict whole-row semantics therefore leave it unmatched.
Searched: N
Reusable comparison — Naturality identifies the two long exact sequences
The naturality diagram identifies the ordinary homology long exact sequence with the mapping-cone/mapping-cylinder version.
Not formalized. partial: triangleOfSESδ_naturality; mapping-cone triangle naturality — Pinned cone/derived naturality identifies the cone and SES triangles, but the source row also identifies the mapping-cylinder long exact sequence, whose required cylinder construction is absent.
Searched: N
Freyd–Mitchell Embedding Theorem 1.6.1 — Embedding small abelian categories into modules
Every small abelian category admits an exact fully faithful functor into mod-R for some ring R.
Formalized. CategoryTheory.Abelian.FreydMitchell module embedding; FreydMitchell exact/full/faithful infrastructure — Pinned Mathlib constructs an exact fully faithful embedding of a small abelian category into a module category.
Lemma 1.6.2 — Criterion for a full subcategory to be abelian
A full subcategory of an abelian category is additive/abelian and exactly embedded under closure conditions on zero object, biproducts, kernels, and cokernels.
Formalized. ObjectProperty closure under zero/kernels/cokernels/finite products; Abelian P.FullSubcategory instance — The pinned criterion is exactly Weibel’s closure test for a full subcategory to inherit an abelian structure and exact inclusion.
Examples 1.6.3 — Abelian and nonabelian full subcategories of modules
Gives finitely generated modules, finite/torsion/p-primary groups, and torsionfree groups as examples distinguishing closure properties.
Not formalized. partial: FGModuleCat and its abelian instance over Noetherian rings — P has the finitely-generated-module case, but no checked whole bundle covers the finite, torsion, p-primary, and torsion-free group examples with the stated abelian/nonabelian distinctions.
Searched: N
Functor Categories 1.6.4 — Functor categories are abelian
For small C and abelian A, A^C is abelian with objectwise exact structure; examples include graded objects and presheaves.
Formalized. CategoryTheory.functorCategoryAbelian in Abelian/FunctorCategory.lean — For small source and abelian target, the functor category is abelian with objectwise kernels/cokernels/exactness.
Definition — Presheaf
A presheaf on X with values in A is a contravariant functor from the poset of open subsets of X to A.
Formalized. TopCat.Presheaf; functor categories on Opens Xᵒᵖ — A presheaf is exactly a contravariant functor from opens to the coefficient category.
Reusable example — Continuous functions as a presheaf with local gluing
U↦C^0(U) is a presheaf and motivates the additional sheaf axiom.
Formalized. TopCat.sheafToTop; Top.Presheaf.toType_isSheaf; sheaf-of-functions APIs — Pinned topology/sheaf code proves continuous functions form a sheaf, hence in particular the motivating presheaf and local gluing statement.
Definition 1.6.5 — Sheaf
A presheaf is a sheaf when compatible local sections glue uniquely; equivalently, the standard product/equalizer sequence is exact for every open cover.
Formalized. Presieve.IsSheafFor; Presheaf.IsSheaf; topological sheaf APIs — The sheaf predicate is the unique compatible gluing condition; its limit/equalizer formulation is built into the site API.
Construction/comparison — Sheaves form an abelian category but not an abelian subcategory of presheaves
Kernels agree objectwise, cokernels require sheafification; the exponential-sequence example exhibits failure of objectwise surjectivity.
Not formalized. partial: CategoryTheory.sheafIsAbelian; sheafification adjunction and limits — P/H prove sheaves are abelian and that cokernels are computed via sheafification, but no checked owner gives the source exponential-sequence example demonstrating failure of objectwise surjectivity; whole-row semantics leave the bundle unmatched.
Searched: N
Definition 1.6.6 — Left exact, right exact, and exact functors
Defines exactness behavior of additive functors on short exact sequences, including the contravariant convention.
Formalized. LeftExactFunctor; RightExactFunctor; ExactFunctor — Pinned definitions are preservation of finite limits, finite colimits, or both, equivalent to the source short-exact behavior in abelian categories.
Example 1.6.7 — Sheaf inclusion and sheafification
The inclusion Sheaves(X)→Presheaves(X) is left exact; sheafification is exact.
Formalized. sheafificationAdjunction; presheafToSheaf preserves finite limits; sheafToPresheaf right adjoint — The inclusion is a right adjoint and hence left exact. Sheafification is a left adjoint and also preserves finite limits, so in the abelian setting it is exact.
Proposition 1.6.8 — Hom(M,-) is left exact
For an abelian category A, Hom_A(M,-):A→Ab is left exact for every M.
Formalized. preadditiveYonedaObj/preadditiveCoyonedaObj limit-preservation APIs — Representable Hom functors preserve limits; in an abelian category this is exactly left exactness of Hom(M,-).
Corollary 1.6.9 — Hom(-,M) is contravariantly left exact
The contravariant Hom functor sends short exact sequences to left-exact sequences of abelian groups.
Formalized. preadditiveYonedaObj; preservesLimits_preadditiveYonedaObj — The opposite/representable formulation gives the contravariant left-exact Hom statement.
Yoneda Embedding 1.6.10 — Additive Yoneda embedding
Embeds an additive category A into Ab{Aop} by A↦Hom_A(-,A).
Formalized. preadditiveYoneda; full_preadditiveYoneda; faithful_preadditiveYoneda — The pinned additive Yoneda functor has exactly the source target Aᵒᵖ ⥤ AddCommGrpCat and is fully faithful.
Yoneda Lemma 1.6.11 — Yoneda reflects exactness
A sequence A→B→C is exact when Hom(M,A)→Hom(M,B)→Hom(M,C) is exact for every M.
Formalized. ShortComplex.exact_of_eval; Functor.reflects_exact_of_faithful; preadditiveYoneda — Compile-checked against P: exactness of every Hom evaluation assembles to exactness after Yoneda, and faithful Yoneda reflects it back to the original sequence.
Definition/construction — Weakly effaceable functors and W(M)
For an additive contravariant F, constructs W(M) as a cokernel over epimorphisms and calls F weakly effaceable when W(M)=0 for all M.
Not formalized. partial: generic cokernels/epimorphism indexing — No P/H/current/external Lean owner defines Weibel’s W(M) cokernel over epimorphisms or his weakly-effaceable contravariant functors. lean-liquid@087fffad55dc1dd8d54ab35c9816926a45b8c0fd uses a different effaceability notion for δ-functors.
Searched: N
Proposition 1.6.12 — Weakly effaceable functors form a localizing subcategory
For small A, weakly effaceable functors form a localizing subcategory W of Ab{Aop}; the quotient L is abelian and the quotient functor is exact.
Not formalized. partial: Serre/localizing quotient infrastructure — No checked declaration proves Weibel’s weakly-effaceable functors form the stated localizing subcategory or constructs the corresponding quotient category.
Searched: N
Reusable comparison — The localizing quotient repairs Yoneda cokernels
The inclusion L→Ab{Aop} is left exact but not exact; quotient cokernels differ by the weakly effaceable correction.
Not formalized. partial: general localization/Serre quotient APIs — The specific comparison showing how the localizing quotient repairs Yoneda cokernels depends on the missing U064–U065 construction and has no checked owner.
Searched: N
Corollary 1.6.13 — Exact fully faithful Yoneda into the quotient
The induced Yoneda embedding h:A→L is exact and fully faithful.
Not formalized. partial: ordinary preadditiveYoneda is fully faithful — Pinned Yoneda is fully faithful but not the source exact embedding into the particular weak-effaceable quotient, which is absent.
Searched: N
Example 1.6.14 — Graded objects and complexes as modules over explicit rings
Realizes graded R-modules, then chain complexes, as full subcategories of module categories over rings built from products/matrix-like generators.
Not formalized. partial: graded-module and chain-complex infrastructure — No checked P/H/current/external construction identifies graded modules and chain complexes with the source explicit module categories over the product/matrix-like rings of Example 1.6.14.
Searched: N