English
The d1 differential in the d1_eq formula is the explicit ε₁-π combination with the applied maps and the ι map.
Русский
Дифференциал d1 в формуле d1_eq выражается через явное сочетание ε₁-π с применёнными отображениями и ι-картой.
LaTeX
$$$d_1 = ε_1 \\cdot (F(map) \\circ ... ) \\circ ι$$$
Lean4
@[reassoc]
theorem mapBifunctorAssociatorX_hom_D₂ (j j' : ι₄) :
(mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom ≫ mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' ≫ (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom :=
by
ext i₁ i₂ i₃ h
rw [mapBifunctor₁₂.ι_D₂_assoc, ι_mapBifunctorAssociatorX_hom_assoc, mapBifunctor₂₃.ι_D₂]
by_cases h₁ : c₂.Rel i₂ (c₂.next i₂)
· have := NatTrans.naturality_app (associator.hom.app (K₁.X i₁)) (K₃.X i₃) (K₂.d i₂ (c₂.next i₂))
dsimp at this
rw [mapBifunctor₁₂.d₂_eq _ _ _ _ _ _ _ _ h₁, mapBifunctor₂₃.d₂_eq _ _ _ _ _ _ _ _ _ h₁, Linear.units_smul_comp,
assoc, ιOrZero_mapBifunctorAssociatorX_hom, reassoc_of% this, Linear.comp_units_smul,
ComplexShape.associative_ε₂_ε₁ c₁ c₂ c₃ c₁₂ c₂₃ c₄]
·
rw [mapBifunctor₁₂.d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₁, mapBifunctor₂₃.d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₁,
comp_zero, zero_comp]
