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.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] : CategoryTheory.MonoidalCategory (Action V G)

Equations

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

@[simp]

theorem Action.leftUnitor_hom_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] (X : Action V G) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.V).hom

@[simp]

theorem Action.whiskerLeft_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [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.leftUnitor_inv_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] (X : Action V G) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.V).inv

@[simp]

theorem Action.whiskerRight_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [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.tensorObj_V {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] (X Y : Action V G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V = CategoryTheory.MonoidalCategoryStruct.tensorObj X.V Y.V

@[simp]

theorem Action.associator_hom_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [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.tensorHom_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [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.associator_inv_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [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.rightUnitor_inv_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] (X : Action V G) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.V).inv

@[simp]

theorem Action.rightUnitor_hom_hom {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] (X : Action V G) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.V).hom

@[simp]

theorem Action.tensorUnit_V {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)).V = CategoryTheory.MonoidalCategoryStruct.tensorUnit V

@[simp]

theorem Action.tensorUnit_ρ {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] {g : G} : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)).ρ g = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)

@[simp]

theorem Action.tensor_ρ {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] {X Y : Action V G} {g : G} : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ g = CategoryTheory.MonoidalCategoryStruct.tensorHom (X.ρ g) (Y.ρ g)

def Action.tensorUnitIso {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.MonoidalCategory V] {X : V} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ≅ X) : CategoryTheory.MonoidalCategoryStruct.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.

Equations

• Action.tensorUnitIso f = Action.mkIso f ⋯

instance Action.instMonoidalForget (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [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.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] : CategoryTheory.Functor.LaxMonoidal.ε (forget V G) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)

@[simp]

theorem Action.forget_η (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] : CategoryTheory.Functor.LaxMonoidal.ε (forget V G) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)

@[simp]

theorem Action.forget_μ {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [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.Category.{u_3, u_1} V] {G : Type u_2} [Monoid G] [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.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] : CategoryTheory.BraidedCategory (Action V G)

Equations

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

@[simp]

theorem Action.β_hom_hom (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {X Y : Action V G} : (β_ X Y).hom.hom = (β_ X.V Y.V).hom

@[simp]

theorem Action.β_inv_hom (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {X Y : Action V G} : (β_ X Y).inv.hom = (β_ X.V Y.V).inv

instance Action.instBraidedForget (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [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 = { toMonoidal := Action.instMonoidalForget V G, braided := ⋯ }

instance Action.instSymmetricCategory (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [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.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] [CategoryTheory.Preadditive V] [CategoryTheory.MonoidalPreadditive V] : CategoryTheory.MonoidalPreadditive (Action V G)

instance Action.instMonoidalLinear (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] [CategoryTheory.Preadditive V] [CategoryTheory.MonoidalPreadditive V] {R : Type u_3} [Semiring R] [CategoryTheory.Linear R V] [CategoryTheory.MonoidalLinear R V] : CategoryTheory.MonoidalLinear R (Action V G)

instance Action.instMonoidalFunctorSingleObjFunctor (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] : FunctorCategoryEquivalence.functor.Monoidal

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

Equations

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

instance Action.instMonoidalFunctorSingleObjFunctorFunctorCategoryEquivalence (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] : (functorCategoryEquivalence V G).functor.Monoidal

Equations

• Action.instMonoidalFunctorSingleObjFunctorFunctorCategoryEquivalence V G = id inferInstance

instance Action.instMonoidalFunctorSingleObjInverse (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] : FunctorCategoryEquivalence.inverse.Monoidal

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

Equations

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

instance Action.instMonoidalFunctorSingleObjInverseFunctorCategoryEquivalence (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] : (functorCategoryEquivalence V G).inverse.Monoidal

Equations

• Action.instMonoidalFunctorSingleObjInverseFunctorCategoryEquivalence V G = id inferInstance

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_ε (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] : CategoryTheory.Functor.LaxMonoidal.ε functor = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor (CategoryTheory.SingleObj G) V))

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_η (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] : CategoryTheory.Functor.OplaxMonoidal.η functor = CategoryTheory.CategoryStruct.id (functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)))

@[simp]

theorem Action.FunctorCategoryEquivalence.functor_μ (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [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.Category.{u_3, u_1} V] (G : Type u_2) [Monoid G] [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.instRightRigidCategoryFunctorSingleObj (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.MonoidalCategory V] (H : Type u_3) [Group H] [CategoryTheory.RightRigidCategory V] : CategoryTheory.RightRigidCategory (CategoryTheory.Functor (CategoryTheory.SingleObj H) V)

Equations

• Action.instRightRigidCategoryFunctorSingleObj V H = inferInstance

instance Action.instRightRigidCategory (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.MonoidalCategory V] (H : Type u_3) [Group H] [CategoryTheory.RightRigidCategory V] : CategoryTheory.RightRigidCategory (Action V H)

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

Equations

• Action.instRightRigidCategory V H = CategoryTheory.rightRigidCategoryOfEquivalence (Action.functorCategoryEquivalence V H).toAdjunction

instance Action.instLeftRigidCategoryFunctorSingleObj (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.MonoidalCategory V] (H : Type u_3) [Group H] [CategoryTheory.LeftRigidCategory V] : CategoryTheory.LeftRigidCategory (CategoryTheory.Functor (CategoryTheory.SingleObj H) V)

Equations

• Action.instLeftRigidCategoryFunctorSingleObj V H = inferInstance

instance Action.instLeftRigidCategory (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.MonoidalCategory V] (H : Type u_3) [Group H] [CategoryTheory.LeftRigidCategory V] : CategoryTheory.LeftRigidCategory (Action V H)

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

Equations

• Action.instLeftRigidCategory V H = CategoryTheory.leftRigidCategoryOfEquivalence (Action.functorCategoryEquivalence V H).toAdjunction

instance Action.instRigidCategoryFunctorSingleObj (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.MonoidalCategory V] (H : Type u_3) [Group H] [CategoryTheory.RigidCategory V] : CategoryTheory.RigidCategory (CategoryTheory.Functor (CategoryTheory.SingleObj H) V)

Equations

• Action.instRigidCategoryFunctorSingleObj V H = inferInstance

instance Action.instRigidCategory (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.MonoidalCategory V] (H : Type u_3) [Group H] [CategoryTheory.RigidCategory V] : CategoryTheory.RigidCategory (Action V H)

If V is rigid, so is Action V G.

Equations

• Action.instRigidCategory V H = CategoryTheory.rigidCategoryOfEquivalence (Action.functorCategoryEquivalence V H).toAdjunction

@[simp]

theorem Action.rightDual_v {V : Type u_1} [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_3} [Group H] (X : Action V H) [CategoryTheory.RightRigidCategory V] : Xᘁ.V = X.Vᘁ

@[simp]

theorem Action.leftDual_v {V : Type u_1} [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_3} [Group H] (X : Action V H) [CategoryTheory.LeftRigidCategory V] : (ᘁX).V = ᘁX.V

theorem Action.rightDual_ρ {V : Type u_1} [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_3} [Group H] (X : Action V H) [CategoryTheory.RightRigidCategory V] (h : H) : Xᘁ.ρ h = X.ρ h⁻¹ᘁ

theorem Action.leftDual_ρ {V : Type u_1} [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_3} [Group H] (X : Action V H) [CategoryTheory.LeftRigidCategory V] (h : H) : (ᘁX).ρ h = ᘁX.ρ h⁻¹

noncomputable def Action.diagonalSuccIsoTensorDiagonal (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.diagonalSuccIsoTensorDiagonal G n = Action.mkIso (Fin.consEquiv fun (a : Fin (n + 1)) => G).symm.toIso ⋯

@[simp]

theorem Action.diagonalSuccIsoTensorDiagonal_inv_hom (G : Type u) [Monoid G] (n : ℕ) (a✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular G) (diagonal G n)).V) : (diagonalSuccIsoTensorDiagonal G n).inv.hom a✝ = (Fin.consEquiv fun (a : Fin (n + 1)) => G) a✝

@[simp]

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

@[deprecated Action.diagonalSuccIsoTensorDiagonal (since := "2025-06-02")]

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

Alias of Action.diagonalSuccIsoTensorDiagonal.

---

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

Equations

• Action.diagonalSucc = Action.diagonalSuccIsoTensorDiagonal

noncomputable def Action.leftRegularTensorIso (G : Type u) [Group G] (X : Action (Type u) G) : CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular G) X ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular G) (trivial G X.V)

Given X : Action (Type u) 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) G) (a✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular G) (trivial G X.V)).V) : (leftRegularTensorIso G X).inv.hom a✝ = (a✝.1, X.ρ a✝.1 a✝.2)

