instMonoidalForget — Mathlib

English

The forgetful functor from Action V G to V is monoidal (the monoidal structure is transported from the base category).

Русский

Функтор забывания из Action V G в V является моноидальным (структура переносится из базовой категории).

LaTeX

$$$\mathrm{Action.forget}\, V\, G \text{ is Monoidal}$$$

Lean4

instance : (Action.forget V G).Monoidal :=
  Functor.CoreMonoidal.toMonoidal
    { εIso := Iso.refl _
      μIso := fun _ _ ↦ Iso.refl _ }

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