# 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)) (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.

Instances For
@[simp]
theorem Action.ρ_one {V : Type (u + 1)} {G : MonCat} (A : Action V G) :
A 1 =
@[simp]
theorem Action.ρAut_apply_hom {V : Type (u + 1)} {G : GroupCat} (A : Action V ()) (g : G) :
(A.ρAut g).hom = A g
@[simp]
theorem Action.ρAut_apply_inv {V : Type (u + 1)} {G : GroupCat} (A : Action V ()) (g : G) :
(A.ρAut g).inv = A g⁻¹
def Action.ρAut {V : Type (u + 1)} {G : GroupCat} (A : Action V ()) :
G

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

Equations
• A.ρAut = { toFun := fun (g : G) => { hom := A g, inv := A g⁻¹, hom_inv_id := , inv_hom_id := }, map_one' := , map_mul' := }
Instances For
Equations

The trivial representation of a group.

Equations
• = { V := , ρ := 1 }
Instances For
Equations
• = { default := }
theorem Action.Hom.ext {V : Type (u + 1)} :
∀ {inst : } {G : MonCat} {M N : Action V G} (x y : M.Hom N), x.hom = y.homx = y
theorem Action.Hom.ext_iff {V : Type (u + 1)} :
∀ {inst : } {G : MonCat} {M N : Action V G} (x y : M.Hom N), x = y x.hom = y.hom
structure Action.Hom {V : Type (u + 1)} {G : MonCat} (M : Action V G) (N : Action V G) :

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

Instances For
theorem Action.Hom.comm {V : Type (u + 1)} {G : MonCat} {M : Action V G} {N : Action V G} (self : M.Hom N) (g : G) :
theorem Action.Hom.comm_assoc {V : Type (u + 1)} {G : MonCat} {M : Action V G} {N : Action V G} (self : M.Hom N) (g : G) {Z : V} (h : N.V Z) :
@[simp]
theorem Action.Hom.id_hom {V : Type (u + 1)} {G : MonCat} (M : Action V G) :
().hom =
def Action.Hom.id {V : Type (u + 1)} {G : MonCat} (M : Action V G) :
M.Hom M

The identity morphism on an Action V G.

