d₁_eq — Mathlib

English

An alternate version: if the relation holds between i₁ and i₁', then d₁ vanishes under a shifted π.

Русский

Альтернативная версия: если выполняется связь между i₁ и i₁', тогда d₁ обращается в ноль при сдвинутой π.

LaTeX

$$d₁ K₁ K₂ F c i₁ i₂ j = 0$$

Lean4

theorem d₁_eq {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 =
      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') :=
  HomologicalComplex₂.d₁_eq _ _ h _ _ h'

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