English
The δ-map applied to X is given by μ at (m1⊗m2,m3) composed with the associator map and δ at (m1,m2⊗m3) and δ at (m2,m3) evaluated at (F.obj m1).obj X.
Русский
Обратное соответствие δ через μ и ассоциатор описывается как композиция μ, ассоциатора и δ на соответствующих аргументах.
LaTeX
$$$ (F.obj m_3).map ((\delta F m_1 m_2).app X) = (\mu F (m_1 \otimes m_2) m_3).app X \\;\cdot (F.map (\alpha_ m_1 m_2 m_3).hom).app X \\;\cdot (\delta F m_1 (m_2 \otimes m_3)).app X \\;\cdot (\delta F m_2 m_3).app ((F.obj m_1).obj X) $$$
Lean4
@[simp, reassoc]
theorem obj_μ_inv_app (m₁ m₂ m₃ : M) (X : C) [F.Monoidal] :
(F.obj m₃).map ((δ F m₁ m₂).app X) =
(μ F (m₁ ⊗ m₂) m₃).app X ≫
(F.map (α_ m₁ m₂ m₃).hom).app X ≫ (δ F m₁ (m₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X) :=
by
rw [map_associator]
dsimp
simp only [Category.id_comp, Category.assoc, μ_δ_app_assoc, μ_δ_app, endofunctorMonoidalCategory_tensorObj_obj,
Category.comp_id]
