d₂_eq_zero' — Mathlib

English

Analogous vanishing criterion for D2 with a mismatch condition.

Русский

Аналогичное условие исчезновения для D2 при несовпадении индексов.

LaTeX

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

Lean4

theorem d₂_eq_zero' (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₁₂ = 0 :=
  by
  rw [totalAux.d₂_eq' K c₁₂ i₁ h i₁₂, K.toGradedObject.ιMapObjOrZero_eq_zero, comp_zero, smul_zero]
  exact h'

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