Schur nonvanishing on the standard super vector space

The nonvanishing half of Deligne 1.9 in SuperVect: on the standard super object of dimension (p, q) the central idempotent of every diagram avoiding the cell (p, q) acts nonzero on the tensor power.

The route is a trace computation. The super trace functional sTr — the plain trace of the even and odd components — is linear, cyclic, and multiplicative for the graded tensor product, so σ ↦ sTr (permMor X n σ) is a class function multiplicative over block embeddings. A partial-trace identity for the Koszul braiding (sTr_swap_conj) evaluates it on the standard cycles, giving the character formula sTr (permMor X n σ) = cycleFun (superPS p q) σ. Evaluating sTr ∘ permAlg on a package idempotent through the Frobenius formula then yields dim λ · s_λ(superPS p q), positive by hook positivity — so the idempotent's action cannot vanish.

The standard super vector space

def RS.stdSuper (p q : ℕ) : SuperVect

The standard super vector space of dimension (p, q): ℂ^p in even degree and ℂ^q in odd degree.

Equations

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

@[simp]

theorem RS.stdSuper_even (p q : ℕ) : (stdSuper p q).even = (Fin p → ℂ)

The even component of the standard super object.

@[simp]

theorem RS.stdSuper_odd (p q : ℕ) : (stdSuper p q).odd = (Fin q → ℂ)

The odd component of the standard super object.

The super trace functional

The plain trace of a grading-preserving endomorphism: the sum of the traces of its two components. (This is the trace of the underlying linear endomorphism, not the supertrace; the Koszul signs of the braiding enter through the action itself.)

noncomputable def RS.sTr {V : SuperVect} (f : V ⟶ V) : ℂ

The trace of an endomorphism in SuperVect: the sum of the traces of its even and odd components.

Equations

• RS.sTr f = (LinearMap.trace ℂ V.even) f.evenMap + (LinearMap.trace ℂ V.odd) f.oddMap

noncomputable def RS.sTrL (V : SuperVect) : (V ⟶ V) →ₗ[ℂ] ℂ

The super trace as a linear functional on endomorphisms.

Equations

• RS.sTrL V = { toFun := RS.sTr, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RS.sTrL_apply (V : SuperVect) (f : V ⟶ V) : (sTrL V) f = sTr f

sTrL evaluates to sTr.

theorem RS.sTr_id (V : SuperVect) : sTr (CategoryTheory.CategoryStruct.id V) = ↑(Module.finrank ℂ V.even) + ↑(Module.finrank ℂ V.odd)

The super trace of the identity is the total dimension.

theorem RS.sTr_comp_comm {V W : SuperVect} (f : V ⟶ W) (g : W ⟶ V) : sTr (CategoryTheory.CategoryStruct.comp f g) = sTr (CategoryTheory.CategoryStruct.comp g f)

Cyclicity of the super trace.

theorem RS.sTr_conj {V W : SuperVect} (e : V ≅ W) (f : V ⟶ V) : sTr (CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.CategoryStruct.comp f e.hom)) = sTr f

The super trace is invariant under conjugation by an isomorphism.

