η_app_obj — Mathlib

English

For a monoidal endofunctor F, the η-component at (F n)(X) equals the μ-component on (n,1_M) evaluated at X, followed by the map of the right unitor on n.

Русский

Для моноидального концу-функторa F компонент η на (F n)(X) равен μ-компоненте при (n, 1_M) в X, затем отображение правого юнитора на n.

LaTeX

$$$ (\eta F).app ((F.obj n).obj X) = (\mu F n (\mathbf{1}_M)).app X \;\gg\; (F.map (\rho_ n).hom).app X $$$

Lean4

@[simp]
theorem η_app_obj (n : M) (X : C) [F.Monoidal] :
    (η F).app ((F.obj n).obj X) = (μ F n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X :=
  by
  rw [map_rightUnitor]
  dsimp
  simp only [Category.comp_id, μ_δ_app_assoc]

Похожие утверждения