d₁_eq' — Mathlib

English

In a context where a certain π-entry does not match a target index, the horizontal differential D1 vanishes: D1 = 0.

Русский

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

LaTeX

$$$\\text{If } h' :\\; ComplexShape.\\pi\\ c_{1} c_{2} c_{12} \\langle i_{1}, i_{2} \\rangle \\neq i_{12} \\text{ then } K.D_{1} c_{12} i_{1} i_{2} i_{12} = 0.$$$

Lean4

theorem d₁_eq' {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) :
    K.d₁ c₁₂ i₁ i₂ i₁₂ =
      ComplexShape.ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ •
        ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (ComplexShape.π c₁ c₂ c₁₂) ⟨i₁', i₂⟩ i₁₂) :=
  by
  obtain rfl := c₁.next_eq' h
  rfl

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