Theorems · Definition · category theory

Action.functorCategoryEquivalence

(V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) → [inst_1 : Monoid G] → Action V G ≌ CategoryTheory.Functor (CategoryTheory.SingleObj G) V

The category of actions of G in the category V is equivalent to the functor category SingleObj G ⥤ V.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

15 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryMonoid