English
Let C, D, E be chain complexes in a preadditive category, and let h be a family of morphisms with domain in C.X i and codomain in D.X j indexed by i, j and a relation r₁₀ = c.Rel k₁ k₀ such that no other index is Rel-related to k₁. Then the k₁-th component of the null-homotopic map produced from h is exactly the composition C.d k₁ k₀ followed by h k₀ k₁ r₁₀.
Русский
Пусть C, D, E — цепочные комплексы в категоризованной преддобавитной категории, возьмём семейство одомомных отображений h с областью определения в C.X_i и областью значения в D.X_j, индексируемых парами i, j и имеющих отношение r₁₀ = c.Rel k₁ k₀ так, что других Rel-связей с k₁ нет. Тогда k₁-ый компонент отображения, полученного из h, равен композиции C.d_{k₁ k₀} ∘ h_{k₀ k₁} r₁₀.
LaTeX
$$$ (\mathrm{nullHomotopicMap'} h ).f_{k_1} = C.d_{k_1 k_0} \circ h_{k_0 k_1} \; r_{1 0} $$$
Lean4
theorem nullHomotopicMap'_f_of_not_rel_right {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₁ : ∀ l : ι, ¬c.Rel l k₁)
(h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) : (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ :=
by
simp only [nullHomotopicMap']
rw [nullHomotopicMap_f_of_not_rel_right r₁₀ hk₁]
split_ifs
rfl