Equations
• = { hom := , comm := }
Instances For
instance Action.Hom.instInhabited {V : Type (u + 1)} {G : MonCat} (M : Action V G) :
Inhabited (M.Hom M)
Equations
• = { default := }
@[simp]
theorem Action.Hom.comp_hom {V : Type (u + 1)} {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (p : M.Hom N) (q : N.Hom K) :
(p.comp q).hom = CategoryTheory.CategoryStruct.comp p.hom q.hom
def Action.Hom.comp {V : Type (u + 1)} {G : MonCat} {M : Action V G} {N : Action V G} {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.

Equations
Instances For
instance Action.instCategory {V : Type (u + 1)} {G : MonCat} :
Equations
• Action.instCategory =
theorem Action.hom_ext {V : Type (u + 1)} {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)} {G : MonCat} (M : Action V G) :
@[simp]
theorem Action.comp_hom {V : Type (u + 1)} {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (f : M N) (g : N K) :
@[simp]
theorem Action.mkIso_hom_hom {V : Type (u + 1)} {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 comm).hom.hom = f.hom
@[simp]
theorem Action.mkIso_inv_hom {V : Type (u + 1)} {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 comm).inv.hom = f.inv
def Action.mkIso {V : Type (u + 1)} {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 comm = { hom := { hom := f.hom, comm := comm }, inv := { hom := f.inv, comm := }, hom_inv_id := , inv_hom_id := }
Instances For
@[instance 100]
instance Action.isIso_of_hom_isIso {V : Type (u + 1)} {G : MonCat} {M : Action V G} {N : Action V G} (f : M N) [CategoryTheory.IsIso f.hom] :
Equations
• =
instance Action.isIso_hom_mk {V : Type (u + 1)} {G : MonCat} {M : Action V G} {N : Action V G} (f : M.V N.V) (w : ∀ (g : G), = ) :
CategoryTheory.IsIso { hom := f, comm := w }
Equations
• =
@[simp]
theorem Action.FunctorCategoryEquivalence.functor_map_app {V : Type (u + 1)} {G : MonCat} :
∀ {X Y : Action V G} (f : X Y) (x : ), (Action.FunctorCategoryEquivalence.functor.map f).app x = f.hom
@[simp]
theorem Action.FunctorCategoryEquivalence.functor_obj_obj {V : Type (u + 1)} {G : MonCat} (M : Action V G) :
∀ (x : ), (Action.FunctorCategoryEquivalence.functor.obj M).obj x = M.V
@[simp]
theorem Action.FunctorCategoryEquivalence.functor_obj_map {V : Type (u + 1)} {G : MonCat} (M : Action V G) :
∀ {X Y : } (g : X Y), (Action.FunctorCategoryEquivalence.functor.obj M).map g = M g

Auxiliary definition for functorCategoryEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Action.FunctorCategoryEquivalence.inverse_obj_V {V : Type (u + 1)} {G : MonCat} (F : ) :
(Action.FunctorCategoryEquivalence.inverse.obj F).V = F.obj PUnit.unit
@[simp]
theorem Action.FunctorCategoryEquivalence.inverse_obj_ρ_apply {V : Type (u + 1)} {G : MonCat} (F : ) (g : G) :
(Action.FunctorCategoryEquivalence.inverse.obj F) g = F.map g
@[simp]
theorem Action.FunctorCategoryEquivalence.inverse_map_hom {V : Type (u + 1)} {G : MonCat} :
∀ {X Y : } (f : X Y), (Action.FunctorCategoryEquivalence.inverse.map f).hom = f.app PUnit.unit

Auxiliary definition for functorCategoryEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Action.FunctorCategoryEquivalence.unitIso_hom_app_hom {V : Type (u + 1)} {G : MonCat} (X : Action V G) :
(Action.FunctorCategoryEquivalence.unitIso.hom.app X).hom =
@[simp]
theorem Action.FunctorCategoryEquivalence.unitIso_inv_app_hom {V : Type (u + 1)} {G : MonCat} (X : Action V G) :
(Action.FunctorCategoryEquivalence.unitIso.inv.app X).hom =
def Action.FunctorCategoryEquivalence.unitIso {V : Type (u + 1)} {G : MonCat} :
Action.FunctorCategoryEquivalence.functor.comp Action.FunctorCategoryEquivalence.inverse

Auxiliary definition for functorCategoryEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Action.FunctorCategoryEquivalence.counitIso_inv_app_app {V : Type (u + 1)} {G : MonCat} (X : ) (X : ) :
(Action.FunctorCategoryEquivalence.counitIso.inv.app X✝).app X =
@[simp]
theorem Action.FunctorCategoryEquivalence.counitIso_hom_app_app {V : Type (u + 1)} {G : MonCat} (X : ) (X : ) :
(Action.FunctorCategoryEquivalence.counitIso.hom.app X✝).app X =
def Action.FunctorCategoryEquivalence.counitIso {V : Type (u + 1)} {G : MonCat} :
Action.FunctorCategoryEquivalence.inverse.comp Action.FunctorCategoryEquivalence.functor

Auxiliary definition for functorCategoryEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Action.functorCategoryEquivalence_inverse (V : Type (u + 1)) (G : MonCat) :
.inverse = Action.FunctorCategoryEquivalence.inverse
@[simp]
theorem Action.functorCategoryEquivalence_functor (V : Type (u + 1)) (G : MonCat) :
.functor = Action.FunctorCategoryEquivalence.functor
@[simp]
theorem Action.functorCategoryEquivalence_unitIso (V : Type (u + 1)) (G : MonCat) :
.unitIso = Action.FunctorCategoryEquivalence.unitIso
@[simp]
theorem Action.functorCategoryEquivalence_counitIso (V : Type (u + 1)) (G : MonCat) :
.counitIso = Action.FunctorCategoryEquivalence.counitIso

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.
Instances For
@[simp]
theorem Action.forget_map (V : Type (u + 1)) (G : MonCat) :
∀ {X Y : Action V G} (f : X Y), ().map f = f.hom
@[simp]
theorem Action.forget_obj (V : Type (u + 1)) (G : MonCat) (M : Action V G) :
().obj M = M.V
def Action.forget (V : Type (u + 1)) (G : MonCat) :

(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
• = { obj := fun (M : Action V G) => M.V, map := fun {X Y : Action V G} (f : X Y) => f.hom, map_id := , map_comp := }
Instances For
instance Action.instFaithfulForget (V : Type (u + 1)) (G : MonCat) :
().Faithful
Equations
• =
instance Action.instConcreteCategory (V : Type (u + 1)) (G : MonCat) :
Equations
instance Action.hasForgetToV (V : Type (u + 1)) (G : MonCat) :
Equations
• = { forget₂ := , forget_comp := }
def Action.functorCategoryEquivalenceCompEvaluation (V : Type (u + 1)) (G : MonCat) :
.functor.comp ()

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.
Instances For
noncomputable instance Action.instPreservesLimitsForget (V : Type (u + 1)) (G : MonCat) :
Equations
noncomputable instance Action.instPreservesColimitsForget (V : Type (u + 1)) (G : MonCat) :
Equations
theorem Action.Iso.conj_ρ {V : Type (u + 1)} {G : MonCat} {M : Action V G} {N : Action V G} (f : M N) (g : G) :
N g = (().mapIso f).conj (M g)

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.
Instances For
@[simp]
theorem Action.res_map_hom (V : Type (u + 1)) {G : MonCat} {H : MonCat} (f : G H) :
∀ {X Y : Action V H} (p : X Y), (().map p).hom = p.hom
@[simp]
theorem Action.res_obj_ρ (V : Type (u + 1)) {G : MonCat} {H : MonCat} (f : G H) (M : Action V H) :
(().obj M) =
@[simp]
theorem Action.res_obj_V (V : Type (u + 1)) {G : MonCat} {H : MonCat} (f : G H) (M : Action V H) :
(().obj M).V = M.V
def Action.res (V : Type (u + 1)) {G : MonCat} {H : MonCat} (f : G H) :

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.
Instances For
@[simp]
theorem Action.resId_inv_app_hom (V : Type (u + 1)) {G : MonCat} (X : Action V G) :
(().inv.app X).hom =
@[simp]
theorem Action.resId_hom_app_hom (V : Type (u + 1)) {G : MonCat} (X : Action V G) :
(().hom.app X).hom =
def Action.resId (V : Type (u + 1)) {G : MonCat} :

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

Equations
Instances For
@[simp]
theorem Action.resComp_hom_app_hom (V : Type (u + 1)) {G : MonCat} {H : MonCat} {K : MonCat} (f : G H) (g : H K) (X : Action V K) :
(().hom.app X).hom =
@[simp]
theorem Action.resComp_inv_app_hom (V : Type (u + 1)) {G : MonCat} {H : MonCat} {K : MonCat} (f : G H) (g : H K) (X : Action V K) :
(().inv.app X).hom =
def Action.resComp (V : Type (u + 1)) {G : MonCat} {H : MonCat} {K : MonCat} (f : G H) (g : H K) :
().comp ()

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.mapAction_obj_ρ_apply {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) (M : Action V G) (g : G) :
((F.mapAction G).obj M) g = F.map (M g)
@[simp]
theorem CategoryTheory.Functor.mapAction_map_hom {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) :
∀ {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)} {W : Type (u + 1)} (F : ) (G : MonCat) (M : Action V G) :
((F.mapAction G).obj M).V = F.obj M.V
def CategoryTheory.Functor.mapAction {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) :

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.
Instances For