d₂_eq — Mathlib

English

The d₂ component equals epsilon₂ times the map given by F and ι maps.

Русский

Компонента d₂ равна эпсилон₂, умноженной на отображение через F и включения.

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₂') ≫ ιMapBifunctor K₁ K₂ F c i₁ i₂' j h)$$

Lean4

theorem d₂_eq (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel 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.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ ιMapBifunctor K₁ K₂ F c i₁ i₂' j h') :=
  HomologicalComplex₂.d₂_eq _ _ _ h _ h'

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