Lean4
/-- The null homotopic map associated to a family `hom` of morphisms `C_i ⟶ D_j`.
This is the same datum as for the field `hom` in the structure `Homotopy`. For
this definition, we do not need the field `zero` of that structure
as this definition uses only the maps `C_i ⟶ C_j` when `c.Rel j i`. -/
def nullHomotopicMap (hom : ∀ i j, C.X i ⟶ D.X j) : C ⟶ D
where
f i := dNext i hom + prevD i hom
comm' i j
hij :=
by
have eq1 : prevD i hom ≫ D.d i j = 0 := by simp only [prevD, AddMonoidHom.mk'_apply, assoc, d_comp_d, comp_zero]
have eq2 : C.d i j ≫ dNext j hom = 0 := by simp only [dNext, AddMonoidHom.mk'_apply, d_comp_d_assoc, zero_comp]
rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2, add_zero, zero_add,
assoc]
