Documentation

Mathlib.RepresentationTheory.Action

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.

• 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 : MonCat) :
Type (u + 1)
• V : V
• ρ : G

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) :
(↑() g).hom = A g
@[simp]
theorem Action.ρAut_apply_inv {V : Type (u + 1)} {G : GroupCat} (A : Action V ()) (g : G) :
(↑() 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.

Instances For

The trivial representation of a group.

Instances For
theorem Action.Hom.ext {V : Type (u + 1)} :
∀ {inst : } {G : MonCat} {M N : Action V G} (x y : ), x.hom = y.homx = y
theorem Action.Hom.ext_iff {V : Type (u + 1)} :
∀ {inst : } {G : MonCat} {M N : Action V G} (x y : ), 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_assoc {V : Type (u + 1)} {G : MonCat} {M : Action V G} {N : Action V G} (self : ) (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) :

The identity morphism on an Action V G.

Instances For
instance Action.Hom.instInhabitedHom {V : Type (u + 1)} {G : MonCat} (M : Action V G) :
@[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 : ) (q : ) :
def Action.Hom.comp {V : Type (u + 1)} {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (p : ) (q : ) :

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

Instances For
instance Action.instCategoryAction {V : Type (u + 1)} {G : MonCat} :
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✝) :
().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✝) :
().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.

