Factorization lemma

Let C be an abelian category with enough injectives. We show that any morphism f : K ⟶ L between bounded below cochain complexes in C can be factored as i ≫ p where i : K ⟶ L' is a monomorphism (with L' bounded below) and p : L' ⟶ L a quasi-isomorphism that is an epimorphism with a degreewise injective kernel. (This is part of the factorization axiom CM5 for a model category structure on bounded below cochain complexes (TODO @joelriou).)

noncomputable def CochainComplex.cm5b.I {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (K : CochainComplex C ℤ) : CochainComplex C ℤ

Given a cochain complex K, this is a cochain complex I K with zero differentials which in degree n consists of the injective object Injective.under (K.X n).

@[simp]

theorem CochainComplex.cm5b.I_X {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (K : CochainComplex C ℤ) (n : ℤ) : (I K).X n = CategoryTheory.Injective.under (K.X n)

@[simp]

theorem CochainComplex.cm5b.I_d {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (K : CochainComplex C ℤ) (x✝ x✝¹ : ℤ) : (I K).d x✝ x✝¹ = 0

instance CochainComplex.cm5b.instInjectiveXIntI {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K : CochainComplex C ℤ} (n : ℤ) : CategoryTheory.Injective ((I K).X n)

instance CochainComplex.cm5b.instIsStrictlyGEI {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K : CochainComplex C ℤ} (n : ℤ) [K.IsStrictlyGE n] : (I K).IsStrictlyGE n

instance CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (n : ℤ) [K.IsStrictlyGE (n + 1)] [L.IsStrictlyGE n] : (mappingCone (CategoryTheory.CategoryStruct.id (I K)) ⊞ L).IsStrictlyGE n

@[reducible, inline]

noncomputable abbrev CochainComplex.cm5b.p {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (K L : CochainComplex C ℤ) : mappingCone (CategoryTheory.CategoryStruct.id (I K)) ⊞ L ⟶ L

The second projection mappingCone (𝟙 (I K)) ⊞ L ⟶ L.

noncomputable def CochainComplex.cm5b.i {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) : K ⟶ mappingCone (CategoryTheory.CategoryStruct.id (I K)) ⊞ L

A lift of a morphism f : K ⟶ L between bounded below cochain complexes as a monomorphism K ⟶ mappingCone (𝟙 (I K)) ⊞ L.

theorem CochainComplex.cm5b.i_f_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ) : CategoryTheory.CategoryStruct.comp ((i f).f n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f n) ((mappingCone.snd (CategoryTheory.CategoryStruct.id (I K))).v n n ⋯)) = CategoryTheory.Injective.ι (K.X n)

theorem CochainComplex.cm5b.i_f_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ) {Z : C} (h : (I K).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((i f).f n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f n) (CategoryTheory.CategoryStruct.comp ((mappingCone.snd (CategoryTheory.CategoryStruct.id (I K))).v n n ⋯) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Injective.ι (K.X n)) h

instance CochainComplex.cm5b.instMonoFIntI {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ) : CategoryTheory.Mono ((i f).f n)

instance CochainComplex.cm5b.instMonoIntI {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) : CategoryTheory.Mono (i f)

@[simp]

theorem CochainComplex.cm5b.fac {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) : CategoryTheory.CategoryStruct.comp (i f) (p K L) = f

@[simp]

theorem CochainComplex.cm5b.fac_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) {Z : CochainComplex C ℤ} (h : L ⟶ Z) : CategoryTheory.CategoryStruct.comp (i f) (CategoryTheory.CategoryStruct.comp (p K L) h) = CategoryTheory.CategoryStruct.comp f h

instance CochainComplex.cm5b.instInjectiveXIntMappingConeIdI {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K : CochainComplex C ℤ} (n : ℤ) : CategoryTheory.Injective ((mappingCone (CategoryTheory.CategoryStruct.id (I K))).X n)

theorem CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (K L : CochainComplex C ℤ) : degreewiseEpiWithInjectiveKernel (p K L)

noncomputable def CochainComplex.cm5b.homotopyEquiv {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (K L : CochainComplex C ℤ) : HomotopyEquiv (mappingCone (CategoryTheory.CategoryStruct.id (I K)) ⊞ L) L

The second projection p K L : mappingCone (𝟙 (I K)) ⊞ L ⟶ L is a homotopy equivalence.

instance CochainComplex.cm5b.instQuasiIsoIntP {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} : QuasiIso (p K L)

theorem CochainComplex.cm5b {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ) [K.IsStrictlyGE (n + 1)] [L.IsStrictlyGE n] : ∃ (L' : CochainComplex C ℤ) (_ : L'.IsStrictlyGE n) (i : K ⟶ L') (p : L' ⟶ L) (_ : CategoryTheory.Mono i) (_ : degreewiseEpiWithInjectiveKernel p) (_ : QuasiIso p), CategoryTheory.CategoryStruct.comp i p = f