The Deligne hypotheses for the envelope

Two of the five hypothesis fields of the abstract Deligne input, read off for the envelope: finite-dimensional Hom-spaces, by the injection chain through the three layers, and scalar unit endomorphisms, the arity-zero Hom space being the line of the empty class, which the normalization f ∅ = 1 keeps nonzero.

The other three are elsewhere: semisimplicity in EnvSemisimple.lean, the tensor generator in EnvGenerator.lean, and moderate growth in EnvGrowth.lean; EnvDelignePackage.lean feeds all five to the cited statement.

Finite-dimensional Hom-spaces

instance RS.envHomFinite {R : ℕ} (f : EdgeRankParameter R) (P Q : Env f) : FiniteDimensional ℂ (P ⟶ Q)

Envelope hom-spaces are finite-dimensional, by the injection chain through the three layers.

theorem RS.env_finDimHom {R : ℕ} (f : EdgeRankParameter R) : HasFinDimHom (Env f)

The envelope has finite-dimensional Hom-spaces.

Scalar unit endomorphisms

noncomputable def RS.unitExtract {R : ℕ} (f : EdgeRankParameter R) (x : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Env f))) : HomSpace f.val 0

The extraction of the arity-zero class from a unit endomorphism.

Equations

• RS.unitExtract f x = (x.f PUnit.unit PUnit.unit).f

theorem RS.unitExtract_injective {R : ℕ} (f : EdgeRankParameter R) : Function.Injective (unitExtract f)

The unit's endomorphisms inject into the arity-zero hom space.

theorem RS.unitExtract_id {R : ℕ} (f : EdgeRankParameter R) : unitExtract f (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Env f))) = HomSpace.ofFragment f.val (strandBundle 0)

It sends the identity to the empty class, which the normalization keeps nonzero — so the unit endomorphisms are the scalars.

theorem RS.unit_id_eq_emptyClass {R : ℕ} (f : EdgeRankParameter R) : HomSpace.ofFragment f.val (strandBundle 0) = emptyClass f.val

The identity of the unit is the empty class.

theorem RS.env_endOne {R : ℕ} (f : EdgeRankParameter R) : HasScalarUnit (Env f)

Scalar unit endomorphisms.