Instances For
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] :
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.CategoryStruct.comp (M g) f = CategoryTheory.CategoryStruct.comp f (N g)) :
@[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
@[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

Auxilliary definition for functorCategoryEquivalence.

Instances For
@[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_obj_V {V : Type (u + 1)} {G : MonCat} (F : ) :
(Action.FunctorCategoryEquivalence.inverse.obj F).V = F.obj PUnit.unit
@[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

Auxilliary definition for functorCategoryEquivalence.

Instances For
@[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 =
@[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 =
def Action.FunctorCategoryEquivalence.unitIso {V : Type (u + 1)} {G : MonCat} :
CategoryTheory.Functor.comp Action.FunctorCategoryEquivalence.functor Action.FunctorCategoryEquivalence.inverse

Auxilliary definition for functorCategoryEquivalence.

Instances For
@[simp]
theorem Action.FunctorCategoryEquivalence.counitIso_hom_app_app {V : Type (u + 1)} {G : MonCat} (X : ) (X : ) :
(Action.FunctorCategoryEquivalence.counitIso.hom.app X).app X =
@[simp]
theorem Action.FunctorCategoryEquivalence.counitIso_inv_app_app {V : Type (u + 1)} {G : MonCat} (X : ) (X : ) :
(Action.FunctorCategoryEquivalence.counitIso.inv.app X).app X =
def Action.FunctorCategoryEquivalence.counitIso {V : Type (u + 1)} {G : MonCat} :
CategoryTheory.Functor.comp Action.FunctorCategoryEquivalence.inverse Action.FunctorCategoryEquivalence.functor

Auxilliary definition for functorCategoryEquivalence.

Instances For
@[simp]
theorem Action.functorCategoryEquivalence_functor (V : Type (u + 1)) (G : MonCat) :
().functor = Action.FunctorCategoryEquivalence.functor
@[simp]
theorem Action.functorCategoryEquivalence_counitIso (V : Type (u + 1)) (G : MonCat) :
().counitIso = Action.FunctorCategoryEquivalence.counitIso
@[simp]
theorem Action.functorCategoryEquivalence_inverse (V : Type (u + 1)) (G : MonCat) :
().inverse = Action.FunctorCategoryEquivalence.inverse
@[simp]
theorem Action.functorCategoryEquivalence_unitIso (V : Type (u + 1)) (G : MonCat) :
().unitIso = Action.FunctorCategoryEquivalence.unitIso

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

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

Instances For
instance Action.hasForgetToV (V : Type (u + 1)) (G : MonCat) :

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

Instances For
noncomputable instance Action.instPreservesLimitsForget (V : Type (u + 1)) (G : MonCat) :
noncomputable instance Action.instPreservesColimitsForget (V : Type (u + 1)) (G : MonCat) :
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 = ↑(CategoryTheory.Iso.conj (().mapIso f)) (M g)
@[simp]
theorem Action.zero_hom {V : Type (u + 1)} {G : MonCat} {X : Action V G} {Y : Action V G} :
0.hom = 0
instance Action.forget_additive {V : Type (u + 1)} {G : MonCat} :
instance Action.forget₂_additive {V : Type (u + 1)} {G : MonCat} :
@[simp]
theorem Action.neg_hom {V : Type (u + 1)} {G : MonCat} {X : Action V G} {Y : Action V G} (f : X Y) :
(-f).hom = -f.hom
@[simp]
theorem Action.add_hom {V : Type (u + 1)} {G : MonCat} {X : Action V G} {Y : Action V G} (f : X Y) (g : X Y) :
(f + g).hom = f.hom + g.hom
@[simp]
theorem Action.sum_hom {V : Type (u + 1)} {G : MonCat} {X : Action V G} {Y : Action V G} {ι : Type u_1} (f : ι → (X Y)) (s : ) :
().hom = Finset.sum s fun i => (f i).hom
instance Action.forget_linear {V : Type (u + 1)} {G : MonCat} {R : Type u_1} [] [] :
instance Action.forget₂_linear {V : Type (u + 1)} {G : MonCat} {R : Type u_1} [] [] :
instance Action.functorCategoryEquivalence_linear {V : Type (u + 1)} {G : MonCat} {R : Type u_1} [] [] :
@[simp]
theorem Action.smul_hom {V : Type (u + 1)} {G : MonCat} {R : Type u_1} [] [] {X : Action V G} {Y : Action V G} (r : R) (f : X Y) :
(r f).hom = r f.hom
def Action.abelianAux {V : Type (u + 1)} {G : MonCat} :
Action V G

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

Instances For
noncomputable instance Action.instAbelianActionInstCategoryAction {V : Type (u + 1)} {G : MonCat} :
@[simp]
theorem Action.tensorUnit_v {V : Type (u + 1)} {G : MonCat} :
theorem Action.tensorUnit_rho {V : Type (u + 1)} {G : MonCat} {g : G} :
@[simp]
theorem Action.tensor_v {V : Type (u + 1)} {G : MonCat} {X : Action V G} {Y : Action V G} :
theorem Action.tensor_rho {V : Type (u + 1)} {G : MonCat} {X : Action V G} {Y : Action V G} {g : G} :
@[simp]
theorem Action.tensorHom {V : Type (u + 1)} {G : MonCat} {W : Action V G} {X : Action V G} {Y : Action V G} {Z : Action V G} (f : W X) (g : Y Z) :
=
theorem Action.associator_hom_hom {V : Type (u + 1)} {G : MonCat} {X : Action V G} {Y : Action V G} {Z : Action V G} :
().hom.hom = ().hom
theorem Action.associator_inv_hom {V : Type (u + 1)} {G : MonCat} {X : Action V G} {Y : Action V G} {Z : Action V G} :
().inv.hom = ().inv
theorem Action.leftUnitor_hom_hom {V : Type (u + 1)} {G : MonCat} {X : Action V G} :
.hom =
theorem Action.leftUnitor_inv_hom {V : Type (u + 1)} {G : MonCat} {X : Action V G} :
.hom =
theorem Action.rightUnitor_hom_hom {V : Type (u + 1)} {G : MonCat} {X : Action V G} :
.hom =
theorem Action.rightUnitor_inv_hom {V : Type (u + 1)} {G : MonCat} {X : Action V G} :
.hom =
def Action.tensorUnitIso {V : Type (u + 1)} {G : MonCat} {X : V} :
{ 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.

Instances For
@[simp]
theorem Action.forgetMonoidal_toLaxMonoidalFunctor_ε (V : Type (u + 1)) (G : MonCat) :
().toLaxMonoidalFunctor =
@[simp]
theorem Action.forgetMonoidal_toLaxMonoidalFunctor_toFunctor (V : Type (u + 1)) (G : MonCat) :
().toLaxMonoidalFunctor.toFunctor =
def Action.forgetMonoidal (V : Type (u + 1)) (G : MonCat) :

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

Instances For
instance Action.forgetMonoidal_faithful (V : Type (u + 1)) (G : MonCat) :
CategoryTheory.Faithful ().toLaxMonoidalFunctor.toFunctor
@[simp]
theorem Action.forgetBraided_μ (V : Type (u + 1)) (G : MonCat) (X : Action V G) (Y : Action V G) :
CategoryTheory.LaxMonoidalFunctor.μ ().toMonoidalFunctor.toLaxMonoidalFunctor X Y =
@[simp]
theorem Action.forgetBraided_ε (V : Type (u + 1)) (G : MonCat) :
().toMonoidalFunctor.toLaxMonoidalFunctor =
@[simp]
theorem Action.forgetBraided_map (V : Type (u + 1)) (G : MonCat) :
∀ {X Y : Action V G} (f : X Y), ().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = f.hom
@[simp]
theorem Action.forgetBraided_obj (V : Type (u + 1)) (G : MonCat) (M : Action V G) :
().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj M = M.V
def Action.forgetBraided (V : Type (u + 1)) (G : MonCat) :

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

Instances For
instance Action.forgetBraided_faithful (V : Type (u + 1)) (G : MonCat) :
CategoryTheory.Faithful ().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor

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

Instances For
@[simp]
theorem Action.functorCategoryMonoidalEquivalence.μ_app (V : Type (u + 1)) (G : MonCat) (A : Action V G) (B : Action V G) :
(CategoryTheory.LaxMonoidalFunctor.μ ().toLaxMonoidalFunctor A B).app PUnit.unit = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj (().toLaxMonoidalFunctor.toFunctor.obj A) (().toLaxMonoidalFunctor.toFunctor.obj B)).obj PUnit.unit)
@[simp]
theorem Action.functorCategoryMonoidalEquivalence.μIso_inv_app (V : Type (u + 1)) (G : MonCat) (A : Action V G) (B : Action V G) :
= CategoryTheory.CategoryStruct.id ((().toLaxMonoidalFunctor.toFunctor.obj ()).obj PUnit.unit)
@[simp]
theorem Action.functorCategoryMonoidalEquivalence.ε_app (V : Type (u + 1)) (G : MonCat) :
().toLaxMonoidalFunctor.app PUnit.unit =
@[simp]
theorem Action.functorCategoryMonoidalEquivalence.inv_counit_app_hom (V : Type (u + 1)) (G : MonCat) (A : Action V G) :
((CategoryTheory.Functor.adjunction (CategoryTheory.Functor.inv ().toLaxMonoidalFunctor.toFunctor)).counit.app A).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (CategoryTheory.Functor.inv (CategoryTheory.Functor.inv ().toLaxMonoidalFunctor.toFunctor)) (CategoryTheory.Functor.inv ().toLaxMonoidalFunctor.toFunctor)).obj A).V
@[simp]
theorem Action.functorCategoryMonoidalEquivalence.counit_app (V : Type (u + 1)) (G : MonCat) (A : ) :
((CategoryTheory.Functor.adjunction ().toLaxMonoidalFunctor.toFunctor).counit.app A).app PUnit.unit = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.comp (CategoryTheory.Functor.inv ().toLaxMonoidalFunctor.toFunctor) ().toLaxMonoidalFunctor.toFunctor).obj A).obj PUnit.unit)
@[simp]
theorem Action.functorCategoryMonoidalEquivalence.inv_unit_app_app (V : Type (u + 1)) (G : MonCat) (A : ) :
((CategoryTheory.Functor.adjunction (CategoryTheory.Functor.inv ().toLaxMonoidalFunctor.toFunctor)).unit.app A).app PUnit.unit =
@[simp]
theorem Action.functorCategoryMonoidalEquivalence.unit_app_hom (V : Type (u + 1)) (G : MonCat) (A : Action V G) :
((CategoryTheory.Functor.adjunction ().toLaxMonoidalFunctor.toFunctor).unit.app A).hom = CategoryTheory.CategoryStruct.id (().obj A).V
@[simp]
theorem Action.functorCategoryMonoidalEquivalence.functor_map (V : Type (u + 1)) (G : MonCat) {A : Action V G} {B : Action V G} (f : A B) :
().toLaxMonoidalFunctor.toFunctor.map f = Action.FunctorCategoryEquivalence.functor.map f
@[simp]
theorem Action.functorCategoryMonoidalEquivalence.inverse_map (V : Type (u + 1)) (G : MonCat) {A : } {B : } (f : A B) :
(CategoryTheory.Functor.inv ().toLaxMonoidalFunctor.toFunctor).map f = Action.FunctorCategoryEquivalence.inverse.map f

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

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

