d₂_eq_zero — Mathlib

English

If the relation h holds, then the d₂ component is the scalar epsilon₂ times the appropriate map, hence zero in certain ranges.

Русский

Если выполняется отношение, то компонент d₂ равен скаляру epsilon₂ умноженному на соответствующее отображение, что в определённых диапазонах даёт ноль.

LaTeX

$$d₂ K₁ K₂ F c i₁ i₂ j = ComplexShape.ε₂ c₁ c₂ c ⟨i₁, i₂⟩ • ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ ιMapBifunctorOrZero K₁ K₂ F c i₁ i₂' j h)$$

Lean4

theorem d₂_eq_zero (h : ¬c₂.Rel i₂ (c₂.next i₂)) : d₂ K₁ K₂ F c i₁ i₂ j = 0 :=
  HomologicalComplex₂.d₂_eq_zero _ _ _ _ _ h

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