functorCategoryEquivalence — Mathlib

English

Let V be a category and G a monoid. The category of actions of G in V is equivalent to the functor category from the one-object category associated to G to V.

Русский

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

LaTeX

$$$\\mathrm{Action}(V,G) \\simeq \\mathrm{Fun}(\\mathrm{SingleObj}(G), V)$$$

Lean4

/-- The category of actions of `G` in the category `V`
is equivalent to the functor category `singleObj G ⥤ V`.
-/
@[simps]
def functorCategoryEquivalence : Action V G ≌ SingleObj G ⥤ V
    where
  functor := functor
  inverse := inverse
  unitIso := unitIso
  counitIso := counitIso

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