Action V G, the category of actions of a monoid G inside some category V.

The prototypical example is V = ModuleCat R, where Action (ModuleCat R) G is the category of R-linear representations of G.

We check Action V G ≌ (CategoryTheory.SingleObj G ⥤ V), and construct the restriction functors res {G H} [Monoid G] [Monoid H] (f : G →* H) : Action V H ⥤ Action V G.

structure Action (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] : Type (max (max u_1 u_2) v_1)

An Action V G represents a bundled action of the monoid G on an object of some category V.

As an example, when V = ModuleCat R, this is an R-linear representation of G, while when V = Type this is a G-action.

• V : V

  The object this action acts on

• ρ : G →* CategoryTheory.End self.V

  The underlying monoid homomorphism of this action

theorem Action.ρ_one {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (A : Action V G) : A.ρ 1 = CategoryTheory.CategoryStruct.id A.V

def Action.ρAut {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Group G] (A : Action V G) : G →* CategoryTheory.Aut A.V

When a group acts, we can lift the action to the group of automorphisms.

@[simp]

theorem Action.ρAut_apply_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Group G] (A : Action V G) (g : G) : (A.ρAut g).hom = A.ρ g

@[simp]

theorem Action.ρAut_apply_inv {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Group G] (A : Action V G) (g : G) : (A.ρAut g).inv = A.ρ g⁻¹

def Action.trivial {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] (X : V) : Action V G

The action defined by sending every monoid element to the identity.

@[simp]

theorem Action.trivial_ρ {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] (X : V) : (trivial G X).ρ = 1

@[simp]

theorem Action.trivial_V {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] (X : V) : (trivial G X).V = X

instance Action.inhabited' (G : Type u_2) [Monoid G] : Inhabited (Action (Type u_3) G)

instance Action.instInhabitedAddCommGrpCat (G : Type u_2) [Monoid G] : Inhabited (Action AddCommGrpCat G)

structure Action.Hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (M N : Action V G) : Type v_1

A homomorphism of Action V Gs is a morphism between the underlying objects, commuting with the action of G.

• hom : M.V ⟶ N.V

  The morphism between the underlying objects of this action

• comm (g : G) : CategoryTheory.CategoryStruct.comp (M.ρ g) self.hom = CategoryTheory.CategoryStruct.comp self.hom (N.ρ g)

theorem Action.Hom.ext_iff {V : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} V} {G : Type u_2} {inst✝¹ : Monoid G} {M N : Action V G} {x y : M.Hom N} : x = y ↔ x.hom = y.hom

theorem Action.Hom.ext {V : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} V} {G : Type u_2} {inst✝¹ : Monoid G} {M N : Action V G} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y

theorem Action.Hom.comm_assoc {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (self : M.Hom N) (g : G) {Z : V} (h : N.V ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.ρ g) (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (N.ρ g) h)

def Action.Hom.id {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (M : Action V G) : M.Hom M

The identity morphism on an Action V G.

@[simp]

theorem Action.Hom.id_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (M : Action V G) : (id M).hom = CategoryTheory.CategoryStruct.id M.V

instance Action.Hom.instInhabited {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (M : Action V G) : Inhabited (M.Hom M)

def Action.Hom.comp {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N K : Action V G} (p : M.Hom N) (q : N.Hom K) : M.Hom K

The composition of two Action V G homomorphisms is the composition of the underlying maps.

@[simp]

theorem Action.Hom.comp_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N K : Action V G} (p : M.Hom N) (q : N.Hom K) : (p.comp q).hom = CategoryTheory.CategoryStruct.comp p.hom q.hom

instance Action.instCategory {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] : CategoryTheory.Category.{v_1, max (max u_2 u_1) v_1} (Action V G)

theorem Action.hom_injective {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} : Function.Injective Hom.hom

theorem Action.hom_ext {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (φ₁ φ₂ : M ⟶ N) (h : φ₁.hom = φ₂.hom) : φ₁ = φ₂

theorem Action.hom_ext_iff {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} {φ₁ φ₂ : M ⟶ N} : φ₁ = φ₂ ↔ φ₁.hom = φ₂.hom

@[simp]

theorem Action.id_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (M : Action V G) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.V

@[simp]

theorem Action.comp_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N K : Action V G} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

theorem Action.comp_hom_assoc {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N K : Action V G} (f : M ⟶ N) (g : N ⟶ K) {Z : V} (h : K.V ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)

@[simp]

theorem Action.hom_inv_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M ≅ N) : CategoryTheory.CategoryStruct.comp f.hom.hom f.inv.hom = CategoryTheory.CategoryStruct.id M.V

@[simp]

theorem Action.hom_inv_hom_assoc {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M ≅ N) {Z : V} (h : M.V ⟶ Z) : CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp f.inv.hom h) = h

