The skein endomorphism tower

Instantiation of the abstract PermTower at the skein category of an EdgeRankParameter R: the family skeinEnd f n of endomorphism algebras carries the symmetric-group representations given by permutation fragments, the exponential dimension bound inherited from the Hom-space rank bound, and vanishing propagation along the standard embeddings (compatibility with symCast).

Main definitions

• skeinEnd f n — the endomorphism algebra of the n-strand object
• permToEnd f n — the monoid hom Perm (Fin n) →* skeinEnd f n
• skeinRep f n — the representation SymGroupAlgebra n →ₐ[ℂ] skeinEnd f n
• skeinPermTower f — the PermTower instance

Implementation notes

skeinEnd is defined as CategoryTheory.End (SkeinObj.mk n), which is definitionally HomSpace f.val (n + n). This lives in Type 1 (since Fragment contains Type-valued fields); the universe polymorphism of PermTower accommodates this.

The monoid-hom direction uses End.mul_def : x * y = y ≫ x, so the map σ ↦ [permFragment σ] is a genuine MonoidHom from Perm (Fin n) to End (SkeinObj.mk n) by permFragmentCompose.

The endomorphism algebra

noncomputable def RS.skeinEnd {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : Type 1

The endomorphism ℂ-algebra of the n-strand object of the skein category. Definitionally HomSpace f.val (n + n).

Equations

• RS.skeinEnd f n = CategoryTheory.End { arity := n }

@[instance_reducible]

noncomputable instance RS.skeinEndRing {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : Ring (skeinEnd f n)

Each level of the tower is a ring.

Equations

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

@[instance_reducible]

noncomputable instance RS.skeinEndAlgebra {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : Algebra ℂ (skeinEnd f n)

And a ℂ-algebra.

Equations

• RS.skeinEndAlgebra f n = { toSMul := RS.skeinEndAlgebra._aux_1 f n, algebraMap := RS.skeinEndAlgebra._aux_3 f n, commutes' := ⋯, smul_def' := ⋯ }

@[instance_reducible]

noncomputable instance RS.skeinEndAddCommGroup {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : AddCommGroup (skeinEnd f n)

Its additive structure.

Equations

• RS.skeinEndAddCommGroup f n = { toAddGroup := (RS.skeinEndRing f n).toAddGroupWithOne.toAddGroup, add_comm := ⋯ }

@[instance_reducible]

noncomputable instance RS.skeinEndModule {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : Module ℂ (skeinEnd f n)

And its ℂ-module structure.

Equations

• RS.skeinEndModule f n = { toDistribMulAction := Algebra.toModule.toDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

The permutation representation

noncomputable def RS.permClass {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) (σ : Equiv.Perm (Fin n)) : skeinEnd f n

The class of a permutation fragment in the endomorphism algebra.

Equations

• RS.permClass f n σ = RS.HomSpace.ofFragment f.val (RS.permFragment σ)

noncomputable def RS.permToEnd {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : Equiv.Perm (Fin n) →* skeinEnd f n

The map σ ↦ [permFragment σ] is a monoid homomorphism. Identity: permFragment 1 = strandBundle n is the categorical identity. Multiplication: End.mul_def reverses composition order, and permFragmentCompose τ σ gives (permFragment τ).compose (permFragment σ) ≃ permFragment (σ * τ), so [P_σ] * [P_τ] = [P_τ] ≫ [P_σ] = [compose P_τ P_σ] = [P_{σ*τ}].

Equations

• RS.permToEnd f n = { toFun := fun (σ : Equiv.Perm (Fin n)) => RS.permClass f n σ, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def RS.skeinRep {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : SymGroupAlgebra n →ₐ[ℂ] skeinEnd f n

The symmetric-group representation on the n-strand endomorphism algebra: the algebra homomorphism SymGroupAlgebra n →ₐ[ℂ] skeinEnd f n obtained by lifting permToEnd through the universal property of the group algebra.

Equations

• RS.skeinRep f n = (MonoidAlgebra.lift ℂ (RS.skeinEnd f n) (Equiv.Perm (Fin n))) (RS.permToEnd f n)

theorem RS.skeinRep_of {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) (σ : Equiv.Perm (Fin n)) : (skeinRep f n) ((MonoidAlgebra.of ℂ (Equiv.Perm (Fin n))) σ) = permClass f n σ

skeinRep on a single permutation is permClass.

Finite-dimensionality and the rank bound

instance RS.homSpace_finite {R : ℕ} (f : EdgeRankParameter R) (t : ℕ) : Module.Finite ℂ (HomSpace f.val t)

The Hom space at arity t is a finite ℂ-module: its rank is bounded by R ^ t, a natural number, so rank < ℵ₀.

instance RS.skeinEnd_finite {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : Module.Finite ℂ (skeinEnd f n)

The skein endomorphism algebra at level n is finite-dimensional.

theorem RS.homSpace_finrank_le {R : ℕ} (f : EdgeRankParameter R) (t : ℕ) : Module.finrank ℂ (HomSpace f.val t) ≤ R ^ t

The finrank of a Hom space is at most R ^ t.

theorem RS.skeinEnd_finrank_le {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : Module.finrank ℂ (skeinEnd f n) ≤ R ^ (2 * n)

The dimension bound: finrank ℂ (skeinEnd f n) ≤ R ^ (2 * n). Uses HomSpace.rank_le at arity n + n and the identity n + n = 2 * n.

Vanishing propagation (compat)

The geometric content: extending a permutation σ ∈ S_m by identity strands to get σ' ∈ S_n corresponds to tensoring the permutation fragment with identity strands: permFragment σ' ≃ tensorFragment (permFragment σ) (strandBundle (n-m)). The linear factorization: both sides of skeinRep n ∘ symCast h and L ∘ skeinRep m (where L = tensor-with-identity) agree on group-algebra generators by the fragment equivalence, hence agree on all elements by linearity; and linear maps send 0 to 0.

noncomputable def RS.permFragmentExtendEquiv {m k : ℕ} (σ : Equiv.Perm (Fin m)) (h : m ≤ m + k) : (tensorFragment (permFragment σ) (strandBundle k)).Equiv (permFragment (σ.viaEmbedding (Fin.castLEEmb h)))

The tensor of a permutation fragment with identity strands is equivalent to the extended permutation fragment.

Equations

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

theorem RS.permClass_extend {R : ℕ} (f : EdgeRankParameter R) (m k : ℕ) (σ : Equiv.Perm (Fin m)) (h : m ≤ m + k) : ((HomSpace.tensor f m m k k) (permClass f m σ)) (HomSpace.ofFragment f.val (strandBundle k)) = permClass f (m + k) (σ.viaEmbedding (Fin.castLEEmb h))

The per-generator tensor identity: extending a permutation class by identity strands agrees with tensoring.

theorem RS.skeinRep_compat {R : ℕ} (f : EdgeRankParameter R) {m n : ℕ} (h : m ≤ n) (x : SymGroupAlgebra m) (hx : (skeinRep f m) x = 0) : (skeinRep f n) ((symCast h) x) = 0

Vanishing propagation: if x is in the kernel of the level-m representation, its image under symCast is in the kernel at level n.

The tower instance

noncomputable def RS.skeinPermTower {R : ℕ} (f : EdgeRankParameter R) : PermTower (skeinEnd f) (↑R ^ 2)

The skein endomorphism tower: the PermTower at growth R ^ 2 on the family skeinEnd f, with the symmetric-group representation given by permutation fragments, compatibility from the tensor extension, and the dimension bound from the Hom-space rank bound. The growth constant is R ^ 2 because the tower's bound is A ^ n while the Hom-space bound is R ^ (2n); its square root, which is what the threshold 2e√A reads, is R.

Equations

• RS.skeinPermTower f = { rep := RS.skeinRep f, compat := ⋯, bound := ⋯ }