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 ≌ (singleObj G ⥤ V), and construct the restriction functors res {G H : Mon} (f : G ⟶ H) : Action V H ⥤ Action V G.

structure Action (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : Type (u + 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
• ρ : G ⟶ MonCat.of (CategoryTheory.End self.V)

@[simp]

theorem Action.ρ_one {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (A : Action V G) : A.ρ 1 = CategoryTheory.CategoryStruct.id A.V

@[simp]

theorem Action.ρAut_apply_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : GroupCat} (A : Action V (MonCat.of ↑G)) (g : ↑G) : ((Action.ρAut A) g).hom = A.ρ g

@[simp]

theorem Action.ρAut_apply_inv {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : GroupCat} (A : Action V (MonCat.of ↑G)) (g : ↑G) : ((Action.ρAut A) g).inv = A.ρ g⁻¹

def Action.ρAut {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : GroupCat} (A : Action V (MonCat.of ↑G)) : G ⟶ GroupCat.of (CategoryTheory.Aut A.V)

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

Equations

• One or more equations did not get rendered due to their size.

instance Action.inhabited' (G : MonCat) : Inhabited (Action (Type u) G)

Equations

• Action.inhabited' G = { default := { V := PUnit.{u + 1} , ρ := 1 } }

def Action.trivial (G : MonCat) : Action AddCommGroupCat G

The trivial representation of a group.

Equations

• Action.trivial G = { V := AddCommGroupCat.of PUnit.{u + 1} , ρ := 1 }

instance Action.instInhabitedActionAddCommGroupCatInstAddCommGroupCatLargeCategory (G : MonCat) : Inhabited (Action AddCommGroupCat G)

Equations

• Action.instInhabitedActionAddCommGroupCatInstAddCommGroupCatLargeCategory G = { default := Action.trivial G }

theorem Action.Hom.ext {V : Type (u + 1)} : ∀ {inst : CategoryTheory.LargeCategory V} {G : MonCat} {M N : Action V G} (x y : Action.Hom M N), x.hom = y.hom → x = y

theorem Action.Hom.ext_iff {V : Type (u + 1)} : ∀ {inst : CategoryTheory.LargeCategory V} {G : MonCat} {M N : Action V G} (x y : Action.Hom M N), x = y ↔ x.hom = y.hom

structure Action.Hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) (N : Action V G) : Type u

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

• hom : M.V ⟶ N.V
• comm : ∀ (g : ↑G), CategoryTheory.CategoryStruct.comp (M.ρ g) self.hom = CategoryTheory.CategoryStruct.comp self.hom (N.ρ g)

theorem Action.Hom.comm_assoc {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (self : Action.Hom M 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)

@[simp]

theorem Action.Hom.id_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : (Action.Hom.id M).hom = CategoryTheory.CategoryStruct.id M.V

def Action.Hom.id {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : Action.Hom M M

The identity morphism on an Action V G.

Equations

• Action.Hom.id M = Action.Hom.mk (CategoryTheory.CategoryStruct.id M.V)

instance Action.Hom.instInhabitedHom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : Inhabited (Action.Hom M M)

Equations

• Action.Hom.instInhabitedHom M = { default := Action.Hom.id M }

@[simp]

theorem Action.Hom.comp_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (p : Action.Hom M N) (q : Action.Hom N K) : (Action.Hom.comp p q).hom = CategoryTheory.CategoryStruct.comp p.hom q.hom

def Action.Hom.comp {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (p : Action.Hom M N) (q : Action.Hom N K) : Action.Hom M K

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

Equations

• Action.Hom.comp p q = Action.Hom.mk (CategoryTheory.CategoryStruct.comp p.hom q.hom)

instance Action.instCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Category.{u, u + 1} (Action V G)

Equations

• Action.instCategoryAction = CategoryTheory.Category.mk

theorem Action.hom_ext {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (φ₁ : M ⟶ N) (φ₂ : M ⟶ N) (h : φ₁.hom = φ₂.hom) : φ₁ = φ₂

@[simp]

theorem Action.id_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.V

@[simp]

theorem Action.comp_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

@[simp]

theorem Action.mkIso_inv_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M.V ≅ N.V) (comm : autoParam (∀ (g : ↑G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g)) _auto✝) : (Action.mkIso f).inv.hom = f.inv

@[simp]

theorem Action.mkIso_hom_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M.V ≅ N.V) (comm : autoParam (∀ (g : ↑G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g)) _auto✝) : (Action.mkIso f).hom.hom = f.hom

def Action.mkIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M.V ≅ N.V) (comm : autoParam (∀ (g : ↑G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g)) _auto✝) : 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.

Equations

• Action.mkIso f = CategoryTheory.Iso.mk (Action.Hom.mk f.hom) (Action.Hom.mk f.inv)

instance Action.isIso_of_hom_isIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M ⟶ N) [CategoryTheory.IsIso f.hom] : CategoryTheory.IsIso f

Equations

• (_ : CategoryTheory.IsIso f) = (_ : CategoryTheory.IsIso (Action.mkIso (CategoryTheory.asIso f.hom)).hom)

instance Action.isIso_hom_mk {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {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 (Action.Hom.mk f)

Equations

• (_ : CategoryTheory.IsIso (Action.Hom.mk f)) = (_ : CategoryTheory.IsIso (Action.mkIso (CategoryTheory.asIso f)).hom)

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_map_app {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : ∀ {X Y : Action V G} (f : X ⟶ Y) (x : CategoryTheory.SingleObj ↑G), (Action.FunctorCategoryEquivalence.functor.toPrefunctor.map f).app x = f.hom

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_obj_map {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : ∀ {X Y : CategoryTheory.SingleObj ↑G} (g : X ⟶ Y), (Action.FunctorCategoryEquivalence.functor.toPrefunctor.obj M).toPrefunctor.map g = M.ρ g

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_obj_obj {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : ∀ (x : CategoryTheory.SingleObj ↑G), (Action.FunctorCategoryEquivalence.functor.toPrefunctor.obj M).toPrefunctor.obj x = M.V

def Action.FunctorCategoryEquivalence.functor {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Functor (Action V G) (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V)

Auxiliary definition for functorCategoryEquivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Action.FunctorCategoryEquivalence.inverse_obj_ρ_apply {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (F : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) (g : ↑G) : (Action.FunctorCategoryEquivalence.inverse.toPrefunctor.obj F).ρ g = F.toPrefunctor.map g

@[simp]

theorem Action.FunctorCategoryEquivalence.inverse_obj_V {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (F : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) : (Action.FunctorCategoryEquivalence.inverse.toPrefunctor.obj F).V = F.toPrefunctor.obj PUnit.unit

@[simp]

theorem Action.FunctorCategoryEquivalence.inverse_map_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : ∀ {X Y : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V} (f : X ⟶ Y), (Action.FunctorCategoryEquivalence.inverse.toPrefunctor.map f).hom = f.app PUnit.unit

def Action.FunctorCategoryEquivalence.inverse {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) (Action V G)

Auxiliary definition for functorCategoryEquivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Action.FunctorCategoryEquivalence.unitIso_hom_app_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : Action V G) : (Action.FunctorCategoryEquivalence.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.V

@[simp]

theorem Action.FunctorCategoryEquivalence.unitIso_inv_app_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : Action V G) : (Action.FunctorCategoryEquivalence.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.V

def Action.FunctorCategoryEquivalence.unitIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Functor.id (Action V G) ≅ CategoryTheory.Functor.comp Action.FunctorCategoryEquivalence.functor Action.FunctorCategoryEquivalence.inverse

Auxiliary definition for functorCategoryEquivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Action.FunctorCategoryEquivalence.counitIso_inv_app_app {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) (X : CategoryTheory.SingleObj ↑G) : (Action.FunctorCategoryEquivalence.counitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.toPrefunctor.obj PUnit.unit)

@[simp]

theorem Action.FunctorCategoryEquivalence.counitIso_hom_app_app {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) (X : CategoryTheory.SingleObj ↑G) : (Action.FunctorCategoryEquivalence.counitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.toPrefunctor.obj PUnit.unit)

def Action.FunctorCategoryEquivalence.counitIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Functor.comp Action.FunctorCategoryEquivalence.inverse Action.FunctorCategoryEquivalence.functor ≅ CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V)

Auxiliary definition for functorCategoryEquivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Action.functorCategoryEquivalence_counitIso (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : (Action.functorCategoryEquivalence V G).counitIso = Action.FunctorCategoryEquivalence.counitIso

@[simp]

theorem Action.functorCategoryEquivalence_functor (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : (Action.functorCategoryEquivalence V G).functor = Action.FunctorCategoryEquivalence.functor

@[simp]

theorem Action.functorCategoryEquivalence_inverse (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : (Action.functorCategoryEquivalence V G).inverse = Action.FunctorCategoryEquivalence.inverse

@[simp]

theorem Action.functorCategoryEquivalence_unitIso (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : (Action.functorCategoryEquivalence V G).unitIso = Action.FunctorCategoryEquivalence.unitIso

def Action.functorCategoryEquivalence (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Action.forget_obj (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) (M : Action V G) : (Action.forget V G).toPrefunctor.obj M = M.V

@[simp]

theorem Action.forget_map (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : ∀ {X Y : Action V G} (f : X ⟶ Y), (Action.forget V G).toPrefunctor.map f = f.hom

def Action.forget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : 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.

Equations

• Action.forget V G = CategoryTheory.Functor.mk { obj := fun (M : Action V G) => M.V, map := fun {X Y : Action V G} (f : X ⟶ Y) => f.hom }

instance Action.instFaithfulActionInstCategoryActionForget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : CategoryTheory.Faithful (Action.forget V G)

Equations

• (_ : CategoryTheory.Faithful (Action.forget V G)) = (_ : CategoryTheory.Faithful (Action.forget V G))

instance Action.instConcreteCategoryActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.ConcreteCategory V] : CategoryTheory.ConcreteCategory (Action V G)

Equations

• Action.instConcreteCategoryActionInstCategoryAction V G = CategoryTheory.ConcreteCategory.mk (CategoryTheory.Functor.comp (Action.forget V G) CategoryTheory.ConcreteCategory.forget)

instance Action.hasForgetToV (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.ConcreteCategory V] : CategoryTheory.HasForget₂ (Action V G) V

Equations

• Action.hasForgetToV V G = CategoryTheory.HasForget₂.mk (Action.forget V G)

def Action.functorCategoryEquivalenceCompEvaluation (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : CategoryTheory.Functor.comp (Action.functorCategoryEquivalence V G).functor ((CategoryTheory.evaluation (CategoryTheory.SingleObj ↑G) V).toPrefunctor.obj PUnit.unit) ≅ Action.forget V G

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Action.instPreservesLimitsForget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.Limits.HasLimits V] : CategoryTheory.Limits.PreservesLimits (Action.forget V G)

Equations

• Action.instPreservesLimitsForget V G = CategoryTheory.Limits.preservesLimitsOfNatIso (Action.functorCategoryEquivalenceCompEvaluation V G)

noncomputable instance Action.instPreservesColimitsForget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.Limits.HasColimits V] : CategoryTheory.Limits.PreservesColimits (Action.forget V G)

Equations

• Action.instPreservesColimitsForget V G = CategoryTheory.Limits.preservesColimitsOfNatIso (Action.functorCategoryEquivalenceCompEvaluation V G)

theorem Action.Iso.conj_ρ {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M ≅ N) (g : ↑G) : N.ρ g = (CategoryTheory.Iso.conj ((Action.forget V G).mapIso f)) (M.ρ g)

def Action.actionPunitEquivalence {V : Type (u + 1)} [CategoryTheory.LargeCategory V] : Action V (MonCat.of PUnit.{u + 1} ) ≌ V

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Action.res_obj_ρ (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G ⟶ H) (M : Action V H) : ((Action.res V f).toPrefunctor.obj M).ρ = CategoryTheory.CategoryStruct.comp f M.ρ

@[simp]

theorem Action.res_obj_V (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G ⟶ H) (M : Action V H) : ((Action.res V f).toPrefunctor.obj M).V = M.V

@[simp]

theorem Action.res_map_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G ⟶ H) : ∀ {X Y : Action V H} (p : X ⟶ Y), ((Action.res V f).toPrefunctor.map p).hom = p.hom

def Action.res (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (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.)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Action.resId_inv_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} (X : Action V G) : ((Action.resId V).inv.app X).hom = CategoryTheory.CategoryStruct.id X.V

@[simp]

theorem Action.resId_hom_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} (X : Action V G) : ((Action.resId V).hom.app X).hom = CategoryTheory.CategoryStruct.id X.V

def Action.resId (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} : Action.res V (CategoryTheory.CategoryStruct.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.

Equations

• Action.resId V = CategoryTheory.NatIso.ofComponents fun (M : Action V G) => Action.mkIso (CategoryTheory.Iso.refl ((Action.res V (CategoryTheory.CategoryStruct.id G)).toPrefunctor.obj M).V)

@[simp]

theorem Action.resComp_hom_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} {K : MonCat} (f : G ⟶ H) (g : H ⟶ K) (X : Action V K) : ((Action.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.LargeCategory V] {G : MonCat} {H : MonCat} {K : MonCat} (f : G ⟶ H) (g : H ⟶ K) (X : Action V K) : ((Action.resComp V f g).inv.app X).hom = CategoryTheory.CategoryStruct.id X.V

def Action.resComp (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} {K : MonCat} (f : G ⟶ H) (g : H ⟶ K) : CategoryTheory.Functor.comp (Action.res V g) (Action.res V f) ≅ Action.res V (CategoryTheory.CategoryStruct.comp f g)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.mapAction_map_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) : ∀ {X Y : Action V G} (f : X ⟶ Y), ((CategoryTheory.Functor.mapAction F G).toPrefunctor.map f).hom = F.toPrefunctor.map f.hom

@[simp]

theorem CategoryTheory.Functor.mapAction_obj_ρ_apply {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) (M : Action V G) (g : ↑G) : ((CategoryTheory.Functor.mapAction F G).toPrefunctor.obj M).ρ g = F.toPrefunctor.map (M.ρ g)

@[simp]

theorem CategoryTheory.Functor.mapAction_obj_V {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) (M : Action V G) : ((CategoryTheory.Functor.mapAction F G).toPrefunctor.obj M).V = F.toPrefunctor.obj M.V

def CategoryTheory.Functor.mapAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) : CategoryTheory.Functor (Action V G) (Action W G)

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

Equations

• One or more equations did not get rendered due to their size.