d₂_eq — Mathlib

English

Under the prescribed total complex shape, the d2-differential vanishes on the boundary region determined by the shape relations.

Русский

При заданной форме общего комплекса, дифференциал d2 обращается в ноль на границе, заданной отношениями формы.

LaTeX

$$$d_2 = 0$ on boundary region$$

Lean4

theorem d₂_eq (i₁ : ι₁) {i₂ i₂' : ι₂} (h₂ : c₂.Rel i₂ i₂') (i₃ : ι₃) (j : ι₄) :
    d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j =
      (ComplexShape.ε₂ c₁ c₂₃ c₄ (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * ComplexShape.ε₁ c₂ c₃ c₂₃ (i₂, i₃)) •
        (F.obj (K₁.X i₁)).map ((G₂₃.map (K₂.d i₂ i₂')).app (K₃.X i₃)) ≫ ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ _ i₃ j :=
  by
  obtain rfl := c₂.next_eq' h₂
  rfl

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