English
The component of the graded map mapping under the π-shape interacts with the horizontal differential D1 via the d1-map; together they express the action on the summand (i1,i2) mapping to i12.
Русский
Компонента градуированного отображения, связанная с π‑формой, взаимодействует с горизонтальным дифференциалом D1 через отображение d1; вместе они описывают действие на слагаемое (i1,i2), индексируемое до i12.
LaTeX
$$$K.toGradedObject.\\ιMapObj(\\mathrm{ComplexShape.π} \\ c_{1} \\ c_{2} \\ c_{12})\\; i\\; i_{12}\\; h \\; \\; \\circ \\; K.D_{1} c_{12} i_{12} i_{12}' = K.d_{1} c_{12} i_{1} i_{2} i_{12}'$$$
Lean4
theorem d₂_eq_zero (h : ¬c₂.Rel i₂ (c₂.next i₂)) : K.d₂ c₁₂ i₁ i₂ i₁₂ = 0 :=
by
dsimp [d₂]
rw [HomologicalComplex.shape _ _ _ h, zero_comp, smul_zero]
