instMonoidalActionMapAction — Mathlib

English

A monoidal functor between V and W induces a monoidal functor between the categories of G-actions in V and W.

Русский

Моноидальная функция между категориями V и W индуцирует моноидальную функцию между категориями G-действий в V и W.

LaTeX

$$$F.mapAction G \;:\; (V^G) \to (W^G) \text{ is Monoidal if } F \text{ is Monoidal}$$$

Lean4

/-- A monoidal functor induces a monoidal functor between
the categories of `G`-actions within those categories. -/
instance [F.Monoidal] : (F.mapAction G).Monoidal
    where
  η_ε := by ext; dsimp; rw [η_ε]
  ε_η := by ext; dsimp; rw [ε_η]
  μ_δ _ _ := by ext; dsimp; rw [μ_δ]
  δ_μ _ _ := by ext; dsimp; rw [δ_μ]

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