English
The postcomposition with a morphism g respects nullHomotopicMap: f ≫ nullHomotopicMap hom = nullHomotopicMap' (hom i j hij ≫ g.f j).
Русский
Постсоставление с морфизмом g сохраняет nullHomotopicMap: f ≫ nullHomotopicMap hom = nullHomotopicMap'(hom i j hij ≫ g.f j).
LaTeX
$$$ f \\;\\circ\\; nullHomotopicMap(\\text{hom}) = nullHomotopicMap'( \\lambda i j hij => f.f i \\circ (hom i j hij) \\circ g.f j ) $$$
Lean4
/-- Compatibility of `nullHomotopicMap'` with the postcomposition by a morphism
of complexes. -/
theorem nullHomotopicMap'_comp (hom : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) (g : D ⟶ E) :
nullHomotopicMap' hom ≫ g = nullHomotopicMap' fun i j hij => hom i j hij ≫ g.f j :=
by
rw [nullHomotopicMap', nullHomotopicMap_comp]
congr
ext i j
split_ifs
· rfl
· rw [zero_comp]
