# mathlibdocumentation

representation_theory.Action

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

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

We check Action V G ≌ (single_obj G ⥤ V), and construct the restriction functors res {G H : Mon} (f : G ⟶ H) : Action V H ⥤ Action V G.

• When V has (co)limits so does Action V G.
• When V is monoidal, braided, or symmetric, so is Action V G.
• When V is preadditive, linear, or abelian so is Action V G.
structure Action (V : Type (u+1)) (G : Mon) :
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 = Module R, this is an R-linear representation of G, while when V = Type this is a G-action.

Instances for Action
@[simp]
theorem Action.ρ_one {V : Type (u+1)} {G : Mon} (A : G) :
(A.ρ) 1 = 𝟙 A.V
def Action.ρ_Aut {V : Type (u+1)} {G : Group} (A : (Mon.of G)) :

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

Equations
@[simp]
theorem Action.ρ_Aut_apply_inv {V : Type (u+1)} {G : Group} (A : (Mon.of G)) (g : G) :
((A.ρ_Aut) g).inv = (A.ρ) g⁻¹
@[simp]
theorem Action.ρ_Aut_apply_hom {V : Type (u+1)} {G : Group} (A : (Mon.of G)) (g : G) :
((A.ρ_Aut) g).hom = (A.ρ) g
def Action.trivial (G : Mon) :

The trivial representation of a group.

Equations
@[protected, instance]
def Action.inhabited (G : Mon) :
Equations
@[ext]
structure Action.hom {V : Type (u+1)} {G : Mon} (M N : G) :
Type u

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

Instances for Action.hom
theorem Action.hom.ext {V : Type (u+1)} {_inst_1 : category_theory.large_category V} {G : Mon} {M N : G} (x y : M.hom N) (h : x.hom = y.hom) :
x = y
theorem Action.hom.ext_iff {V : Type (u+1)} {_inst_1 : category_theory.large_category V} {G : Mon} {M N : G} (x y : M.hom N) :
x = y x.hom = y.hom
theorem Action.hom.comm {V : Type (u+1)} {G : Mon} {M N : G} (self : M.hom N) (g : G) :
(M.ρ) g self.hom = self.hom (N.ρ) g
def Action.hom.id {V : Type (u+1)} {G : Mon} (M : G) :
M.hom M

The identity morphism on a Action V G.

Equations
@[simp]
theorem Action.hom.id_hom {V : Type (u+1)} {G : Mon} (M : G) :
.hom = 𝟙 M.V
@[protected, instance]
def Action.hom.inhabited {V : Type (u+1)} {G : Mon} (M : G) :
Equations
def Action.hom.comp {V : Type (u+1)} {G : Mon} {M N K : 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
@[simp]
theorem Action.hom.comp_hom {V : Type (u+1)} {G : Mon} {M N K : G} (p : M.hom N) (q : N.hom K) :
(p.comp q).hom = p.hom q.hom
@[protected, instance]
def Action.category_theory.category {V : Type (u+1)} {G : Mon} :
Equations
@[simp]
theorem Action.id_hom {V : Type (u+1)} {G : Mon} (M : G) :
(𝟙 M).hom = 𝟙 M.V
@[simp]
theorem Action.comp_hom {V : Type (u+1)} {G : Mon} {M N K : G} (f : M N) (g : N K) :
(f g).hom = f.hom g.hom
@[simp]
theorem Action.mk_iso_inv_hom {V : Type (u+1)} {G : Mon} {M N : G} (f : M.V N.V) (comm : ∀ (g : G), (M.ρ) g f.hom = f.hom (N.ρ) g) :
comm).inv.hom = f.inv
@[simp]
theorem Action.mk_iso_hom_hom {V : Type (u+1)} {G : Mon} {M N : G} (f : M.V N.V) (comm : ∀ (g : G), (M.ρ) g f.hom = f.hom (N.ρ) g) :
comm).hom.hom = f.hom
def Action.mk_iso {V : Type (u+1)} {G : Mon} {M N : G} (f : M.V N.V) (comm : ∀ (g : G), (M.ρ) g f.hom = f.hom (N.ρ) g) :
M N

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

