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_rightUnitor_hom_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] (X : Action V G) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor 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.MonoidalCategoryStruct.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategoryStruct.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.MonoidalCategoryStruct.tensorObj X Y).V = CategoryTheory.MonoidalCategoryStruct.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_leftUnitor_inv_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] (X : Action V G) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.V).inv

@[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.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom

@[simp]

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

@[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.MonoidalCategoryStruct.associator X Y Z).hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator X.V Y.V Z.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.MonoidalCategoryStruct.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.V).hom

@[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.MonoidalCategoryStruct.whiskerLeft X f).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.V f.hom

@[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.MonoidalCategoryStruct.whiskerRight f X).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom X.V

@[simp]

theorem Action.tensorUnit_ρ' {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} [CategoryTheory.MonoidalCategory V] {g : ↑G} : (MonCat.Hom.hom (𝟙_ (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} : (CategoryTheory.ConcreteCategory.hom (𝟙_ (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} : (MonCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ) g = CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.ConcreteCategory.hom X.ρ) g) ((CategoryTheory.ConcreteCategory.hom 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.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ) g = CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.ConcreteCategory.hom X.ρ) g) ((CategoryTheory.ConcreteCategory.hom 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] : (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.ε (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.ε (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.μ (forget V G) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj ((forget V G).obj X) ((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.δ (forget V G) X Y = CategoryTheory.CategoryStruct.id ((forget V G).obj (CategoryTheory.MonoidalCategoryStruct.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] : (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.instMonoidalFunctorSingleObjCarrierFunctor (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : FunctorCategoryEquivalence.functor.Monoidal

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

Equations

• Action.instMonoidalFunctorSingleObjCarrierFunctor V G = inferInstanceAs (CategoryTheory.Monoidal.equivalenceTransported (Action.functorCategoryEquivalence V G).symm).inverse.Monoidal

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

Equations

• Action.instMonoidalFunctorSingleObjCarrierFunctorFunctorCategoryEquivalence V G = id inferInstance

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

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

Equations

• Action.instMonoidalFunctorSingleObjCarrierInverse V G = inferInstanceAs (CategoryTheory.Monoidal.equivalenceTransported (Action.functorCategoryEquivalence V G).symm).functor.Monoidal

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

Equations

• Action.instMonoidalFunctorSingleObjCarrierInverseFunctorCategoryEquivalence V G = id inferInstance

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_ε (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : CategoryTheory.Functor.LaxMonoidal.ε 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.η functor = CategoryTheory.CategoryStruct.id (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.μ functor A B = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (functor.obj A) (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.δ functor A B = CategoryTheory.CategoryStruct.id (functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B))

instance Action.instRightRigidCategoryFunctorSingleObjCarrierObjGrpMonCatForget₂ (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.instRightRigidCategoryFunctorSingleObjCarrierObjGrpMonCatForget₂ 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.instLeftRigidCategoryFunctorSingleObjCarrierObjGrpMonCatForget₂ (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.instLeftRigidCategoryFunctorSingleObjCarrierObjGrpMonCatForget₂ 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.instRigidCategoryFunctorSingleObjCarrierObjGrpMonCatForget₂ (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.instRigidCategoryFunctorSingleObjCarrierObjGrpMonCatForget₂ 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

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) : (CategoryTheory.ConcreteCategory.hom Xᘁ.ρ) h = (CategoryTheory.ConcreteCategory.hom X.ρ) h⁻¹ᘁ

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) : (CategoryTheory.ConcreteCategory.hom (ᘁX).ρ) h = ᘁ(CategoryTheory.ConcreteCategory.hom X.ρ) h⁻¹

noncomputable def Action.leftRegularTensorIso (G : Type u) [Group G] (X : Action (Type u) (MonCat.of G)) : CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular G) X ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (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_hom_hom (G : Type u) [Group G] (X : Action (Type u) (MonCat.of G)) (g : (CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular G) X).V) : (leftRegularTensorIso G X).hom.hom g = (g.1, (CategoryTheory.ConcreteCategory.hom X.ρ) g.1⁻¹ g.2)

@[simp]

theorem Action.leftRegularTensorIso_inv_hom (G : Type u) [Group G] (X : Action (Type u) (MonCat.of G)) (g : (CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular G) { V := X.V, ρ := 1 }).V) : (leftRegularTensorIso G X).inv.hom g = (g.1, (CategoryTheory.ConcreteCategory.hom X.ρ) g.1 g.2)

noncomputable def Action.diagonalSucc (G : Type u) [Monoid G] (n : ℕ) : diagonal G (n + 1) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular G) (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.MonoidalCategoryStruct.tensorObj (leftRegular G) (diagonal G n)).V) : (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✝ : (diagonal G (n + 1)).V) : (diagonalSucc G n).hom.hom a✝ = (Fin.consEquiv fun (a : Fin (n + 1)) => G).symm a✝

instance CategoryTheory.Functor.instLaxMonoidalActionMapAction {V : Type (u + 1)} [LargeCategory V] {G : MonCat} {W : Type (u + 1)} [LargeCategory W] [MonoidalCategory V] [MonoidalCategory W] (F : 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)} [LargeCategory V] {G : MonCat} {W : Type (u + 1)} [LargeCategory W] [MonoidalCategory V] [MonoidalCategory W] (F : Functor V W) [F.LaxMonoidal] : (LaxMonoidal.ε (F.mapAction G)).hom = LaxMonoidal.ε F

@[simp]

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

instance CategoryTheory.Functor.instOplaxMonoidalActionMapAction {V : Type (u + 1)} [LargeCategory V] {G : MonCat} {W : Type (u + 1)} [LargeCategory W] [MonoidalCategory V] [MonoidalCategory W] (F : 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)} [LargeCategory V] {G : MonCat} {W : Type (u + 1)} [LargeCategory W] [MonoidalCategory V] [MonoidalCategory W] (F : Functor V W) [F.OplaxMonoidal] : (OplaxMonoidal.η (F.mapAction G)).hom = OplaxMonoidal.η F

@[simp]

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

instance CategoryTheory.Functor.instMonoidalActionMapAction {V : Type (u + 1)} [LargeCategory V] {G : MonCat} {W : Type (u + 1)} [LargeCategory W] [MonoidalCategory V] [MonoidalCategory W] (F : 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 ⋯ ⋯ ⋯ ⋯