d₂_eq' — Mathlib

English

If the relation h holds, the d₁ component vanishes and is given by an epsilon₁-term with a map and injection.

Русский

Если выполняется связь 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' (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (j : 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₂') ≫ ιMapBifunctorOrZero K₁ K₂ F c i₁ i₂' j) :=
  HomologicalComplex₂.d₂_eq' _ _ _ h _

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