The even-component restriction of the super permutation action

The even and odd components of a SuperVect endomorphism, and the even-component representation of SymGroupAlgebra n they give: superPermAction followed by the even-component extraction, which is linear, so the composite is again linear.

Extraction is a linear map, so it carries zero to zero: whatever the super permutation action kills, the even-component representation kills too. That containment is what the sector trace needs.

Even and odd components

def RS.evenComponent (W : SuperVect) (g : CategoryTheory.End W) : Module.End ℂ W.even

The even component of a SuperVect endomorphism, viewed as a module endomorphism.

Equations

• RS.evenComponent W g = g.evenMap

def RS.oddComponent (W : SuperVect) (g : CategoryTheory.End W) : Module.End ℂ W.odd

The odd component of a SuperVect endomorphism.

Equations

• RS.oddComponent W g = g.oddMap

@[simp]

theorem RS.evenComponent_zero (W : SuperVect) : evenComponent W 0 = 0

The even component of zero is zero.

@[simp]

theorem RS.oddComponent_zero (W : SuperVect) : oddComponent W 0 = 0

The odd component of zero is zero.

theorem RS.evenComponent_add (W : SuperVect) (g₁ g₂ : CategoryTheory.End W) : evenComponent W (g₁ + g₂) = evenComponent W g₁ + evenComponent W g₂

Even extraction is additive.

theorem RS.evenComponent_smul (W : SuperVect) (r : ℂ) (g : CategoryTheory.End W) : evenComponent W (r • g) = r • evenComponent W g

Even extraction commutes with scaling.

def RS.evenComponentLinear (W : SuperVect) : CategoryTheory.End W →ₗ[ℂ] Module.End ℂ W.even

The even-component extraction is a linear map from the endomorphism algebra to the module endomorphism ring.

Equations

• RS.evenComponentLinear W = { toFun := RS.evenComponent W, map_add' := ⋯, map_smul' := ⋯ }

The even-component representation

noncomputable def RS.evenPermRep {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (n : ℕ) : SymGroupAlgebra n →ₗ[ℂ] Module.End ℂ (superPow (strandImage f P) n).even

The even-component representation of SymGroupAlgebra n on (superPow V n).even: the composite of superPermAction with the even-component linear extraction.

Equations

• RS.evenPermRep f P n = RS.evenComponentLinear (RS.superPow (RS.strandImage f P) n) ∘ₗ (RS.superPermAction f P n).toLinearMap

theorem RS.superPermAction_zero_imp_evenPermRep_zero {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (n : ℕ) (x : SymGroupAlgebra n) : (superPermAction f P n) x = 0 → (evenPermRep f P n) x = 0

Even-restriction zero implication: if the super-permutation action kills an element, so does the even-component representation. This is immediate because the even component of a zero SuperVect morphism is zero.