English
Let F be a monoidal endofunctor on C-valued endofunctors over a monoidal category M. Then for any object n in M and X in C, the component of the epsilon at (F n)(X) factors as the inverse right unitor mapped by F, followed by the δ-map at (n, 1_M) evaluated at X.
Русский
Пусть F — моноидальная концу-функторальная над сенами C, и пусть ε — соответствующая компонентная монадическая структура. Тогда для любого n ∈ M и X ∈ C компонент ε_F((F.obj n).obj X) раскладывается как образ F от (ρ_n)^{-1} на X, затем применяем δ F n (1_M) на X.
LaTeX
$$$ (\varepsilon F).app ((F.obj n).obj X) = (F.map (\rho_n).inv).app X \;\gg\; (\delta F n (\mathbf{1}_M)).app X $$$
Lean4
@[simp]
theorem ε_app_obj (n : M) (X : C) [F.Monoidal] :
(ε F).app ((F.obj n).obj X) = (F.map (ρ_ n).inv).app X ≫ (δ F n (𝟙_ M)).app X :=
by
rw [map_rightUnitor_inv]
dsimp
simp only [Category.id_comp, Category.assoc, μ_δ_app, endofunctorMonoidalCategory_tensorObj_obj, Category.comp_id]
