English
For a monoid object M in a monoidal category, the multiplication is compatible with the right unitor; i.e., the coherence relation involving μ and the right unitor ρ_M holds.
Русский
Для моноидального объекта M в моноидальной категории умножение совместимо с правым унитором; тождество совместимости между μ и правым унитором ρ_M выполняется.
LaTeX
$$$(\\mu ⊗ 1_{M}) \\circ (1_{M} ⊗ ρ_{M}) = ρ_{M} \\circ μ$$$
Lean4
theorem mul_rightUnitor {M : C} [MonObj M] :
(tensorμ M (𝟙_ C) M (𝟙_ C) ≫ (μ ⊗ₘ (λ_ (𝟙_ C)).hom)) ≫ (ρ_ M).hom = ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ μ :=
by
rw [← Category.id_comp μ, ← Category.comp_id (λ_ (𝟙_ C)).hom, ← tensorHom_comp_tensorHom]
simp only [tensorHom_id, id_tensorHom]
slice_lhs 3 4 => rw [rightUnitor_naturality]
slice_lhs 1 3 => rw [← rightUnitor_monoidal]
simp only [Category.id_comp]