theorem RS.sTr_tensorHom {V W : SuperVect} (f : V ⟶ V) (g : W ⟶ W) : sTr (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = sTr f * sTr g

Multiplicativity of the super trace for the graded tensor product of endomorphisms.

The parity involution

def RS.parHom (V : SuperVect) : V ⟶ V

The parity involution of a super vector space: the identity on the even component and minus the identity on the odd component.

Equations

• RS.parHom V = { evenMap := LinearMap.id, oddMap := -LinearMap.id }

@[simp]

theorem RS.parHom_evenMap (V : SuperVect) : (parHom V).evenMap = LinearMap.id

The even component of the parity involution.

@[simp]

theorem RS.parHom_oddMap (V : SuperVect) : (parHom V).oddMap = -LinearMap.id

The odd component of the parity involution.

theorem RS.parHom_comm {V W : SuperVect} (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp f (parHom W) = CategoryTheory.CategoryStruct.comp (parHom V) f

The parity involution commutes with every morphism.

def RS.parPow (V : SuperVect) : ℕ → (V ⟶ V)

The iterated parity involution.

Equations

• RS.parPow V 0 = CategoryTheory.CategoryStruct.id V
• RS.parPow V n.succ = CategoryTheory.CategoryStruct.comp (RS.parPow V n) (RS.parHom V)

theorem RS.parPow_evenMap (V : SuperVect) (n : ℕ) : (parPow V n).evenMap = LinearMap.id

The even component of the iterated parity involution.

theorem RS.parPow_oddMap (V : SuperVect) (n : ℕ) : (parPow V n).oddMap = (-1) ^ n • LinearMap.id

The odd component of the iterated parity involution.

theorem RS.sTr_parPow (V : SuperVect) (n : ℕ) : sTr (parPow V n) = ↑(Module.finrank ℂ V.even) + (-1) ^ n * ↑(Module.finrank ℂ V.odd)

The super trace of an iterated parity involution.

The total space and the total tensor identification

The underlying vector space of a super vector space is the product of its components; the graded tensor product's total space is the tensor product of the total spaces, by the four-block shuffle totTensor. All structure maps of SuperVect are conjugates of plain linear maps under this identification, which is what the braiding trace identity is proved through.

theorem RS.sTr_eq_trace_tot {V : SuperVect} (f : V ⟶ V) : sTr f = (LinearMap.trace ℂ (Tot V)) (tot f)

The super trace is the plain trace of the total map.

def RS.prodShuffle (A : Type u_1) (B : Type u_2) (C : Type u_3) (D : Type u_4) [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] : ((A × B) × C × D) ≃ₗ[ℂ] (A × D) × B × C

The middle shuffle of four product components: ((A × B) × (C × D)) ≃ₗ ((A × D) × (B × C)).

Equations

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

@[simp]

theorem RS.prodShuffle_apply (A : Type u_1) (B : Type u_2) (C : Type u_3) (D : Type u_4) [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] (x : (A × B) × C × D) : (prodShuffle A B C D) x = ((x.1.1, x.2.2), x.1.2, x.2.1)

The shuffle, applied.

def RS.totTensor (V W : SuperVect) : TensorProduct ℂ (Tot V) (Tot W) ≃ₗ[ℂ] Tot (V.tensorObj W)

The total tensor identification: the total space of a graded tensor product is the tensor product of the total spaces, by the four-block shuffle.

Equations

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

@[simp]

theorem RS.totTensor_tmul (V W : SuperVect) (x : Tot V) (y : Tot W) : (totTensor V W) (x ⊗ₜ[ℂ] y) = ((x.1 ⊗ₜ[ℂ] y.1, x.2 ⊗ₜ[ℂ] y.2), x.1 ⊗ₜ[ℂ] y.2, x.2 ⊗ₜ[ℂ] y.1)

The total tensor identification on a pure tensor.

theorem RS.tot_tensorHom {V₁ V₂ W₁ W₂ : SuperVect} (f : V₁ ⟶ V₂) (g : W₁ ⟶ W₂) : tot (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) ∘ₗ ↑(totTensor V₁ W₁) = ↑(totTensor V₂ W₂) ∘ₗ TensorProduct.map (tot f) (tot g)

Naturality of the total tensor identification: the total map of a graded tensor of morphisms is the plain tensor of the total maps, conjugated by totTensor.

The associator under the total identification

theorem RS.prodRight_symm_tmul {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddCommGroup A] [Module ℂ A] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] (a : A) (b : B) (c : C) : (TensorProduct.prodRight ℂ ℂ A B C).symm (a ⊗ₜ[ℂ] b, a ⊗ₜ[ℂ] c) = a ⊗ₜ[ℂ] (b, c)

The inverse of prodRight reassembles a pair of tensors with a common first factor.

theorem RS.assocAux_pure {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {C₁ : Type u_5} {C₂ : Type u_6} [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] (a₁ : A₁) (a₂ : A₂) (b₁ : B₁) (b₂ : B₂) (c₁ : C₁) (c₂ : C₂) : (SuperVect.assocAux A₁ A₂ B₁ B₂ C₁ C₂) ((a₁ ⊗ₜ[ℂ] b₁, a₂ ⊗ₜ[ℂ] b₂) ⊗ₜ[ℂ] c₁, (a₁ ⊗ₜ[ℂ] b₂, a₂ ⊗ₜ[ℂ] b₁) ⊗ₜ[ℂ] c₂) = (a₁ ⊗ₜ[ℂ] (b₁ ⊗ₜ[ℂ] c₁, b₂ ⊗ₜ[ℂ] c₂), a₂ ⊗ₜ[ℂ] (b₁ ⊗ₜ[ℂ] c₂, b₂ ⊗ₜ[ℂ] c₁))

The module-level associator block of SuperVect, applied to the pure elements produced by the total identification.

theorem RS.tot_associator (V W Z : SuperVect) : tot (CategoryTheory.MonoidalCategoryStruct.associator V W Z).hom ∘ₗ ↑(totTensor (V.tensorObj W) Z) ∘ₗ TensorProduct.map (↑(totTensor V W)) LinearMap.id = (↑(totTensor V (W.tensorObj Z)) ∘ₗ TensorProduct.map LinearMap.id ↑(totTensor W Z)) ∘ₗ ↑(TensorProduct.assoc ℂ (Tot V) (Tot W) (Tot Z))

The associator under the total identification is the plain associator of the total spaces.

The Koszul braiding under the total identification

def RS.totEvenProj (V : SuperVect) : Tot V →ₗ[ℂ] Tot V

Projection onto the even summand of a total space.

Equations

• RS.totEvenProj V = LinearMap.inl ℂ V.even V.odd ∘ₗ LinearMap.fst ℂ V.even V.odd

def RS.totOddProj (V : SuperVect) : Tot V →ₗ[ℂ] Tot V

Projection onto the odd summand of a total space.

Equations

• RS.totOddProj V = LinearMap.inr ℂ V.even V.odd ∘ₗ LinearMap.snd ℂ V.even V.odd

def RS.signedFlip (V W : SuperVect) : TensorProduct ℂ (Tot V) (Tot W) →ₗ[ℂ] TensorProduct ℂ (Tot W) (Tot V)

The signed flip of total spaces: the plain flip on the even part of the first factor, and the parity-twisted flip on its odd part — the Koszul rule (−1)^{|x||y|} in operator form.

Equations

• RS.signedFlip V W = ↑(TensorProduct.comm ℂ (RS.Tot V) (RS.Tot W)) ∘ₗ (TensorProduct.map (RS.totEvenProj V) LinearMap.id + TensorProduct.map (RS.totOddProj V) (RS.tot (RS.parHom W)))

theorem RS.signedFlip_tmul (V W : SuperVect) (x : Tot V) (y : Tot W) : (signedFlip V W) (x ⊗ₜ[ℂ] y) = y ⊗ₜ[ℂ] (x.1, 0) + (y.1, -y.2) ⊗ₜ[ℂ] (0, x.2)

The signed flip on a pure tensor.

theorem RS.koszulBraidingEven_pair (V W : SuperVect) (a : TensorProduct ℂ V.even W.even) (b : TensorProduct ℂ V.odd W.odd) : (V.koszulBraidingEven W) (a, b) = ((TensorProduct.comm ℂ V.even W.even) a, -(TensorProduct.comm ℂ V.odd W.odd) b)

The even Koszul block on a pair.

theorem RS.tot_koszulBraiding (V W : SuperVect) : tot (β_ V W).hom ∘ₗ ↑(totTensor V W) = ↑(totTensor W V) ∘ₗ signedFlip V W

The Koszul braiding under the total identification is the signed flip.

Plain trace identities

The linear-algebra core of the braiding trace computation: tracing a tensor of maps against the flip contracts to the trace of the composite, and the same identity holds with a spectator factor and a twist on the last slot.

theorem RS.trace_map_comp_comm {V : Type u_2} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (f g : V →ₗ[ℂ] V) : (LinearMap.trace ℂ (TensorProduct ℂ V V)) (TensorProduct.map f g ∘ₗ ↑(TensorProduct.comm ℂ V V)) = (LinearMap.trace ℂ V) (f ∘ₗ g)

The contraction identity: the trace of f ⊗ g against the flip is the trace of f ∘ g.

theorem RS.trace_flip_twist {U : Type u_1} {V : Type u_2} [AddCommGroup U] [Module ℂ U] [FiniteDimensional ℂ U] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (G : TensorProduct ℂ U V →ₗ[ℂ] TensorProduct ℂ U V) (H s t : V →ₗ[ℂ] V) : (LinearMap.trace ℂ (TensorProduct ℂ (TensorProduct ℂ U V) V)) (TensorProduct.map LinearMap.id H ∘ₗ TensorProduct.map G LinearMap.id ∘ₗ ↑(TensorProduct.assoc ℂ U V V).symm ∘ₗ TensorProduct.map LinearMap.id (↑(TensorProduct.comm ℂ V V) ∘ₗ TensorProduct.map s t) ∘ₗ ↑(TensorProduct.assoc ℂ U V V)) = (LinearMap.trace ℂ (TensorProduct ℂ U V)) (G ∘ₗ TensorProduct.map LinearMap.id ((t ∘ₗ H) ∘ₗ s))

The spectator contraction identity: with a spectator factor U, a twist H on the outer slot and modifications s, t inside the flip, the trace contracts to a trace over U ⊗ V.

The braiding partial-trace identity

theorem RS.sTr_swap_conj (P X : SuperVect) (g : P.tensorObj X ⟶ P.tensorObj X) (h : X ⟶ X) : sTr (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (β_ X X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P X X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (P.tensorObj X) h))))) = sTr (CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.CategoryStruct.comp h (parHom X))))

