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)) [CategoryTheory.LargeCategory V] (G : MonCat) : Type (u + 1)

• V : V
• ρ : G ⟶ MonCat.of (CategoryTheory.End s.V)

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.

@[simp]

theorem Action.ρ_one {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (A : Action V G) : ↑A.ρ 1 = CategoryTheory.CategoryStruct.id A.V

@[simp]

theorem Action.ρAut_apply_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : GroupCat} (A : Action V (MonCat.of ↑G)) (g : ↑G) : (↑(Action.ρAut A) g).hom = ↑A.ρ g

@[simp]

theorem Action.ρAut_apply_inv {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : GroupCat} (A : Action V (MonCat.of ↑G)) (g : ↑G) : (↑(Action.ρAut A) g).inv = ↑A.ρ g⁻¹

def Action.ρAut {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : GroupCat} (A : Action V (MonCat.of ↑G)) : G ⟶ GroupCat.of (CategoryTheory.Aut A.V)

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

instance Action.inhabited' (G : MonCat) : Inhabited (Action (Type u) G)

def Action.trivial (G : MonCat) : Action AddCommGroupCat G

The trivial representation of a group.

instance Action.instInhabitedActionAddCommGroupCatInstAddCommGroupCatLargeCategory (G : MonCat) : Inhabited (Action AddCommGroupCat G)

theorem Action.Hom.ext {V : Type (u + 1)} : ∀ {inst : CategoryTheory.LargeCategory V} {G : MonCat} {M N : Action V G} (x y : Action.Hom M N), x.hom = y.hom → x = y

theorem Action.Hom.ext_iff {V : Type (u + 1)} : ∀ {inst : CategoryTheory.LargeCategory V} {G : MonCat} {M N : Action V G} (x y : Action.Hom M N), x = y ↔ x.hom = y.hom

structure Action.Hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) (N : Action V G) : Type u

• hom : M.V ⟶ N.V
• comm : ∀ (g : ↑G), CategoryTheory.CategoryStruct.comp (↑M.ρ g) s.hom = CategoryTheory.CategoryStruct.comp s.hom (↑N.ρ g)

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

