# 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).

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

## Instances For

## Equations

- ⋯ = ⋯