Theorems · Definition · category theory

CategoryTheory.Functor.mapAction

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

A functor between categories induces a functor between the categories of G-actions within those categories.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

21 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryMonoid