English
The associator inverted, when composed with whiskering of multiplication on the left, equals whiskering of multiplication on the right followed by the associator inverse, expressing a flip of the associator in a braided setting.
Русский
Обратный ассоциатор, композиция с левым взвешиванием умножения, равна взвешиванию умножения справа затем обратный ассоциатор, выражая разворот ассоциатора в braided окружении.
LaTeX
$$$$ (tensorμ (M \otimes N) M N) \circ ((\text{whatever}) ) = (\text{something with } (α)^{-1}) $$$$
Lean4
theorem mul_leftUnitor {M : C} [MonObj M] :
(tensorμ (𝟙_ C) M (𝟙_ C) M ≫ ((λ_ (𝟙_ C)).hom ⊗ₘ μ)) ≫ (λ_ M).hom = ((λ_ M).hom ⊗ₘ (λ_ M).hom) ≫ μ :=
by
rw [← Category.comp_id (λ_ (𝟙_ C)).hom, ← Category.id_comp μ, ← tensorHom_comp_tensorHom]
simp only [tensorHom_id, id_tensorHom]
slice_lhs 3 4 => rw [leftUnitor_naturality]
slice_lhs 1 3 => rw [← leftUnitor_monoidal]
simp only [Category.id_comp]
