Theorems · Theorem · category theory

CochainComplex.mappingCone.descCocycle.congr_simp

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α α_1 : CochainComplex.HomComplex.Cochain F K m) (e_α : α = α_1)
  (β β_1 : CochainComplex.HomComplex.Cocycle G K n) (e_β : β = β_1) (h : m + 1 = n)
  (eq : CochainComplex.HomComplex.δ m n α = n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯),
  CochainComplex.mappingCone.descCocycle φ α β h eq = CochainComplex.mappingCone.descCocycle φ α_1 β_1 h ⋯

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveHomologicalComplex.HasHomotopyCofiber