Basic definitions for factorizations lemmas

We define the class of morphisms degreewiseEpiWithInjectiveKernel : MorphismProperty (CochainComplex C ℤ) in the category of cochain complexes in an abelian category C.

When restricted to the full subcategory of bounded below cochain complexes in an abelian category C that has enough injectives, this is the class of fibrations for a model category structure on the bounded below category of cochain complexes in C. In this folder, we intend to prove two factorization lemmas in the category of bounded below cochain complexes (TODO):

• CM5a: any morphism K ⟶ L can be factored as K ⟶ K' ⟶ L where i : K ⟶ K' is a trivial cofibration (a mono that is also a quasi-isomorphisms) and p : K' ⟶ L is a fibration.
• CM5b: any morphism K ⟶ L can be factored as K ⟶ L' ⟶ L where i : K ⟶ L' is a cofibration (i.e. a mono) and p : L' ⟶ L is a trivial fibration (i.e. a quasi-isomorphism which is also a fibration)

The difficult part is CM5a (whose proof uses CM5b). These lemmas shall be essential ingredients in the proof that the bounded below derived category of an abelian category C with enough injectives identifies to the bounded below homotopy category of complexes of injective objects in C. This will be used in the construction of total derived functors (and a refactor of the sequence of derived functors).

def CochainComplex.degreewiseEpiWithInjectiveKernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.MorphismProperty (CochainComplex C ℤ)

A morphism of cochain complexes φ in an abelian category satisfies degreewiseEpiWithInjectiveKernel φ if for any i : ℤ, the morphism φ.f i is an epimorphism with an injective kernel.

Equations

• CochainComplex.degreewiseEpiWithInjectiveKernel φ = ∀ (i : ℤ), CategoryTheory.Abelian.epiWithInjectiveKernel (φ.f i)

instance CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CochainComplex.degreewiseEpiWithInjectiveKernel.IsMultiplicative

Equations

• ⋯ = ⋯