If V is rigid, so is Action V G.

@[simp]
theorem Action.rightDual_v {V : Type (u + 1)} {H : GroupCat} (X : Action V (().obj H)) :
X.V = X.V
@[simp]
theorem Action.leftDual_v {V : Type (u + 1)} {H : GroupCat} (X : Action V (().obj H)) :
(X).V = X.V
@[simp]
theorem Action.rightDual_ρ {V : Type (u + 1)} {H : GroupCat} (X : Action V (().obj H)) (h : H) :
X h = X h⁻¹
@[simp]
theorem Action.leftDual_ρ {V : Type (u + 1)} {H : GroupCat} (X : Action V (().obj H)) (h : H) :
(X).ρ h = X h⁻¹
def Action.actionPunitEquivalence {V : Type (u + 1)} :
V

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

Instances For
@[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
@[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
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.)

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

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

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

Instances For
instance Action.res_additive (V : Type (u + 1)) {G : MonCat} {H : MonCat} (f : G H) :
instance Action.res_linear (V : Type (u + 1)) {G : MonCat} {H : MonCat} (f : G H) {R : Type u_1} [] [] :
def Action.ofMulAction (G : Type u) (H : Type u) [] [] :
Action (Type u) ()

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

Instances For
@[simp]
theorem Action.ofMulAction_apply {G : Type u} {H : Type u} [] [] (g : G) (x : H) :
().ρ g x = g x
def Action.ofMulActionLimitCone {ι : Type v} (G : Type (max v u)) [] (F : ιType (max v u)) [(i : ι) → MulAction 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.

Instances For
@[simp]
theorem Action.leftRegular_V (G : Type u) [] :
().V = G
@[simp]
theorem Action.leftRegular_ρ_apply (G : Type u) [] :
∀ (x : ↑()) (x_1 : G), ().ρ x x_1 = x x_1
def Action.leftRegular (G : Type u) [] :
Action (Type u) ()

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

Instances For
@[simp]
theorem Action.diagonal_V (G : Type u) [] (n : ) :
().V = (Fin nG)
@[simp]
theorem Action.diagonal_ρ_apply (G : Type u) [] (n : ) :
∀ (x : ↑()) (x_1 : Fin nG) (a : Fin n), ().ρ x x_1 a = ) (Fin nG)) (Fin nG) instHSMul x x_1 a
def Action.diagonal (G : Type u) [] (n : ) :
Action (Type u) ()

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

