Appendix A. Category Theory Language
FC05 — Weibel, An Introduction to Homological Algebra.
This chapter contains 26 definitions, 1 theorem, 12 examples, 4 constructions, 1 convention and 8 other statements.
Of the 52 statements checked against Lean, 39 are formalized somewhere and 13 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 39 | 75% | Mathlib states and proves it. |
| not formalized | 13 | 25% | A documented search found no Lean statement of it anywhere. |
| checked in total | 52 |
- Project-first search was performed at repository HEAD
f90173886bc881c2d43c0a7eb2d9fe7f110ac9a5. No project declaration owns a complete Appendix-A source row under strict bundle semantics. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0 and directly project-compatible. Every P target promoted in the Appendix table was inspected at that exact revision. The generic category/functor/natural-transformation, skeleton, limits/colimits, filtered-category and adjunction interfaces substantially overlap FC03 (Riehl); the already-recorded FC03 Sweep-II audits were reused, while Weibel-specific bundled examples and Appendix-only clauses were checked independently. - Current Mathlib was refreshed on 2026-09-06 at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f, Apache-2.0, Lean 4.34.0-rc2. Targeted H searches did not add a general arbitrary subcategory interface matching U017, the abelian-monoid translation category U045, the full AB5 directed-subobject-lattice equivalence U037, or the noncommutative tensor-Hom adjunctions required by U014/U049. - U014 and U049 are deliberately not inferred from the pinned closed monoidal
ModuleCatAPI.Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean::monoidalClosedHomEquivis formulated over a commutative base ring. Open Mathlib PR #8495, audited at head5b358de183c6084a8378e2d6418ce48cf2d7fb68, develops a Hom-tensor adjunction but likewise assumes[CommRing R]. Weibel’s rows use the general right/left module tensor-Hom adjunction over an arbitrary ring, so neither checked interface owns the whole source bundle. - U017 asks for an arbitrary subcategory obtained by selecting both objects and a composition-closed subset of ambient morphisms, with faithful inclusion. P/H have full-subcategory and wide-subcategory infrastructure, but no checked declaration realizes that whole general source construction; a full or wide specialization is not credited.
- U033 is direct at P even though Mathlib does not use the labels AB3/AB3*: the source conditions are arbitrary coproducts/products, and
Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean::has_colimits_of_hasCoequalizers_and_coproductsandhas_limits_of_hasEqualizers_and_products, together with the automatic (co)equalizers of an abelian category, give the stated equivalence with cocompleteness/completeness. - U035 is direct at P.
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean::AB4andAB4Stardefine exact coproducts/products, whilehasExactColimitsOfShape_of_preservesMonoandhasExactLimitsOfShape_of_preservesEpisupply the converse from preservation of monomorphisms/epimorphisms. Thus the source direct-sum-of-monos/product-of-epis formulation is represented at the pinned revision. - U037 is bundled more strongly than Mathlib’s AB5 definition. P has
AB5/AB5Staras exact filtered colimits/cofiltered limits, andMathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean::subobjectMk_of_isColimit_eq_iSuprelates filtered colimits of subobjects to suprema. The audit found no declaration giving Weibel’s full distributivity equivalenceB ∩ (sup A_i) = sup (B ∩ A_i)together with its dual. Therefore U037 remains unmatched rather than receiving partial credit. - U034, U036 and U038 are heterogeneous example rows that include both positive and negative assertions. Although P contains many positive AB3/AB4/AB5 instances for standard algebraic categories and sheaves, the complete source bundles also assert failures for finite/torsion abelian groups or sheaf categories. The checked P/H/open sources do not formalize every clause, so these rows remain unmatched.
- U045’s translation category of an abelian monoid, with its proof of filteredness and localization role, was not found in P, H, TauCeti, indexed GitHub Lean search, or open Mathlib work. Generic
IsFilteredand one-object/monoid categories are prerequisites only and do not own this example. - U002 contains the metatheoretic assertion that the collection of all sets is a proper class; universe-polymorphic
Type usupplies the set-category paradigm but does not formalize that proper-class clause as the source states it. U005, U024 and U025 likewise bundle several examples/comparisons beyond the adjacent exact definitions, and U010 includes the negative assertion that an opposite module category need not be a module category over another ring. Strict bundle semantics leave all of these rows unmatched. - U052 is direct:
Mathlib/Algebra/Category/Grp/Adjunctions.lean::GrpCat.abelianizeAdjgives abelianization as the reflector from groups to abelian groups, whileMathlib/CategoryTheory/Sites/Sheafification.lean::sheafificationAdjunctionandsheafification_reflectivegive sheafification as the reflector from presheaves to sheaves. Ndenotes dated 2026-09-06 negative evidence after project-first inspection, P, H/current Mathlib, reuse of the FC03 recorded audits, TauCeti where relevant, indexed GitHub Lean search, open Mathlib PR search, and the targeted external checks above. A specialization, one clause/example of a bundled row, an unformalized negative assertion, or a theorem requiring reconstruction of a missing source clause is not credited as that row’s route.
Definition A.1.1
A category C consists of a class of objects, Hom sets, identity morphisms, and composition functions. The extraction ends with “subject to two axioms:” but the two axioms themselves are absent before A.1.2.
Formalized. Mathlib/CategoryTheory/Category/Basic.lean::CategoryStruct, Category — Pinned Mathlib packages objects/Hom types, identities and composition in CategoryStruct/Category, including associativity and identity laws, exactly the source category definition.
Paradigm A.1.2
Sets is the paradigm category: objects are sets, morphisms are functions, composition is ordinary composition, and identities are identity functions; the object collection is a proper class rather than a set.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: Sets is the paradigm category: objects are sets, morphisms are functions, composition is ordinary composition, and identities are identity functions; the object collection is a proper class rather than a set. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
Examples A.1.3
Records Ab, Groups, Rings, left/right module categories, and discrete categories as standard examples; a discrete category has only identity morphisms.
Formalized. Mathlib/CategoryTheory/Types.lean::instance : Category (Type u); Mathlib/Algebra/Category/Grp/Basic.lean::AddCommGrpCat, GrpCat; Mathlib/Algebra/Category/Ring/Basic.lean::RingCat; Mathlib/Algebra/Category/ModuleCat/Basic.lean::ModuleCat; Mathlib/CategoryTheory/Discrete/Basic.lean::Discrete — Pinned Mathlib has the source’s sets, abelian groups, groups, rings, module, and discrete-category paradigms as concrete category instances.
Definition/comparison — Small categories A.1.4
A category is small when its objects form a set; a poset becomes a small category with at most one arrow p→q, and a one-object category is a monoid, hence a group is a one-object category.
Formalized. Mathlib/CategoryTheory/Category/Basic.lean::SmallCategory; Mathlib/CategoryTheory/Category/Preorder.lean::Preorder.smallCategory; Mathlib/CategoryTheory/SingleObj.lean::SingleObj — These declarations give the small-category notion, the category attached to a preorder/poset, and the one-object category attached to a monoid (hence a group), matching the source examples.
Definition — isomorphism
A morphism f:B→C is an isomorphism when it has a two-sided inverse, which is unique; the paragraph compares categorical isomorphisms with bijections, homeomorphisms, diffeomorphisms, and group elements.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: A morphism f:B→C is an isomorphism when it has a two-sided inverse, which is unique; the paragraph compares categorical isomorphisms with bijections, homeomorphisms, diffeomorphisms, and group elements. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
A.1.5 (monic, epi, subobject)
Defines monic by left cancellation and epi by right cancellation; in concrete algebraic categories these agree with injective/surjective maps in the stated cases. A subobject is represented by a monic, technically up to mutual factorization.
Formalized. Mathlib/CategoryTheory/EpiMono.lean::Mono, Epi; Mathlib/CategoryTheory/Subobject/Basic.lean::Subobject, Subobject.mk, Subobject.mk_le_mk_of_comm; concrete mono/epi instances in Mathlib/Algebra/Category/Grp/Basic.lean and Mathlib/Algebra/Category/ModuleCat/Basic.lean — Pinned Mathlib formalizes categorical monomorphisms/epimorphisms and subobjects as isomorphism classes of monomorphisms ordered by factorization; the standard algebraic concrete categories identify these with the expected injective/surjective maps.
A.1.6 (initial, terminal, zero objects)
Defines initial and terminal objects by unique maps out of/into them and a zero object as both; gives Sets and module-category examples.
Formalized. Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean::IsInitial, IsTerminal; Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean::HasZeroObject, IsZero; standard instances for Type and ModuleCat — Pinned Mathlib has the source universal properties for initial, terminal and zero objects, with the standard sets/module examples.
Definition — zero morphisms, kernels, and cokernels
In a category with zero object, defines zero maps via B→0→C; defines kernels and cokernels by their universal factorization properties, noting kernels are monic and cokernels epi.
Formalized. Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean::HasZeroMorphisms; Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean::kernel, kernelIsKernel, cokernel, cokernelIsCokernel, instance : Mono (kernel.ι f), instance : Epi (cokernel.π f) — The pinned kernel/cokernel API is stated by the same zero-composite universal properties and records kernel arrows monic and cokernel arrows epic, exactly the source bundle.
Definition/construction — Opposite Category A.1.7
C^op has the same objects and reversed morphisms/composition; taking opposites interchanges monic/epi, kernel/cokernel, and initial/terminal objects.
Formalized. Mathlib/CategoryTheory/Opposites.lean::Category.opposite; Mathlib/CategoryTheory/EpiMono.lean::op_epi_iff, op_mono_of_epi; Mathlib/CategoryTheory/Limits/Opposites.lean::hasLimitsOfShape_opposite_iff, hasColimitsOfShape_opposite_iff; Mathlib/CategoryTheory/Abelian/Opposite.lean::kernelOpOp, cokernelOpOp — Pinned Mathlib reverses arrows in the opposite category and explicitly exchanges mono/epi, limits/colimits (hence initial/terminal), and kernel/cokernel, matching the source duality statement.
Example A.1.8
For a ring R viewed as a one-object category, R^op reverses multiplication and (R^op)-mod≅mod-R; the opposite of R-mod need not itself be S-mod for a ring S.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: For a ring R viewed as a one-object category, R^op reverses multiplication and (R^op)-mod≅mod-R; the opposite of R-mod need not itself be S-mod for a ring S. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
Definition — Products and Coproducts A.1.9
Defines arbitrary products by projections and their universal property and coproducts dually by injections; records uniqueness up to isomorphism and standard examples in Sets, Groups, and R-mod.
Formalized. Mathlib/CategoryTheory/Limits/Shapes/Products.lean::HasProduct, productIsProduct, HasCoproduct, coproductIsCoproduct — Pinned Mathlib’s product and coproduct cones/cocones carry the same universal properties and uniqueness up to unique isomorphism as the source definition.
Definition — functor
A functor F:C→D maps objects and morphisms, preserves identities and composition, induces maps on Hom sets, and composes in the evident way.
Formalized. Mathlib/CategoryTheory/Functor/Basic.lean::Functor — Pinned Mathlib’s Functor preserves identities and composition on the nose and supplies object/morphism maps, exactly the source definition.
Construction — identity functor and Cat
Defines id_C and forms Cat, the category of small categories and functors, avoiding the set-theoretic difficulty of a category of all categories.
Formalized. Mathlib/CategoryTheory/Functor/Basic.lean::Functor.id; Mathlib/CategoryTheory/Category/Cat/Basic.lean::Cat — Pinned Mathlib has the identity functor and the category whose objects are small categories and arrows are functors, matching the source examples.
Example/comparison — Hom and Tensor Product A.2.1
For a right R-module M, M⊗_R− is a functor R-mod→Ab and Hom_R(M,−) is a functor mod-R→Ab.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: For a right R-module M, M⊗_R− is a functor R-mod→Ab and Hom_R(M,−) is a functor mod-R→Ab. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
Definition/example — Forgetful Functors A.2.2
A forgetful functor discards specified structure; examples include R-mod→Ab→Sets and their composite.
Formalized. Mathlib/Algebra/Category/ModuleCat/Basic.lean::forget₂ (ModuleCat R) AddCommGrpCat; Mathlib/CategoryTheory/ConcreteCategory/Basic.lean::forget AddCommGrpCat — The pinned concrete-category forgetful functors realize the source chain from modules through additive groups to underlying types.
Definition — Faithful Functors A.2.3
F:C→D is faithful when every induced Hom-set map is injective; a category admitting a faithful underlying-set functor U:C→Sets is concrete.
Formalized. Mathlib/CategoryTheory/Functor/FullyFaithful.lean::Functor.Faithful; Mathlib/CategoryTheory/ConcreteCategory/Basic.lean::ConcreteCategory, forget — Pinned Mathlib defines faithful functors by injectivity on Hom maps and concrete categories by a faithful forgetful functor to types, exactly the source criterion.
Definition — subcategory
A subcategory selects objects and morphisms closed under identities and composition; its inclusion functor is faithful.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: A subcategory selects objects and morphisms closed under identities and composition; its inclusion functor is faithful. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
Definition — full subcategory
A subcategory B⊂C is full when Hom_B(B,B′)=Hom_C(B,B′) for all its objects, so it is determined by its object class.
Formalized. Mathlib/CategoryTheory/FullSubcategory.lean::ObjectProperty.FullSubcategory, ObjectProperty.ι — Pinned Mathlib constructs the full subcategory on any selected object property, with all ambient morphisms between selected objects, exactly the source full-subcategory definition.
Definition — full and fully faithful functors
A functor is full when each induced Hom map is surjective and fully faithful when it is both full and faithful; inclusions of full subcategories and the Yoneda embedding are examples.
Formalized. Mathlib/CategoryTheory/Functor/FullyFaithful.lean::Functor.Full, Functor.Faithful, Functor.FullyFaithful; Mathlib/CategoryTheory/Yoneda.lean::Yoneda.fullyFaithful; Mathlib/CategoryTheory/FullSubcategory.lean::ObjectProperty.ι — Pinned Mathlib defines full and faithful functors by surjectivity/injectivity on Hom maps; both the full-subcategory inclusion and Yoneda have the stated fully-faithful behavior.
Definition — Skeletal Subcategories A.2.4
A skeletal subcategory S⊂C is full and contains exactly one representative from each isomorphism class of objects of C.
Formalized. Mathlib/CategoryTheory/Skeletal.lean::Skeletal, IsSkeletonOf, Skeleton, skeleton_skeletal, skeleton_isSkeleton — Pinned Mathlib chooses one object per isomorphism class via Skeleton C and proves the resulting category skeletal and a skeleton of C, exactly the source notion.
Construction — reflection onto a skeletal subcategory
Choosing representatives FC∈S and isomorphisms θ_C:C≅FC defines F(f)=θ_C f θ_B^{-1}; this reflection functor is fully faithful.
Formalized. Mathlib/CategoryTheory/Skeletal.lean::toSkeletonFunctor, fromSkeleton, skeletonEquivalence; instances (fromSkeleton C).Full, (fromSkeleton C).Faithful — Pinned Mathlib constructs the choice-based functor from C to its skeleton and the inverse inclusion, proves them an equivalence, and records the inclusion fully faithful; this is the source skeleton-reflection construction.
Definition/example — Contravariant Functors A.2.5
A contravariant F:C→D is a covariant functor C^op→D, reversing arrows and composition; examples include Hom_R(−,N) and presheaves.
Formalized. Mathlib/CategoryTheory/Opposites.lean::Category.opposite; Mathlib/CategoryTheory/Yoneda.lean::yoneda; presheaf abbreviations in Mathlib/CategoryTheory/Sites/Sheaf.lean — A contravariant functor is represented exactly as a functor out of Cᵒᵖ; representable Hom and presheaf examples use that convention.
Definition — natural transformation and natural isomorphism
For F,G:C→D, a natural transformation η:F⇒G assigns η_C:F(C)→G(C) commuting with every morphism square; it is a natural isomorphism when every component is an isomorphism.
Formalized. Mathlib/CategoryTheory/NatTrans.lean::NatTrans; Mathlib/CategoryTheory/NatIso.lean::NatTrans.isIso_iff_isIso_app — Pinned Mathlib packages the component maps and naturality squares of natural transformations and identifies natural isomorphisms with componentwise isomorphisms, matching the source definition.
Examples A.3.1
Gives the torsion-subgroup inclusion, tensor maps induced by a module homomorphism, and precomposition maps on Hom as natural transformations, with links to Tor/Ext and δ-functors.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: Gives the torsion-subgroup inclusion, tensor maps induced by a module homomorphism, and precomposition maps on Hom as natural transformations, with links to Tor/Ext and δ-functors. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
Definition — Equivalence A.3.2
F:C→D is an equivalence when some G:D→C has natural isomorphisms id_C≅GF and id_D≅FG; skeletal inclusion and forgetting a chosen basis are examples.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: F:C→D is an equivalence when some G:D→C has natural isomorphisms id_C≅GF and id_D≅FG; skeletal inclusion and forgetting a chosen basis are examples. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
Definition/construction — Functor Categories A.3.3
For small I and category A, A^I has functors I→A as objects and natural transformations as morphisms, composed componentwise; if A is abelian then A^I is abelian.
Formalized. Mathlib/CategoryTheory/Functor/Category.lean::Functor.category; Mathlib/CategoryTheory/Abelian/FunctorCategory.lean::functorCategoryAbelian — Pinned Mathlib makes the diagram/functor category I ⥤ A a category and proves it abelian whenever A is abelian, exactly the source theorem.
Example A.3.4 (Yoneda embedding)
The Yoneda functor h:I→Sets{Iop}, i↦Hom_I(−,i), is fully faithful; for an Ab-category it lands in Ab{Iop}, embedding additive categories as full subcategories of abelian categories.
Formalized. Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean::preadditiveYoneda, full and faithful instances; Mathlib/CategoryTheory/Abelian/FunctorCategory.lean::functorCategoryAbelian — Pinned Mathlib’s preadditive Yoneda lands in additive-group-valued functors and is full and faithful; that functor category is abelian, giving precisely the source additive embedding into a full subcategory of an abelian category.
A.4.1 (Ab-category)
An Ab-category has an abelian-group structure on every Hom set with composition bilinear; endomorphisms form rings, and R-mod is the basic example.
Formalized. Mathlib/CategoryTheory/Preadditive/Basic.lean::Preadditive, instance {X : C} : Ring (End X); Mathlib/Algebra/Category/ModuleCat/Basic.lean::ModuleCat — Pinned Mathlib equips each Hom with an additive commutative group and composition with bilinearity, induces the endomorphism ring, and has the standard module-category example.
Definition — additive category
An additive category is an Ab-category with a zero object and all binary products; finite products then coincide with finite coproducts and are written A⊕B.
Formalized. Mathlib/CategoryTheory/Preadditive/Basic.lean::Preadditive; Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean::HasZeroObject; Mathlib/CategoryTheory/Preadditive/Biproducts.lean::HasBinaryBiproducts.of_hasBinaryProducts; Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean::HasBinaryBiproducts — Pinned Mathlib expresses the source additive-category structure through preadditivity, a zero object and finite biproducts, and proves binary products in a preadditive setting induce biproducts, hence finite products and coproducts coincide as stated.
Definition A.4.2
An abelian category is additive, every map has kernel and cokernel, every monic is the kernel of its cokernel, and every epi is the cokernel of its kernel.
Formalized. Mathlib/CategoryTheory/Abelian/Basic.lean::Abelian, Abelian.mk', Abelian.hasZeroObject, Abelian.hasFiniteBiproducts; normal mono/epi interfaces in Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean — Pinned Mathlib’s Abelian is an equivalent packaged form of the source axioms: preadditivity/additivity together with kernels/cokernels and every mono/epi normal; Abelian.mk' supplies the standard constructor from kernel/cokernel data.
Construction — image factorization in an abelian category
Every f:B→C factors as an epi B→im(f) followed by the monic im(f)=ker(coker f)→C; this defines the image subobject.
Formalized. Mathlib/CategoryTheory/Abelian/Basic.lean::Abelian.image, imageMonoFactorisation, imageFactorisation, Abelian.factorThruImage — Pinned Mathlib defines the abelian image through the kernel-of-cokernel construction and provides the canonical epi-mono factorization through it, exactly the source statement.
Definition — exact sequence
A sequence A→B→C in an abelian category is exact at B when ker(g)=im(f), which in particular forces gf=0.
Formalized. Mathlib/CategoryTheory/Abelian/Exact.lean::exact_iff_image_eq_kernel; Mathlib/Algebra/Homology/ShortComplex/Basic.lean::ShortComplex.Exact — Pinned Mathlib characterizes exactness of a composable zero pair by equality of image and kernel subobjects, exactly Weibel’s definition; the short-complex condition includes the required composite-zero relation.
A.4.3 (AB3 and AB3)
AB3 requires all set-indexed coproducts and is called cocompleteness; AB3* requires all set-indexed products and is called completeness.
Formalized. Mathlib/CategoryTheory/Limits/Shapes/Products.lean::HasCoproducts, HasProducts; Mathlib/CategoryTheory/Abelian/Basic.lean::Abelian.hasEqualizers, Abelian.hasCoequalizers; Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean::has_colimits_of_hasCoequalizers_and_coproducts, has_limits_of_hasEqualizers_and_products — Mathlib uses the underlying conditions rather than the names AB3/AB3*: arbitrary coproducts/products. In an abelian category the pinned construction theorems combine these with automatic coequalizers/equalizers to obtain all colimits/limits, matching the source cocomplete/complete equivalence.
Example A.4.4
Ab and R-mod satisfy AB3 and AB3; finite abelian groups satisfy neither, torsion abelian groups satisfy AB3 but not AB3, and countable products/coproducts already suffice for several homological constructions.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: Ab and R-mod satisfy AB3 and AB3; finite abelian groups satisfy neither, torsion abelian groups satisfy AB3 but not AB3, and countable products/coproducts already suffice for several homological constructions. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
Definition — AB4 and AB4
AB4 means cocomplete with direct sums of monics monic; AB4* means complete with products of epis epi. This main text resumes after Exercise A.4.4.
Formalized. Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean::AB4, AB4Star, hasExactColimitsOfShape_of_preservesMono, hasExactLimitsOfShape_of_preservesEpi — Pinned Mathlib defines AB4/AB4* as exact coproducts/products. Exactness gives preservation of monos/epis, and the cited converse lemmas reconstruct exactness from preservation of monomorphisms/epimorphisms in an abelian category, matching the source direct-sum/product formulation.
Example A.4.5
Ab and R-mod satisfy AB4 and AB4; Sheaves(X) is complete but does not satisfy AB4.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: Ab and R-mod satisfy AB4 and AB4; Sheaves(X) is complete but does not satisfy AB4. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
A.4.6 (AB5 and AB5)
AB5 means cocomplete with filtered colimits of exact sequences exact, equivalently the stated distributivity identity for directed lattices of subobjects; AB5* is the dual filtered-inverse-limit condition with its dual identity.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: AB5 means cocomplete with filtered colimits of exact sequences exact, equivalently the stated distributivity identity for directed lattices of subobjects; AB5* is the dual filtered-inverse-limit condition with its dual identity. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
Examples A.4.7
Ab and R-mod satisfy AB5 but not AB5; Sheaves(X) likewise satisfies AB5 but not AB5.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: Ab and R-mod satisfy AB5 but not AB5; Sheaves(X) likewise satisfies AB5 but not AB5. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
A.5.1 (limit)
A limit of F:I→A is an object L with compatible maps L→F_i universal among compatible cones; it is unique up to isomorphism, and products are limits over discrete indexing categories.
Formalized. Mathlib/CategoryTheory/Limits/HasLimits.lean::limit, limit.π, limit.isLimit, limit.existsUnique; Mathlib/CategoryTheory/Limits/Shapes/Products.lean::productIsProduct — Pinned Mathlib gives limits by terminal cones with unique mediating maps and treats products as limits of discrete diagrams, exactly the source definition and example.
Definition — complete category
A is complete when every functor F:I→A with small I has a limit; Sets, Ab, and R-mod are complete.
Formalized. Mathlib/CategoryTheory/Limits/HasLimits.lean::HasLimits; Mathlib/CategoryTheory/Limits/Types/Limits.lean::Types.hasLimitsOfShape; Mathlib/Algebra/Category/Grp/Limits.lean::AddCommGrpCat.hasLimits; Mathlib/Algebra/Category/ModuleCat/Limits.lean::ModuleCat.hasLimits — Pinned Mathlib expresses completeness as existence of all small limits and supplies it for sets, abelian groups and module categories, matching the source examples.
Definition — colimit (main text resumes after Exercise A.5.1)
Dually, a colimit of F:I→A is an object C with compatible maps F_i→C universal among cocones; coproducts are special colimits and colimits in A are limits in A^op.
Formalized. Mathlib/CategoryTheory/Limits/HasLimits.lean::colimit, colimit.ι, colimit.isColimit; Mathlib/CategoryTheory/Limits/Opposites.lean::hasColimit_op_iff_hasLimit; Mathlib/CategoryTheory/Limits/Shapes/Products.lean::coproductIsCoproduct — Pinned Mathlib gives the dual cocone universal property, coproducts as discrete colimits, and the equivalence between colimits in C and limits in the opposite category, exactly the source bundle.
Definition — cocomplete category
A is cocomplete when every functor from a small indexing category has a colimit; Sets, Ab, and R-mod are cocomplete.
Formalized. Mathlib/CategoryTheory/Limits/HasLimits.lean::HasColimits; Mathlib/CategoryTheory/Limits/Types/Colimits.lean::Types.hasColimitsOfShape; Mathlib/Algebra/Category/Grp/Colimits.lean::AddCommGrpCat.hasColimitsOfShape; Mathlib/Algebra/Category/ModuleCat/Colimits.lean::ModuleCat.hasColimitsOfSize — Pinned Mathlib expresses cocompleteness as existence of all small colimits and supplies it for sets, abelian groups and module categories, matching the source examples.
Construction/comparison — As a Natural Transformation A.5.2
The diagonal Δ:A→A^I sends A to the constant diagram. The structure maps of a limit form Δ(lim F)⇒F and those of a colimit form F⇒Δ(colim F), anticipating the adjunctions with Δ.
Formalized. Mathlib/CategoryTheory/Functor/Const.lean::Functor.const; Mathlib/CategoryTheory/Limits/HasLimits.lean::constLimAdj, colimConstAdj — The constant/diagonal functor is the source diagonal functor into the diagram category; pinned Mathlib proves it left-adjoint to lim and right-adjoint to colim, so limit cones and colimit cocones are exactly the corresponding natural-transformation universal properties.
Definition — Filtered Categories and Direct Limits A.5.3
A small category I is filtered when any two objects admit a common successor and any two parallel arrows become equal after postcomposition; directed posets are the special poset case.
Formalized. Mathlib/CategoryTheory/Filtered/Basic.lean::IsFilteredOrEmpty, IsFiltered, isDirectedOrder — Pinned Mathlib’s filtered-category structure contains the common-target/common-equalizer axioms plus nonemptiness, and relates filtered preorders to directed orders, exactly the source definition/example.
Example/comparison — translation category of an abelian monoid
For an abelian monoid M, the category with objects M and morphisms i→j given by multipliers m with mi=j is filtered; this is the translation-category example used for localization.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: For an abelian monoid M, the category with objects M and morphisms i→j given by multipliers m with mi=j is filtered; this is the translation-category example used for localization. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
Convention/notation — filtered colimits and direct limits
A filtered colimit is the colimit of a functor from a filtered category; over a directed poset it is also called a direct limit. The paragraph records the colim/lim notation used in the book.
Formalized. Mathlib/CategoryTheory/Filtered/Basic.lean::IsFiltered; Mathlib/CategoryTheory/Limits/HasLimits.lean::colimit, colimit.ι; Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean — A filtered/direct limit is represented in pinned Mathlib literally as the colimit of a diagram whose index category carries IsFiltered; the generic colimit object and structure maps supply the source notation/interface.
Example A.5.4
For I=N, a covariant diagram is a sequence A_0→A_1→⋯ with direct limit colim A_i; a contravariant diagram is an inverse tower with inverse limit.
Formalized. Mathlib/CategoryTheory/Category/Preorder.lean::Preorder.smallCategory; Mathlib/CategoryTheory/Limits/HasLimits.lean::limit, colimit — The natural numbers and their opposite are categories via their preorder structures, so functors from them are precisely direct sequences and inverse towers; pinned generic limits/colimits give their inverse/direct limits as stated.
A.6.1 (adjoint functors)
L:A→B and R:B→A are adjoint when Hom_B(LA,B)≅Hom_A(A,RB) naturally in A and B; L is the left adjoint and R the right adjoint.
Formalized. Mathlib/CategoryTheory/Adjunction/Basic.lean::Adjunction, Adjunction.mkOfHomEquiv, Adjunction.homEquiv — Pinned Mathlib defines an adjunction by the same natural family of Hom-set equivalences (and equivalent unit/counit data), exactly the source definition.
Example/comparison — standard adjunctions
The free k-vector-space functor is left adjoint to the underlying-set functor; for an R-module B, −⊗_R B is left adjoint to Hom_Ab(B,−) with the indicated module structure.
Not formalized. none; only partial/specialized adjacent category-theory infrastructure was found — As of 2026-09-06, no checked A/P/H/open/external/indexed Lean declaration realizes the whole source bundle: The free k-vector-space functor is left adjoint to the underlying-set functor; for an R-module B, −⊗_R B is left adjoint to Hom_Ab(B,−) with the indicated module structure. Strict bundle semantics reject a specialization, one example among several, a metatheoretic comment, an unformalized negative clause, or a proper subset as the route for the row.
Searched: N
Theorem A.6.2
An adjunction determines unit η:id_A⇒RL and counit ε:LR⇒id_B; transposition is expressed by R(f)η and εL(g), and the two triangle composites are identities.
Formalized. Mathlib/CategoryTheory/Adjunction/Basic.lean::Adjunction.unit, Adjunction.counit, Adjunction.left_triangle_components, right_triangle_components, homEquiv_id, homEquiv_symm_id — Pinned Mathlib exposes unit/counit, triangle identities, and the Hom-equivalence transposition formulas, exactly the source construction.
Definition — Reflective Subcategories A.6.3
A subcategory B⊂A is reflective when its inclusion has a left adjoint L:A→B, called the reflection; for full B the reflected B-objects are naturally isomorphic to themselves.
Formalized. Mathlib/CategoryTheory/Adjunction/Reflective.lean::Reflective, reflector, reflectorAdjunction, Functor.fullyFaithfulOfReflective, Functor.essImage.unit_isIso — Pinned Mathlib defines a reflective full subcategory by a fully faithful right adjoint with a left reflector and proves the unit is an isomorphism on reflected objects, exactly the source definition and self-reflection property.
examples of reflective subcategories
Ab is reflective in Groups via abelianization G↦G/[G,G]; sheaves on X are reflective in presheaves via sheafification.
Formalized. Mathlib/Algebra/Category/Grp/Adjunctions.lean::GrpCat.abelianize, GrpCat.abelianizeAdj; Mathlib/CategoryTheory/Sites/Sheafification.lean::presheafToSheaf, sheafificationAdjunction, sheafification_reflective — Pinned Mathlib proves abelianization left adjoint to the inclusion/forgetful functor from abelian groups and sheafification left adjoint to inclusion of sheaves into presheaves, exactly the two reflective examples.