English
The naturality of the associator with respect to the i₁,i₂,i₃ indices is captured by a commutativity identity at component level.
Русский
Натуральность ассоциатора по индексам i₁,i₂,i₃ зафиксирована идейным равенством на уровне компонент.
LaTeX
$$Naturality of the associator with respect to i₁,i₂,i₃$$
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₃)
· rw [mapBifunctor₁₂.d₃_eq _ _ _ _ _ _ _ _ _ h₁, mapBifunctor₂₃.d₃_eq _ _ _ _ _ _ _ _ _ _ h₁, Linear.comp_units_smul,
Linear.units_smul_comp, assoc, ιOrZero_mapBifunctorAssociatorX_hom, NatTrans.naturality_assoc,
ComplexShape.associative_ε₂_eq_mul c₁ c₂ c₃ c₁₂ c₂₃ c₄]
dsimp
·
rw [mapBifunctor₁₂.d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₁, mapBifunctor₂₃.d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₁,
comp_zero, zero_comp]