Equations
@[protected, instance]
def Action.is_iso_of_hom_is_iso {V : Type (u+1)} {G : Mon} {M N : G} (f : M N)  :
@[protected, instance]
def Action.is_iso_hom_mk {V : Type (u+1)} {G : Mon} {M N : G} (f : M.V N.V) (w : (∀ (g : G), (M.ρ) g f = f (N.ρ) g) . "obviously") :
@[simp]
@[simp]
theorem Action.functor_category_equivalence.functor_obj_map {V : Type (u+1)} {G : Mon} (M : G) (_x _x_1 : category_theory.single_obj G) (g : _x _x_1) :
= (M.ρ) g
@[simp]
theorem Action.functor_category_equivalence.functor_map_app {V : Type (u+1)} {G : Mon} (M N : G) (f : M N) (_x : category_theory.single_obj G) :
def Action.functor_category_equivalence.functor {V : Type (u+1)} {G : Mon} :
G

Auxilliary definition for functor_category_equivalence.

Equations
@[simp]
theorem Action.functor_category_equivalence.inverse_obj_ρ_apply {V : Type (u+1)} {G : Mon} (F : V) (g : G) :
= F.map g
def Action.functor_category_equivalence.inverse {V : Type (u+1)} {G : Mon} :
G

Auxilliary definition for functor_category_equivalence.

Equations
@[simp]
theorem Action.functor_category_equivalence.inverse_map_hom {V : Type (u+1)} {G : Mon} (M N : V) (f : M N) :
= f.app punit.star
@[simp]
theorem Action.functor_category_equivalence.inverse_obj_V {V : Type (u+1)} {G : Mon} (F : V) :
= F.obj punit.star

Auxilliary definition for functor_category_equivalence.

Equations
@[simp]
theorem Action.functor_category_equivalence.unit_iso_inv_app_hom {V : Type (u+1)} {G : Mon} (X : G) :
@[simp]
theorem Action.functor_category_equivalence.unit_iso_hom_app_hom {V : Type (u+1)} {G : Mon} (X : G) :
@[simp]
theorem Action.functor_category_equivalence.counit_iso_hom_app_app {V : Type (u+1)} {G : Mon} (X : V) (X_1 : category_theory.single_obj G) :
= (punit.rec (category_theory.iso.refl (X.obj punit.star)) X_1).hom
@[simp]
theorem Action.functor_category_equivalence.counit_iso_inv_app_app {V : Type (u+1)} {G : Mon} (X : V) (X_1 : category_theory.single_obj G) :
= (punit.rec (category_theory.iso.refl (X.obj punit.star)) X_1).inv

Auxilliary definition for functor_category_equivalence.

Equations
def Action.functor_category_equivalence (V : Type (u+1)) (G : Mon) :
G

The category of actions of G in the category V is equivalent to the functor category single_obj G ⥤ V.

Equations
@[simp]
theorem Action.functor_category_equivalence_counit_iso (V : Type (u+1)) (G : Mon) :
@[simp]
theorem Action.functor_category_equivalence_inverse (V : Type (u+1)) (G : Mon) :
@[simp]
theorem Action.functor_category_equivalence_unit_iso (V : Type (u+1)) (G : Mon) :
@[simp]
theorem Action.functor_category_equivalence_functor (V : Type (u+1)) (G : Mon) :
@[protected, instance]
@[protected, instance]
def Action.category_theory.limits.has_limits (V : Type (u+1)) (G : Mon)  :
@[protected, instance]
def Action.category_theory.limits.has_colimits (V : Type (u+1)) (G : Mon)  :
def Action.forget (V : Type (u+1)) (G : Mon) :
G V

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

Use the category_theory.forget API provided by the concrete_category instance below, rather than using this directly.

