Theorems · Theorem · category theory

CategoryTheory.NatTrans.mapHomotopyCategory_id

∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} W] [inst_3 : CategoryTheory.Preadditive W]
  (c : ComplexShape ι) (F : CategoryTheory.Functor V W) [inst_4 : F.Additive],
  CategoryTheory.NatTrans.mapHomotopyCategory (CategoryTheory.CategoryStruct.id F) c =
    CategoryTheory.CategoryStruct.id (F.mapHomotopyCategory c)

Defined in

Mathlib.Algebra.Homology.HomotopyCategory

Cited by

0 results in Mathlib

Foundations

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

Assumes

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