Theorems · Theorem · category theory

DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE

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

Defined in

Mathlib.Algebra.Homology.DerivedCategory.Fractions

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianHasDerivedCategoryCochainComplex.IsStrictlyGECochainComplex.IsStrictlyLECochainComplex.IsStrictlyGE