English
The additive functor maps nullHomotopicMap' hom to the corresponding nullHomotopicMap' of the mapped hom.
Русский
Аддитивный функтор переводит nullHomotopicMap' hom в соответствующий nullHomotopicMap' для отображения, полученного после отображения.
LaTeX
$$$ (G.mapHomologicalComplex c).map (nullHomotopicMap' hom) = nullHomotopicMap' (\\lambda i j hij => G.map (hom i j hij)) $$$
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.Rel j i → (C.X i ⟶ D.X j)) :
(G.mapHomologicalComplex c).map (nullHomotopicMap' hom) =
nullHomotopicMap' fun i j hij => by exact G.map (hom i j hij) :=
by
rw [nullHomotopicMap', map_nullHomotopicMap]
congr
ext i j
split_ifs
· rfl
· rw [G.map_zero]
