d₃_eq_zero — Mathlib

English

Let i1, i2, i3, j be indices and assume that the index relation at level 3 does not hold, i.e., c3.Rel i3 (c3.next i3) is false. Then the third differential in the totalized bifunctor complex is zero.

Русский

Пусть i1, i2, i3, j являются индексами и условие на уровне 3 выполняется неверно, то есть c3.Rel i3 (c3.next i3) ложно. Тогда третий дифференциал в суммарном комплексе нулевой.

LaTeX

$$$\neg c_3.Rel\, i_3\,(c_3.next\,i_3) \Rightarrow d_3 F_{1 2} G K_1 K_2 K_3 c_{1 2} c_4 i_1 i_2 i_3 j = 0$$$

Lean4

theorem d₃_eq_zero (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ¬c₃.Rel i₃ (c₃.next i₃)) :
    d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0 := by
  dsimp [d₃]
  rw [shape _ _ _ h, Functor.map_zero, zero_comp, smul_zero]

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