English
The action of μ at the endofunctor, evaluated at X, matches the natural nesting of μ and associator after transporting X through F.obj m1.
Русский
Действие μ на объекте X согласуется с вложенностью μ и ассоциатора, после переноса через F.obj m1.
LaTeX
$$$ (F.obj m_3).map ((\mu F m_1 m_2).app X) = (\mu F m_2 m_3).app ((F.obj m_1).obj X) \;\gg\; (\mu F m_1 (m_2 \otimes m_3)).app X \;\gg\; (F.map (\alpha_ m_1 m_2 m_3).inv).app X \;\gg\; (\delta F (m_1 \otimes m_2) m_3).app X $$$
Lean4
@[simp, reassoc]
theorem obj_μ_app (m₁ m₂ m₃ : M) (X : C) [F.Monoidal] :
(F.obj m₃).map ((μ F m₁ m₂).app X) =
(μ F m₂ m₃).app ((F.obj m₁).obj X) ≫
(μ F m₁ (m₂ ⊗ m₃)).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (δ F (m₁ ⊗ m₂) m₃).app X :=
by
rw [← associativity_app_assoc]
simp
