Skip to content

chore(CategoryTheory): deprecate leftExactFunctor - #45418

Open
joelriou wants to merge 11 commits into
leanprover-community:masterfrom
joelriou:deprecate-left-exact-functor
Open

chore(CategoryTheory): deprecate leftExactFunctor#45418
joelriou wants to merge 11 commits into
leanprover-community:masterfrom
joelriou:deprecate-left-exact-functor

Conversation

@joelriou

@joelriou joelriou commented Oct 28, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

The property of objects leftExactFunctor in functor categories is deprecated in favour of ObjectProperty.preservesFiniteLimits. The definition of the typeclass HasExactColimitsOfShape is moved to a separate file Mathlib/CategoryTheory/Limits/HasExactLimitsOfShape.lean with reduced imports in order to avoid a cycle of imports. Results about exact colimits are moved out of Mathlib/CategoryTheory/ObjectProperty/FunctorCategory/PreservesLimits.lean to a new file ExactColimits.lean. A new file Mathlib/CategoryTheory/ObjectProperty/BinaryProductsClosure.lean is also added by part of the content of FiniteProducts.lean in order to avoid importing set theory definitions in some algebra files.

The large-import label is probably not too bad. Two files have more imports, but overall it seems that many other files have reduced imports (I had to manually add some import lines in downstream files because they were no longer imported).

@joelriou joelriou added the t-category-theory Category theory label Oct 28, 2026
@github-actions github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Oct 28, 2026
@github-actions

github-actions Bot commented Oct 28, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary be687079c1

Import changes exceeding 2%

