Theorems · Theorem · category theory

HomotopyEquiv.trans_homotopyHomInvId

∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : HomotopyEquiv C D) (g : HomotopyEquiv D E),
  (f.trans g).homotopyHomInvId =
    ⋯.mpr (⋯.mp (((g.homotopyHomInvId.compRightId f.inv).compLeft f.hom).trans f.homotopyHomInvId))

Defined in

Mathlib.Algebra.Homology.Homotopy

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive