right_unitality_app — Mathlib

English

Right unitality condition for the monoidal structure at a given n and X, relating ε and μ with the right unitor.

Русский

Условие правой единицы моноидальной структуры для данного n и X, связывающее ε и μ с правой юниторой.

LaTeX

$$$ (\\varepsilon F).app ((F.obj n).obj X) \\circ (\\mu F n (\\mathbb{1}_M)).app X \\circ (F.map (\\rho_ n).hom).app X = \\mathrm{id} $$$

Lean4

@[reassoc]
theorem right_unitality_app (n : M) (X : C) [F.Monoidal] :
    (ε F).app ((F.obj n).obj X) ≫ (μ F n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X = 𝟙 _ :=
  congr_app (Functor.LaxMonoidal.right_unitality F n).symm X

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