English
The null-homotopic maps Hσ q commute with additive functors: applying G to Hσ q is the same as applying Hσ q to the image under G, up to straightforward functoriality.
Русский
Отображения Hσ q, являющиеся нулевыми гомотопиями, коммьютируют с аддитивными функторeми: применение G к Hσ q равно применению Hσ q к изображению под G (с точной математической естественной зависимостью).
LaTeX
$$$$ G.map \big(Hσ q\big) = Hσ q \;\text{(on objects after mapping)} $$$$
Lean4
/-- The null homotopic maps `Hσ` are compatible with the application of additive functors. -/
theorem map_Hσ {D : Type*} [Category D] [Preadditive D] (G : C ⥤ D) [G.Additive] (X : SimplicialObject C) (q n : ℕ) :
(Hσ q : K[((whiskering C D).obj G).obj X] ⟶ _).f n = G.map ((Hσ q : K[X] ⟶ _).f n) :=
by
unfold Hσ
have eq := HomologicalComplex.congr_hom (map_nullHomotopicMap' G (@hσ' _ _ _ X q)) n
simp only [Functor.mapHomologicalComplex_map_f, ← map_hσ'] at eq
rw [eq]
let h := (Functor.congr_obj (map_alternatingFaceMapComplex G) X).symm
congr
