Moderate growth of tensor powers

The two ways of asking that the tensor powers of every object grow at most exponentially: by the dimension of their endomorphism algebras (ModerateEndGrowth, here), and by their composition length (ModerateLengthGrowth, defined in RS/Definitions.lean). In a semisimple category with finite-dimensional Hom-spaces the first implies the second, because length is bounded by the endomorphism dimension.

Length is the measure Deligne's theorem states its growth hypothesis in; the endomorphism dimension is the measure the envelope's rank bound supplies directly.

def RS.ModerateEndGrowth (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] : Prop

Every object has moderate tensor-power growth, measured by endomorphism dimensions.

Equations

• RS.ModerateEndGrowth A = ∀ (Y : A), ∃ (C : ℕ) (c : ℕ), ∀ (N : ℕ), Module.finrank ℂ (RS.tensorPow A Y N ⟶ RS.tensorPow A Y N) ≤ C * c ^ N

theorem RS.moderateLengthGrowth_of_endGrowth (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.Limits.HasFiniteBiproducts A] (hab : CategoryTheory.Abelian A) (hss : IsSemisimple A) (hfd : HasFinDimHom A) (hgrow : ModerateEndGrowth A) : ModerateLengthGrowth A

Endomorphism growth bounds length growth in a semisimple category with finite-dimensional Hom-spaces: the length of an object is at most the dimension of its endomorphism algebra, so an exponential bound on the latter is one on the former.