English
In the total complex, the composition of the second differential with itself is zero: D2 ∘ D2 = 0.
Русский
В суммарном комплексе композиция второго дифференциала с самим собой равна нулю: D2 ∘ D2 = 0.
LaTeX
$$$K.D_2 c_{12} i_{12} i_{12}' \\;\\circ\\; K.D_2 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₁₂ i₁ h₃ i₁₂']; swap
· rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃, ← 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₁₂ i₁ h₄ i₁₂'', Linear.comp_units_smul, HomologicalComplex.d_comp_d_assoc, zero_comp,
smul_zero, smul_zero]
rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃, h, c₁₂.next_eq' h₁,
c₁₂.next_eq' h₂]
· rw [K.d₂_eq_zero c₁₂ _ _ _ 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]