theorem Action.Hom.comm_assoc {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (self : Action.Hom M N) (g : ↑G) {Z : V} (h : N.V ⟶ Z) : CategoryTheory.CategoryStruct.comp (↑M.ρ g) (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (↑N.ρ g) h)

@[simp]

theorem Action.Hom.id_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : (Action.Hom.id M).hom = CategoryTheory.CategoryStruct.id M.V

def Action.Hom.id {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : Action.Hom M M

The identity morphism on an Action V G.

instance Action.Hom.instInhabitedHom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : Inhabited (Action.Hom M M)

@[simp]

theorem Action.Hom.comp_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (p : Action.Hom M N) (q : Action.Hom N K) : (Action.Hom.comp p q).hom = CategoryTheory.CategoryStruct.comp p.hom q.hom

def Action.Hom.comp {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (p : Action.Hom M N) (q : Action.Hom N K) : Action.Hom M K

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

instance Action.instCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Category.{u, u + 1} (Action V G)

theorem Action.hom_ext {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {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)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.V

@[simp]

theorem Action.comp_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} {K : Action V G} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

@[simp]

theorem Action.mkIso_hom_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {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).hom.hom = f.hom

@[simp]

theorem Action.mkIso_inv_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {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).inv.hom = f.inv

def Action.mkIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {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.

instance Action.isIso_of_hom_isIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M ⟶ N) [CategoryTheory.IsIso f.hom] : CategoryTheory.IsIso f

instance Action.isIso_hom_mk {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M.V ⟶ N.V) [CategoryTheory.IsIso f] (w : ∀ (g : ↑G), CategoryTheory.CategoryStruct.comp (↑M.ρ g) f = CategoryTheory.CategoryStruct.comp f (↑N.ρ g)) : CategoryTheory.IsIso (Action.Hom.mk f)

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_obj_obj {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : ∀ (x : CategoryTheory.SingleObj ↑G), (Action.FunctorCategoryEquivalence.functor.obj M).obj x = M.V

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_obj_map {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M : Action V G) : ∀ {X Y : CategoryTheory.SingleObj ↑G} (g : X ⟶ Y), (Action.FunctorCategoryEquivalence.functor.obj M).map g = ↑M.ρ g

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_map_app {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : ∀ {X Y : Action V G} (f : X ⟶ Y) (x : CategoryTheory.SingleObj ↑G), (Action.FunctorCategoryEquivalence.functor.map f).app x = f.hom

def Action.FunctorCategoryEquivalence.functor {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Functor (Action V G) (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V)

Auxilliary definition for functorCategoryEquivalence.

@[simp]

theorem Action.FunctorCategoryEquivalence.inverse_obj_ρ_apply {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (F : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) (g : ↑G) : ↑(Action.FunctorCategoryEquivalence.inverse.obj F).ρ g = F.map g

@[simp]

theorem Action.FunctorCategoryEquivalence.inverse_obj_V {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (F : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) : (Action.FunctorCategoryEquivalence.inverse.obj F).V = F.obj PUnit.unit

@[simp]

theorem Action.FunctorCategoryEquivalence.inverse_map_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : ∀ {X Y : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V} (f : X ⟶ Y), (Action.FunctorCategoryEquivalence.inverse.map f).hom = f.app PUnit.unit

def Action.FunctorCategoryEquivalence.inverse {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) (Action V G)

Auxilliary definition for functorCategoryEquivalence.

@[simp]

theorem Action.FunctorCategoryEquivalence.unitIso_inv_app_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : Action V G) : (Action.FunctorCategoryEquivalence.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.V

@[simp]

theorem Action.FunctorCategoryEquivalence.unitIso_hom_app_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : Action V G) : (Action.FunctorCategoryEquivalence.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.V

def Action.FunctorCategoryEquivalence.unitIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Functor.id (Action V G) ≅ CategoryTheory.Functor.comp Action.FunctorCategoryEquivalence.functor Action.FunctorCategoryEquivalence.inverse

Auxilliary definition for functorCategoryEquivalence.

@[simp]

theorem Action.FunctorCategoryEquivalence.counitIso_hom_app_app {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) (X : CategoryTheory.SingleObj ↑G) : (Action.FunctorCategoryEquivalence.counitIso.hom.app X).app X = CategoryTheory.CategoryStruct.id (X.obj PUnit.unit)

@[simp]

theorem Action.FunctorCategoryEquivalence.counitIso_inv_app_app {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (X : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) (X : CategoryTheory.SingleObj ↑G) : (Action.FunctorCategoryEquivalence.counitIso.inv.app X).app X = CategoryTheory.CategoryStruct.id (X.obj PUnit.unit)

def Action.FunctorCategoryEquivalence.counitIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} : CategoryTheory.Functor.comp Action.FunctorCategoryEquivalence.inverse Action.FunctorCategoryEquivalence.functor ≅ CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V)

Auxilliary definition for functorCategoryEquivalence.

@[simp]

theorem Action.functorCategoryEquivalence_functor (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : (Action.functorCategoryEquivalence V G).functor = Action.FunctorCategoryEquivalence.functor

@[simp]

theorem Action.functorCategoryEquivalence_counitIso (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : (Action.functorCategoryEquivalence V G).counitIso = Action.FunctorCategoryEquivalence.counitIso

@[simp]

theorem Action.functorCategoryEquivalence_inverse (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : (Action.functorCategoryEquivalence V G).inverse = Action.FunctorCategoryEquivalence.inverse

@[simp]

theorem Action.functorCategoryEquivalence_unitIso (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : (Action.functorCategoryEquivalence V G).unitIso = Action.FunctorCategoryEquivalence.unitIso

def Action.functorCategoryEquivalence (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : Action V G ≌ CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V

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

instance Action.instHasFiniteProductsActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.Limits.HasFiniteProducts V] : CategoryTheory.Limits.HasFiniteProducts (Action V G)

instance Action.instHasFiniteLimitsActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.Limits.HasFiniteLimits V] : CategoryTheory.Limits.HasFiniteLimits (Action V G)

instance Action.instHasLimitsActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.Limits.HasLimits V] : CategoryTheory.Limits.HasLimits (Action V G)

instance Action.instHasColimitsActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.Limits.HasColimits V] : CategoryTheory.Limits.HasColimits (Action V G)

@[simp]

theorem Action.forget_obj (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) (M : Action V G) : (Action.forget V G).obj M = M.V

@[simp]

theorem Action.forget_map (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : ∀ {X Y : Action V G} (f : X ⟶ Y), (Action.forget V G).map f = f.hom

def Action.forget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : CategoryTheory.Functor (Action V G) V

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

instance Action.instFaithfulActionInstCategoryActionForget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : CategoryTheory.Faithful (Action.forget V G)

instance Action.instConcreteCategoryActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.ConcreteCategory V] : CategoryTheory.ConcreteCategory (Action V G)

instance Action.hasForgetToV (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.ConcreteCategory V] : CategoryTheory.HasForget₂ (Action V G) V

def Action.functorCategoryEquivalenceCompEvaluation (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) : CategoryTheory.Functor.comp (Action.functorCategoryEquivalence V G).functor ((CategoryTheory.evaluation (CategoryTheory.SingleObj ↑G) V).obj PUnit.unit) ≅ Action.forget V G

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

noncomputable instance Action.instPreservesLimitsForget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.Limits.HasLimits V] : CategoryTheory.Limits.PreservesLimits (Action.forget V G)

noncomputable instance Action.instPreservesColimitsForget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.Limits.HasColimits V] : CategoryTheory.Limits.PreservesColimits (Action.forget V G)

theorem Action.Iso.conj_ρ {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {M : Action V G} {N : Action V G} (f : M ≅ N) (g : ↑G) : ↑N.ρ g = ↑(CategoryTheory.Iso.conj ((Action.forget V G).mapIso f)) (↑M.ρ g)

instance Action.instZeroHomActionToQuiverToCategoryStructInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] {X : Action V G} {Y : Action V G} : Zero (X ⟶ Y)

@[simp]

theorem Action.zero_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] {X : Action V G} {Y : Action V G} : 0.hom = 0

instance Action.instHasZeroMorphismsActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Limits.HasZeroMorphisms (Action V G)

instance Action.forget_preservesZeroMorphisms {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor.PreservesZeroMorphisms (Action.forget V G)

instance Action.forget₂_preservesZeroMorphisms {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.ConcreteCategory V] : CategoryTheory.Functor.PreservesZeroMorphisms (CategoryTheory.forget₂ (Action V G) V)

instance Action.functorCategoryEquivalence_preservesZeroMorphisms {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor.PreservesZeroMorphisms (Action.functorCategoryEquivalence V G).functor

instance Action.instPreadditiveActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] : CategoryTheory.Preadditive (Action V G)

instance Action.forget_additive {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] : CategoryTheory.Functor.Additive (Action.forget V G)

instance Action.forget₂_additive {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] [CategoryTheory.ConcreteCategory V] : CategoryTheory.Functor.Additive (CategoryTheory.forget₂ (Action V G) V)

instance Action.functorCategoryEquivalence_additive {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] : CategoryTheory.Functor.Additive (Action.functorCategoryEquivalence V G).functor

@[simp]

theorem Action.neg_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} (f : X ⟶ Y) : (-f).hom = -f.hom

@[simp]

theorem Action.add_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {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)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {X : Action V G} {Y : Action V G} {ι : Type u_1} (f : ι → (X ⟶ Y)) (s : Finset ι) : (Finset.sum s f).hom = Finset.sum s fun i => (f i).hom

instance Action.instLinearActionInstCategoryActionInstPreadditiveActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] : CategoryTheory.Linear R (Action V G)

instance Action.forget_linear {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] : CategoryTheory.Functor.Linear R (Action.forget V G)

instance Action.forget₂_linear {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] [CategoryTheory.ConcreteCategory V] : CategoryTheory.Functor.Linear R (CategoryTheory.forget₂ (Action V G) V)

instance Action.functorCategoryEquivalence_linear {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] : CategoryTheory.Functor.Linear R (Action.functorCategoryEquivalence V G).functor

@[simp]

theorem Action.smul_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Preadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] {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)} [CategoryTheory.LargeCategory V] {G : MonCat} : Action V G ≌ CategoryTheory.Functor (ULift.{u, 0} (CategoryTheory.SingleObj ↑G)) V

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

noncomputable instance Action.instAbelianActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.Abelian V] : CategoryTheory.Abelian (Action V G)

instance Action.instMonoidalCategoryActionInstCategoryAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] : CategoryTheory.MonoidalCategory (Action V G)

