English
The vertical differential D2 for fixed indices is determined by the shape ε2 and the differential X i1 along i2, composed with the appropriate graded map to i12.
Русский
Вертикальный дифференциал D2 для фиксированных индексов задаётся через ε2 и дифференциал X i1 вдоль i2, с композиционным входом в i12 через соответствующее градуированное отображение.
LaTeX
$$$K.d_{2} c_{12} i_{1} i_{2} i_{12} = \\varepsilon_{2} c_{1} c_{2} c_{12} \\langle i_{1}, i_{2} \\rangle \\;\\big( (K.X i_{1}).d i_{2} i_{2}' \\;\\circ\\; K.toGradedObject.ιMapObj (\\mathrm{π} c_{1} c_{2} c_{12}) \\langle i_{1}, i_{2}' \\rangle i_{12} h' \\big)$$$$
Lean4
theorem d₂_eq' (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) :
K.d₂ c₁₂ i₁ i₂ i₁₂ =
ComplexShape.ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ •
((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObjOrZero (ComplexShape.π c₁ c₂ c₁₂) ⟨i₁, i₂'⟩ i₁₂) :=
by
obtain rfl := c₂.next_eq' h
rfl
