instIsEquivalenceFunctorSingleObjFunctor

English

The functor CategoryEquivalence between Action V G and the functor category is an equivalence of categories.

Русский

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

LaTeX

$$The functor ${\\text{functorCategoryEquivalence}}: \\mathrm{Action}(V,G) \\to \\mathrm{Fun}(\\mathrm{SingleObj}(G), V)$ is an equivalence.$$

Lean4

instance : (FunctorCategoryEquivalence.functor (V := V) (G := G)).IsEquivalence :=
  (functorCategoryEquivalence V G).isEquivalence_functor

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