mathlib3 documentation

representation_theory.Action

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

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) :

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
@[protected, instance]
@[protected, instance]
def Action.is_iso_hom_mk {V : Type (u+1)} [category_theory.large_category V] {G : Mon} {M N : Action V G} (f : M.V N.V) [category_theory.is_iso f] (w : ( (g : G), (M.ρ) g f = f (N.ρ) g) . "obviously") :

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
@[simp]
theorem Action.sum_hom {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.preadditive V] {X Y : Action V G} {ι : Type u_1} (f : ι (X Y)) (s : finset ι) :
(s.sum f).hom = s.sum (λ (i : ι), (f i).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
def Action.tensor_unit_iso {V : Type (u+1)} [category_theory.large_category V] {G : Mon} [category_theory.monoidal_category V] {X : V} (f : 𝟙_ V X) :
𝟙_ (Action V G) {V := X, ρ := 1}

Given an object X isomorphic to the tensor unit of V, X equipped with the trivial action is isomorphic to the tensor unit of Action V G.

Equations

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

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]
def Action.of_mul_action (G H : Type u) [monoid G] [mul_action G H] :

Bundles a type H with a multiplicative action of G as an Action.

Equations
@[simp]
theorem Action.of_mul_action_apply {G H : Type u} [monoid G] [mul_action G H] (g : G) (x : H) :
def Action.of_mul_action_limit_cone {ι : Type v} (G : Type (max v u)) [monoid G] (F : ι Type (max v u)) [Π (i : ι), mul_action G (F i)] :

Given a family F of types with G-actions, this is the limit cone demonstrating that the product of F as types is a product in the category of G-sets.

Equations
def Action.left_regular (G : Type u) [monoid G] :

The G-set G, acting on itself by left multiplication.

Equations
@[simp]
theorem Action.left_regular_ρ_apply (G : Type u) [monoid G] (ᾰ : (Mon.of G)) (ᾰ_1 : G) :
((Action.left_regular G).ρ) ᾰ_1 = * ᾰ_1
@[simp]
theorem Action.left_regular_V (G : Type u) [monoid G] :
def Action.diagonal (G : Type u) [monoid G] (n : ) :

The G-set Gⁿ, acting on itself by left multiplication.

Equations
@[simp]
theorem Action.diagonal_ρ_apply (G : Type u) [monoid G] (n : ) (ᾰ : (Mon.of G)) (ᾰ_1 : fin n G) (ᾰ_2 : fin n) :
((Action.diagonal G n).ρ) ᾰ_1 ᾰ_2 = * ᾰ_1 ᾰ_2
@[simp]
theorem Action.diagonal_V (G : Type u) [monoid G] (n : ) :
(Action.diagonal G n).V = (fin n G)

We have fin 1 → G ≅ G as G-sets, with G acting by left multiplication.

Equations
@[simp]
theorem Action.left_regular_tensor_iso_inv_hom (G : Type u) [group G] (X : Action (Type u) (Mon.of G)) (g : (Action.left_regular G {V := X.V, ρ := 1}).V) :

Given X : Action (Type u) (Mon.of G) for G a group, then G × X (with G acting as left multiplication on the first factor and by X.ρ on the second) is isomorphic as a G-set to G × X (with G acting as left multiplication on the first factor and trivially on the second). The isomorphism is given by (g, x) ↦ (g, g⁻¹ • x).

Equations
@[simp]
@[simp]
@[simp]
theorem Action.diagonal_succ_hom_hom (G : Type u) [monoid G] (n : ) (ᾰ : (Action.diagonal G (n + 1)).V) :
(Action.diagonal_succ G n).hom.hom = (ᾰ 0, λ (j : fin n), ᾰ j.succ)

The natural isomorphism of G-sets Gⁿ⁺¹ ≅ G × Gⁿ, where G acts by left multiplication on each factor.

Equations
@[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

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)