[Merged by Bors] - feat(Algebra/Homology): a homology data from an epi-mono factorization

[joelriou]

Let S be a short complex in an abelian category. If K is a kernel of S.g and Q a cokernel of S.f, and K ⟶ H ⟶ Q is an epi-mono factorization of K ⟶ S.X₂ ⟶ Q, then H identifies to the homology of S.
(That shall be used when computing the homology of the differentials on pages of spectral sequences #33842.)
In this PR, we also show that ShortComplex C is an abelian category if C is abelian.

---

• depends on: [Merged by Bors] - feat(Algebra/Homology/ShortComplex): cycles can be computed with a limit kernel fork #33874

[github-actions]

PR summary 62a82d6d0a

Import changes exceeding 2%

%	File
+3.70%	Mathlib.Algebra.Homology.ShortComplex.Abelian

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Homology.ShortComplex.Abelian	729	756	+27 (+3.70%)
Mathlib.Algebra.Homology.ShortComplex.Exact	762	764	+2 (+0.26%)

Import changes for all files

Files	Import difference
97 files Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Localization Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.CochainComplexOpposite 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.TruncLE 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.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.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.HomologicalComplex Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Module.PID 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.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution 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.Coinvariants Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.Resolution Mathlib.RepresentationTheory.Induced Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Regular.Category Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Successor	1
63 files Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Homology.ExactSequenceFour Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.CategoryTheory.Abelian.CommSq Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization 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.Injective.Basic Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.SerreClass.Basic Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.ObjectProperty.EpiMono Mathlib.CategoryTheory.ObjectProperty.Extensions Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.OpOp Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Condensed.AB Mathlib.Condensed.Light.AB Mathlib.Topology.Sheaves.MayerVietoris	2
Mathlib.Algebra.Category.ModuleCat.Topology.Homology	3
Mathlib.Algebra.Homology.ShortComplex.Abelian	27

---

Declarations diff

+ cokernelSequence
+ cokernelSequence_exact
+ f'_eq
+ g'_eq
+ homologyIsoImageICyclesCompPOpcycles
+ homologyIsoImageICyclesCompPOpcycles_ι
+ homologyπ_isoHomology_inv
+ instance : Abelian (ShortComplex C)
+ instance : Epi (cokernelSequence f).g := by
+ instance : IsNormalEpiCategory (ShortComplex C) := ⟨fun p _ => ⟨by
+ instance : IsNormalMonoCategory (ShortComplex C) := ⟨fun i _ => ⟨by
+ instance : Mono (kernelSequence f).f := by
+ isoHomology
+ isoHomology_hom_comp_ι
+ isoHomology_inv_homologyι
+ isoImage
+ isoImage_ι
+ kernelSequence
+ kernelSequence_exact
+ leftHomologyData
+ ofEpiMonoFactorisation
+ rightHomologyData
+ π_comp_isoHomology_hom

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-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Algebra/Homology/ShortComplex): cycles can be computed with a limit kernel fork #33874
  By Dependent Issues (🤖). Happy coding!

[dagurtomas]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

[mathlib4-merge-conflict-bot]

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

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Post-Build Step
• Build