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 has its δ constraint equal to the identity for all X,Y in Action V G; i.e., δ_{X,Y} = id.

Русский

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

LaTeX

$$$\delta_{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

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