mathlib documentation

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.

@[simp]
theorem Action.ρ_one {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (A : Action V G) :
(A.ρ) 1 = 𝟙 A.V

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)} [category_theory.large_category V] {G : Group} (A : Action V (Mon.of G)) (g : G) :
((A.ρ_Aut) g).inv = (A.ρ) g⁻¹
@[simp]
theorem Action.ρ_Aut_apply_hom {V : Type (u+1)} [category_theory.large_category V] {G : Group} (A : Action V (Mon.of G)) (g : G) :
((A.ρ_Aut) g).hom = (A.ρ) g

The trivial representation of a group.

Equations
@[protected, instance]
Equations
@[ext]
structure Action.hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M 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.

Instances for Action.hom
theorem Action.hom.ext {V : Type (u+1)} {_inst_1 : category_theory.large_category V} {G : Mon} {M N : Action V 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 : Action V G} (x y : M.hom N) :
x = y x.hom = y.hom
theorem Action.hom.comm {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N : Action V G} (self : M.hom N) (g : G) :
(M.ρ) g self.hom = self.hom (N.ρ) g
def Action.hom.id {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M : Action V G) :
M.hom M

The identity morphism on a Action V G.

Equations
@[simp]
theorem Action.hom.id_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M : Action V G) :
@[protected, instance]
def Action.hom.inhabited {V : Type (u+1)} [category_theory.large_category V] {G : Mon} (M : Action V G) :
Equations
def Action.hom.comp {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {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.

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

Auxilliary definition for functor_category_equivalence.

Equations

Auxilliary definition for functor_category_equivalence.

Equations
def Action.forget (V : Type (u+1)) [category_theory.large_category V] (G : Mon) :
Action V 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)) [category_theory.large_category V] (G : Mon) (M N : Action V G) (f : M N) :
@[simp]
theorem Action.forget_obj (V : Type (u+1)) [category_theory.large_category V] (G : Mon) (M : Action V G) :
(Action.forget V G).obj M = M.V
theorem Action.iso.conj_ρ {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N : Action V G} (f : M N) (g : G) :
(N.ρ) g = (((Action.forget V G).map_iso f).conj) ((M.ρ) g)
@[protected, instance]
Equations
@[simp]
theorem Action.zero_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {X Y : Action V G} :
0.hom = 0
@[simp]
theorem Action.neg_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {X Y : Action V G} (f : X Y) :
(-f).hom = -f.hom
@[simp]
theorem Action.add_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {X Y : Action V G} (f g : X Y) :
(f + g).hom = f.hom + g.hom
@[protected, instance]
Equations
@[simp]
theorem Action.smul_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {R : Type u_1} [semiring R] [category_theory.linear R V] {X Y : Action V G} (r : R) (f : X Y) :
(r f).hom = r f.hom
@[simp]
theorem Action.tensor_V {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X Y : Action V G} :
(X Y).V = X.V Y.V
@[simp]
theorem Action.tensor_rho {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X Y : Action V G} {g : G} :
((X Y).ρ) g = (X.ρ) g (Y.ρ) g
@[simp]
theorem Action.tensor_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {W X Y Z : Action V G} (f : W X) (g : Y Z) :
(f g).hom = f.hom g.hom
@[simp]
theorem Action.associator_hom_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X Y Z : Action V G} :
(α_ X Y Z).hom.hom = (α_ X.V Y.V Z.V).hom
@[simp]
theorem Action.associator_inv_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X Y Z : Action V G} :
(α_ X Y Z).inv.hom = (α_ X.V Y.V Z.V).inv
@[simp]
@[simp]
@[simp]
@[simp]

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

Equations

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

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

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)) [category_theory.large_category V] {G : Mon} (X : Action V G) :
@[simp]
theorem Action.res_id_inv_app_hom (V : Type (u+1)) [category_theory.large_category V] {G : Mon} (X : Action V G) :
def Action.res_comp (V : Type (u+1)) [category_theory.large_category V] {G H K : Mon} (f : G H) (g : H K) :

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)) [category_theory.large_category V] {G H K : Mon} (f : G H) (g : H K) (X : Action V K) :
((Action.res_comp V f g).inv.app X).hom = 𝟙 X.V
@[simp]
theorem Action.res_comp_hom_app_hom (V : Type (u+1)) [category_theory.large_category V] {G H K : Mon} (f : G H) (g : H K) (X : Action V K) :
((Action.res_comp V f g).hom.app X).hom = 𝟙 X.V
@[protected, instance]
@[protected, instance]
@[simp]
theorem category_theory.functor.map_Action_map_hom {V : Type (u+1)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] (F : V W) (G : Mon) (M N : Action V 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)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] (F : V W) (G : Mon) :
Action V G Action W 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)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] (F : V W) (G : Mon) (M : Action V 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)} [category_theory.large_category V] {W : Type (u+1)} [category_theory.large_category W] (F : V W) (G : Mon) (M : Action V G) (g : G) :
(((F.map_Action G).obj M).ρ) g = F.map ((M.ρ) g)