English
In the total complex, the composition of the first differential with itself is zero: D1 followed by D1 is zero.
Русский
В суммарном комплексe композиция первого градиентного оператора с самим собой равна нулю: D1 ∘ D1 = 0.
LaTeX
$$$K.D_1 c_{12} i_{12} i_{12}' \\;\\circ\\; K.D_1 c_{12} i_{12}' i_{12}'' = 0$$$
Lean4
@[reassoc (attr := simp)]
theorem D₁_D₁ (i₁₂ i₁₂' i₁₂'' : I₁₂) : K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0 :=
by
by_cases h₁ : c₁₂.Rel i₁₂ i₁₂'
· by_cases h₂ : c₁₂.Rel i₁₂' i₁₂''
· ext ⟨i₁, i₂⟩ h
simp only [totalAux.ιMapObj_D₁_assoc, comp_zero]
by_cases h₃ : c₁.Rel i₁ (c₁.next i₁)
· rw [totalAux.d₁_eq K c₁₂ h₃ i₂ i₁₂']; swap
· rw [← ComplexShape.next_π₁ c₂ c₁₂ h₃ i₂, ← c₁₂.next_eq' h₁, h]
simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]
by_cases h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
· rw [totalAux.d₁_eq K c₁₂ h₄ i₂ i₁₂'', Linear.comp_units_smul, d_f_comp_d_f_assoc, zero_comp, smul_zero,
smul_zero]
rw [← ComplexShape.next_π₁ c₂ c₁₂ h₄, ← ComplexShape.next_π₁ c₂ c₁₂ h₃, h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]
· rw [K.d₁_eq_zero _ _ _ _ h₄, comp_zero, smul_zero]
· rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, zero_comp]
· rw [K.D₁_shape c₁₂ _ _ h₂, comp_zero]
· rw [K.D₁_shape c₁₂ _ _ h₁, zero_comp]