@[simp]

theorem Action.tensorUnit_v {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] : (CategoryTheory.MonoidalCategory.tensorUnit (Action V G)).V = CategoryTheory.MonoidalCategory.tensorUnit V

theorem Action.tensorUnit_rho {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {g : ↑G} : ↑(CategoryTheory.MonoidalCategory.tensorUnit (Action V G)).ρ g = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit V)

@[simp]

theorem Action.tensor_v {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {X : Action V G} {Y : Action V G} : (CategoryTheory.MonoidalCategory.tensorObj X Y).V = CategoryTheory.MonoidalCategory.tensorObj X.V Y.V

theorem Action.tensor_rho {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {X : Action V G} {Y : Action V G} {g : ↑G} : ↑(CategoryTheory.MonoidalCategory.tensorObj X Y).ρ g = CategoryTheory.MonoidalCategory.tensorHom (↑X.ρ g) (↑Y.ρ g)

@[simp]

theorem Action.tensorHom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {W : Action V G} {X : Action V G} {Y : Action V G} {Z : Action V G} (f : W ⟶ X) (g : Y ⟶ Z) : (CategoryTheory.MonoidalCategory.tensorHom f g).hom = CategoryTheory.MonoidalCategory.tensorHom f.hom g.hom

theorem Action.associator_hom_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {X : Action V G} {Y : Action V G} {Z : Action V G} : (CategoryTheory.MonoidalCategory.associator X Y Z).hom.hom = (CategoryTheory.MonoidalCategory.associator X.V Y.V Z.V).hom

theorem Action.associator_inv_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {X : Action V G} {Y : Action V G} {Z : Action V G} : (CategoryTheory.MonoidalCategory.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategory.associator X.V Y.V Z.V).inv

theorem Action.leftUnitor_hom_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {X : Action V G} : (CategoryTheory.MonoidalCategory.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategory.leftUnitor X.V).hom

theorem Action.leftUnitor_inv_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {X : Action V G} : (CategoryTheory.MonoidalCategory.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategory.leftUnitor X.V).inv

theorem Action.rightUnitor_hom_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {X : Action V G} : (CategoryTheory.MonoidalCategory.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategory.rightUnitor X.V).hom

theorem Action.rightUnitor_inv_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {X : Action V G} : (CategoryTheory.MonoidalCategory.rightUnitor X).inv.hom = (CategoryTheory.MonoidalCategory.rightUnitor X.V).inv

def Action.tensorUnitIso {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {X : V} (f : CategoryTheory.MonoidalCategory.tensorUnit V ≅ X) : CategoryTheory.MonoidalCategory.tensorUnit (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.

@[simp]

theorem Action.forgetMonoidal_toLaxMonoidalFunctor_ε (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : (Action.forgetMonoidal V G).toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit V)

@[simp]

theorem Action.forgetMonoidal_toLaxMonoidalFunctor_toFunctor (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : (Action.forgetMonoidal V G).toLaxMonoidalFunctor.toFunctor = Action.forget V G

@[simp]

theorem Action.forgetMonoidal_toLaxMonoidalFunctor_μ (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] (X : Action V G) (Y : Action V G) : CategoryTheory.LaxMonoidalFunctor.μ (Action.forgetMonoidal V G).toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk (Action.forget V G).toPrefunctor).obj X) ((CategoryTheory.Functor.mk (Action.forget V G).toPrefunctor).obj Y))

def Action.forgetMonoidal (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : CategoryTheory.MonoidalFunctor (Action V G) V

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

instance Action.forgetMonoidal_faithful (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : CategoryTheory.Faithful (Action.forgetMonoidal V G).toLaxMonoidalFunctor.toFunctor

instance Action.instBraidedCategoryActionInstCategoryActionInstMonoidalCategoryActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] : CategoryTheory.BraidedCategory (Action V G)

@[simp]

theorem Action.forgetBraided_μ (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (X : Action V G) (Y : Action V G) : CategoryTheory.LaxMonoidalFunctor.μ (Action.forgetBraided V G).toMonoidalFunctor.toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.V Y.V)

@[simp]

theorem Action.forgetBraided_ε (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] : (Action.forgetBraided V G).toMonoidalFunctor.toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit V)

@[simp]

theorem Action.forgetBraided_map (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] : ∀ {X Y : Action V G} (f : X ⟶ Y), (Action.forgetBraided V G).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = f.hom

@[simp]

theorem Action.forgetBraided_obj (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (M : Action V G) : (Action.forgetBraided V G).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj M = M.V

def Action.forgetBraided (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] : CategoryTheory.BraidedFunctor (Action V G) V

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

instance Action.forgetBraided_faithful (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] : CategoryTheory.Faithful (Action.forgetBraided V G).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor

instance Action.instSymmetricCategoryActionInstCategoryActionInstMonoidalCategoryActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] : CategoryTheory.SymmetricCategory (Action V G)

instance Action.instMonoidalPreadditiveActionInstCategoryActionInstPreadditiveActionInstCategoryActionInstMonoidalCategoryActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.Preadditive V] [CategoryTheory.MonoidalPreadditive V] : CategoryTheory.MonoidalPreadditive (Action V G)

instance Action.instMonoidalLinearActionInstCategoryActionInstPreadditiveActionInstCategoryActionInstLinearActionInstCategoryActionInstPreadditiveActionInstCategoryActionInstMonoidalCategoryActionInstCategoryActionInstMonoidalPreadditiveActionInstCategoryActionInstPreadditiveActionInstCategoryActionInstMonoidalCategoryActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.Preadditive V] [CategoryTheory.MonoidalPreadditive V] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] [CategoryTheory.MonoidalLinear R V] : CategoryTheory.MonoidalLinear R (Action V G)