@[simp]

theorem Action.inv_hom_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M ≅ N) : CategoryTheory.CategoryStruct.comp f.inv.hom f.hom.hom = CategoryTheory.CategoryStruct.id N.V

@[simp]

theorem Action.inv_hom_hom_assoc {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M ≅ N) {Z : V} (h : N.V ⟶ Z) : CategoryTheory.CategoryStruct.comp f.inv.hom (CategoryTheory.CategoryStruct.comp f.hom.hom h) = h

def Action.mkIso {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V ≅ N.V) (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g) := by cat_disch) : M ≅ N

Construct an isomorphism of G actions/representations from an isomorphism of the underlying objects, where the forward direction commutes with the group action.

@[simp]

theorem Action.mkIso_inv_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V ≅ N.V) (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g) := by cat_disch) : (mkIso f comm).inv.hom = f.inv

@[simp]

theorem Action.mkIso_hom_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V ≅ N.V) (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g) := by cat_disch) : (mkIso f comm).hom.hom = f.hom

@[instance 100]

instance Action.isIso_of_hom_isIso {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M ⟶ N) [CategoryTheory.IsIso f.hom] : CategoryTheory.IsIso f

instance Action.isIso_hom_mk {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M.V ⟶ N.V) [CategoryTheory.IsIso f] (w : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f = CategoryTheory.CategoryStruct.comp f (N.ρ g)) : CategoryTheory.IsIso { hom := f, comm := w }

instance Action.instIsIsoHomHom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M ≅ N) : CategoryTheory.IsIso f.hom.hom

instance Action.instIsIsoHomInv {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M ≅ N) : CategoryTheory.IsIso f.inv.hom

def Action.FunctorCategoryEquivalence.functor {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] : CategoryTheory.Functor (Action V G) (CategoryTheory.Functor (CategoryTheory.SingleObj G) V)

