English
The i-th component of nullHomotopicMap applied to a hom equals the sum of two composites: the differential followed by hom, plus hom followed by the differential.
Русский
i-й компонент nullHomotopicMap равен сумме двух композитов: дифференциал за ним и hom, плюс hom затем дифференциал.
LaTeX
$$$ (\\mathrm{nullHomotopicMap} \\; \\mathrm{hom}).f\\; i = C.d_{i,i-1} \\circ hom_{i-1,i} + hom_{i,i+1} \\circ D.d_{i+1,i} $$$
Lean4
theorem nullHomotopicMap_f {k₂ k₁ k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r₁₀ : c.Rel k₁ k₀) (hom : ∀ i j, C.X i ⟶ D.X j) :
(nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁ :=
by
dsimp only [nullHomotopicMap]
rw [dNext_eq hom r₁₀, prevD_eq hom r₂₁]
-- Cannot be @[simp] because `k₀` and `k₂` cannot be inferred by `simp`.
