d₂_eq — Mathlib

English

If the target π-shape does not hit the index i12, the vertical differential D2 vanishes: D2 = 0.

Русский

Если π‑форма не попадёт в индекс i12, то D2 = 0.

LaTeX

$$$K.d_{2} c_{12} i_{1} i_{2} i_{12} = 0 \\quad\\text{when } h' : ComplexShape.π c_{1} c_{2} c_{12} \\langle i_{1}, i_{2}' \\rangle \\neq i_{12}$$$

Lean4

theorem d₂_eq (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂'⟩ = i₁₂) :
    K.d₂ c₁₂ i₁ i₂ i₁₂ =
      ComplexShape.ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ •
        ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (ComplexShape.π c₁ c₂ c₁₂) ⟨i₁, i₂'⟩ i₁₂ h') :=
  by rw [d₂_eq' K c₁₂ i₁ h i₁₂, K.toGradedObject.ιMapObjOrZero_eq]

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