Auxiliary definition for functorCategoryEquivalence.

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_obj_obj {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (M : Action V G) (x✝ : CategoryTheory.SingleObj G) : (functor.obj M).obj x✝ = M.V

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_obj_map {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (M : Action V G) {X✝ Y✝ : CategoryTheory.SingleObj G} (g : X✝ ⟶ Y✝) : (functor.obj M).map g = M.ρ g

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_map_app {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {X✝ Y✝ : Action V G} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.SingleObj G) : (functor.map f).app x✝ = f.hom

def Action.FunctorCategoryEquivalence.inverse {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] : CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (Action V G)

Auxiliary definition for functorCategoryEquivalence.

@[simp]

theorem Action.FunctorCategoryEquivalence.inverse_obj_V {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (F : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) : (inverse.obj F).V = F.obj PUnit.unit

@[simp]

theorem Action.FunctorCategoryEquivalence.inverse_map_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.SingleObj G) V} (f : X✝ ⟶ Y✝) : (inverse.map f).hom = f.app PUnit.unit

@[simp]

theorem Action.FunctorCategoryEquivalence.inverse_obj_ρ_apply {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (F : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (g : G) : (inverse.obj F).ρ g = F.map g

def Action.FunctorCategoryEquivalence.unitIso {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] : CategoryTheory.Functor.id (Action V G) ≅ functor.comp inverse

Auxiliary definition for functorCategoryEquivalence.

@[simp]

theorem Action.FunctorCategoryEquivalence.unitIso_inv_app_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (X : Action V G) : (unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.V

@[simp]

theorem Action.FunctorCategoryEquivalence.unitIso_hom_app_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (X : Action V G) : (unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.V

def Action.FunctorCategoryEquivalence.counitIso {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] : inverse.comp functor ≅ CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.SingleObj G) V)

Auxiliary definition for functorCategoryEquivalence.

@[simp]

theorem Action.FunctorCategoryEquivalence.counitIso_inv_app_app {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (X : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (X✝ : CategoryTheory.SingleObj G) : (counitIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj PUnit.unit)

@[simp]

theorem Action.FunctorCategoryEquivalence.counitIso_hom_app_app {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] (X : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (X✝ : CategoryTheory.SingleObj G) : (counitIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj PUnit.unit)

def Action.functorCategoryEquivalence (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [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.

@[simp]

theorem Action.functorCategoryEquivalence_inverse (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] : (functorCategoryEquivalence V G).inverse = FunctorCategoryEquivalence.inverse

@[simp]

theorem Action.functorCategoryEquivalence_unitIso (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] : (functorCategoryEquivalence V G).unitIso = FunctorCategoryEquivalence.unitIso

@[simp]

theorem Action.functorCategoryEquivalence_functor (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] : (functorCategoryEquivalence V G).functor = FunctorCategoryEquivalence.functor

@[simp]

theorem Action.functorCategoryEquivalence_counitIso (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] : (functorCategoryEquivalence V G).counitIso = FunctorCategoryEquivalence.counitIso

instance Action.instIsEquivalenceFunctorSingleObjFunctor (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] : FunctorCategoryEquivalence.functor.IsEquivalence

instance Action.instIsEquivalenceFunctorSingleObjInverse (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] : FunctorCategoryEquivalence.inverse.IsEquivalence

def Action.forget (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] : CategoryTheory.Functor (Action V G) V

(implementation) The forgetful functor from bundled actions to the underlying objects.

Use the CategoryTheory.forget API provided by the ConcreteCategory instance below, rather than using this directly.

@[simp]

theorem Action.forget_map (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] {X✝ Y✝ : Action V G} (f : X✝ ⟶ Y✝) : (forget V G).map f = f.hom

@[simp]

theorem Action.forget_obj (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] (M : Action V G) : (forget V G).obj M = M.V

instance Action.instFaithfulForget (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] : (forget V G).Faithful

@[reducible, inline]

abbrev Action.HomSubtype (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] {FV : V → V → Type u_3} {CV : V → Type u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] (M N : Action V G) : Type u_3

The type of V-morphisms that can be lifted back to morphisms in the category Action.

instance Action.instFunLikeHomSubtypeV (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] {FV : V → V → Type u_3} {CV : V → Type u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] (M N : Action V G) : FunLike (HomSubtype V G M N) (CV M.V) (CV N.V)

instance Action.instConcreteCategoryHomSubtypeV (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] {FV : V → V → Type u_3} {CV : V → Type u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] : CategoryTheory.ConcreteCategory (Action V G) (HomSubtype V G)

instance Action.hasForgetToV (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] {FV : V → V → Type u_3} {CV : V → Type u_4} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] : CategoryTheory.HasForget₂ (Action V G) V

def Action.functorCategoryEquivalenceCompEvaluation (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] : (functorCategoryEquivalence V G).functor.comp ((CategoryTheory.evaluation (CategoryTheory.SingleObj G) V).obj PUnit.unit) ≅ forget V G

The forgetful functor is intertwined by functorCategoryEquivalence with evaluation at PUnit.star.

instance Action.preservesLimits_forget (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.Limits.HasLimits V] : CategoryTheory.Limits.PreservesLimits (forget V G)

instance Action.preservesColimits_forget (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.Limits.HasColimits V] : CategoryTheory.Limits.PreservesColimits (forget V G)

theorem Action.Iso.conj_ρ {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] {M N : Action V G} (f : M ≅ N) (g : G) : N.ρ g = ((forget V G).mapIso f).conj (M.ρ g)

def Action.actionPUnitEquivalence {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] : Action V PUnit.{u_3 + 1} ≌ V

Actions/representations of the trivial monoid are just objects in the ambient category.

@[deprecated Action.actionPUnitEquivalence (since := "2026-02-08")]

def Action.actionPunitEquivalence {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] : Action V PUnit.{u_3 + 1} ≌ V

Alias of Action.actionPUnitEquivalence.

---

Actions/representations of the trivial monoid are just objects in the ambient category.

def Action.res (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) : CategoryTheory.Functor (Action V H) (Action V G)

The "restriction" functor along a monoid homomorphism f : G →* H, taking actions of H to actions of G.

(This makes sense for any homomorphism, but the name is natural when f is a monomorphism.)

@[simp]

theorem Action.res_obj_V (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) (M : Action V H) : ((res V f).obj M).V = M.V

@[simp]

theorem Action.res_obj_ρ (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) (M : Action V H) : ((res V f).obj M).ρ = M.ρ.comp f

@[simp]

theorem Action.res_map_hom (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) {X✝ Y✝ : Action V H} (p : X✝ ⟶ Y✝) : ((res V f).map p).hom = p.hom

def Action.resId (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} [Monoid G] : res V (MonoidHom.id G) ≅ CategoryTheory.Functor.id (Action V G)

The natural isomorphism from restriction along the identity homomorphism to the identity functor on Action V G.

@[simp]

theorem Action.resId_inv_app_hom (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} [Monoid G] (X : Action V G) : ((resId V).inv.app X).hom = CategoryTheory.CategoryStruct.id X.V

@[simp]

theorem Action.resId_hom_app_hom (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} [Monoid G] (X : Action V G) : ((resId V).hom.app X).hom = CategoryTheory.CategoryStruct.id X.V

def Action.resComp (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} {K : Type u_5} [Monoid G] [Monoid H] [Monoid K] (f : G →* H) (g : H →* K) : (res V g).comp (res V f) ≅ res V (g.comp f)

The natural isomorphism from the composition of restrictions along homomorphisms to the restriction along the composition of homomorphism.

@[simp]

theorem Action.resComp_hom_app_hom (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} {K : Type u_5} [Monoid G] [Monoid H] [Monoid K] (f : G →* H) (g : H →* K) (X : Action V K) : ((resComp V f g).hom.app X).hom = CategoryTheory.CategoryStruct.id X.V

@[simp]

theorem Action.resComp_inv_app_hom (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} {K : Type u_5} [Monoid G] [Monoid H] [Monoid K] (f : G →* H) (g : H →* K) (X : Action V K) : ((resComp V f g).inv.app X).hom = CategoryTheory.CategoryStruct.id X.V

def Action.resCongr (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] {f f' : G →* H} (h : f = f') : res V f ≅ res V f'

Restricting scalars along equal maps is naturally isomorphic.

@[simp]

theorem Action.resCongr_hom (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] {f f' : G →* H} (h : f = f') : (resCongr V h).hom = { app := fun (X : Action V H) => (mkIso (CategoryTheory.Iso.refl X.V) ⋯).hom, naturality := ⋯ }

@[simp]

theorem Action.resCongr_inv (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] {f f' : G →* H} (h : f = f') : (resCongr V h).inv = { app := fun (X : Action V H) => (mkIso (CategoryTheory.Iso.refl X.V) ⋯).inv, naturality := ⋯ }

def Action.resEquiv (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G ≃* H) : Action V H ≌ Action V G

Restricting scalars along a monoid isomorphism induces an equivalence of categories.

@[simp]

theorem Action.resEquiv_inverse (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G ≃* H) : (resEquiv V f).inverse = res V ↑f.symm

@[simp]

theorem Action.resEquiv_functor (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G ≃* H) : (resEquiv V f).functor = res V ↑f

instance Action.instFaithfulRes (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) : (res V f).Faithful

The functor from Action V H to Action V G induced by a monoid homomorphism f : G →* H is faithful.

theorem Action.full_res (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [Monoid G] [Monoid H] (f : G →* H) (f_surj : Function.Surjective ⇑f) : (res V f).Full

The functor from Action V H to Action V G induced by a monoid homomorphism f : G →* H is full if f is surjective.

def CategoryTheory.Functor.mapAction {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (F : Functor V W) (G : Type u_3) [Monoid G] : Functor (Action V G) (Action W G)

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

@[simp]

theorem CategoryTheory.Functor.mapAction_map_hom {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (F : Functor V W) (G : Type u_3) [Monoid G] {X✝ Y✝ : Action V G} (f : X✝ ⟶ Y✝) : ((F.mapAction G).map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.mapAction_obj_V {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (F : Functor V W) (G : Type u_3) [Monoid G] (M : Action V G) : ((F.mapAction G).obj M).V = F.obj M.V

@[simp]

theorem CategoryTheory.Functor.mapAction_obj_ρ_apply {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (F : Functor V W) (G : Type u_3) [Monoid G] (M : Action V G) (g : G) : ((F.mapAction G).obj M).ρ g = F.map (M.ρ g)

instance CategoryTheory.Functor.instFaithfulActionMapAction {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (F : Functor V W) (G : Type u_3) [Monoid G] [F.Faithful] : (F.mapAction G).Faithful

def CategoryTheory.Functor.FullyFaithful.mapAction {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] {F : Functor V W} (h : F.FullyFaithful) (G : Type u_3) [Monoid G] : (F.mapAction G).FullyFaithful

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

instance CategoryTheory.Functor.instFullActionMapActionOfFaithful {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (F : Functor V W) (G : Type u_3) [Monoid G] [F.Faithful] [F.Full] : (F.mapAction G).Full

def CategoryTheory.Functor.mapActionComp {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (G : Type u_3) [Monoid G] {T : Type u_4} [Category.{v_3, u_4} T] (F : Functor V W) (F' : Functor W T) : (F.comp F').mapAction G ≅ (F.mapAction G).comp (F'.mapAction G)

Functor.mapAction is functorial in the functor.

@[simp]

theorem CategoryTheory.Functor.mapActionComp_inv {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (G : Type u_3) [Monoid G] {T : Type u_4} [Category.{v_3, u_4} T] (F : Functor V W) (F' : Functor W T) : (mapActionComp G F F').inv = { app := fun (X : Action V G) => CategoryStruct.id (((F.comp F').mapAction G).obj X), naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapActionComp_hom {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (G : Type u_3) [Monoid G] {T : Type u_4} [Category.{v_3, u_4} T] (F : Functor V W) (F' : Functor W T) : (mapActionComp G F F').hom = { app := fun (X : Action V G) => CategoryStruct.id (((F.comp F').mapAction G).obj X), naturality := ⋯ }

def CategoryTheory.Functor.mapActionCongr {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (G : Type u_3) [Monoid G] {F F' : Functor V W} (e : F ≅ F') : F.mapAction G ≅ F'.mapAction G

Functor.mapAction preserves isomorphisms of functors.

@[simp]

theorem CategoryTheory.Functor.mapActionCongr_hom {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (G : Type u_3) [Monoid G] {F F' : Functor V W} (e : F ≅ F') : (mapActionCongr G e).hom = { app := fun (X : Action V G) => (Action.mkIso (e.app X.V) ⋯).hom, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapActionCongr_inv {V : Type u_1} [Category.{v_1, u_1} V] {W : Type u_2} [Category.{v_2, u_2} W] (G : Type u_3) [Monoid G] {F F' : Functor V W} (e : F ≅ F') : (mapActionCongr G e).inv = { app := fun (X : Action V G) => (Action.mkIso (e.app X.V) ⋯).inv, naturality := ⋯ }

def CategoryTheory.Equivalence.mapAction {V : Type u_2} {W : Type u_3} [Category.{v_2, u_2} V] [Category.{v_3, u_3} W] (G : Type u_4) [Monoid G] (E : V ≌ W) : Action V G ≌ Action W G

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

@[simp]

theorem CategoryTheory.Equivalence.mapAction_inverse {V : Type u_2} {W : Type u_3} [Category.{v_2, u_2} V] [Category.{v_3, u_3} W] (G : Type u_4) [Monoid G] (E : V ≌ W) : (mapAction G E).inverse = E.inverse.mapAction G

@[simp]

theorem CategoryTheory.Equivalence.mapAction_functor {V : Type u_2} {W : Type u_3} [Category.{v_2, u_2} V] [Category.{v_3, u_3} W] (G : Type u_4) [Monoid G] (E : V ≌ W) : (mapAction G E).functor = E.functor.mapAction G