English
Similar vanishing criterion holds for D1 with a different shape condition h and h' -> 0 equality under next relation.
Русский
Схожее условие исчезновения действует для D1 с другой формой условия и перехода к следующему индексу.
LaTeX
$$$\\text{If } h : c_{1}.Rel i_{1} i_{1}' \\text{ and } h' : ComplexShape.π 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₁₂) (h' : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁', i₂⟩ = i₁₂) :
K.d₁ c₁₂ i₁ i₂ i₁₂ =
ComplexShape.ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ •
((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (ComplexShape.π c₁ c₂ c₁₂) ⟨i₁', i₂⟩ i₁₂ h') :=
by rw [d₁_eq' K c₁₂ h i₂ i₁₂, K.toGradedObject.ιMapObjOrZero_eq]