Equations
Instances for Action.forget
@[simp]
theorem Action.forget_map (V : Type (u+1)) (G : Mon) (M N : G) (f : M N) :
G).map f = f.hom
@[simp]
theorem Action.forget_obj (V : Type (u+1)) (G : Mon) (M : G) :
G).obj M = M.V
@[protected, instance]
def Action.forget.category_theory.faithful (V : Type (u+1)) (G : Mon) :
@[protected, instance]
def Action.category_theory.concrete_category (V : Type (u+1)) (G : Mon)  :
Equations
@[protected, instance]
def Action.has_forget_to_V (V : Type (u+1)) (G : Mon)  :
Equations
def Action.functor_category_equivalence_comp_evaluation (V : Type (u+1)) (G : Mon) :
punit.star

The forgetful functor is intertwined by functor_category_equivalence with evaluation at punit.star.

Equations
@[protected, instance]
noncomputable def Action.forget.category_theory.limits.preserves_limits (V : Type (u+1)) (G : Mon)  :
Equations
@[protected, instance]
noncomputable def Action.forget.category_theory.limits.preserves_colimits (V : Type (u+1)) (G : Mon)  :
Equations
theorem Action.iso.conj_ρ {V : Type (u+1)} {G : Mon} {M N : G} (f : M N) (g : G) :
(N.ρ) g = (((Action.forget V G).map_iso f).conj) ((M.ρ) g)
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def Action.category_theory.preadditive {V : Type (u+1)} {G : Mon}  :
Equations
@[protected, instance]
def Action.functor.category_theory.functor.additive {V : Type (u+1)} {G : Mon}  :
@[simp]
theorem Action.zero_hom {V : Type (u+1)} {G : Mon} {X Y : G} :
0.hom = 0
@[simp]
theorem Action.neg_hom {V : Type (u+1)} {G : Mon} {X Y : G} (f : X Y) :
(-f).hom = -f.hom
@[simp]
theorem Action.add_hom {V : Type (u+1)} {G : Mon} {X Y : G} (f g : X Y) :
(f + g).hom = f.hom + g.hom
@[protected, instance]
def Action.category_theory.linear {V : Type (u+1)} {G : Mon} {R : Type u_1} [semiring R]  :
(Action V G)
Equations
@[protected, instance]
def Action.functor.category_theory.functor.linear {V : Type (u+1)} {G : Mon} {R : Type u_1} [semiring R]  :
@[simp]
theorem Action.smul_hom {V : Type (u+1)} {G : Mon} {R : Type u_1} [semiring R] {X Y : G} (r : R) (f : X Y) :
(r f).hom = r f.hom
def Action.abelian_aux {V : Type (u+1)} {G : Mon} :
G

Auxilliary construction for the abelian (Action V G) instance.

Equations
@[protected, instance]
noncomputable def Action.category_theory.abelian {V : Type (u+1)} {G : Mon}  :
Equations
@[protected, instance]
def Action.category_theory.monoidal_category {V : Type (u+1)} {G : Mon}  :
Equations
@[simp]
theorem Action.tensor_unit_V {V : Type (u+1)} {G : Mon}  :
(𝟙_ (Action V G)).V = 𝟙_ V
@[simp]
theorem Action.tensor_unit_rho {V : Type (u+1)} {G : Mon} {g : G} :
((𝟙_ (Action V G)).ρ) g = 𝟙 (𝟙_ V)
@[simp]
theorem Action.tensor_V {V : Type (u+1)} {G : Mon} {X Y : G} :
(X Y).V = X.V Y.V
@[simp]
theorem Action.tensor_rho {V : Type (u+1)} {G : Mon} {X Y : G} {g : G} :
((X Y).ρ) g = (X.ρ) g (Y.ρ) g
@[simp]
theorem Action.tensor_hom {V : Type (u+1)} {G : Mon} {W X Y Z : G} (f : W X) (g : Y Z) :
(f g).hom = f.hom g.hom
@[simp]
theorem Action.associator_hom_hom {V : Type (u+1)} {G : Mon} {X Y Z : G} :
(α_ X Y Z).hom.hom = (α_ X.V Y.V Z.V).hom
@[simp]
theorem Action.associator_inv_hom {V : Type (u+1)} {G : Mon} {X Y Z : G} :
(α_ X Y Z).inv.hom = (α_ X.V Y.V Z.V).inv
@[simp]
theorem Action.left_unitor_hom_hom {V : Type (u+1)} {G : Mon} {X : G} :
(λ_ X).hom.hom = (λ_ X.V).hom
@[simp]
theorem Action.left_unitor_inv_hom {V : Type (u+1)} {G : Mon} {X : G} :
(λ_ X).inv.hom = (λ_ X.V).inv
@[simp]
theorem Action.right_unitor_hom_hom {V : Type (u+1)} {G : Mon} {X : G} :
(ρ_ X).hom.hom = (ρ_ X.V).hom
@[simp]
theorem Action.right_unitor_inv_hom {V : Type (u+1)} {G : Mon} {X : G} :
(ρ_ X).inv.hom = (ρ_ X.V).inv
def Action.forget_monoidal (V : Type (u+1)) (G : Mon)  :

