D₂_shape — Mathlib

English

The vertical differential vanishes when the π relation misses the i₁₂ index.

Русский

Вертикальный дифференциал D2 обнуляется при отсутствии совпадения π‑отношения с i₁₂.

LaTeX

$$$K.D_{2} c_{12} i_{12} i_{12}' = 0 \\quad\\text{if } ¬ c_{12}.Rel(i_{12},i_{12}').$$$

Lean4

theorem D₂_shape (i₁₂ i₁₂' : I₁₂) (h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂') : K.D₂ c₁₂ i₁₂ i₁₂' = 0 :=
  by
  ext ⟨i₁, i₂⟩ h
  simp only [totalAux.ιMapObj_D₂, comp_zero]
  by_cases h₂ : c₂.Rel i₂ (c₂.next i₂)
  · rw [K.d₂_eq_zero' c₁₂ i₁ h₂ i₁₂']
    intro h₁
    exact h₁₂ (by simpa only [← h, ← h₁] using ComplexShape.rel_π₂ c₁ c₁₂ i₁ h₂)
  · exact d₂_eq_zero _ _ _ _ _ h₂

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