Theorems · Definition · category theory

CochainComplex.cm5b.homotopyEquiv

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.EnoughInjectives C] →
        (K L : CochainComplex C ℤ) →
          HomotopyEquiv (CochainComplex.mappingCone (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K)) ⊞ L) L

The second projection p K L : mappingCone (𝟙 (I K)) ⊞ L ⟶ L is a homotopy equivalence.

Defined in: Mathlib.Algebra.Homology.Factorizations.CM5b
Cited by: 0 results in Mathlib
Foundations: Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Abelian CategoryTheory.EnoughInjectives

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites28

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.CategoryStruct.compproof · cited by 17,999
CategoryTheory.CategoryStruct.idstatement and proof · cited by 6,235
HomologicalComplex.Xstatement · cited by 1,839
CategoryTheory.Abelianstatement and proof · cited by 1,753
HomologicalComplexstatement · cited by 1,691
ComplexShape.upstatement · cited by 1,123
CochainComplexstatement and proof · cited by 1,016
CategoryTheory.Limits.biprodstatement · cited by 312
CochainComplex.mappingConestatement and proof · cited by 181
CategoryTheory.Limits.biprod.sndproof · cited by 132
CategoryTheory.Limits.biprod.inlproof · cited by 127

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.