def Action.functorCategoryMonoidalEquivalence (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : CategoryTheory.MonoidalFunctor (Action V G) (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V)

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

instance Action.instIsEquivalenceActionInstCategoryActionFunctorSingleObjαMonoidCategoryInstMonoidαCategoryToFunctorInstMonoidalCategoryActionInstCategoryActionFunctorCategoryMonoidalToLaxMonoidalFunctorFunctorCategoryMonoidalEquivalence (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : CategoryTheory.IsEquivalence (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor

@[simp]

theorem Action.functorCategoryMonoidalEquivalence.μ_app (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] (A : Action V G) (B : Action V G) : (CategoryTheory.LaxMonoidalFunctor.μ (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor A B).app PUnit.unit = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj ((Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj A) ((Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj B)).obj PUnit.unit)

@[simp]

theorem Action.functorCategoryMonoidalEquivalence.μIso_inv_app (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] (A : Action V G) (B : Action V G) : (CategoryTheory.MonoidalFunctor.μIso (Action.functorCategoryMonoidalEquivalence V G) A B).inv.app PUnit.unit = CategoryTheory.CategoryStruct.id (((Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj (CategoryTheory.MonoidalCategory.tensorObj A B)).obj PUnit.unit)

@[simp]

theorem Action.functorCategoryMonoidalEquivalence.ε_app (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.ε.app PUnit.unit = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V)).obj PUnit.unit)

@[simp]

theorem Action.functorCategoryMonoidalEquivalence.inv_counit_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] (A : Action V G) : ((CategoryTheory.Functor.adjunction (CategoryTheory.Functor.inv (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor)).counit.app A).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (CategoryTheory.Functor.inv (CategoryTheory.Functor.inv (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor)) (CategoryTheory.Functor.inv (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor)).obj A).V

@[simp]

theorem Action.functorCategoryMonoidalEquivalence.counit_app (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] (A : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) : ((CategoryTheory.Functor.adjunction (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor).counit.app A).app PUnit.unit = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.comp (CategoryTheory.Functor.inv (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor) (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor).obj A).obj PUnit.unit)

@[simp]

theorem Action.functorCategoryMonoidalEquivalence.inv_unit_app_app (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] (A : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V) : ((CategoryTheory.Functor.adjunction (CategoryTheory.Functor.inv (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor)).unit.app A).app PUnit.unit = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V)).obj A).obj PUnit.unit)