@[simp]

theorem Action.leftRegularTensorIso_hom_hom (G : Type u) [Group G] (X : Action (Type u) G) (a✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular G) X).V) : (leftRegularTensorIso G X).hom.hom a✝ = (a✝.1, X.ρ a✝.1⁻¹ a✝.2)

noncomputable def Action.diagonalSuccIsoTensorTrivial (G : Type u) [Group G] (n : ℕ) : diagonal G (n + 1) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular G) (trivial G (Fin n → G))

An isomorphism of G-sets Gⁿ⁺¹ ≅ G × Gⁿ, where G acts by left multiplication on Gⁿ⁺¹ and G but trivially on Gⁿ. The map sends (g₀, ..., gₙ) ↦ (g₀, (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ)), and the inverse is (g₀, (g₁, ..., gₙ)) ↦ (g₀, g₀g₁, g₀g₁g₂, ..., g₀g₁...gₙ).

Equations

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

@[simp]

theorem Action.diagonalSuccIsoTensorTrivial_hom_hom_apply {G : Type u} [Group G] {n : ℕ} (f : Fin (n + 1) → G) : (diagonalSuccIsoTensorTrivial G n).hom.hom f = (f 0, fun (i : Fin n) => (f i.castSucc)⁻¹ * f i.succ)

@[simp]

theorem Action.diagonalSuccIsoTensorTrivial_inv_hom_apply {G : Type u} [Group G] {n : ℕ} (g : G) (f : Fin n → G) : (diagonalSuccIsoTensorTrivial G n).inv.hom (g, f) = g • Fin.partialProd f

instance CategoryTheory.Functor.instLaxMonoidalActionMapAction {V : Type u_1} [Category.{u_4, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [Category.{u_5, u_3} 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} [Category.{u_4, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [Category.{u_5, u_3} 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} [Category.{u_4, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [Category.{u_5, u_3} 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} [Category.{u_4, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [Category.{u_5, u_3} 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} [Category.{u_4, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [Category.{u_5, u_3} 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} [Category.{u_4, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [Category.{u_5, u_3} 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} [Category.{u_4, u_1} V] {G : Type u_2} [Monoid G] {W : Type u_3} [Category.{u_5, u_3} 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 = { toLaxMonoidal := F.instLaxMonoidalActionMapAction, toOplaxMonoidal := F.instOplaxMonoidalActionMapAction, ε_η := ⋯, η_ε := ⋯, μ_δ := ⋯, δ_μ := ⋯ }