Theorems · Theorem · category theory

CochainComplex.Lifting.hasLift

∀ {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ι))
  (α : CochainComplex.HomComplex.Cochain Q K 0),
  CochainComplex.HomComplex.δ 0 1 α = ↑(CochainComplex.Lifting.cocycle₁ sq hsq hQ hK) → sq.HasLift

Consider a commutative square in the category CochainComplex C ℤ where C is an abelian category. `` t A ⟶ X i| |p v v B ⟶ Y b ` Assume that there exists a degreewise lifting B.X n ⟶ X.X n for any n : ℤ, that Q is a cokernel of i, and K is a kernel of p. If the cocycle cocycle₁ sq hsq hQ hK : Cocycle Q K 1 is a coboundary, we show that the square admits a lifting B ⟶ X`.

Defined in

Mathlib.Algebra.Homology.ModelCategory.Lifting

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian