Theorems · Theorem · category theory

HomologicalComplex.pathObject.homotopyEquiv_inv

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  (hc : ∀ (i : α), ∃ j, c.Rel i j),
  (HomologicalComplex.pathObject.homotopyEquiv K hc).inv = HomologicalComplex.pathObject.π₀ K

Defined in

Mathlib.Algebra.Homology.HomotopyFiber

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveDecidableRelCategoryTheory.Limits.HasBinaryBiproductHomologicalComplex.HasPathObject