obj_η_app — Mathlib

English

The η-component on objects interacts with left unitor via a relation showing the compatibility of η with the unit of the tensor.

Русский

Компонента η на объекте взаимодействует с левой юниторой через совместимость η с единицей тензора.

LaTeX

$$$ (\\eta F).app X = (\\mu F (\\mathbb{1}_M) n).app X \\circ (F.map (\\lambda_ n).hom).app X $$$

Lean4

@[simp, reassoc]
theorem obj_η_app (n : M) (X : C) [F.Monoidal] :
    (F.obj n).map ((η F).app X) = (μ F (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X :=
  by
  rw [← cancel_mono ((F.obj n).map ((ε F).app X)), ← Functor.map_comp]
  simp

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