Calculus of fractions in the derived category

We obtain various consequences of the calculus of left and right fractions for HomotopyCategory.quasiIso C (ComplexShape.up ℤ) as lemmas about factorizations of morphisms f : Q.obj X ⟶ Q.obj Y (where X and Y are cochain complexes). These f can be factored as a right fraction inv (Q.map s) ≫ Q.map g or as a left fraction Q.map g ≫ inv (Q.map s), with s a quasi-isomorphism (to X or from Y). When strict bounds are known on X or Y, certain bounds may also be ensured on the auxiliary object appearing in the fraction.

instance DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasLeftCalculusOfFractions

instance DerivedCategory.instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasRightCalculusOfFractions

theorem DerivedCategory.right_fac {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {X Y : CochainComplex C ℤ} (f : Q.obj X ⟶ Q.obj Y) : ∃ (X' : CochainComplex C ℤ) (s : X' ⟶ X) (x : CategoryTheory.IsIso (Q.map s)) (g : X' ⟶ Y), f = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (Q.map s)) (Q.map g)

Any morphism f : Q.obj X ⟶ Q.obj Y in the derived category can be written as f = inv (Q.map s) ≫ Q.map g with s : X' ⟶ X a quasi-isomorphism and g : X' ⟶ Y.

theorem DerivedCategory.left_fac {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {X Y : CochainComplex C ℤ} (f : Q.obj X ⟶ Q.obj Y) : ∃ (Y' : CochainComplex C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x : CategoryTheory.IsIso (Q.map s)), f = CategoryTheory.CategoryStruct.comp (Q.map g) (CategoryTheory.inv (Q.map s))

Any morphism f : Q.obj X ⟶ Q.obj Y in the derived category can be written as f = Q.map g ≫ inv (Q.map s) with g : X ⟶ Y' and s : Y ⟶ Y' a quasi-isomorphism.

theorem DerivedCategory.right_fac_of_isStrictlyLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {X Y : CochainComplex C ℤ} (f : Q.obj X ⟶ Q.obj Y) (n : ℤ) [X.IsStrictlyLE n] : ∃ (X' : CochainComplex C ℤ) (_ : X'.IsStrictlyLE n) (s : X' ⟶ X) (x : CategoryTheory.IsIso (Q.map s)) (g : X' ⟶ Y), f = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (Q.map s)) (Q.map g)

Any morphism f : Q.obj X ⟶ Q.obj Y in the derived category with X strictly ≤ n can be written as f = inv (Q.map s) ≫ Q.map g with s : X' ⟶ X a quasi-isomorphism with X' strictly ≤ n and g : X' ⟶ Y.

theorem DerivedCategory.left_fac_of_isStrictlyGE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {X Y : CochainComplex C ℤ} (f : Q.obj X ⟶ Q.obj Y) (n : ℤ) [Y.IsStrictlyGE n] : ∃ (Y' : CochainComplex C ℤ) (_ : Y'.IsStrictlyGE n) (g : X ⟶ Y') (s : Y ⟶ Y') (x : CategoryTheory.IsIso (Q.map s)), f = CategoryTheory.CategoryStruct.comp (Q.map g) (CategoryTheory.inv (Q.map s))

Any morphism f : Q.obj X ⟶ Q.obj Y in the derived category with Y strictly ≥ n can be written as f = Q.map g ≫ inv (Q.map s) with g : X ⟶ Y' and s : Y ⟶ Y' a quasi-isomorphism with Y' strictly ≥ n.

theorem DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {X Y : CochainComplex C ℤ} (a b : ℤ) [X.IsStrictlyGE a] [X.IsStrictlyLE b] [Y.IsStrictlyGE a] (f : Q.obj X ⟶ Q.obj Y) : ∃ (X' : CochainComplex C ℤ) (_ : X'.IsStrictlyGE a) (_ : X'.IsStrictlyLE b) (s : X' ⟶ X) (x : CategoryTheory.IsIso (Q.map s)) (g : X' ⟶ Y), f = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (Q.map s)) (Q.map g)

Any morphism f : Q.obj X ⟶ Q.obj Y in the derived category with X strictly ≥ a and ≤ b, and Y strictly ≥ a can be written as f = inv (Q.map s) ≫ Q.map g with s : X' ⟶ X a quasi-isomorphism with X' strictly ≥ a and ≤ b, and g : X' ⟶ Y.

theorem DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {X Y : CochainComplex C ℤ} (a b : ℤ) [X.IsStrictlyLE b] [Y.IsStrictlyGE a] [Y.IsStrictlyLE b] (f : Q.obj X ⟶ Q.obj Y) : ∃ (Y' : CochainComplex C ℤ) (_ : Y'.IsStrictlyGE a) (_ : Y'.IsStrictlyLE b) (g : X ⟶ Y') (s : Y ⟶ Y') (x : CategoryTheory.IsIso (Q.map s)), f = CategoryTheory.CategoryStruct.comp (Q.map g) (CategoryTheory.inv (Q.map s))

Any morphism f : Q.obj X ⟶ Q.obj Y in the derived category with X strictly ≤ b, and Y strictly ≥ a and ≤ b can be written as f = Q.map g ≫ inv (Q.map s) with g : X ⟶ Y' and s : Y ⟶ Y' a quasi-isomorphism with Y' strictly ≥ a and ≤ b.

theorem DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X Y : CochainComplex C ℤ) (a b : ℤ) (h : a < b) [X.IsStrictlyLE a] [Y.IsStrictlyGE b] : Subsingleton (Q.obj X ⟶ Q.obj Y)