obj_ε_app — Mathlib

English

General naturality condition for δ with respect to f: the diagram commutes with the action of F on tensor objects.

Русский

Общее условие натурализма δ относительно f: диаграмма коммутирует с действием F над тензор-объектами.

LaTeX

$$$ (\\delta F m n).app X \\circ (F.obj n).map ((F.map f).app X) = (F.obj (tensorObj m n)).map f \\circ (\\delta F m n).app Y $$$

Lean4

@[simp, reassoc]
theorem obj_ε_app (n : M) (X : C) [F.Monoidal] :
    (F.obj n).map ((ε F).app X) = (F.map (λ_ n).inv).app X ≫ (δ F (𝟙_ M) n).app X :=
  by
  rw [map_leftUnitor_inv]
  dsimp
  simp only [Category.id_comp, Category.assoc, μ_δ_app, endofunctorMonoidalCategory_tensorObj_obj, Category.comp_id]

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