English
An additive functor G preserves the structure of nullHomotopicMap up to mapping the underlying homs.
Русский
Аддитивный функтор сохраняет структуру nullHomotopicMap, применяя отображения к базовым гомоморфизмам.
LaTeX
$$$ (G.mapHomologicalComplex c).map (nullHomotopicMap hom) = nullHomotopicMap (\\lambda i j, G.map (hom i j)) $$$
Lean4
/-- Compatibility of `nullHomotopicMap` with the application of additive functors -/
theorem map_nullHomotopicMap {W : Type*} [Category W] [Preadditive W] (G : V ⥤ W) [G.Additive]
(hom : ∀ i j, C.X i ⟶ D.X j) :
(G.mapHomologicalComplex c).map (nullHomotopicMap hom) = nullHomotopicMap (fun i j => by exact G.map (hom i j)) :=
by
ext i
dsimp [nullHomotopicMap, dNext, prevD]
simp only [G.map_comp, Functor.map_add]
