English
The overall differential of the map bifunctor equals the sum of the three elementary differentials D1, D2, D3.
Русский
Общий дифференциал отображения бифункторной карты равен сумме трёх элементарных дифференциалов D1, D2, D3.
LaTeX
$$$d = D_1 + D_2 + D_3$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_D₁ :
ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j' =
d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' :=
by
dsimp only [D₁]
rw [ι_eq _ _ _ _ _ _ _ _ _ _ _ _ _ rfl (by rw [← h, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]; rfl), assoc,
mapBifunctor.ι_D₁]
by_cases h₁ : c₁.Rel i₁ (c₁.next i₁)
· rw [d₁_eq _ _ _ _ _ _ _ _ h₁]
by_cases h₂ : ComplexShape.π c₁ c₂₃ c₄ (c₁.next i₁, ComplexShape.π c₂ c₃ c₂₃ (i₂, i₃)) = j'
· rw [mapBifunctor.d₁_eq _ _ _ _ h₁ _ _ h₂, ιOrZero_eq, Linear.comp_units_smul, NatTrans.naturality_assoc]
· rfl
· rw [← h₂, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]
rfl
·
rw [mapBifunctor.d₁_eq_zero' _ _ _ _ h₁ _ _ h₂, comp_zero,
ιOrZero_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ (by simpa only [← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄] using h₂),
comp_zero, smul_zero]
· rw [mapBifunctor.d₁_eq_zero _ _ _ _ _ _ _ h₁, d₁_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₁, comp_zero]