The braiding partial-trace identity: composing the braiding of the top two slots with a whiskered endomorphism and a twist of the top slot traces to the endomorphism alone, with the twist parity-corrected and moved down one slot. This is the engine of the cycle evaluation.

The trace of the standard cycles

Unrolling the bubbling insertTop X n n through the braiding partial-trace identity leaves an iterated parity twist: each braiding step converts one slot's twist into a parity correction.

theorem RS.sTr_insertTop_full (X : SuperVect) (n : ℕ) (h : X ⟶ X) : sTr (CategoryTheory.CategoryStruct.comp (insertTop X n n) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow SuperVect X n) h)) = sTr (CategoryTheory.CategoryStruct.comp (parPow X n) h)

The bubbling trace, with a twist: the full insertion composed with a twist of the top slot traces to the n-fold parity correction of the twist.

theorem RS.sTr_permMor_topCycle_zero (X : SuperVect) (n : ℕ) : sTr (permMor X (n + 1) (topCycle 0)) = sTr (parPow X n)

The trace of the standard cycle on the tensor power is the alternating parity trace.

The super character of the permutation action

noncomputable def RS.superChar (p q n : ℕ) (σ : Equiv.Perm (Fin n)) : ℂ

The super character: the trace of a permutation's action on the tensor power of the standard super object.

