actionRight — Mathlib

English

Symmetrically, the unit of the monoidal category acts trivially on objects of D via the right action.

Русский

Аналогично, единичный объект моноидальной категории действует тривиально на объектах D через правое действие.

LaTeX

$$actionHomRight (tensorUnit) = id$$

Lean4

/-- Bundle `c ↦ c ⊙ₗ d` as a functor. -/
@[simps!]
abbrev actionRight (d : D) : C ⥤ D :=
  curriedAction C D |>.flip.obj d

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