Theorems · Theorem · category theory

Homotopy.map_nullHomotopicMap

∀ {ι : 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] (G : CategoryTheory.Functor V W) [inst_4 : G.Additive]
  (hom : (i j : ι) → C.X i ⟶ D.X j),
  (G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap hom) = Homotopy.nullHomotopicMap fun i j => G.map (hom i j)

Compatibility of nullHomotopicMap with the application of additive functors

Defined in

Mathlib.Algebra.Homology.Homotopy

Cited by

1 results in Mathlib

Foundations

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

Assumes

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