Tensor powers of actions on underlying objects

For a monoidal category V, a monoid H, and X : Action V H, the underlying object (tensorPow X n).V of the n-th tensor power in Action V H agrees definitionally with tensorPow X.V n at each concrete n, but not uniformly in a variable n : ℕ because tensorPow recurses in Action V H on the left and in V on the right.

Action.tensorPowVIso X n : (tensorPow X n).V ≅ tensorPow X.V n constructs the canonical comparison isomorphism by recursion on n using whiskerLeftIso, avoiding eqToHom casts. It intertwines the action of g : H on tensorPow X n with tensorPowMap (X.ρ g).asHom n, commutes with tensorPowSuccIso, and, when V is braided, intertwines the cyclic shift tensorPowShiftIso X n with tensorPowShiftIso X.V n.

Main declarations

• Action.tensorPowVIso: the recursive comparison (tensorPow X n).V ≅ tensorPow X.V n, with Action.tensorPowVIso_zero, Action.tensorPowVIso_succ, Action.tensorPowVIso_succ_hom, and Action.tensorPowVIso_succ_inv;
• Action.ρ_comp_tensorPowVIso_hom: tensorPowVIso intertwines (tensorPow X n).ρ g with tensorPowMap (X.ρ g).asHom n;
• Action.tensorPowSuccIso_hom_comp_tensorPowVIso_hom and Action.tensorPowShiftIso_hom_comp_tensorPowVIso_hom: compatibility of tensorPowVIso with tensorPowSuccIso and tensorPowShiftIso.

def Action.tensorPowVIso {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] (X : Action V H) (n : ℕ) : (TauCeti.tensorPow X n).V ≅ TauCeti.tensorPow X.V n

Recursive comparison isomorphism (tensorPow X n).V ≅ tensorPow X.V n on underlying objects, built by whiskering without object casts.

@[simp]

theorem Action.tensorPowVIso_zero {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] (X : Action V H) : X.tensorPowVIso 0 = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)

At n = 0, tensorPowVIso is the identity of 𝟙_ V.

theorem Action.tensorPowVIso_succ {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] (X : Action V H) (n : ℕ) : X.tensorPowVIso (n + 1) = CategoryTheory.MonoidalCategory.whiskerLeftIso X.V (X.tensorPowVIso n)

Recursive step of tensorPowVIso.

@[simp]

theorem Action.tensorPowVIso_succ_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] (X : Action V H) (n : ℕ) : (X.tensorPowVIso (n + 1)).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.V (X.tensorPowVIso n).hom

Forward morphism of tensorPowVIso at n + 1.

@[simp]

theorem Action.tensorPowVIso_succ_inv {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] (X : Action V H) (n : ℕ) : (X.tensorPowVIso (n + 1)).inv = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.V (X.tensorPowVIso n).inv

Inverse morphism of tensorPowVIso at n + 1.

theorem Action.ρ_comp_tensorPowVIso_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] (X : Action V H) (g : H) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((TauCeti.tensorPow X n).ρ g).asHom (X.tensorPowVIso n).hom = CategoryTheory.CategoryStruct.comp (X.tensorPowVIso n).hom (TauCeti.tensorPowMap (X.ρ g).asHom n)

tensorPowVIso intertwines the action of g on tensorPow X n with tensorPowMap of the action of g on X.

theorem Action.ρ_comp_tensorPowVIso_hom_assoc {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] (X : Action V H) (g : H) (n : ℕ) {Z : V} (h : TauCeti.tensorPow X.V n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((TauCeti.tensorPow X n).ρ g).asHom (CategoryTheory.CategoryStruct.comp (X.tensorPowVIso n).hom h) = CategoryTheory.CategoryStruct.comp (X.tensorPowVIso n).hom (CategoryTheory.CategoryStruct.comp (TauCeti.tensorPowMap (X.ρ g).asHom n) h)

tensorPowVIso intertwines the action of g on tensorPow X n with tensorPowMap of the action of g on X.

theorem Action.tensorPowSuccIso_hom_comp_tensorPowVIso_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] (X : Action V H) (n : ℕ) : CategoryTheory.CategoryStruct.comp (TauCeti.tensorPowSuccIso X n).hom.hom (X.tensorPowVIso (n + 1)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.tensorPowVIso n).hom X.V) (TauCeti.tensorPowSuccIso X.V n).hom

tensorPowVIso commutes with appending a tensor factor on the right via tensorPowSuccIso.

theorem Action.tensorPowSuccIso_hom_comp_tensorPowVIso_hom_assoc {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] (X : Action V H) (n : ℕ) {Z : V} (h : TauCeti.tensorPow X.V (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (TauCeti.tensorPowSuccIso X n).hom.hom (CategoryTheory.CategoryStruct.comp (X.tensorPowVIso (n + 1)).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.tensorPowVIso n).hom X.V) (CategoryTheory.CategoryStruct.comp (TauCeti.tensorPowSuccIso X.V n).hom h)

tensorPowVIso commutes with appending a tensor factor on the right via tensorPowSuccIso.

theorem Action.tensorPowShiftIso_hom_comp_tensorPowVIso_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] [CategoryTheory.BraidedCategory V] (X : Action V H) (n : ℕ) : CategoryTheory.CategoryStruct.comp (TauCeti.tensorPowShiftIso X n).hom.hom (X.tensorPowVIso (n + 1)).hom = CategoryTheory.CategoryStruct.comp (X.tensorPowVIso (n + 1)).hom (TauCeti.tensorPowShiftIso X.V n).hom

In a braided monoidal category, tensorPowVIso intertwines the cyclic shift on tensorPow X with the cyclic shift on tensorPow X.V.

theorem Action.tensorPowShiftIso_hom_comp_tensorPowVIso_hom_assoc {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.MonoidalCategory V] {H : Type u_2} [Monoid H] [CategoryTheory.BraidedCategory V] (X : Action V H) (n : ℕ) {Z : V} (h : TauCeti.tensorPow X.V (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (TauCeti.tensorPowShiftIso X n).hom.hom (CategoryTheory.CategoryStruct.comp (X.tensorPowVIso (n + 1)).hom h) = CategoryTheory.CategoryStruct.comp (X.tensorPowVIso (n + 1)).hom (CategoryTheory.CategoryStruct.comp (TauCeti.tensorPowShiftIso X.V n).hom h)

In a braided monoidal category, tensorPowVIso intertwines the cyclic shift on tensorPow X with the cyclic shift on tensorPow X.V.