English
For monoid objects M,N in a braided category, the right whiskered tensor of μ with η yields the left unit coherence for tensor MN.
Русский
Для моноидальных объектов M,N в braided категории правый тензор μ с η дает левый тензорный узор для MN.
LaTeX
$$$ (μ[M] \otimes μ[N]) \text{ускоряет через } tensorμ \text{ к } (λ_{M \otimes N})^{hom} $$$
Lean4
theorem Mon_tensor_mul_assoc (M N : C) [MonObj M] [MonObj N] :
((tensorμ M N M N ≫ (μ ⊗ₘ μ)) ▷ (M ⊗ N)) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) =
(α_ (M ⊗ N : C) (M ⊗ N) (M ⊗ N)).hom ≫
((M ⊗ N : C) ◁ (tensorμ M N M N ≫ (μ ⊗ₘ μ))) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) :=
by
simp only [comp_whiskerRight_assoc, whiskerLeft_comp_assoc]
slice_lhs 2 3 => rw [tensorμ_natural_left]
slice_lhs 3 4 =>
rw [tensorHom_comp_tensorHom, mul_assoc, mul_assoc, ← tensorHom_comp_tensorHom, ← tensorHom_comp_tensorHom]
slice_lhs 1 3 => rw [tensor_associativity]
slice_lhs 3 4 => rw [← tensorμ_natural_right]
simp
