Theorems · Theorem · category theory

DerivedCategory.left_fac_of_isStrictlyGE

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {X Y : CochainComplex C ℤ} (f : DerivedCategory.Q.obj X ⟶ DerivedCategory.Q.obj Y)
  (n : ℤ) [Y.IsStrictlyGE n],
  ∃ Y',
    ∃ (_ : Y'.IsStrictlyGE n),
      ∃ g s,
        ∃ (x : CategoryTheory.IsIso (DerivedCategory.Q.map s)),
          f =
            CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map g) (CategoryTheory.inv (DerivedCategory.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.

Defined in

Mathlib.Algebra.Homology.DerivedCategory.Fractions

Cited by

2 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategoryCochainComplex.IsStrictlyGE