forget_μ — Mathlib

English

Let V be a category and G a monoid acting on V. The forgetful functor forget from Action V G to V is strictly monoidal, so its associativity constraint is the identity on all pairs of objects; equivalently μ_{X,Y} = id for all X,Y in Action V G.

Русский

Пусть V — категория, а G — моноид, действующий на V. Забывающий функтор forget: Action V G → V строго моноидален, следовательно ассоциативное преобразование μ равно тождественному морфизму для всех X,Y в Action V G; то есть μ_{X,Y} = id.

LaTeX

$$$\mu_{X,Y} = \mathrm{id}_{X.V \otimes Y.V}$$$

Lean4

@[simp]
theorem forget_μ (X Y : Action V G) : μ (Action.forget V G) X Y = 𝟙 _ :=
  rfl

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