D₁_shape — Mathlib

English

The horizontal differential D1 vanishes when a certain non‑relational condition holds on π; this is a shape-is-zero lemma.

Русский

Горизонтальный дифференциал D1 обнуляется при выполнении некоторого условия формы на π.

LaTeX

$$$D_{1\\_shape}(i_{12},i_{12}') : K.D_{1} c_{12} i_{12} i_{12}' = 0 \\quad\\text{if } \\neg 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₁₂ h₁ i₂ i₁₂']
    intro h₂
    exact h₁₂ (by simpa only [← h, ← h₂] using ComplexShape.rel_π₁ c₂ c₁₂ h₁ i₂)
  · exact d₁_eq_zero _ _ _ _ _ h₁

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