Induced monoidal structure on Action V G

We show:

• When V is monoidal, braided, or symmetric, so is Action V G.

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

Equations

• Action.instMonoidalCategory = CategoryTheory.Monoidal.transport (Action.functorCategoryEquivalence V G).symm

@[simp]

theorem Action.instMonoidalCategory_whiskerRight_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {X₁✝ X₂✝ : Action V G} (f : X₁✝ ⟶ X₂✝) (X : Action V G) : (CategoryTheory.MonoidalCategory.whiskerRight f X).hom = CategoryTheory.MonoidalCategory.whiskerRight f.hom X.V

@[simp]

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

@[simp]

theorem Action.instMonoidalCategory_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

@[simp]

theorem Action.instMonoidalCategory_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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Action.instMonoidalCategory_whiskerLeft_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] (X x✝ x✝¹ : Action V G) (f : x✝ ⟶ x✝¹) : (CategoryTheory.MonoidalCategory.whiskerLeft X f).hom = CategoryTheory.MonoidalCategory.whiskerLeft X.V f.hom

@[simp]

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

@[simp]

theorem Action.instMonoidalCategory_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

@[simp]

theorem Action.instMonoidalCategory_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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

• Action.tensorUnitIso f = Action.mkIso f ⋯

instance Action.instMonoidalForget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : (Action.forget V G).Monoidal

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Action.forget_ε (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : CategoryTheory.Functor.LaxMonoidal.ε (Action.forget V G) = CategoryTheory.CategoryStruct.id (𝟙_ V)

@[simp]

theorem Action.forget_η (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : CategoryTheory.Functor.LaxMonoidal.ε (Action.forget V G) = CategoryTheory.CategoryStruct.id (𝟙_ V)

@[simp]

theorem Action.forget_μ {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] (X Y : Action V G) : CategoryTheory.Functor.LaxMonoidal.μ (Action.forget V G) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((Action.forget V G).obj X) ((Action.forget V G).obj Y))

@[simp]

theorem Action.forget_δ {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] (X Y : Action V G) : CategoryTheory.Functor.OplaxMonoidal.δ (Action.forget V G) X Y = CategoryTheory.CategoryStruct.id ((Action.forget V G).obj (CategoryTheory.MonoidalCategory.tensorObj X Y))

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Action.instBraidedForget V G = CategoryTheory.Functor.Braided.mk ⋯

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

Equations

• Action.instSymmetricCategory V G = CategoryTheory.symmetricCategoryOfFaithful (Action.forget V G)

instance Action.instMonoidalPreadditive (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.instMonoidalLinear (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)

instance Action.instMonoidalFunctorSingleObjαMonoidFunctor (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : Action.FunctorCategoryEquivalence.functor.Monoidal

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

Equations

• Action.instMonoidalFunctorSingleObjαMonoidFunctor V G = inferInstanceAs (CategoryTheory.Monoidal.equivalenceTransported (Action.functorCategoryEquivalence V G).symm).inverse.Monoidal

instance Action.instMonoidalFunctorSingleObjαMonoidFunctorFunctorCategoryEquivalence (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : (Action.functorCategoryEquivalence V G).functor.Monoidal

Equations

• Action.instMonoidalFunctorSingleObjαMonoidFunctorFunctorCategoryEquivalence V G = id inferInstance

instance Action.instMonoidalFunctorSingleObjαMonoidInverse (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : Action.FunctorCategoryEquivalence.inverse.Monoidal

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

Equations

• Action.instMonoidalFunctorSingleObjαMonoidInverse V G = inferInstanceAs (CategoryTheory.Monoidal.equivalenceTransported (Action.functorCategoryEquivalence V G).symm).functor.Monoidal

instance Action.instMonoidalFunctorSingleObjαMonoidInverseFunctorCategoryEquivalence (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : (Action.functorCategoryEquivalence V G).inverse.Monoidal

Equations

• Action.instMonoidalFunctorSingleObjαMonoidInverseFunctorCategoryEquivalence V G = id inferInstance

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_ε (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : CategoryTheory.Functor.LaxMonoidal.ε Action.FunctorCategoryEquivalence.functor = CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V))

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_η (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : CategoryTheory.Functor.OplaxMonoidal.η Action.FunctorCategoryEquivalence.functor = CategoryTheory.CategoryStruct.id (Action.FunctorCategoryEquivalence.functor.obj (𝟙_ (Action V G)))

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_μ (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] (A B : Action V G) : CategoryTheory.Functor.LaxMonoidal.μ Action.FunctorCategoryEquivalence.functor A B = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj (Action.FunctorCategoryEquivalence.functor.obj A) (Action.FunctorCategoryEquivalence.functor.obj B))

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_δ (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] (A B : Action V G) : CategoryTheory.Functor.OplaxMonoidal.δ Action.FunctorCategoryEquivalence.functor A B = CategoryTheory.CategoryStruct.id (Action.FunctorCategoryEquivalence.functor.obj (CategoryTheory.MonoidalCategory.tensorObj A B))

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

Equations

• Action.instRightRigidCategoryFunctorSingleObjαMonoidObjGrpMonCatForget₂ V H = id inferInstance

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Action.instLeftRigidCategoryFunctorSingleObjαMonoidObjGrpMonCatForget₂ V H = id inferInstance

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Action.instRigidCategoryFunctorSingleObjαMonoidObjGrpMonCatForget₂ V H = id inferInstance

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

If V is rigid, so is Action V G.

Equations

• Action.instRigidCategoryObjGrpMonCatForget₂ V H = CategoryTheory.rigidCategoryOfEquivalence (Action.functorCategoryEquivalence V ((CategoryTheory.forget₂ Grp MonCat).obj H)).toAdjunction

@[simp]

theorem Action.rightDual_v {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.MonoidalCategory V] {H : Grp} (X : Action V ((CategoryTheory.forget₂ Grp 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 : Grp} (X : Action V ((CategoryTheory.forget₂ Grp 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 : Grp} (X : Action V ((CategoryTheory.forget₂ Grp 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 : Grp} (X : Action V ((CategoryTheory.forget₂ Grp MonCat).obj H)) [CategoryTheory.LeftRigidCategory V] (h : ↑H) : (ᘁX).ρ h = ᘁX.ρ h⁻¹

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

• One or more equations did not get rendered due to their size.

@[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.leftRegularTensorIso G X).inv.hom g = (g.1, X.ρ g.1 g.2)

@[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.leftRegularTensorIso G X).hom.hom g = (g.1, X.ρ g.1⁻¹ g.2)

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.

Equations

• Action.diagonalSucc G n = Action.mkIso (Fin.consEquiv fun (a : Fin (n + 1)) => G).symm.toIso ⋯

@[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.diagonalSucc G n).inv.hom a✝ = (Fin.consEquiv fun (a : Fin (n + 1)) => G) a✝

@[simp]

theorem Action.diagonalSucc_hom_hom (G : Type u) [Monoid G] (n : ℕ) (a✝ : (Action.diagonal G (n + 1)).V) : (Action.diagonalSucc G n).hom.hom a✝ = (Fin.consEquiv fun (a : Fin (n + 1)) => G).symm a✝

instance CategoryTheory.Functor.instLaxMonoidalActionMapAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] : (F.mapAction G).LaxMonoidal

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

instance CategoryTheory.Functor.instOplaxMonoidalActionMapAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.OplaxMonoidal] : (F.mapAction G).OplaxMonoidal

An oplax monoidal functor induces an oplax monoidal functor between the categories of G-actions within those categories.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.mapAction_η_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.OplaxMonoidal] : (CategoryTheory.Functor.OplaxMonoidal.η (F.mapAction G)).hom = CategoryTheory.Functor.OplaxMonoidal.η F

@[simp]

theorem CategoryTheory.Functor.mapAction_δ_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.OplaxMonoidal] (X Y : Action V G) : (CategoryTheory.Functor.OplaxMonoidal.δ (F.mapAction G) X Y).hom = CategoryTheory.Functor.OplaxMonoidal.δ F X.V Y.V

instance CategoryTheory.Functor.instMonoidalActionMapAction {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.Monoidal] : (F.mapAction G).Monoidal

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

Equations

• F.instMonoidalActionMapAction = CategoryTheory.Functor.Monoidal.mk ⋯ ⋯ ⋯ ⋯