English
For the horizontal differential D1 on a fixed summand, D1 is given by the ε1-structure times the differential along i1 → i1' composed with the canonical map into the π-shape and evaluated at i1',i2 with the appropriate h' relation.
Русский
Горизонтальный дифференциал D1 на фиксированном слагаемом задан как произведение ε1-структуры на дифференциал вдоль i1 → i1' с канонической картой в π‑форму и взятием значения в i1', i2 при подходящем отношении h'.
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 horizontal 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.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObjOrZero (ComplexShape.π c₁ c₂ c₁₂) ⟨_, i₂⟩ i₁₂)
