English
The associator in the target category, transferred by μ and mapped via F, satisfies a pentagon-like inverse relation expressing coherence of μ with associativity of the tensor product.
Русский
Ассоциативность в целевой категории через μ и отображение F удовлетворяют отношению противоличной координации с ассоциативностью тензорной операции.
LaTeX
$$$\\mu_F X Y \\;\\triangleright F X Z \\;\\circ μ_F(X\\otimes Y) Z = (α_{F X,F Y,F Z})^{-1} \\circ μ_F X Y \\triangleright F Z \\circ μ_F (X\\otimes Y) Z \\circ F(map α_{X,Y,Z})^{-1}$$$
Lean4
@[reassoc (attr := simp)]
theorem associativity_inv (X Y Z : C) :
F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv =
(α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z :=
by rw [Iso.eq_inv_comp, ← associativity_assoc, ← F.map_comp, Iso.hom_inv_id, F.map_id, comp_id]
