Documentation

LeanPool.RegtsSevenster.RS.Novel.Envelope.TensorPowHom

The tensor power of an endomorphism #

An endomorphism g of X induces an endomorphism of the tensor power X ^ ⊗ n, one copy of g acting on each factor (powHom). It commutes with the symmetric-group action of SymPerm.lean: every factor carries the same endomorphism, so permuting the factors and applying g to each may be done in either order (permMor_comp_powHom).

The tensor power of an endomorphism #

source
noncomputable def RS.powHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) (g : CategoryTheory.End X) (n : ℕ) :
CategoryTheory.End (tensorPow A X n)

The tensor power of an endomorphism: powHom X g n acts by g on each of the n factors of X ^ ⊗ n.

Equations
Instances For
    source
    @[simp]
    theorem RS.powHom_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) (g : CategoryTheory.End X) :
    powHom X g 0 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)

    On the empty tensor power the endomorphism power is the identity of the unit.

    source
    @[simp]
    theorem RS.powHom_succ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) (g : CategoryTheory.End X) (n : ℕ) :
    powHom X g (n + 1) = CategoryTheory.MonoidalCategoryStruct.tensorHom (powHom X g n) g

    The recursion equation: the endomorphism power on one more factor tensors on one more copy of g.

    Commutation with whiskering #

    source
    theorem RS.whiskerRight_comp_powHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) (g : CategoryTheory.End X) (n : ℕ) (f : tensorPow A X n ⟶ tensorPow A X n) (h : CategoryTheory.CategoryStruct.comp f (powHom X g n) = CategoryTheory.CategoryStruct.comp (powHom X g n) f) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) (powHom X g (n + 1)) = CategoryTheory.CategoryStruct.comp (powHom X g (n + 1)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)

    Adding a factor preserves commutation with the endomorphism power.

    Equivariance #

    source
    theorem RS.swapTop_comp_powHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] (X : A) (g : CategoryTheory.End X) (n : ℕ) :
    CategoryTheory.CategoryStruct.comp (swapTop X n) (powHom X g (n + 2)) = CategoryTheory.CategoryStruct.comp (powHom X g (n + 2)) (swapTop X n)

    The top braiding commutes with the endomorphism power: the two braided factors carry the same endomorphism.

    source
    theorem RS.insertTop_comp_powHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] (X : A) (g : CategoryTheory.End X) (n k : ℕ) :
    CategoryTheory.CategoryStruct.comp (insertTop X n k) (powHom X g (n + 1)) = CategoryTheory.CategoryStruct.comp (powHom X g (n + 1)) (insertTop X n k)

    Bubbling the top factor down commutes with the endomorphism power, one braiding step at a time.

    source
    theorem RS.permMor_comp_powHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] (X : A) (g : CategoryTheory.End X) (n : ℕ) (σ : Equiv.Perm (Fin n)) :
    CategoryTheory.CategoryStruct.comp (permMor X n σ) (powHom X g n) = CategoryTheory.CategoryStruct.comp (powHom X g n) (permMor X n σ)

    Equivariance of the endomorphism power: the symmetric-group action commutes with g ^ ⊗ n. Every factor carries the same endomorphism, so permuting the factors and applying g to each may be done in either order.