Theorems · Definition · category theory

CategoryTheory.Equivalence.mapAction

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

An equivalence of categories induces an equivalence of the categories of G-actions within those categories.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryMonoid