English
The associator hom component in the localized monoidal category is given by a canonical composite built from μ, its tensor with the identity, and the image under L' of the original associator from C, with a post-composition by μ inverse and an adjustment by identities.
Русский
Гомоморфизм ассоциатора в локализованной моноидальной категории задается каноническим композитом, составленным из μ, его тензора с единицей и образа L' исходного ассоциатора из C, затем с обратной μ и идентичностями.
LaTeX
$$$(\\alpha_{{L'X_1},{L'X_2},{L'X_3}})^{\\mathrm{hom}} = ((\\mu L W ε _ _).hom \\otimes \\mathrm{Id}_) \\\\; \\circ (\\mu L W ε _ _).hom \\\\; \\circ (L').map (\\alpha_{X_1 X_2 X_3})^{hom} \\circ (\\mu L W ε _ _).inv \\circ (\\mathrm{Id} \\otimes (\\mu L W ε _ _).inv)$$$
Lean4
theorem associator_hom_app (X₁ X₂ X₃ : C) :
(α_ ((L').obj X₁) ((L').obj X₂) ((L').obj X₃)).hom =
((μ L W ε _ _).hom ⊗ₘ 𝟙 _) ≫
(μ L W ε _ _).hom ≫ (L').map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε _ _).inv ≫ (𝟙 _ ⊗ₘ (μ L W ε _ _).inv) :=
by
dsimp [monoidalCategoryStruct, associator]
simp only [Functor.map_id, comp_id, NatTrans.id_app, id_comp]
rw [Localization.associator_hom_app_app_app]
rfl
