English
The interaction between the ι-map from the π-shape and the horizontal differential D1 equals the d1-map for the summand; this expresses a compatibility between the two maps on the i₁,i₂-summand.
Русский
Взаимодействие между ι-map из π‑формы и горизонтальным дифференциалом D1 даёт совместимость между картами на сумме (i₁,i₂).
LaTeX
$$$\\; K.toGradedObject.ιMapObj (\\mathrm{π} 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
@[reassoc (attr := simp)]
theorem ιMapObj_D₁ (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : ComplexShape.π c₁ c₂ c₁₂ i = i₁₂) :
K.toGradedObject.ιMapObj (ComplexShape.π c₁ c₂ c₁₂) i i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' = K.d₁ c₁₂ i.1 i.2 i₁₂' := by
simp [D₁]
