English
For all m1,m2,m3 in M and X in C, a coherence equation for μ and α holds: mapping μ at m1,m2 along F then composing with μ at (m1⊗m2,m3) and α equals composing μ at m2,m3 and μ at m1,m2⊗m3, then applying F.map to α.
Русский
Для любых m1,m2,m3 в M и X в C выполняется координационная тождественность для μ и α: последовательности узаконенного отображения μ и α совпадают с другой последовательностью μ.
LaTeX
$$$ (F.obj m_3).map ((\mu F m_1 m_2).app X) \;\gg\; (\mu F (m_1 \otimes m_2) m_3).app X \;\gg\; (F.map (\alpha_ m_1 m_2 m_3).hom).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 $$$
Lean4
@[reassoc]
theorem associativity_app (m₁ m₂ m₃ : M) (X : C) [F.LaxMonoidal] :
(F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
(μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X :=
by
have := congr_app (associativity F m₁ m₂ m₃) X
dsimp at this
simpa using this
