Theorems · Theorem · category theory

CochainComplex.Lifting.exists_hom

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) {Q : CochainComplex C ℤ} {π : B ⟶ Q} {hπ : CategoryTheory.CategoryStruct.comp i π = 0}
  (hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ)) {K : CochainComplex C ℤ}
  {ι : K ⟶ X} {hι : CategoryTheory.CategoryStruct.comp ι p = 0}
  (hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι)) (n m : ℤ)
  (hnm : autoParam (n + 1 = m) CochainComplex.Lifting.exists_hom._auto_1),
  ∃ φ,
    CategoryTheory.CategoryStruct.comp (π.f n) (CategoryTheory.CategoryStruct.comp φ (ι.f m)) =
      (↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm

Defined in

Mathlib.Algebra.Homology.ModelCategory.Lifting

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian