English
Under the same setup, the horizontal differential D1 is explicitly equal to the ε1-structure times the composition of K.d with the graded map into the π-shape, matching the index i1'.
Русский
При той же постановке горизонтальный дифференциал D1 равен явным образом структуре ε1, умноженной на композицию K.d с гредированным отображением в π‑форму, соответствующим индексу i1'.
LaTeX
$$$K.D_{1}\\, c_{12}\\; i_{1}\\; i_{2}\\; i_{1\\,2} = \\varepsilon_{1} c_{1} c_{2} c_{12} \\langle i_{1}, i_{2} \\rangle \\cdot\\left( (K.d\\; i_{1}\\; i_{1}').f\\; i_{2} \\\\circ K.toGradedObject.ιMapObj (\\mathrm{ComplexShape.π}\\ c_{1} c_{2} c_{12}) \\langle i_{1}', i_{2} \\rangle i_{12} h' \\right)$$
Lean4
/-- The vertical differential in the total complex on a given summand. -/
noncomputable def d₂ : (K.X i₁).X i₂ ⟶ (K.toGradedObject.mapObj (ComplexShape.π c₁ c₂ c₁₂)) i₁₂ :=
ComplexShape.ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ •
((K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObjOrZero (ComplexShape.π c₁ c₂ c₁₂) ⟨i₁, _⟩ i₁₂)
