Tensor powers of an object

The iterated tensor power X ^ ⊗ n, its mixed form and the condition that a single object tensor-generates are defined in RS/Definitions.lean. This module carries the defining recursion equations, the stronger retract form of generation the envelope satisfies, and the implication from it to Deligne's subquotient form.

theorem RS.tensorPow_zero (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) : tensorPow A X 0 = CategoryTheory.MonoidalCategoryStruct.tensorUnit A

The empty tensor power is the unit.

theorem RS.tensorPow_succ (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) (n : ℕ) : tensorPow A X (n + 1) = CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow A X n) X

X ^ ⊗ (n + 1) is X ^ ⊗ n ⊗ X. Together with tensorPow_zero this is the defining recursion.

def RS.RetractGeneratedBy (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasFiniteBiproducts A] (X : A) : Prop

Generation by retracts of pure powers: every object is a retract of a finite biproduct of tensor powers of X alone. This is how the envelope generates, and it is stronger than Deligne's hypothesis in two ways at once — a retract rather than a subquotient, and no duals among the powers.

Equations

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

def RS.tensorPowIsoMixed (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] (X : A) (n : ℕ) : tensorPow A X n ≅ mixedPow A X n 0

A pure tensor power is the mixed power with no dual factors.

Equations

• RS.tensorPowIsoMixed A X n = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (RS.tensorPow A X n)).symm

theorem RS.tensorGeneratedBy_of_retract (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasFiniteBiproducts A] [CategoryTheory.RigidCategory A] {X : A} (h : RetractGeneratedBy A X) : TensorGeneratedBy A X

The retract formulation implies Deligne's. A splitting ι ≫ π = 𝟙 makes ι a split mono, hence a mono, and Y is a quotient of itself, so a retract of a biproduct of pure powers is a subquotient of the corresponding biproduct of mixed powers.