d₃_eq — Mathlib

English

Under the total complex structure, the differential d3 vanishes on boundary indices.

Русский

При общей структуре комплекса, дифференциал d3 равен нулю на индексах границы.

LaTeX

$$$d_3 = 0$ on boundary indices$$

Lean4

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

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