@[simp]

theorem Action.functorCategoryMonoidalEquivalence.unit_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] (A : Action V G) : ((CategoryTheory.Functor.adjunction (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor).unit.app A).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (Action V G)).obj A).V

@[simp]

theorem Action.functorCategoryMonoidalEquivalence.functor_map (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] {A : Action V G} {B : Action V G} (f : A ⟶ B) : (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.map f = Action.FunctorCategoryEquivalence.functor.map f

@[simp]

theorem Action.functorCategoryMonoidalEquivalence.inverse_map (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] {A : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V} {B : CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V} (f : A ⟶ B) : (CategoryTheory.Functor.inv (Action.functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor).map f = Action.FunctorCategoryEquivalence.inverse.map f

instance Action.instRightRigidCategoryFunctorSingleObjαMonoidObjGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryMonCatInstMonCatLargeCategoryToPrefunctorForget₂ConcreteCategoryConcreteCategoryHasForgetToMonCatCategoryInstMonoidαCategoryFunctorCategoryMonoidal (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] (H : GroupCat) [CategoryTheory.RightRigidCategory V] : CategoryTheory.RightRigidCategory (CategoryTheory.Functor (CategoryTheory.SingleObj ↑((CategoryTheory.forget₂ GroupCat MonCat).obj H)) V)

instance Action.instRightRigidCategoryActionObjGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryMonCatInstMonCatLargeCategoryToPrefunctorForget₂ConcreteCategoryConcreteCategoryHasForgetToMonCatInstCategoryActionInstMonoidalCategoryActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] (H : GroupCat) [CategoryTheory.RightRigidCategory V] : CategoryTheory.RightRigidCategory (Action V ((CategoryTheory.forget₂ GroupCat MonCat).obj H))

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

instance Action.instLeftRigidCategoryFunctorSingleObjαMonoidObjGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryMonCatInstMonCatLargeCategoryToPrefunctorForget₂ConcreteCategoryConcreteCategoryHasForgetToMonCatCategoryInstMonoidαCategoryFunctorCategoryMonoidal (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] (H : GroupCat) [CategoryTheory.LeftRigidCategory V] : CategoryTheory.LeftRigidCategory (CategoryTheory.Functor (CategoryTheory.SingleObj ↑((CategoryTheory.forget₂ GroupCat MonCat).obj H)) V)

instance Action.instLeftRigidCategoryActionObjGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryMonCatInstMonCatLargeCategoryToPrefunctorForget₂ConcreteCategoryConcreteCategoryHasForgetToMonCatInstCategoryActionInstMonoidalCategoryActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] (H : GroupCat) [CategoryTheory.LeftRigidCategory V] : CategoryTheory.LeftRigidCategory (Action V ((CategoryTheory.forget₂ GroupCat MonCat).obj H))

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

