ιMapObj_D₂ — Mathlib

English

Similarly, the interaction between ι-map and the vertical differential D2 gives the expected relation on i₁,i₂; this is a compatibility statement for the vertical part.

Русский

Аналогично, взаимодействие ι-map и вертикального дифференциала D2 даёт ожидаемое соотношение для i₁,i₂.

LaTeX

$$$\\; K.toGradedObject.ιMapObj (\\mathrm{π} c_{1} c_{2} c_{12}) i i_{12} h \\; \\circ \\; K.D_{2} c_{12} i_{12} i_{12}' = K.d_{2} 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₂]

Похожие утверждения