Factorization lemma

In this file, we shall show that if f : K ⟶ L is a morphism between bounded below cochain complexes in an abelian category with enough injectives, there exists a factorization ι ≫ π = f with ι : K ⟶ K' a monomorphism that is also a quasimorphism and π : K' ⟶ L a morphism which degreewise is an epimorphism with an injective kernel, while K' is also bounded below (with precise bounds depending on the available bounds for K and L): this is CochainComplex.Plus.modelCategoryQuillen.cm5a (TODO). Using the factorization obtained in the file Mathlib/Algebra/Homology/Factorizations/CM5b.lean, we may assume f : K ⇨ L is a monomorphism (a case which appears as the lemma CochainComplex.Plus.modelCategoryQuillen.cm5a_cof (TODO)).

In the proof, the key (private) lemma shall be CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step which shows that if f is a monomorphism which is a quasi-isomorphism in degrees ≤ n₀ and n₀ + 1 = n₁, then f has a factorisation ι ≫ π = f where ι is a monomorphism that is a quasi-isomorphism in degrees ≤ n₁, and π is an isomorphism in degrees ≤ n₀ that is also a degreewise epimorphism with an injective kernel. The proof of step decomposes a two separate lemmas step₁ and step₂ (TODO): we first ensure that ι induces a monomorphism in homology in degree n₁, and we proceed further in step₂.

As we assume that both K and L are bounded below, we may find n₀ : ℤ such that K and L are striclty ≥ n₀ + 1: in particular, f induces an isomorphism in degrees ≤ n₀. Iterating the lemma step, we construct a projective system ℕᵒᵖ ⥤ CochainComplex C ℤ (see CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cochainComplexFunctor). Degreewise, this projective system is essentially constant, which allows to take its limit, which shall be the intermediate object in the lemma cm5a_cof (TODO).

def CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cofFib {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} (f : K ⟶ L) : CategoryTheory.ObjectProperty (CategoryTheory.Factorisation f)

Given a morphism f : K ⟶ L, this is the property of factorisations of f consisting of a monomorphism followed by a degreewise epimorphism with injective kernel.

Equations

• CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cofFib f F = (CategoryTheory.Mono F.ι ∧ CochainComplex.degreewiseEpiWithInjectiveKernel F.π)

def CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.quasiIsoLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {f : K ⟶ L} (n : ℤ) : CategoryTheory.ObjectProperty (cofFib f).FullSubcategory

The property that the first morphism of a factorisation is a quasi-isomorphisms in degrees ≤ n.

Equations

• CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.quasiIsoLE n F = ∀ i ≤ n, QuasiIsoAt F.obj.ι i

def CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isIsoLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {f : K ⟶ L} (n : ℤ) : CategoryTheory.ObjectProperty (cofFib f).FullSubcategory

The property that the second morphism of a factorisation is an isomorphism in degrees ≤ n.

Equations

• CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isIsoLE n F = ∀ i ≤ n, CategoryTheory.IsIso (F.obj.π.f i)

This section provides the material in order to prove the lemma step₁ below. Given a monomorphism f : K ⟶ L in CochainComplex C ℤ which is a quasi-isomorphism in degrees ≤ n₀ (with n₀ + 1 = n₁), we construct a factorization ι f n₁ ≫ π K L n₁ = f where the intermediate object mid K L n₁ is S K n₁ ⊞ L, with S K n₁ the single complex in degree n₁ given by an injective object containing K.opcycles n₁ (which is a cokernel of the differential K.X n₀ ⟶ K.X n₁). We obtain that ι f n₁ is a quasi-isomorphism in degrees ≤ n₀ and induces a monomorphism in homology in degree n₀, and that π K L n₁ is an isomorphism in degrees ≤ n₀ that is also a degreewise epimorphism with an injective kernel.

theorem CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} (f : K ⟶ L) [CategoryTheory.EnoughInjectives C] [CategoryTheory.Mono f] (n₀ n₁ : ℤ) (hf : ∀ i ≤ n₀, QuasiIsoAt f i) (hn₁ : n₀ + 1 = n₁ := by lia) : ∃ (F : (cofFib f).FullSubcategory), quasiIsoLE n₀ F ∧ isIsoLE n₀ F ∧ CategoryTheory.Mono (HomologicalComplex.homologyMap F.obj.ι n₁)