English
Compatibility between a canonical isomorphism XXIsoOfEq and the inclusion ιTotal: the hom component composed with ιTotal equals the corresponding inclusion with indices adjusted.
Русский
Совместимость между каноническим изоморфизмом XXIsoOfEq и включением ιTotal: гом-часть, умноженная на ιTotal, равно включению с соответствующими индексами.
LaTeX
$$$\\big(\\text{XXIsoOfEq} \\; K \\; c_{12} \\; i_1 \\; i_2 \\; i_{12} \\; h_1 \\; h_2\\big).hom \\; \\; K.ιTotal c_{12} y_1 y_2 i_{12} h = K.ιTotal c_{12} x_1 x_2 i_{12} (by rw [h_1, h_2, h])$$$
Lean4
/-- The inclusion of a summand in the total complex. -/
noncomputable def ιTotal (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) :
(K.X i₁).X i₂ ⟶ (K.total c₁₂).X i₁₂ :=
K.toGradedObject.ιMapObj (ComplexShape.π c₁ c₂ c₁₂) ⟨i₁, i₂⟩ i₁₂ h
