English
A detailed vanishing statement that if certain shape condition holds, the horizontal differential on a specified indexing vanishes.
Русский
Подробное условие исчезновения: если выполняется определённое условие формы, горизонтальный дифференциал на заданном индексе равен нулю.
LaTeX
$$$\\forall (i_1) (i_1') (i_2) (i_{12}), c_{1}.Rel i_1 i_1' \\Rightarrow (h' : ComplexShape.π c_{1} c_{2} c_{1 2} \\langle i_1', i_2 \\rangle = i_{12}) \Rightarrow K.d_{1} c_{12} i_1 i_2 i_{12} = 0$$$
Lean4
/-- The horizontal differential in the total complex. -/
noncomputable def D₁ (i₁₂ i₁₂' : I₁₂) :
K.toGradedObject.mapObj (ComplexShape.π c₁ c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (ComplexShape.π c₁ c₂ c₁₂) i₁₂' :=
GradedObject.descMapObj _ (ComplexShape.π c₁ c₂ c₁₂) (fun ⟨i₁, i₂⟩ _ => K.d₁ c₁₂ i₁ i₂ i₁₂')
