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

theorem Action.tensorUnit_rho {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 {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.tensor_hom {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

@[simp]

theorem Action.whiskerLeft_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} (f : Y ⟶ Z) : (CategoryTheory.MonoidalCategory.whiskerLeft X f).hom = CategoryTheory.MonoidalCategory.whiskerLeft X.V f.hom

@[simp]

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

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 : 𝟙_ 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 ⋯

@[simp]

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

@[simp]

theorem Action.forgetMonoidal_toLaxMonoidalFunctor_toFunctor (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : (Action.forgetMonoidal V G).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) : (Action.forgetMonoidal V G).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((Action.forget V G).obj X) ((Action.forget V G).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.

Equations

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

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

Equations

• ⋯ = ⋯

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.

@[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).obj M = M.V

@[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) : (Action.forgetBraided V G).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.V Y.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).map f = f.hom

@[simp]

theorem Action.forgetBraided_ε (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] : (Action.forgetBraided V G).ε = CategoryTheory.CategoryStruct.id (𝟙_ 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.

Equations

• Action.forgetBraided V G = let __src := Action.forgetMonoidal V G; { toMonoidalFunctor := __src, braided := ⋯ }

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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.

Equations

• Action.functorCategoryMonoidalEquivalence V G = CategoryTheory.Monoidal.fromTransported (Action.functorCategoryEquivalence V G).symm

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

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

Equations

• Action.functorCategoryMonoidalEquivalenceInverse V G = CategoryTheory.Monoidal.toTransported (Action.functorCategoryEquivalence V G).symm

def Action.functorCategoryMonoidalAdjunction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : (Action.functorCategoryMonoidalEquivalence V G).toFunctor ⊣ (Action.functorCategoryMonoidalEquivalenceInverse V G).toFunctor

The adjunction (which is an equivalence) between the categories Action V G and (SingleObj G ⥤ V).

Equations

• Action.functorCategoryMonoidalAdjunction V G = (Action.functorCategoryEquivalence V G).toAdjunction

instance Action.instIsEquivalenceFunctorSingleObjαMonoidFunctorCategoryMonoidalEquivalence (V : Type (u + 1)) [CategoryTheory.LargeCategory V] (G : MonCat) [CategoryTheory.MonoidalCategory V] : (Action.functorCategoryMonoidalEquivalence V G).IsEquivalence

Equations

• ⋯ = ⋯

@[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) : ((Action.functorCategoryMonoidalEquivalence V G).μ A B).app PUnit.unit = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj ((Action.functorCategoryMonoidalEquivalence V G).obj A) ((Action.functorCategoryMonoidalEquivalence V G).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) : ((Action.functorCategoryMonoidalEquivalence V G).μIso A B).inv.app PUnit.unit = CategoryTheory.CategoryStruct.id (((Action.functorCategoryMonoidalEquivalence V G).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).ε.app PUnit.unit = CategoryTheory.CategoryStruct.id ((𝟙_ (CategoryTheory.Functor (CategoryTheory.SingleObj ↑G) V)).obj PUnit.unit)

@[simp]

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

@[simp]

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

@[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).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) : (Action.functorCategoryMonoidalEquivalenceInverse V G).map f = Action.FunctorCategoryEquivalence.inverse.map f

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 = let_fun this := inferInstance; this

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

• Action.instRightRigidCategoryObjGrpMonCatForget₂ V H = CategoryTheory.rightRigidCategoryOfEquivalence (Action.functorCategoryMonoidalAdjunction V ((CategoryTheory.forget₂ Grp MonCat).obj H))

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 = let_fun this := inferInstance; this

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

• Action.instLeftRigidCategoryObjGrpMonCatForget₂ V H = CategoryTheory.leftRigidCategoryOfEquivalence (Action.functorCategoryMonoidalAdjunction V ((CategoryTheory.forget₂ Grp MonCat).obj H))

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 = let_fun this := inferInstance; this

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.functorCategoryMonoidalAdjunction V ((CategoryTheory.forget₂ Grp MonCat).obj H))

@[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⁻¹

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

Equations

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

@[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 = (Equiv.piFinSuccAbove (fun (a : Fin (n + 1)) => G) 0) a

@[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 = (Equiv.piFinSuccAbove (fun (a : Fin (n + 1)) => G) 0).symm 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.

Equations

• Action.diagonalSucc G n = Action.mkIso (Equiv.piFinSuccAbove (fun (a : Fin (n + 1)) => G) 0).toIso ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.MonoidalFunctor.mapActionLax_toFunctor_obj_V {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.LaxMonoidalFunctor V W) (G : MonCat) : ∀ (a : Action V G), ((CategoryTheory.MonoidalFunctor.mapActionLax F G).obj a).V = F.obj a.V

@[simp]

theorem CategoryTheory.MonoidalFunctor.mapActionLax_toFunctor_map_hom {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.LaxMonoidalFunctor V W) (G : MonCat) : ∀ {X Y : Action V G} (a : X ⟶ Y), ((CategoryTheory.MonoidalFunctor.mapActionLax F G).map a).hom = F.map a.hom

@[simp]

theorem CategoryTheory.MonoidalFunctor.mapActionLax_toFunctor_obj_ρ_apply {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {W : Type (u + 1)} [CategoryTheory.LargeCategory W] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.LaxMonoidalFunctor V W) (G : MonCat) : ∀ (a : Action V G) (g : ↑G), ((CategoryTheory.MonoidalFunctor.mapActionLax F G).obj a).ρ g = F.map (a.ρ g)

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

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.MonoidalFunctor.mapAction_toLaxMonoidalFunctor_toFunctor_obj_ρ_apply {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) : ∀ (a : Action V G) (g : ↑G), ((F.mapAction G).obj a).ρ g = F.map (a.ρ 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) : (F.mapAction G).ε.hom = F.ε

@[simp]

theorem CategoryTheory.MonoidalFunctor.mapAction_toLaxMonoidalFunctor_toFunctor_map_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 Y : Action V G} (a : X ⟶ Y), ((F.mapAction G).map a).hom = F.map a.hom

@[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) : ((F.mapAction G).μ X Y).hom = F.μ X.V Y.V

@[simp]

theorem CategoryTheory.MonoidalFunctor.mapAction_toLaxMonoidalFunctor_toFunctor_obj_V {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) : ∀ (a : Action V G), ((F.mapAction G).obj a).V = F.obj a.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.

Equations

• F.mapAction G = let __src := CategoryTheory.MonoidalFunctor.mapActionLax F.toLaxMonoidalFunctor G; { toLaxMonoidalFunctor := __src, ε_isIso := ⋯, μ_isIso := ⋯ }

@[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 (F.mapAction G).ε).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 ((F.mapAction G).μ X Y)).hom = CategoryTheory.inv (F.μ X.V Y.V)