Moderate growth of the envelope

The Deligne moderate-growth hypothesis: the endomorphism algebras of tensor powers grow at most exponentially. The dimension of an envelope Hom-space is bounded by the underlying matrix Hom-space, which is a finite product of skein Hom-spaces of dimension at most (R+1)^(2m); tensor powers multiply index cardinalities and add arities, so the total bound is exponential in the power.

The envelope Hom bound

theorem RS.env_hom_finrank_le {R : ℕ} (f : EdgeRankParameter R) (P Q : Env f) : Module.finrank ℂ (P ⟶ Q) ≤ Module.finrank ℂ (P.X ⟶ Q.X)

Envelope Hom-spaces are no larger than the underlying matrix Hom-spaces.

The matrix Hom bound

noncomputable def RS.matHomEntries {R : ℕ} (f : EdgeRankParameter R) (M N : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) : (M ⟶ N) →ₗ[ℂ] (p : M.ι × N.ι) → HomSpace f.val ((M.X p.1).X.arity + (N.X p.2).X.arity)

The entrywise reading of a matrix morphism into skein Hom-spaces.

Equations

• RS.matHomEntries f M N = { toFun := fun (φ : M ⟶ N) (p : M.ι × N.ι) => (φ p.1 p.2).f, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.matHomEntries_injective {R : ℕ} (f : EdgeRankParameter R) (M N : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) : Function.Injective ⇑(matHomEntries f M N)

A matrix of morphisms is determined by its entries, so the hom-space dimension is bounded by their total.

theorem RS.mat_hom_finrank_le {R : ℕ} (f : EdgeRankParameter R) (M N : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) (m : ℕ) (hM : ∀ (i : M.ι), (M.X i).X.arity ≤ m) (hN : ∀ (j : N.ι), (N.X j).X.arity ≤ m) : Module.finrank ℂ (M ⟶ N) ≤ Fintype.card M.ι * Fintype.card N.ι * (R + 1) ^ (2 * m)

The dimension of a matrix Hom-space, bounded by index counts and a uniform arity bound.

Tensor powers of matrix objects

theorem RS.env_pow_X {R : ℕ} (f : EdgeRankParameter R) (Y : Env f) (N : ℕ) : (tensorPow (Env f) Y N).X = tensorPow (CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) Y.X N

The underlying matrix object of an envelope tensor power.

theorem RS.mat_pow_card {R : ℕ} (f : EdgeRankParameter R) (A : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) (N : ℕ) : Fintype.card (tensorPow (CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) A N).ι = Fintype.card A.ι ^ N

The index cardinality of a matrix tensor power.

theorem RS.mat_pow_arity {R : ℕ} (f : EdgeRankParameter R) (A : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) (m : ℕ) (hA : ∀ (i : A.ι), (A.X i).X.arity ≤ m) (N : ℕ) (p : (tensorPow (CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) A N).ι) : ((tensorPow (CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) A N).X p).X.arity ≤ N * m

The arity bound of a matrix tensor power.

The moderate-growth field

theorem RS.env_deligneModerateGrowth {R : ℕ} (f : EdgeRankParameter R) : ModerateEndGrowth (Env f)

Moderate growth of the envelope: endomorphism algebras of tensor powers grow at most exponentially.