English
Let K and L be double complexes and φ: K → L a morphism. The natural compatibility between the γ-total components with φ holds componentwise: the corresponding ιTotalOrZero maps satisfy the same commutation relation with total.map φ.
Русский
Пусть K и L — двойные комплексы, φ: K → L — морфизм. Соответствующие компоненты ιTotalOrZero совместимы с φ по компонентам так же, как и в случае ιTotal.
LaTeX
$$$\\forall i_1,i_2,i_{12},\\; K.ιTotalOrZero\\, c_{12}\\, i_1\\, i_2\\, i_{12} \\;≫\\; (total.map φ c_{12}).f_{i_{12}} = (φ.f_{i_1}).f_{i_2} \\;≫\\; L.ιTotalOrZero\\, c_{12}\\, i_1\\, i_2\\, i_{12}.$$$
Lean4
@[reassoc (attr := simp)]
theorem ιTotalOrZero_map (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) :
K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ ≫ (total.map φ c₁₂).f i₁₂ = (φ.f i₁).f i₂ ≫ L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ := by
simp [total.map, ιTotalOrZero]
