d₁_eq_zero' — Mathlib

English

If c₁.Rel i₁ i₁' and h', the d₁ component vanishes and is given by the ε₁-term with a map and inclusion.

Русский

Если c₁Rel i₁ i₁' и h', компонент d₁ обращает ноль и задаётся через ε₁ с отображением и включением.

LaTeX

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

Lean4

theorem d₁_eq_zero' {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (j : J) (h' : ComplexShape.π c₁ c₂ c ⟨i₁', i₂⟩ ≠ j) :
    d₁ K₁ K₂ F c i₁ i₂ j = 0 :=
  HomologicalComplex₂.d₁_eq_zero' _ _ h _ _ h'

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