Equations

• RS.superChar p q n σ = RS.sTr (RS.permMor (RS.stdSuper p q) n σ)

theorem RS.superChar_conj (p q : ℕ) {n : ℕ} (τ σ : Equiv.Perm (Fin n)) : superChar p q n (τ * σ * τ⁻¹) = superChar p q n σ

The super character is a class function.

theorem RS.superChar_blockEmbed (p q : ℕ) {a b : ℕ} (σ : Equiv.Perm (Fin a)) (τ : Equiv.Perm (Fin b)) : superChar p q (a + b) (blockEmbed σ τ) = superChar p q a σ * superChar p q b τ

The super character is multiplicative over block embeddings.

noncomputable def RS.nfCycle (c : ℕ) : Equiv.Perm (Fin c)

The standard cycle of each length: the full rotation.

Equations

• RS.nfCycle 0 = 1
• RS.nfCycle n.succ = RS.topCycle 0

theorem RS.superChar_nfCycle (p q : ℕ) {c : ℕ} (hc : 1 ≤ c) : superChar p q c (nfCycle c) = superPS p q c

The super character of a standard cycle is the super power sum.

Normal forms and cycle types

theorem RS.cycleType_viaEmbedding {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : Equiv.Perm α) (ι : α ↪ β) : (e.viaEmbedding ι).cycleType = e.cycleType

Relabelling along an embedding preserves the cycle type.

theorem RS.blockEmbed_fst_viaEmbedding {a b : ℕ} (σ : Equiv.Perm (Fin a)) : blockEmbed σ 1 = σ.viaEmbedding (Fin.castAddEmb b)

A one-sided block embedding is a relabelling along the first-block embedding.

theorem RS.blockEmbed_snd_viaEmbedding {a b : ℕ} (τ : Equiv.Perm (Fin b)) : blockEmbed 1 τ = τ.viaEmbedding (Fin.natAddEmb a)

A one-sided block embedding is a relabelling along the last-block embedding.

theorem RS.blockEmbed_disjoint {a b : ℕ} (σ : Equiv.Perm (Fin a)) (τ : Equiv.Perm (Fin b)) : (blockEmbed σ 1).Disjoint (blockEmbed 1 τ)

The two one-sided block embeddings are disjoint.

