English
For monoid objects M and N in a braided monoidal category, the left whiskered tensor of one with η and μ satisfies a standard left-unital coherence with tensor μ.
Русский
Для моноидальных объектов M и N в braided моноидальной категории равенство когерентий левого единичного закона для η и μ после тензорирования.
LaTeX
$$$ (η[M] \otimes μ[N]) \text{взаимодействует через } tensorμ \text{ к } (λ_{M \otimes N})^{hom} $$$
Lean4
theorem Mon_tensor_mul_one (M N : C) [MonObj M] [MonObj N] :
(M ⊗ N) ◁ ((λ_ (𝟙_ C)).inv ≫ (η[M] ⊗ₘ η[N])) ≫ tensorμ M N M N ≫ (μ[M] ⊗ₘ μ[N]) = (ρ_ (M ⊗ N)).hom :=
by
simp only [whiskerLeft_comp_assoc]
slice_lhs 2 3 => rw [tensorμ_natural_right]
slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, mul_one, mul_one]
symm
exact tensor_right_unitality M N
