Theorems · Theorem · category theory

CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId

∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W]
  [inst_3 : CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [inst_4 : F.Additive]
  (h : HomotopyEquiv C D), (F.mapHomotopyEquiv h).homotopyInvHomId = ⋯.mpr (⋯.mpr (F.mapHomotopy h.homotopyInvHomId))

Defined in

Mathlib.Algebra.Homology.Homotopy

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Functor.Additive