instance Action.instRigidCategoryFunctorSingleObjαMonoidObjGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryMonCatInstMonCatLargeCategoryToPrefunctorForget₂ConcreteCategoryConcreteCategoryHasForgetToMonCatCategoryInstMonoidαCategoryFunctorCategoryMonoidal (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] (H : GroupCat) [CategoryTheory.RigidCategory V] : CategoryTheory.RigidCategory (CategoryTheory.Functor (CategoryTheory.SingleObj ↑((CategoryTheory.forget₂ GroupCat MonCat).obj H)) V)

instance Action.instRigidCategoryActionObjGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryMonCatInstMonCatLargeCategoryToPrefunctorForget₂ConcreteCategoryConcreteCategoryHasForgetToMonCatInstCategoryActionInstMonoidalCategoryActionInstCategoryAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] (H : GroupCat) [CategoryTheory.RigidCategory V] : CategoryTheory.RigidCategory (Action V ((CategoryTheory.forget₂ GroupCat MonCat).obj H))

If V is rigid, so is Action V G.

@[simp]

theorem Action.rightDual_v {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] {H : GroupCat} (X : Action V ((CategoryTheory.forget₂ GroupCat MonCat).obj H)) [CategoryTheory.RightRigidCategory V] : Xᘁ.V = X.Vᘁ

@[simp]

theorem Action.leftDual_v {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] {H : GroupCat} (X : Action V ((CategoryTheory.forget₂ GroupCat MonCat).obj H)) [CategoryTheory.LeftRigidCategory V] : (ᘁX).V = ᘁX.V

@[simp]

theorem Action.rightDual_ρ {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] {H : GroupCat} (X : Action V ((CategoryTheory.forget₂ GroupCat MonCat).obj H)) [CategoryTheory.RightRigidCategory V] (h : ↑H) : ↑Xᘁ.ρ h = ↑X.ρ h⁻¹ᘁ

@[simp]

theorem Action.leftDual_ρ {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] {H : GroupCat} (X : Action V ((CategoryTheory.forget₂ GroupCat MonCat).obj H)) [CategoryTheory.LeftRigidCategory V] (h : ↑H) : ↑(ᘁX).ρ h = ᘁ↑X.ρ h⁻¹

def Action.actionPunitEquivalence {V : Type (u + 1)} [CategoryTheory.LargeCategory V] : Action V (MonCat.of PUnit.{u + 1} ) ≌ V

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

@[simp]

theorem Action.res_obj_ρ (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G ⟶ H) (M : Action V H) : ((Action.res V f).obj M).ρ = CategoryTheory.CategoryStruct.comp f M.ρ

@[simp]

theorem Action.res_obj_V (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G ⟶ H) (M : Action V H) : ((Action.res V f).obj M).V = M.V

@[simp]

theorem Action.res_map_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G ⟶ H) : ∀ {X Y : Action V H} (p : X ⟶ Y), ((Action.res V f).map p).hom = p.hom