When V is monoidal the forgetful functor Action V G to V is monoidal.

Equations
@[simp]
theorem Action.forget_monoidal_to_lax_monoidal_functor_ε (V : Type (u+1)) (G : Mon)  :
= 𝟙 (𝟙_ V)
@[simp]
@[simp]
theorem Action.forget_monoidal_to_lax_monoidal_functor_μ (V : Type (u+1)) (G : Mon) (X Y : G) :
= 𝟙 ({obj := G).obj, map := G).map, map_id' := _, map_comp' := _}.obj X {obj := G).obj, map := G).map, map_id' := _, map_comp' := _}.obj Y)
@[protected, instance]
@[protected, instance]
def Action.category_theory.braided_category (V : Type (u+1)) (G : Mon)  :
Equations
@[simp]
theorem Action.forget_braided_to_monoidal_functor (V : Type (u+1)) (G : Mon)  :
def Action.forget_braided (V : Type (u+1)) (G : Mon)  :

When V is braided the forgetful functor Action V G to V is braided.

Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def Action.category_theory.monoidal_linear (V : Type (u+1)) (G : Mon) {R : Type u_1} [semiring R]  :
Equations
noncomputable def Action.functor_category_monoidal_equivalence (V : Type (u+1)) (G : Mon)  :

Upgrading the functor Action V G ⥤ (single_obj G ⥤ V) to a monoidal functor.

Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def Action.category_theory.functor.category_theory.right_rigid_category (V : Type (u+1)) (H : Group)  :
Equations
@[protected, instance]
noncomputable def Action.category_theory.right_rigid_category (V : Type (u+1)) (H : Group)  :

If V is right rigid, so is Action V G.

Equations
@[protected, instance]
noncomputable def Action.category_theory.functor.category_theory.left_rigid_category (V : Type (u+1)) (H : Group)  :
Equations
@[protected, instance]
noncomputable def Action.category_theory.left_rigid_category (V : Type (u+1)) (H : Group)  :

If V is left rigid, so is Action V G.

Equations
@[protected, instance]
noncomputable def Action.category_theory.functor.category_theory.rigid_category (V : Type (u+1)) (H : Group)  :
Equations
@[protected, instance]
noncomputable def Action.category_theory.rigid_category (V : Type (u+1)) (H : Group)  :

If V is rigid, so is Action V G.

Equations
@[simp]
theorem Action.right_dual_V {V : Type (u+1)} {H : Group} (X : H)  :
X.V = X.V
@[simp]
theorem Action.left_dual_V {V : Type (u+1)} {H : Group} (X : H)  :
X.V = (X.V)
@[simp]
theorem Action.right_dual_ρ {V : Type (u+1)} {H : Group} (X : H) (h : H) :
(X.ρ) h = ((X.ρ) h⁻¹)
@[simp]
theorem Action.left_dual_ρ {V : Type (u+1)} {H : Group} (X : H) (h : H) :
(X.ρ) h = ((X.ρ) h⁻¹)
def Action.Action_punit_equivalence {V : Type (u+1)}  :
V

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

