English
Postcomposition with a morphism of complexes commutes with the construction nullHomotopicMap. In other words, composing the null-homotopic map with g on the right is the same as taking the null-homotopic map of the compositions with g.
Русский
Посткомпозиция с морфизмом комплексов коммутирует с построением nullHomotopicMap. Другими словами, композиция нулевой гомотопии справа равна гомотопии состоящей из композиции с g.
LaTeX
$$$\text{nullHomotopicMap}\!\bigl(\text{hom}\bigr) \;\circ\; g = \text{nullHomotopicMap}\!\bigl(\lambda i j,\; \text{hom}(i,j) \circ g.f\!j\bigr).$$$
Lean4
/-- Compatibility of `nullHomotopicMap` with the postcomposition by a morphism
of complexes. -/
theorem nullHomotopicMap_comp (hom : ∀ i j, C.X i ⟶ D.X j) (g : D ⟶ E) :
nullHomotopicMap hom ≫ g = nullHomotopicMap fun i j => hom i j ≫ g.f j :=
by
ext n
dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
simp only [Preadditive.add_comp, assoc, g.comm]
