Theorems · Definition · category theory

Action.FunctorCategoryEquivalence.functor

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

Auxiliary definition for functorCategoryEquivalence.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

14 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryMonoid