Documentation

Mathlib.RepresentationTheory.Action.Monoidal

Induced monoidal structure on Action V G #

We show:

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

    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.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.

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

      Equations
      Instances For

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

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

          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.
          Instances For
            @[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

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

            Equations
            Instances For

              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.
              Instances For

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

                Equations
                Instances For