Theorems · Theorem · category theory

CochainComplex.Plus.modelCategoryQuillen.cm5a_cof

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [CategoryTheory.EnoughInjectives C] (n : ℤ) [K.IsStrictlyGE n]
  [L.IsStrictlyGE n] [CategoryTheory.Mono f],
  ∃ K',
    ∃ (_ : K'.IsStrictlyGE n),
      ∃ ι π,
        CategoryTheory.Mono ι ∧
          QuasiIso ι ∧ CochainComplex.degreewiseEpiWithInjectiveKernel π ∧ CategoryTheory.CategoryStruct.comp ι π = f

Defined in

Mathlib.Algebra.Homology.Factorizations.CM5a

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.EnoughInjectivesCochainComplex.IsStrictlyGECochainComplex.IsStrictlyGECategoryTheory.Mono