theorem RS.cycleType_blockEmbed {a b : ℕ} (σ : Equiv.Perm (Fin a)) (τ : Equiv.Perm (Fin b)) : (blockEmbed σ τ).cycleType = σ.cycleType + τ.cycleType

The cycle type of a block embedding is the sum of the cycle types.

theorem RS.cycleType_nfCycle_of_two_le {c : ℕ} (hc : 2 ≤ c) : (nfCycle c).cycleType = {c}

The cycle type of a standard cycle of length at least two.

theorem RS.cycleType_nfCycle_of_le_one {c : ℕ} (hc : c ≤ 1) : (nfCycle c).cycleType = 0

The cycle type of a short standard cycle is empty.

def RS.nfPerm (cs : List ℕ) : Equiv.Perm (Fin cs.sum)

The normal form of a cycle-length list: the block product of standard cycles.

Equations

• RS.nfPerm [] = 1
• RS.nfPerm (c :: cs) = RS.blockEmbed (RS.nfCycle c) (RS.nfPerm cs)

theorem RS.cycleType_nfPerm (cs : List ℕ) : (nfPerm cs).cycleType = ↑(List.filter (fun (c : ℕ) => decide (2 ≤ c)) cs)

The cycle type of a normal form: the cycle lengths of at least two.

theorem RS.superChar_nfPerm (p q : ℕ) (cs : List ℕ) : (∀ c ∈ cs, 1 ≤ c) → superChar p q cs.sum (nfPerm cs) = (List.map (fun (c : ℕ) => superPS p q c) cs).prod

The super character of a normal form is the product of the super power sums of its cycle lengths.

theorem RS.superChar_permCast (p q : ℕ) {m n : ℕ} (h : m = n) (σ : Equiv.Perm (Fin m)) : superChar p q n ((permCast h) σ) = superChar p q m σ

Relabelling along an equality of sizes preserves the super character.

The character formula

theorem RS.sTr_permMor (p q : ℕ) {n : ℕ} (σ : Equiv.Perm (Fin n)) : sTr (permMor (stdSuper p q) n σ) = cycleFun (superPS p q) σ

The super character formula (super Schur–Weyl, character side): the trace of a permutation's action on the tensor power of the standard super object of dimension (p, q) is the completed cycle product of the super power sums.

Nonvanishing of the idempotent action

theorem RS.sTr_permAlg_e (P : SchurPackage) (p q : ℕ) (lam : YoungDiagram) : sTr ((permAlg (stdSuper p q) lam.card) (P.e lam)) = ↑(P.dim lam) * diagramSchur lam (superPS p q)

The idempotent trace formula: the super trace of a package idempotent's action on the tensor power of the standard super object is the dimension times the Schur specialisation at the super power sums.

theorem RS.not_schurKilled_stdSuper (P : SchurPackage) {p q : ℕ} {lam : YoungDiagram} (h : (p, q) ∉ lam) : ¬SchurKilled P (stdSuper p q) lam

Schur nonvanishing on the standard super vector space (Deligne 1.9, nonvanishing direction): a diagram avoiding the cell (p, q) does not kill the standard super object of dimension (p, q) — the central idempotent of its block acts nonzero on the tensor power.

The graded signed permutation representation

The same action, packaged as a genuine representation of the symmetric group on the total space of the tensor power — the free module on colourings carrying the Koszul signs, in its categorical presentation.

noncomputable def RS.gradedSignRep (p q n : ℕ) : Representation ℂ (Equiv.Perm (Fin n)) (Tot (tensorPow SuperVect (stdSuper p q) n))

The graded signed permutation representation: the symmetric group acting on the total space of the tensor power of the standard super object, by the categorical action with its Koszul signs.

Equations

• RS.gradedSignRep p q n = { toFun := fun (σ : Equiv.Perm (Fin n)) => RS.tot (RS.permMor (RS.stdSuper p q) n σ), map_one' := ⋯, map_mul' := ⋯ }

theorem RS.gradedSignRep_apply (p q n : ℕ) (σ : Equiv.Perm (Fin n)) : (gradedSignRep p q n) σ = tot (permMor (stdSuper p q) n σ)

The representation of a permutation is the total map of its categorical action.

theorem RS.gradedSignRep_asAlgebraHom (p q n : ℕ) (z : SymGroupAlgebra n) : (gradedSignRep p q n).asAlgebraHom z = tot ((permAlg (stdSuper p q) n) z)

The algebra action of the representation is the total map of the categorical algebra action.