Equations
def Action.res (V : Type (u+1)) {G H : Mon} (f : G H) :
H 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
Instances for Action.res
@[simp]
theorem Action.res_obj_V (V : Type (u+1)) {G H : Mon} (f : G H) (M : H) :
((Action.res V f).obj M).V = M.V
@[simp]
theorem Action.res_obj_ρ (V : Type (u+1)) {G H : Mon} (f : G H) (M : H) :
((Action.res V f).obj M).ρ = f M.ρ
@[simp]
theorem Action.res_map_hom (V : Type (u+1)) {G H : Mon} (f : G H) (M N : H) (p : M N) :
((Action.res V f).map p).hom = p.hom
def Action.res_id (V : Type (u+1)) {G : Mon} :
(𝟙 G) 𝟭 (Action V G)

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

Equations
@[simp]
theorem Action.res_id_hom_app_hom (V : Type (u+1)) {G : Mon} (X : G) :
@[simp]
theorem Action.res_id_inv_app_hom (V : Type (u+1)) {G : Mon} (X : G) :
def Action.res_comp (V : Type (u+1)) {G H K : Mon} (f : G H) (g : H K) :
g f (f g)

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

Equations
@[simp]
theorem Action.res_comp_inv_app_hom (V : Type (u+1)) {G H K : Mon} (f : G H) (g : H K) (X : K) :
f g).inv.app X).hom = 𝟙 X.V
@[simp]
theorem Action.res_comp_hom_app_hom (V : Type (u+1)) {G H K : Mon} (f : G H) (g : H K) (X : K) :
f g).hom.app X).hom = 𝟙 X.V
@[protected, instance]
def Action.res_additive (V : Type (u+1)) {G H : Mon} (f : G H)  :
@[protected, instance]
def Action.res_linear (V : Type (u+1)) {G H : Mon} (f : G H) {R : Type u_1} [semiring R]  :
@[simp]
theorem category_theory.functor.map_Action_map_hom {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) (M N : G) (f : M N) :
((F.map_Action G).map f).hom = F.map f.hom
def category_theory.functor.map_Action {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) :
G G

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

Equations
Instances for category_theory.functor.map_Action
@[simp]
theorem category_theory.functor.map_Action_obj_V {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) (M : G) :
((F.map_Action G).obj M).V = F.obj M.V
@[simp]
theorem category_theory.functor.map_Action_obj_ρ_apply {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) (M : G) (g : G) :
(((F.map_Action G).obj M).ρ) g = F.map ((M.ρ) g)
@[protected, instance]
def category_theory.functor.map_Action_preadditive {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) [F.additive] :
@[protected, instance]
def category_theory.functor.map_Action_linear {V : Type (u+1)} {W : Type (u+1)} (F : V W) (G : Mon) {R : Type u_1} [semiring R] [F.additive]  :
@[simp]
theorem category_theory.monoidal_functor.map_Action_to_lax_monoidal_functor_μ_hom {V : Type (u+1)} {W : Type (u+1)} (F : W) (G : Mon) (X Y : G) :
.μ X Y).hom = Y.V
def category_theory.monoidal_functor.map_Action {V : Type (u+1)} {W : Type (u+1)} (F : W) (G : Mon) :
(Action W G)

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

Equations
@[simp]
theorem category_theory.monoidal_functor.map_Action_to_lax_monoidal_functor_to_functor {V : Type (u+1)} {W : Type (u+1)} (F : W) (G : Mon) :
@[simp]
theorem category_theory.monoidal_functor.map_Action_to_lax_monoidal_functor_ε_hom {V : Type (u+1)} {W : Type (u+1)} (F : W) (G : Mon) :