feat(Algebra/Homology): the injective model structure on bounded below cochain complexes

[joelriou]

When C is an abelian category with enough injectives, the category CochainComplex.Plus C of bounded below cochain complexes is endowed with a model category structure, where weak equivalences are quasi-isomorphisms, cofibrations are monomorphisms and fibrations are the epimorphisms that have a degreewise injective kernel.

In future PR, we shall deduce the injective derivability structures on bounded below cochain complexes in C and its homotopy category, which shall allow the construction of right derived functors, and when it is shown that these derived functors are triangulated, it will be possible to refactor Functor.rightDerived.

---

• depends on: [Merged by Bors] - feat(CategoryTheory/Shift): lifting of single functors #38632
• depends on: feat(CategoryTheory/Triangulated): localizing subcategories #38651
• depends on: [Merged by Bors] - chore(Algebra/Homology): fix name #38995
• depends on: [Merged by Bors] - feat(CategoryTheory/Limits): biprod.opIso #38996
• depends on: feat(Algebra/Homology): the homotopy fiber and the path object #38997
• depends on: feat(AlgebraicTopology/ModelCategory): precylinders in full subcategories #38998
• depends on: feat(Algebra/Homology): homology sequence and acyclic complexes #38999

[github-actions]

PR summary e336692c24

Import changes exceeding 2%

%	File
+3.55%	Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel	789	817	+28 (+3.55%)
Mathlib.Algebra.Homology.Factorizations.Basic	845	854	+9 (+1.07%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Homology.Factorizations.CM5a	3
Mathlib.Algebra.Homology.Factorizations.CM5b	8
Mathlib.Algebra.Homology.Factorizations.Basic	9
Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel	28
Mathlib.Algebra.Homology.HomotopyFiber (new file)	986
Mathlib.Algebra.Homology.Precylinder (new file)	1002
Mathlib.Algebra.Homology.HomotopyCategory.Plus (new file)	1395
Mathlib.Algebra.Homology.ModelCategory.Injective (new file)	1409

---

Declarations diff

+ HasCylinder
+ HasHomotopyFiber
+ HasPathObject
+ IsKInjective.eq_δ_of_cocycle
+ IsKInjective.eq_δ_of_cocycle'
+ IsTriangulatedClosed₂.of_isTriangulatedClosed₃
+ Plus
+ Plus.precylinder
+ Plus.prepathObject
+ Quotient.functor_obj_shift
+ acyclic_X₁
+ acyclic_X₃
+ cofibration_iff
+ commShiftIso_hom_inv_id_app
+ commShiftIso_inv_hom_id_app
+ decidableRelSymm
+ degreewiseEpiWithInjectiveKernel.epi
+ degreewiseEpiWithInjectiveKernel_iff_of_isZero
+ epiWithInjectiveKernel.hasLiftingProperty
+ epiWithInjectiveKernel_iff_of_isZero
+ fibration_iff
+ fullyFaithfulι
+ homotopyEquiv
+ homotopyFiber
+ homotopy₀₁
+ instance (i : α) : HasBinaryBiproduct (K.op.X i) (K.op.X i) := by
+ instance (n : ℤ) : (singleFunctor C n).Additive := by
+ instance :
+ instance : (cofibrations (Plus C)).HasFactorization (trivialFibrations (Plus C))
+ instance : (cofibrations (Plus C)).IsStableUnderRetracts
+ instance : (degreewiseEpiWithInjectiveKernel (C := C)).IsStableUnderRetracts
+ instance : (epiWithInjectiveKernel (C := C)).IsStableUnderRetracts
+ instance : (fibrations (Plus C)).IsStableUnderRetracts
+ instance : (opFunctor V c).IsEquivalence := (opEquivalence V c).isEquivalence_functor
+ instance : (opInverse V c).IsEquivalence := (opEquivalence V c).isEquivalence_inverse
+ instance : (plus C).IsStableUnderShift ℤ
+ instance : (quasiIso A).IsCompatibleWithShift ℤ
+ instance : (quasiIso A).RespectsIso := by
+ instance : (quasiIso C c).IsMultiplicative
+ instance : (quotient C).EssSurj
+ instance : (quotient C).Full := by dsimp [quotient]; infer_instance
+ instance : (trivialCofibrations (Plus C)).HasFactorization (fibrations (Plus C))
+ instance : (unopFunctor V c).IsEquivalence := (unopEquivalence V c).isEquivalence_functor
+ instance : (unopInverse V c).IsEquivalence := (unopEquivalence V c).isEquivalence_inverse
+ instance : (weakEquivalences (Plus C)).HasTwoOutOfThreeProperty
+ instance : (weakEquivalences (Plus C)).IsStableUnderRetracts
+ instance : HasHomotopyCofiber ((opFunctor C c).map φ.op)
+ instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms]
+ instance [A.IsVerdierRightLocalizing B] :
+ instance [HasBinaryBiproducts C] : HasHomotopyFiber φ
+ instance [HasZeroObject C] : (plus C).ContainsZero
+ instance [HasZeroObject C] [HasBinaryBiproducts C] :
+ instance [HasZeroObject C] [HasBinaryBiproducts C] : (plus C).IsTriangulated
+ instance [K.HasPathObject] :
+ instance {A B : CochainComplex.Plus C} (i : A ⟶ B) [Cofibration i] :
+ inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op
+ isFibrant_iff
+ isStrictlyGE_mappingCone
+ lift
+ lift_π₀
+ lift_π₁
+ lifting
+ op
+ pathObject
+ plus
+ plus_cylinder
+ plus_pathObject
+ plus_quotient_obj_iff
+ precylinder
+ prepathObject
+ quasiIso
+ quasiIso_iff
+ quotient
+ quotientCompι
+ quotient_obj_surjective
+ singleFunctor
+ singleFunctorCompιIso
+ singleFunctors
+ trW_inverseImage_ι_iff
+ triangulatedLocalizerMorphism
+ unop
+ weakEquivalence_iff
+ π₀
+ π₀CompιHomotopy
+ π₀_ι
+ π₁
+ π₁_ι
++ fullSubcategoryEquiv
++ instance [A.IsTriangulated] :
++ instance {A B X Y : CochainComplex.Plus C} (i : A ⟶ B) (p : X ⟶ Y)
++ isZero_X
++ map
++ toFullSubcategory
++ ι

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory/Shift): lifting of single functors #38632
• feat(CategoryTheory/Triangulated): localizing subcategories #38651
• [Merged by Bors] - chore(Algebra/Homology): fix name #38995
• [Merged by Bors] - feat(CategoryTheory/Limits): biprod.opIso #38996
• feat(Algebra/Homology): the homotopy fiber and the path object #38997
• feat(AlgebraicTopology/ModelCategory): precylinders in full subcategories #38998
• feat(Algebra/Homology): homology sequence and acyclic complexes #38999
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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