The Deligne package for the skein category

The payoff of the envelope construction: the envelope satisfies all hypotheses of the abstract Deligne statement, so it receives a fibre functor; restricting along the braided linear embedding of the skein category yields the Deligne package that the extraction consumes — with Deligne's theorem itself as the only transcendental input, applied to the concretely constructed envelope.

noncomputable def RS.skeinToEnv {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.Functor (SkeinObj f) (Env f)

The braided linear embedding of the skein category into its envelope.

Equations

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

@[instance_reducible]

noncomputable instance RS.skeinToEnvBraided {R : ℕ} (f : EdgeRankParameter R) : (skeinToEnv f).Braided

The embedding of the skein category into its envelope is braided.

Equations

• RS.skeinToEnvBraided f = id inferInstance

instance RS.skeinToEnvAdditive {R : ℕ} (f : EdgeRankParameter R) : (skeinToEnv f).Additive

It is additive.

instance RS.skeinToEnvLinear {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.Functor.Linear ℂ (skeinToEnv f)

And ℂ-linear — so restricting the envelope's fibre functor along it gives a package on the skein category.

theorem RS.env_deligneGenerated {R : ℕ} (f : EdgeRankParameter R) : TensorGeneratedBy (Env f) (envStrand f 1)

The strand tensor-generates in Deligne's sense. The envelope generates more strongly than the theorem asks — every object is a retract of a finite biproduct of pure tensor powers of the strand, where a subquotient of a biproduct of mixed powers would do.

theorem RS.env_delignePackage {R : ℕ} (f : EdgeRankParameter R) (hD : DeligneTheoremStatement) : Nonempty (DelignePackage (Env f))

The Deligne package for the envelope: Deligne's theorem applies to the envelope. Its growth hypothesis is stated by composition length, which the envelope's bound on endomorphism dimensions supplies through semisimplicity and finite-dimensional Hom-spaces — properties of the envelope, not hypotheses of the theorem; and its conclusion carries exactness and faithfulness, which the package drops.

theorem RS.skein_delignePackage {R : ℕ} (f : EdgeRankParameter R) (hD : DeligneTheoremStatement) : Nonempty (DelignePackage (SkeinObj f))

The Deligne package for the skein category: restrict the envelope's fibre functor along the embedding.