Instances For

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

Instances For
@[simp]
theorem Action.leftRegularTensorIso_inv_hom (G : Type u) [] (X : Action (Type u) ()) (g : (CategoryTheory.MonoidalCategory.tensorObj () { V := X.V, ρ := 1 }).V) :
Action.Hom.hom ().inv g = (g.fst, X g.fst g.snd)
@[simp]
theorem Action.leftRegularTensorIso_hom_hom (G : Type u) [] (X : Action (Type u) ()) (g : ) :
Action.Hom.hom ().hom g = (g.fst, X g.fst⁻¹ g.snd)
noncomputable def Action.leftRegularTensorIso (G : Type u) [] (X : Action (Type u) ()) :

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

Instances For
@[simp]
theorem Action.diagonalSucc_inv_hom (G : Type u) [] (n : ) :
∀ (a : ), Action.Hom.hom (Type u) CategoryTheory.types () () (Action.diagonal G (n + 1)) ().inv a = (Equiv.piFinSuccAboveEquiv (fun a => G) 0).symm a
@[simp]
theorem Action.diagonalSucc_hom_hom (G : Type u) [] (n : ) :
∀ (a : (Action.diagonal G (n + 1)).V), Action.Hom.hom ().hom a = ↑(Equiv.piFinSuccAboveEquiv (fun a => G) 0) a
noncomputable def Action.diagonalSucc (G : Type u) [] (n : ) :

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

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

Instances For
instance CategoryTheory.Functor.mapAction_preadditive {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) :
instance CategoryTheory.Functor.mapAction_linear {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) {R : Type u_1} [] [] [] :
@[simp]
theorem CategoryTheory.MonoidalFunctor.mapAction_toLaxMonoidalFunctor_ε_hom {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) :
().toLaxMonoidalFunctor.hom = F
@[simp]
theorem CategoryTheory.MonoidalFunctor.mapAction_toLaxMonoidalFunctor_toFunctor {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) :
().toLaxMonoidalFunctor.toFunctor = CategoryTheory.Functor.mapAction F.toFunctor G
@[simp]
theorem CategoryTheory.MonoidalFunctor.mapAction_toLaxMonoidalFunctor_μ_hom {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) (X : Action V G) (Y : Action V G) :
(CategoryTheory.LaxMonoidalFunctor.μ ().toLaxMonoidalFunctor X Y).hom = CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V
def CategoryTheory.MonoidalFunctor.mapAction {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) :

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

Instances For
@[simp]
theorem CategoryTheory.MonoidalFunctor.mapAction_ε_inv_hom {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) :
(CategoryTheory.inv ().toLaxMonoidalFunctor).hom =
@[simp]
theorem CategoryTheory.MonoidalFunctor.mapAction_μ_inv_hom {V : Type (u + 1)} {W : Type (u + 1)} (F : ) (G : MonCat) (X : Action V G) (Y : Action V G) :
(CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ ().toLaxMonoidalFunctor X Y)).hom = CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)