def Action.res (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G ⟶ H) : CategoryTheory.Functor (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.)

@[simp]

theorem Action.resId_hom_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} (X : Action V G) : ((Action.resId V).hom.app X).hom = CategoryTheory.CategoryStruct.id X.V

@[simp]

theorem Action.resId_inv_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} (X : Action V G) : ((Action.resId V).inv.app X).hom = CategoryTheory.CategoryStruct.id X.V

def Action.resId (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} : Action.res V (CategoryTheory.CategoryStruct.id G) ≅ CategoryTheory.Functor.id (Action V G)

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

@[simp]

theorem Action.resComp_hom_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} {K : MonCat} (f : G ⟶ H) (g : H ⟶ K) (X : Action V K) : ((Action.resComp V f g).hom.app X).hom = CategoryTheory.CategoryStruct.id X.V

@[simp]

theorem Action.resComp_inv_app_hom (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} {K : MonCat} (f : G ⟶ H) (g : H ⟶ K) (X : Action V K) : ((Action.resComp V f g).inv.app X).hom = CategoryTheory.CategoryStruct.id X.V

def Action.resComp (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} {K : MonCat} (f : G ⟶ H) (g : H ⟶ K) : CategoryTheory.Functor.comp (Action.res V g) (Action.res V f) ≅ Action.res V (CategoryTheory.CategoryStruct.comp f g)

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

instance Action.res_additive (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G ⟶ H) [CategoryTheory.Preadditive V] : CategoryTheory.Functor.Additive (Action.res V f)

instance Action.res_linear (V : Type (u + 1)) [CategoryTheory.LargeCategory V] {G : MonCat} {H : MonCat} (f : G ⟶ H) {R : Type u_1} [Semiring R] [CategoryTheory.Preadditive V] [CategoryTheory.Linear R V] : CategoryTheory.Functor.Linear R (Action.res V f)

def Action.ofMulAction (G : Type u) (H : Type u) [Monoid G] [MulAction G H] : Action (Type u) (MonCat.of G)

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

@[simp]

theorem Action.ofMulAction_apply {G : Type u} {H : Type u} [Monoid G] [MulAction G H] (g : G) (x : H) : ↑(Action.ofMulAction G H).ρ g x = g • x

def Action.ofMulActionLimitCone {ι : Type v} (G : Type (max v u)) [Monoid G] (F : ι → Type (max v u)) [(i : ι) → MulAction G (F i)] : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor fun i => Action.ofMulAction 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.

@[simp]

theorem Action.leftRegular_V (G : Type u) [Monoid G] : (Action.leftRegular G).V = G

@[simp]

theorem Action.leftRegular_ρ_apply (G : Type u) [Monoid G] : ∀ (x : ↑(MonCat.of G)) (x_1 : G), ↑(Action.leftRegular G).ρ x x_1 = x • x_1

def Action.leftRegular (G : Type u) [Monoid G] : Action (Type u) (MonCat.of G)

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

@[simp]

theorem Action.diagonal_V (G : Type u) [Monoid G] (n : ℕ) : (Action.diagonal G n).V = (Fin n → G)

@[simp]

theorem Action.diagonal_ρ_apply (G : Type u) [Monoid G] (n : ℕ) : ∀ (x : ↑(MonCat.of G)) (x_1 : Fin n → G) (a : Fin n), ↑(Action.diagonal G n).ρ x x_1 a = (↑(MonCat.of G) • (Fin n → G)) (Fin n → G) instHSMul x x_1 a

def Action.diagonal (G : Type u) [Monoid G] (n : ℕ) : Action (Type u) (MonCat.of G)

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

def Action.diagonalOneIsoLeftRegular (G : Type u) [Monoid G] : Action.diagonal G 1 ≅ Action.leftRegular G

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

@[simp]

theorem Action.leftRegularTensorIso_inv_hom (G : Type u) [Group G] (X : Action (Type u) (MonCat.of G)) (g : (CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) { V := X.V, ρ := 1 }).V) : Action.Hom.hom (Action.leftRegularTensorIso G X).inv g = (g.fst, ↑X.ρ g.fst g.snd)

@[simp]

theorem Action.leftRegularTensorIso_hom_hom (G : Type u) [Group G] (X : Action (Type u) (MonCat.of G)) (g : (CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) X).V) : Action.Hom.hom (Action.leftRegularTensorIso G X).hom g = (g.fst, ↑X.ρ g.fst⁻¹ g.snd)

