English
A dual identity relation between μ and δ involving left/right unitor adjustments holds; a specific rearrangement yields equality of two composites.
Русский
Двойные идентичности μ и δ с левым/правым унитором дают равенство двух композиций.
LaTeX
$$$ (\mu F (\mathbf{1}_M) m_2).app X \;\gg\; (F.map (\alpha_ m_1 (\mathbf{1}_M) m_2).inv).app X \gg\; (\delta F (m_1 \otimes \mathbf{1}_M) m_2).app X = \\; (\mu F (\mathbf{1}_M) m_2).app ((F.obj m_1).obj X) \;\gg\; (F.map (\lambda_ m_2).hom).app ((F.obj m_1).obj X) \;\gg\; (F.obj m_2).map ((F.map (\rho_ m_1).inv).app X) $$$
Lean4
@[simp]
theorem obj_μ_zero_app (m₁ m₂ : M) (X : C) [F.Monoidal] :
(μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
(μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
(μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
(F.map (λ_ m₂).hom).app ((F.obj m₁).obj X) ≫ (F.obj m₂).map ((F.map (ρ_ m₁).inv).app X) :=
by
rw [← obj_η_app_assoc, ← Functor.map_comp]
simp
