English
In the total differential of the bifunctor map, the differential d placed at level j is the sum of three components: D1, D2, and D3.
Русский
В суммарном дифференциале отображения бифункторной карты дифференциал d на уровне j равен сумме трех частей: D1, D2 и D3.
LaTeX
$$$\bigl(\mathrm{mapBifunctor}\ K_1 (\mathrm{mapBifunctor}\ K_2 K_3 G_{2 3} c_{2 3}) F c_4\bigr).d_{j j'} = D_1 F G_{2 3} K_1 K_2 K_3 c_{2 3} c_4 j j' + D_2 F G_{2 3} K_1 K_2 K_3 c_{1 2 2} c_{2 3} c_4 j j' + D_3 F G_{2 3} K_1 K_2 K_3 c_{1 2 3} c_{2 3} c_4 j j'$$$
Lean4
theorem d_eq :
(mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄).d j j' =
D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j' + D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' + D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' :=
by
rw [mapBifunctor.d_eq]
rw [add_assoc]
congr 1
apply mapBifunctor₂₃.hom_ext (c₁₂ := c₁₂)
intro i₁ i₂ i₃ h
simp only [Preadditive.comp_add, ι_D₂, ι_D₃]
rw [ι_eq _ _ _ _ _ _ _ _ _ _ _ _ _ rfl (by rw [← h, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]; rfl), assoc,
mapBifunctor.ι_D₂]
set i₂₃ := ComplexShape.π c₂ c₃ c₂₃ ⟨i₂, i₃⟩
by_cases h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
· by_cases h₂ : ComplexShape.π c₁ c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
· rw [mapBifunctor.d₂_eq _ _ _ _ _ h₁ _ h₂, mapBifunctor.d_eq, Linear.comp_units_smul, Functor.map_add,
Preadditive.add_comp, Preadditive.comp_add, smul_add]
congr 1
· rw [← Functor.map_comp_assoc, mapBifunctor.ι_D₁]
by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
·
rw [d₂_eq _ _ _ _ _ _ _ _ _ h₃, mapBifunctor.d₁_eq _ _ _ _ h₃ _ _ (ComplexShape.next_π₁ c₃ c₂₃ h₃ i₃).symm,
Functor.map_units_smul, Functor.map_comp, Linear.units_smul_comp, assoc, smul_smul, smul_left_cancel_iff,
ιOrZero_eq _ _ _ _ _ _ _ _ _ _ _ _
(by
dsimp [ComplexShape.r]
rw [← h₂, ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄, ComplexShape.next_π₁ c₃ c₂₃ h₃ i₃]),
ι_eq]
·
rw [d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₃, mapBifunctor.d₁_eq_zero _ _ _ _ _ _ _ h₃, Functor.map_zero,
zero_comp, smul_zero]
· rw [← Functor.map_comp_assoc, mapBifunctor.ι_D₂]
by_cases h₃ : c₃.Rel i₃ (c₃.next i₃)
· rw [d₃_eq _ _ _ _ _ _ _ _ _ _ h₃, mapBifunctor.d₂_eq _ _ _ _ _ h₃ _ (ComplexShape.next_π₂ c₂ c₂₃ i₂ h₃).symm,
Functor.map_units_smul, Functor.map_comp, Linear.units_smul_comp, assoc, smul_smul, smul_left_cancel_iff]
rw [ιOrZero_eq _ _ _ _ _ _ _ _ _ _ _ _
(by
dsimp [ComplexShape.r]
rw [← h₂, ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄, ComplexShape.next_π₂ c₂ c₂₃ i₂ h₃]),
ι_eq]
·
rw [d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₃, mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₃, Functor.map_zero,
zero_comp, smul_zero]
· rw [mapBifunctor.d₂_eq_zero' _ _ _ _ _ h₁ _ h₂, comp_zero]
trans 0 + 0
· simp
· congr 1
· by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
· rw [d₂_eq _ _ _ _ _ _ _ _ _ h₃, ιOrZero_eq_zero, comp_zero, smul_zero]
intro h₄
apply h₂
rw [← h₄]
dsimp [ComplexShape.r]
rw [ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄, ComplexShape.next_π₁ c₃ c₂₃ h₃ i₃]
· rw [d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₃]
· by_cases h₃ : c₃.Rel i₃ (c₃.next i₃)
· rw [d₃_eq _ _ _ _ _ _ _ _ _ _ h₃, ιOrZero_eq_zero, comp_zero, smul_zero]
intro h₄
apply h₂
rw [← h₄]
dsimp [ComplexShape.r]
rw [ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄, ComplexShape.next_π₂ c₂ c₂₃ i₂ h₃]
· rw [d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₃]
· rw [mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₁, comp_zero]
trans 0 + 0
· simp only [add_zero]
· congr 1
· rw [d₂_eq_zero]
intro h₂
apply h₁
simpa only [← ComplexShape.next_π₁ c₃ c₂₃ h₂ i₃] using ComplexShape.rel_π₁ c₃ c₂₃ h₂ i₃
· rw [d₃_eq_zero]
intro h₂
apply h₁
simpa only [i₂₃, ComplexShape.next_π₂ c₂ c₂₃ i₂ h₂] using ComplexShape.rel_π₂ c₂ c₂₃ i₂ h₂