noncomputable def Action.leftRegularTensorIso (G : Type u) [Group G] (X : Action (Type u) (MonCat.of G)) : CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) X ≅ CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) { V := X.V, ρ := 1 }

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

@[simp]

theorem Action.diagonalSucc_inv_hom (G : Type u) [Monoid G] (n : ℕ) : ∀ (a : (CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) (Action.diagonal G n)).V), Action.Hom.hom (Type u) CategoryTheory.types (MonCat.of G) (CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) (Action.diagonal G n)) (Action.diagonal G (n + 1)) (Action.diagonalSucc G n).inv a = ↑(Equiv.piFinSuccAboveEquiv (fun a => G) 0).symm a

@[simp]

theorem Action.diagonalSucc_hom_hom (G : Type u) [Monoid G] (n : ℕ) : ∀ (a : (Action.diagonal G (n + 1)).V), Action.Hom.hom (Action.diagonalSucc G n).hom a = ↑(Equiv.piFinSuccAboveEquiv (fun a => G) 0) a

noncomputable def Action.diagonalSucc (G : Type u) [Monoid G] (n : ℕ) : Action.diagonal G (n + 1) ≅ CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) (Action.diagonal G n)

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

@[simp]

theorem CategoryTheory.Functor.mapAction_obj_V {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) (M : Action V G) : ((CategoryTheory.Functor.mapAction F G).obj M).V = F.obj M.V

@[simp]

theorem CategoryTheory.Functor.mapAction_map_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) : ∀ {X Y : Action V G} (f : X ⟶ Y), ((CategoryTheory.Functor.mapAction F G).map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.mapAction_obj_ρ_apply {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) (M : Action V G) (g : ↑G) : ↑((CategoryTheory.Functor.mapAction F G).obj M).ρ g = F.map (↑M.ρ g)

def CategoryTheory.Functor.mapAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) : CategoryTheory.Functor (Action V G) (Action W G)

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

instance CategoryTheory.Functor.mapAction_preadditive {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) [CategoryTheory.Preadditive V] [CategoryTheory.Preadditive W] [CategoryTheory.Functor.Additive F] : CategoryTheory.Functor.Additive (CategoryTheory.Functor.mapAction F G)

instance CategoryTheory.Functor.mapAction_linear {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] (F : CategoryTheory.Functor V W) (G : MonCat) [CategoryTheory.Preadditive V] [CategoryTheory.Preadditive W] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R V] [CategoryTheory.Linear R W] [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Linear R F] : CategoryTheory.Functor.Linear R (CategoryTheory.Functor.mapAction F G)

@[simp]

theorem CategoryTheory.MonoidalFunctor.mapAction_toLaxMonoidalFunctor_ε_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.MonoidalFunctor V W) (G : MonCat) : (CategoryTheory.MonoidalFunctor.mapAction F G).toLaxMonoidalFunctor.ε.hom = F.ε

@[simp]

theorem CategoryTheory.MonoidalFunctor.mapAction_toLaxMonoidalFunctor_toFunctor {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.MonoidalFunctor V W) (G : MonCat) : (CategoryTheory.MonoidalFunctor.mapAction F G).toLaxMonoidalFunctor.toFunctor = CategoryTheory.Functor.mapAction F.toFunctor G

@[simp]

theorem CategoryTheory.MonoidalFunctor.mapAction_toLaxMonoidalFunctor_μ_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.MonoidalFunctor V W) (G : MonCat) (X : Action V G) (Y : Action V G) : (CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.MonoidalFunctor.mapAction F G).toLaxMonoidalFunctor X Y).hom = CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V

def CategoryTheory.MonoidalFunctor.mapAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.MonoidalFunctor V W) (G : MonCat) : CategoryTheory.MonoidalFunctor (Action V G) (Action W G)

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

@[simp]

theorem CategoryTheory.MonoidalFunctor.mapAction_ε_inv_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.MonoidalFunctor V W) (G : MonCat) : (CategoryTheory.inv (CategoryTheory.MonoidalFunctor.mapAction F G).toLaxMonoidalFunctor.ε).hom = CategoryTheory.inv F.ε

@[simp]

theorem CategoryTheory.MonoidalFunctor.mapAction_μ_inv_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.MonoidalFunctor V W) (G : MonCat) (X : Action V G) (Y : Action V G) : (CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.MonoidalFunctor.mapAction F G).toLaxMonoidalFunctor X Y)).hom = CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)