instMonoidalCategory — Mathlib

English

The category Action V G is a Monoidal category, obtained by transporting the Monoidal structure along the equivalence with the functor category.

Русский

Категория Action V G является моноидальной, структура которой переносится вдоль эквивалентности с категорией функторов.

LaTeX

$$$\mathrm{Monoidal}(\mathrm{Action}(V,G))$$$

Lean4

@[simps! tensorUnit_V tensorObj_V tensorHom_hom whiskerLeft_hom whiskerRight_hom associator_hom_hom associator_inv_hom
      leftUnitor_hom_hom leftUnitor_inv_hom rightUnitor_hom_hom rightUnitor_inv_hom]
instance instMonoidalCategory : MonoidalCategory (Action V G) :=
  Monoidal.transport (Action.functorCategoryEquivalence _ _).symm

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