functorMonoidal — Mathlib

English

Upgrading the relevant functor to a monoidal functor: FunctorCategoryEquivalence.functor becomes monoidal.

Русский

Смещение соответствующего функторa к моноидальному функтору: F = FunctorCategoryEquivalence.functor становится моноидальным.

LaTeX

$$$\text{Monoidal} \left( \mathrm{FunctorCategoryEquivalence.functor}(V,G) \right)$$$

Lean4

/-- Upgrading the functor `Action V G ⥤ (SingleObj G ⥤ V)` to a monoidal functor. -/
instance functorMonoidal : (FunctorCategoryEquivalence.functor (V := V) (G := G)).Monoidal :=
  inferInstanceAs (Monoidal.equivalenceTransported (Action.functorCategoryEquivalence V G).symm).inverse.Monoidal

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