% File
+7.18% Mathlib.CategoryTheory.Limits.ExactFunctor
+4.47% Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits 1189 790 -399 (-33.56%)
Mathlib.CategoryTheory.ObjectProperty.FiniteProducts 1043 788 -255 (-24.45%)
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory 1023 795 -228 (-22.29%)
Mathlib.CategoryTheory.Limits.ExactFunctor 738 791 +53 (+7.18%)
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor 850 888 +38 (+4.47%)
Mathlib.Algebra.Category.Grp.LeftExactFunctor 957 963 +6 (+0.63%)
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic 1022 1027 +5 (+0.49%)
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected 1024 1029 +5 (+0.49%)
Mathlib.Algebra.Homology.GrothendieckAbelian 1053 1058 +5 (+0.47%)
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim 1067 1072 +5 (+0.47%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda 1244 1249 +5 (+0.40%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives 1294 1299 +5 (+0.39%)
Mathlib.Algebra.Category.Grp.AB 1543 1548 +5 (+0.32%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu 1672 1677 +5 (+0.30%)
Mathlib.Topology.Sheaves.Abelian 1772 1777 +5 (+0.28%)
Mathlib.Topology.Sheaves.AddCommGrpCat 1773 1778 +5 (+0.28%)
Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Limits.Types.PreservesLimit Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits -399
Mathlib.CategoryTheory.ObjectProperty.FiniteLimits Mathlib.CategoryTheory.ObjectProperty.FiniteProducts -255
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory -228
Mathlib.CategoryTheory.Abelian.Subcategory -172
Mathlib.CategoryTheory.Galois.ContAction Mathlib.CategoryTheory.Galois.FullSubcategory -28
18 files Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.OpOp Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated Mathlib.CategoryTheory.Triangulated.Orthogonal Mathlib.CategoryTheory.Triangulated.SpectralObject Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc Mathlib.CategoryTheory.Triangulated.TStructure.Induced Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject Mathlib.CategoryTheory.Triangulated.TStructure.TExact Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE Mathlib.CategoryTheory.Triangulated.Yoneda
 -26
46 files Mathlib.Algebra.Category.ModuleCat.Ext.Basic Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting Mathlib.Algebra.Category.ModuleCat.Ext.HasExt Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear Mathlib.Algebra.Homology.DerivedCategory.Ext.MapAdjunction Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective Mathlib.Algebra.Homology.DerivedCategory.Ext.Map Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure Mathlib.Algebra.Homology.DerivedCategory.Fractions Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.KInjective Mathlib.Algebra.Homology.DerivedCategory.KProjective Mathlib.Algebra.Homology.DerivedCategory.Linear Mathlib.Algebra.Homology.DerivedCategory.Plus Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom Mathlib.Algebra.Homology.DerivedCategory.TStructure Mathlib.Algebra.Homology.Factorizations.CM5a Mathlib.Algebra.Homology.HomotopyCategory.Acyclic Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.KInjective Mathlib.Algebra.Homology.HomotopyCategory.KProjective Mathlib.Algebra.Homology.HomotopyCategory.Plus Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject Mathlib.Algebra.Homology.ModelCategory.Injective Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Injective.Ext Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Ext Mathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Projective Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.ExactSequences Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
 -25
Mathlib.Algebra.Category.ModuleCat.Ext.Baer Mathlib.Algebra.Category.ModuleCat.InjectiveDimension -24
Mathlib.Algebra.Category.Ring.Under.Property -4
6 files Mathlib.Algebra.Category.ModuleCat.Ext.Finite Mathlib.RingTheory.Depth.Basic Mathlib.RingTheory.Depth.Rees Mathlib.RingTheory.LocalProperties.InjectiveDimension Mathlib.RingTheory.LocalProperties.ProjectiveDimension Mathlib.RingTheory.Regular.ProjectiveDimension
 -2
Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt 1
Mathlib.CategoryTheory.Triangulated.Generators 3
259 files Mathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Category.CommBialgCat Mathlib.Algebra.Category.CommHopfAlgCat Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.Localization Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.OfCommRing Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf.Submodule Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.ModuleCat.Stalk Mathlib.Algebra.Category.ModuleCat.Ulift Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.CochainComplexPlus Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.Algebra.Homology.EulerCharacteristic Mathlib.Algebra.Homology.Factorizations.CM5b Mathlib.Algebra.Homology.HomotopyCategory.ChainComplex Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Homology.ModelCategory.Lifting Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Module.PID Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.AlgClosed.Basic Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.Birational.Birational Mathlib.AlgebraicGeometry.Birational.Composition Mathlib.AlgebraicGeometry.Birational.Dominant Mathlib.AlgebraicGeometry.Birational.RationalMap Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EffectiveEpi Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.Geometrically.Basic Mathlib.AlgebraicGeometry.Geometrically.Connected Mathlib.AlgebraicGeometry.Geometrically.Integral Mathlib.AlgebraicGeometry.Geometrically.Irreducible Mathlib.AlgebraicGeometry.Geometrically.Reduced Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Affine Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono Mathlib.AlgebraicGeometry.Morphisms.FlatRank Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.OrderOfVanishing Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.Affine Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.ConstantSheaf Mathlib.AlgebraicGeometry.Sites.Fpqc Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularHomology.HomologyZero Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Injective.Extend Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Extend Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Limits.Indization.Category Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Sites.Abelian Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Module Mathlib.Condensed.EffectiveEpi Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.EffectiveEpi Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.InternallyProjective Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.Monoidal Mathlib.Condensed.Light.Sequence Mathlib.Condensed.Light.Small Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.FieldTheory.Galois.NormalBasis Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.LinearAlgebra.FreeModule.ModN Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.RepresentationTheory.Action Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.ContCohomology.Basic Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree Mathlib.RepresentationTheory.Homological.ContCohomology.Sha Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro Mathlib.RepresentationTheory.Homological.GroupHomology.Basic Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro Mathlib.RepresentationTheory.Homological.Resolution Mathlib.RepresentationTheory.Homological.TateCohomology.Basic Mathlib.RepresentationTheory.Induced Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Rep.Basic Mathlib.RepresentationTheory.Rep.Iso Mathlib.RepresentationTheory.Rep.Res Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Regular.Category Mathlib.RingTheory.SimpleRing.DivisionRing Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.Sheaves.Module
 4
60 files Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Sites.AffineEtale Mathlib.AlgebraicGeometry.Sites.EtalePoint Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.PresheafOfModules Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.SheafOfModules Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Sites.LocalSite Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Sites.Point.Comap Mathlib.CategoryTheory.Sites.Point.Conservative Mathlib.CategoryTheory.Sites.Point.IsMonoidalW Mathlib.CategoryTheory.Sites.Point.Map Mathlib.CategoryTheory.Sites.Point.Monoidal Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered Mathlib.CategoryTheory.Sites.Point.Over Mathlib.CategoryTheory.Sites.Point.Presheaf Mathlib.CategoryTheory.Sites.Point.Skyscraper Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.Condensed.AB Mathlib.Condensed.Light.AB Mathlib.Topology.Sheaves.Abelian Mathlib.Topology.Sheaves.AddCommGrpCat Mathlib.Topology.Sheaves.Flasque Mathlib.Topology.Sheaves.Points
 5
114 files Mathlib.Algebra.Category.Grp.LeftExactFunctor Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.CochainComplexOpposite Mathlib.Algebra.Homology.Embedding.AreComplementary Mathlib.Algebra.Homology.Embedding.Connect Mathlib.Algebra.Homology.Embedding.ExtendHomology Mathlib.Algebra.Homology.Embedding.ExtendHomotopy Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.Embedding.Splitting Mathlib.Algebra.Homology.Embedding.StupidTrunc Mathlib.Algebra.Homology.Embedding.TruncGEHomology Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.Algebra.Homology.Embedding.TruncLEHomology Mathlib.Algebra.Homology.Embedding.TruncLE Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.HomotopyFiber Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.LeftResolution.Basic Mathlib.Algebra.Homology.LeftResolution.Reduced Mathlib.Algebra.Homology.LeftResolution.Transport Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.Precylinder Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.SpectralObject.Cycles Mathlib.Algebra.Homology.SpectralObject.Differentials Mathlib.Algebra.Homology.SpectralObject.EpiMono Mathlib.Algebra.Homology.SpectralObject.FirstPage Mathlib.Algebra.Homology.SpectralObject.Homology Mathlib.Algebra.Homology.SpectralObject.Page Mathlib.Algebra.Homology.SpectralObject.SpectralSequence Mathlib.Algebra.Homology.SpectralSequence.Basic Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance Mathlib.AlgebraicTopology.SimplicialSet.Homology.MapHomologicalComplex Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate Mathlib.AlgebraicTopology.SimplicialSet.Homology.Relative Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.OrthogonalClosed Mathlib.CategoryTheory.Abelian.Preradical.Colon Mathlib.CategoryTheory.Abelian.Preradical.Radical Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.SerreClass.Localization Mathlib.CategoryTheory.Abelian.ShortExact Mathlib.CategoryTheory.Abelian.TorsionTheory.Basic Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Functor.ReflectsIso.Exact Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ Mathlib.CategoryTheory.Monoidal.Cartesian.Grp Mathlib.CategoryTheory.Monoidal.Cartesian.Normal Mathlib.CategoryTheory.Monoidal.Cartesian.Over Mathlib.CategoryTheory.Monoidal.Cartesian.Ring Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda Mathlib.CategoryTheory.Monoidal.CommGrp_ Mathlib.CategoryTheory.Monoidal.Grp_ Mathlib.CategoryTheory.Monoidal.Grp Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp Mathlib.CategoryTheory.Monoidal.Ring Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.ObjectProperty.Kernels Mathlib.CategoryTheory.ObjectProperty.Subobject Mathlib.CategoryTheory.Preadditive.CommGrp_ Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
 6
7 files Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.Linear Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.ObjectProperty.OrthogonalLimits
 7
99 files Mathlib.Algebra.Category.CommAlgCat.FiniteType Mathlib.Algebra.Category.Ring.Small Mathlib.Algebra.Lie.Basis.Base Mathlib.Algebra.Lie.Basis Mathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Algebra.Module.MinimalGenerators Mathlib.Algebra.Module.SpanRankOperations Mathlib.Algebra.Module.StablyFree.FreeOfInvertible Mathlib.Algebra.Module.Torsion.PrimaryComponent Mathlib.AlgebraicGeometry.EllipticCurve.LFunction Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty Mathlib.CategoryTheory.Localization.DerivabilityStructure.DerivesTriangulated Mathlib.LinearAlgebra.Matrix.Cartan.Realisation Mathlib.LinearAlgebra.RootSystem.BaseChange Mathlib.LinearAlgebra.RootSystem.BaseExists Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.RootSystem.CartanMatrix Mathlib.LinearAlgebra.RootSystem.Chain Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.Finite.G2 Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.Irreducible Mathlib.LinearAlgebra.RootSystem.IsValuedIn Mathlib.LinearAlgebra.RootSystem.Reduced Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion.FinitePlace Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.ExistsRamified Mathlib.NumberTheory.NumberField.FiniteAdeleRing Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.HilbertTheory Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.NumberTheory.RamificationInertia.Valuation Mathlib.RingTheory.AdicCompletion.LocalRing Mathlib.RingTheory.DedekindDomain.AdicValuation.Ramification Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.Etale.Descent Mathlib.RingTheory.Etale.Finite Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Etale.Weakly Mathlib.RingTheory.Flat.LocallyFree Mathlib.RingTheory.Flat.Rank Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.Ideal.Pure Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.LocalRing.Etale Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.Localization.AtPrime.Extension Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.RamificationInertia.Basic Mathlib.RingTheory.RamificationInertia.Ramification Mathlib.RingTheory.RegularLocalRing.Defs Mathlib.RingTheory.RegularLocalRing.Polynomial Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.LocallyStandardSmooth Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.Smooth.Fiber Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.Quotient Mathlib.RingTheory.Smooth.StandardSmoothOfFree Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.TotallySplit Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.LocalStructure Mathlib.Topology.Algebra.Ring.Compact
 11
Mathlib.CategoryTheory.Abelian.CommSq Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel 12
Mathlib.CategoryTheory.Distributive.Monoidal 14
Mathlib.CategoryTheory.Idempotents.SimplicialObject 18
Mathlib.Algebra.Category.Grp.IsFinite 19
5 files Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Equivalence Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full
 20
6 files Mathlib.Algebra.Category.FGModuleCat.Abelian Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Algebra.Homology.ShortComplex.Ab
 21
10 files Mathlib.Algebra.Category.CommAlgCat.Basic Mathlib.Algebra.Category.FGModuleCat.Colimits Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.RepresentationTheory.Continuous.TopRep
 22
11 files Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.LargeColimits Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Module.CharacterModule Mathlib.CategoryTheory.Abelian.SerreClass.Basic Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.Tensor Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.Morita.Matrix
 23
23 files Mathlib.Algebra.Category.AlgCat.FilteredColimits Mathlib.Algebra.Category.AlgCat.Limits Mathlib.Algebra.Category.AlgCat.TensorAlgebra Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.CategoryTheory.ObjectProperty.EpiMono Mathlib.CategoryTheory.ObjectProperty.Extensions Mathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
 24
16 files Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Homology.ExactSequenceFour Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.Pullback Mathlib.Algebra.Homology.ShortComplex.Pushout Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Algebra.Homology.SpectralObject.Basic Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Action.Limits Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures
 25
8 files Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.CategoryTheory.Abelian.Opposite Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.CategoryTheory.Idempotents.Karoubi Mathlib.CategoryTheory.Preadditive.LeftExact
 26
Mathlib.Algebra.Category.ModuleCat.FilteredColimits 32
11 files Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall Mathlib.CategoryTheory.Functor.Derived.LeftDerivedTriangulated Mathlib.CategoryTheory.Functor.Derived.RightDerivedTriangulated Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TStructure.Heart Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.CategoryTheory.Triangulated.WeakKernels
 33
Mathlib.CategoryTheory.Triangulated.TriangleShift 34
10 files Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.ExteriorPower Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
 35
15 files Mathlib.Algebra.Category.AlgCat.Monoidal Mathlib.Algebra.Category.AlgCat.Symmetric Mathlib.Algebra.Category.BialgCat.Basic Mathlib.Algebra.Category.BialgCat.Monoidal Mathlib.Algebra.Category.CoalgCat.Basic Mathlib.Algebra.Category.CoalgCat.ComonEquivalence Mathlib.Algebra.Category.CoalgCat.Monoidal Mathlib.Algebra.Category.HopfAlgCat.Basic Mathlib.Algebra.Category.HopfAlgCat.Monoidal Mathlib.Algebra.Category.ModuleCat.Products Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Shift.CommShiftTwo Mathlib.CategoryTheory.Triangulated.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Triangle Mathlib.CategoryTheory.Triangulated.Rotate
 36
6 files Mathlib.Algebra.Category.AlgCat.Basic Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.CategoryTheory.Monoidal.Internal.Module
 37
39 files Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Center.Linear Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Linear.Basic Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Limits.Cokernels Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Comma Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.CategoryTheory.Preadditive.Transfer Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Linear Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Shift.SingleFunctorsLift Mathlib.CategoryTheory.Triangulated.Opposite.Basic
 38
Mathlib.CategoryTheory.Limits.ExactFunctor 53
Mathlib.CategoryTheory.Limits.HasExactLimitsOfShape (new file) 794
Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.ExactColimits (new file) 813
Mathlib.CategoryTheory.ObjectProperty.BinaryProductsClosure (new file) 1044

Declarations diff (regex)

+ exactFunctor_le_preservesFiniteColimits
+ exactFunctor_le_preservesFiniteLimits
+ preservesFiniteColimits_le_additiveFunctor
+ preservesFiniteLimits_le_additiveFunctor
- instance : (leftExactFunctor C D).IsClosedUnderIsomorphisms
- instance : (rightExactFunctor C D).IsClosedUnderIsomorphisms

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit be68707).

  • +6 new declarations
  • −4 removed declarations
+CategoryTheory.exactFunctor_le_preservesFiniteColimits
+CategoryTheory.exactFunctor_le_preservesFiniteLimits
-CategoryTheory.instIsClosedUnderIsomorphismsFunctorLeftExactFunctor
-CategoryTheory.instIsClosedUnderIsomorphismsFunctorRightExactFunctor
+CategoryTheory.instPreservesFiniteColimitsObjFunctorPreservesFiniteColimits
-CategoryTheory.instPreservesFiniteColimitsObjFunctorRightExactFunctor
-CategoryTheory.instPreservesFiniteLimitsObjFunctorLeftExactFunctor
+CategoryTheory.instPreservesFiniteLimitsObjFunctorPreservesFiniteLimits
+CategoryTheory.preservesFiniteColimits_le_additiveFunctor
+CategoryTheory.preservesFiniteLimits_le_additiveFunctor

No changes to strong technical debt.
No changes to weak technical debt.

Current commit be687079c1
Reference commit 6100109f1d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@pre-commit-ci-lite
[pre-commit.ci lite] lake exe mk_all
bbda470 
These commands made the changes in this commit.
To make the same fixes yourself, run them in your mathlib4 checkout.
@joelriou joelriou changed the title chore(CategoryTheory): deprecated leftExactFunctor chore(CategoryTheory): deprecate leftExactFunctor Oct 28, 2026
@joelriou joelriou mentioned this pull request Oct 28, 2026
Open
1 task

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@joelriou