English
The ι-map composed with D1 is equal to the corresponding D1-map under the natural transformation associator.
Русский
Карта ι, композиционная с D1, равна соответствующей карте D1 под естественным преобразованием ассоциатора.
LaTeX
$$$ι F G_{23} \; D_1 = D_1 \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₄ 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_app associator.hom (K₁.d i₁ (c₁.next i₁)) (K₂.X i₂) (K₃.X i₃)
dsimp at this
rw [mapBifunctor₁₂.d₁_eq _ _ _ _ _ _ _ h₁, mapBifunctor₂₃.d₁_eq _ _ _ _ _ _ _ _ h₁, Linear.comp_units_smul,
Linear.units_smul_comp, assoc, ComplexShape.associative_ε₁_eq_mul c₁ c₂ c₃ c₁₂ c₂₃ c₄,
ιOrZero_mapBifunctorAssociatorX_hom, smul_left_cancel_iff, reassoc_of% this]
·
rw [mapBifunctor₁₂.d₁_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₁, mapBifunctor₂₃.d₁_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₁,
comp_zero, zero_comp]
