feat(CategoryTheory): the localization w.r.t. a Serre class is an abelian category

[joelriou]

---

• depends on: [Merged by Bors] - feat(CategoryTheory): results abouts kernels and pullback squares #34495
• depends on: [Merged by Bors] - feat(CategoryTheory): transport a NormalMono structure via an isomorphism of arrows #34496
• depends on: [Merged by Bors] - feat(CategoryTheory/Abelian): mono/epi/iso modulo a Serre class are stable under (co)base change #34498

[github-actions]

PR summary 24d904ee7b

Import changes exceeding 2%

%	File
+3.59%	Mathlib.CategoryTheory.Abelian.Basic
+4.10%	Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty	781	813	+32 (+4.10%)
Mathlib.CategoryTheory.Abelian.Basic	724	750	+26 (+3.59%)

Import changes for all files

Files	Import difference
161 files Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.AlgCat.Basic Mathlib.Algebra.Category.AlgCat.Limits 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.CommAlgCat.Basic Mathlib.Algebra.Category.CommAlgCat.FiniteType Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.Colimits Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Grp.LargeColimits Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.HopfAlgCat.Basic Mathlib.Algebra.Category.HopfAlgCat.Monoidal Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.ExteriorPower Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric 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.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Algebra.Module.CharacterModule Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.CategoryTheory.Abelian.CommSq Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Limits.ExactFunctor Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.CategoryTheory.Preadditive.Transfer Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.CommShiftTwo 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.Triangulated.Basic Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Triangle Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.Rotate Mathlib.CategoryTheory.Triangulated.SpectralObject Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat 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.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.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.Tensor Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.Morita.Matrix Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.LocallyStandardSmooth Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.StandardSmoothOfFree Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Unramified.LocalRing	1
11 files Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Condensed.AB Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.EffectiveEpi Mathlib.Condensed.Light.InternallyProjective Mathlib.Condensed.Light.Monoidal	3
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization	4
192 files Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting Mathlib.Algebra.Category.ModuleCat.Ext.Finite Mathlib.Algebra.Category.ModuleCat.Ext.HasExt Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Localization Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.CochainComplexOpposite Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.DerivedCategory.Basic 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.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.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom Mathlib.Algebra.Homology.DerivedCategory.TStructure Mathlib.Algebra.Homology.Embedding.AreComplementary Mathlib.Algebra.Homology.Embedding.CochainComplex 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.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.Factorizations.CM5b Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.HomotopyCategory.Acyclic 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.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.KInjective Mathlib.Algebra.Homology.HomotopyCategory.KProjective Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.LeftResolution.Basic Mathlib.Algebra.Homology.LeftResolution.Reduced Mathlib.Algebra.Homology.LeftResolution.Transport Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Module.PID 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.MooreComplex Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Injective.Ext Mathlib.CategoryTheory.Abelian.Injective.Extend Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Ext Mathlib.CategoryTheory.Abelian.Projective.Extend Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Module Mathlib.Condensed.EffectiveEpi Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.Small Mathlib.FieldTheory.Galois.NormalBasis Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.MulChar.Duality Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality 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.Induced Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Regular.Category Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Successor	5
3 files Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid	6
Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent	7
4 files Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free	8
6 files Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Equivalence Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full	10
3 files Mathlib.CategoryTheory.Action.Monoidal Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Rep	11
Mathlib.CategoryTheory.Sites.Abelian	18
Mathlib.CategoryTheory.Idempotents.SimplicialObject	19
3 files Mathlib.Algebra.Category.FGModuleCat.Abelian Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield Mathlib.CategoryTheory.Triangulated.Yoneda	20
3 files Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Opposite.OpOp	21
Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Homology.ShortComplex.Ab	22
9 files Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated	23
Mathlib.CategoryTheory.Action.Limits	24
16 files Mathlib.Algebra.Homology.ExactSequenceFour Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.CategoryTheory.Abelian.Basic Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.SerreClass.Basic Mathlib.CategoryTheory.Idempotents.Basic Mathlib.CategoryTheory.ObjectProperty.EpiMono Mathlib.CategoryTheory.ObjectProperty.Extensions Mathlib.CategoryTheory.Triangulated.HomologicalFunctor	26
8 files Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.CategoryTheory.Abelian.Opposite Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.CategoryTheory.Idempotents.Karoubi	27
Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty	32
Mathlib.CategoryTheory.Abelian.SerreClass.Localization (new file)	855

---

Declarations diff

+ abelian
+ epiModSerre.isoModSerre_image_ι
+ epiModSerre_zero_iff
+ epi_iff
+ epi_map_iff
+ essImage_whiskeringLeft
+ exactFunctor_comp_iff
+ exists_comp_isoModSerre_eq_zero_iff
+ exists_comp_monoModSerre_eq_zero_iff
+ exists_epiModSerre_comp_eq_zero_iff
+ exists_isoModSerre_comp_eq_zero_iff
+ hasBinaryProducts
+ hasCoequalizers
+ hasCokernels
+ hasEqualizers
+ hasFiniteProducts
+ hasKernels
+ hasZeroObject
+ instance : (MorphismProperty.epimorphisms C).IsStableUnderBaseChange
+ instance : (MorphismProperty.monomorphisms C).IsStableUnderCobaseChange
+ instance : (exactFunctor C D).IsClosedUnderIsomorphisms := by
+ instance : (leftExactFunctor C D).IsClosedUnderIsomorphisms
+ instance : (rightExactFunctor C D).IsClosedUnderIsomorphisms
+ instance : (whiskeringLeft L P E).Faithful
+ instance : (whiskeringLeft L P E).Full
+ instance : P.epiModSerre.IsStableUnderBaseChange
+ instance : P.epiModSerre.IsStableUnderCobaseChange
+ instance : P.isoModSerre.HasLeftCalculusOfFractions
+ instance : P.isoModSerre.HasRightCalculusOfFractions
+ instance : P.isoModSerre.IsStableUnderBaseChange := by
+ instance : P.isoModSerre.IsStableUnderCobaseChange := by
+ instance : P.monoModSerre.IsStableUnderBaseChange
+ instance : P.monoModSerre.IsStableUnderCobaseChange
+ instance : W.Q.EssSurj
+ inverseImage_epimorphisms
+ inverseImage_isomorphisms
+ inverseImage_monomorphisms
+ isIso_map_iff
+ isNormalEpiCategory
+ isNormalMonoCategory
+ isZero_obj_iff
+ isoModSerre_zero_iff
+ map_comp_eq_zero_iff_of_epi_mono
+ map_eq_zero_iff
+ monoModSerre.isoModSerre_factorThruImage
+ monoModSerre_zero_iff
+ mono_iff
+ mono_map_iff
+ preservesCokernel
+ preservesEpimorphisms
+ preservesFiniteColimits
+ preservesFiniteColimits_comp_iff
+ preservesFiniteLimits
+ preservesFiniteLimits_comp_iff
+ preservesKernel
+ preservesMonomorphisms
+ whiskeringLeft
+ whiskeringLeft_obj_obj
++ fullyFaithfulWhiskeringLeft

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh 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).

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory): results abouts kernels and pullback squares #34495
• [Merged by Bors] - feat(CategoryTheory): transport a NormalMono structure via an isomorphism of arrows #34496
• [Merged by Bors] - feat(CategoryTheory/Abelian): mono/epi/iso modulo a Serre class are stable under (co)base change #34498
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.