Tensor-power decomposition of the fibre-functor image

The fibre functor ω of a Deligne package sends the skein object SkeinObj.mk n to a super vector space that is canonically isomorphic to the n-th monoidal power of V := ω.obj (SkeinObj.mk 1). This file builds the chain:

Part A — Iterated tensorator

• omegaPow n : superPow V n ≅ ω.obj (SkeinObj.mk n) — by induction on n using the unit comparison ε/η and the tensorator μ/δ.

Part B — Conjugated action

• superPermAction n — the algebra homomorphism SymGroupAlgebra n →ₐ[ℂ] End (superPow V n) obtained by conjugating omegaSkeinRep through omegaPow.
• superPermAction_eq_zero_iff — conjugation by an iso preserves zero: superPermAction x = 0 ↔ omegaSkeinRep x = 0.

Part C — The permutation-level formula

• superPermAction_perm — on a single permutation σ, superPermAction σ equals the conjugation of ω.map (permClass σ) by omegaPow.

Part A: The iterated tensorator

@[reducible, inline]

abbrev RS.strandImage {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) : SuperVect

Abbreviation for the strand image.

Equations

• RS.strandImage f P = P.ω.obj { arity := 1 }

noncomputable def RS.omegaPowHom {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (n : ℕ) : superPow (strandImage f P) n ⟶ P.ω.obj { arity := n }

The forward map of the iterated tensorator: superPow V n ⟶ ω.obj (SkeinObj.mk n), built left-nested using the unit comparison and the tensorator.

Equations

• One or more equations did not get rendered due to their size.
• RS.omegaPowHom f P 0 = CategoryTheory.Functor.LaxMonoidal.ε P.ω

noncomputable def RS.omegaPowInv {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (n : ℕ) : P.ω.obj { arity := n } ⟶ superPow (strandImage f P) n

The backward map of the iterated tensorator: ω.obj (SkeinObj.mk n) ⟶ superPow V n, built by inverting the tensorator at each step.

Equations

• One or more equations did not get rendered due to their size.
• RS.omegaPowInv f P 0 = CategoryTheory.Functor.OplaxMonoidal.η P.ω

theorem RS.omegaPow_inv_hom {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (omegaPowInv f P n) (omegaPowHom f P n) = CategoryTheory.CategoryStruct.id (P.ω.obj { arity := n })

The backward-then-forward composite is the identity (the fibre side).

theorem RS.omegaPow_hom_inv {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (omegaPowHom f P n) (omegaPowInv f P n) = CategoryTheory.CategoryStruct.id (superPow (strandImage f P) n)

The forward-then-backward composite is the identity (the model side).

noncomputable def RS.omegaPow {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (n : ℕ) : superPow (strandImage f P) n ≅ P.ω.obj { arity := n }

The iterated tensorator: the n-th monoidal power of the strand image is isomorphic to ω.obj (SkeinObj.mk n), built by iterating the tensorator μ/δ.

Equations

• RS.omegaPow f P n = { hom := RS.omegaPowHom f P n, inv := RS.omegaPowInv f P n, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Part B: The conjugated action

def RS.isoConj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (e : X ≅ Y) (f : CategoryTheory.End Y) : CategoryTheory.End X

Conjugation of an endomorphism by an isomorphism: e.hom ≫ f ≫ e.inv, transporting f : End Y to End X via e : X ≅ Y.

Equations

• RS.isoConj e f = CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp f e.inv)

@[simp]

theorem RS.isoConj_unfold {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (e : X ≅ Y) (f : CategoryTheory.End Y) : isoConj e f = CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp f e.inv)

Conjugation by an isomorphism, unfolded.

theorem RS.isoConj_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (e : X ≅ Y) : isoConj e (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id X

It preserves the identity.

theorem RS.isoConj_mul {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (e : X ≅ Y) (f g : CategoryTheory.End Y) : isoConj e (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (isoConj e f) (isoConj e g)

And composition.

theorem RS.isoConj_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} (e : X ≅ Y) : isoConj e 0 = 0

It sends zero to zero.

theorem RS.isoConj_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} (e : X ≅ Y) (f g : CategoryTheory.End Y) : isoConj e (f + g) = isoConj e f + isoConj e g

And is additive — so it is an algebra map on endomorphisms.

theorem RS.isoConj_smul {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] {X Y : C} (e : X ≅ Y) (r : ℂ) (f : CategoryTheory.End Y) : isoConj e (r • f) = r • isoConj e f

Conjugation by an iso preserves scalar multiplication.

theorem RS.isoConj_injective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (e : X ≅ Y) : Function.Injective (isoConj e)

Conjugation by an iso is injective.

theorem RS.isoConj_eq_zero_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} (e : X ≅ Y) (f : CategoryTheory.End Y) : isoConj e f = 0 ↔ f = 0

Conjugation by an iso preserves zero iff: isoConj e f = 0 ↔ f = 0.

noncomputable def RS.superPermAction {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (n : ℕ) : SymGroupAlgebra n →ₐ[ℂ] CategoryTheory.End (superPow (strandImage f P) n)

The transported symmetric-group action on the tensor power: the algebra homomorphism obtained by conjugating omegaSkeinRep through the iterated tensorator omegaPow.

Equations

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

theorem RS.superPermAction_eq_zero_iff {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (n : ℕ) (x : SymGroupAlgebra n) : (superPermAction f P n) x = 0 ↔ (omegaSkeinRep f P n) x = 0

Zero equivalence: the transported action kills an element if and only if the original fibre-functor action does.

Part C: Permutation-level formula

theorem RS.superPermAction_perm {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (n : ℕ) (σ : Equiv.Perm (Fin n)) : (superPermAction f P n) ((MonoidAlgebra.of ℂ (Equiv.Perm (Fin n))) σ) = isoConj (omegaPow f P n) (P.ω.map (permClass f n σ))

On a single permutation, superPermAction is the conjugation of ω.map (permClass σ) by omegaPow.