The standard super object and the mixed sum

Two letter systems and the conclusion they force. In an ambient symmetric ℂ-linear category with an odd invertible line U the mixed biproduct sum 𝟙 ^ ⊕ (p+1) ⊞ U ^ ⊕ (q+1) carries one; so does the standard super object of RS.SuperVect, whose braiding on the odd line is −1. A group-algebra element killing the ambient tensor power has vanishing colour sums by Letters.lean, hence kills the standard super object as well — contradicting not_schurKilled_stdSuper.

• mixedSumLetters, stdSuperLetters: the two letter systems, built from the biproduct insertions and projections sumPowIns/sumPowPrj and from the coordinates of the standard super object.
• The MonoidalPreadditive and MonoidalLinear structures of RS.SuperVect, and stdSuper_braiding_neg: the odd line of RS.SuperVect is odd.
• tensorPow_id_ne_zero: a tensor power of a nonzero unit is nonzero.
• not_schurKilled_sum: the mixed sum is not Schur-killed at any diagram avoiding the cell (p + 1, q + 1) — the exact complement of schurKilled_unit_odd.

The letter system of a mixed biproduct sum

In an ambient category with binary biproducts, the object 𝟙 ^ ⊕ (p+1) ⊞ U ^ ⊕ (q+1) carries the evident letter system: unit letters through the first summand, odd letters through the second.

@[reducible, inline]

abbrev RS.mixedPar {p q : ℕ} : Fin (p + 1) ⊕ Fin (q + 1) → Bool

The parity of a mixed letter label: even on the first summand, odd on the second.

Equations

• RS.mixedPar k = Sum.rec (fun (x : Fin (p + 1)) => false) (fun (x : Fin (q + 1)) => true) k

noncomputable def RS.sumPowIns {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X : A) (k : ℕ) : Fin (k + 1) → (X ⟶ sumPow X k)

The inclusion of one copy into an iterated biproduct sum.

Equations

• One or more equations did not get rendered due to their size.
• RS.sumPowIns X 0 x_2 = CategoryTheory.CategoryStruct.id X

noncomputable def RS.sumPowPrj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X : A) (k : ℕ) : Fin (k + 1) → (sumPow X k ⟶ X)

The projection onto one copy of an iterated biproduct sum.

Equations

• One or more equations did not get rendered due to their size.
• RS.sumPowPrj X 0 x_2 = CategoryTheory.CategoryStruct.id X

theorem RS.sumPowIns_succ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X : A) (k : ℕ) (i : Fin (k + 2)) : sumPowIns X (k + 1) i = Fin.lastCases CategoryTheory.Limits.biprod.inr (fun (j : Fin (k + 1)) => CategoryTheory.CategoryStruct.comp (sumPowIns X k j) CategoryTheory.Limits.biprod.inl) i

The recursion of the copy inclusion.

theorem RS.sumPowPrj_succ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X : A) (k : ℕ) (i : Fin (k + 2)) : sumPowPrj X (k + 1) i = Fin.lastCases CategoryTheory.Limits.biprod.snd (fun (j : Fin (k + 1)) => CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst (sumPowPrj X k j)) i

The recursion of the copy projection.

theorem RS.sumPowIns_prj_same {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X : A) (k : ℕ) (i : Fin (k + 1)) : CategoryTheory.CategoryStruct.comp (sumPowIns X k i) (sumPowPrj X k i) = CategoryTheory.CategoryStruct.id X

A copy's round trip through the sum is the identity.

theorem RS.sumPowIns_prj_ne {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X : A) (k : ℕ) {i i' : Fin (k + 1)} : i ≠ i' → CategoryTheory.CategoryStruct.comp (sumPowIns X k i) (sumPowPrj X k i') = 0

Distinct copies' round trips vanish.

theorem RS.sumPow_total {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X : A) (k : ℕ) : ∑ i : Fin (k + 1), CategoryTheory.CategoryStruct.comp (sumPowPrj X k i) (sumPowIns X k i) = CategoryTheory.CategoryStruct.id (sumPow X k)

The copies decompose the identity of the sum.

noncomputable def RS.mixedSumLetters {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (p q : ℕ) (U : A) : MixedLetters (Fin (p + 1) ⊕ Fin (q + 1)) mixedPar U (sumPow (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) p ⊞ sumPow U q)

The letter system of the mixed sum: p + 1 unit letters through the first summand and q + 1 odd letters through the second.

Equations

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

Nonvanishing of the odd-line powers

theorem RS.tensorPow_id_ne_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] (hone : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) {U : A} (hUU : CategoryTheory.MonoidalCategoryStruct.tensorObj U U ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit A) (k : ℕ) : CategoryTheory.CategoryStruct.id (tensorPow A U k) ≠ 0

Powers of an invertible line are nonzero when the unit is: tensoring with one more copy of the line is undone through its self-pairing.

The ambient extraction

theorem RS.colourSum_eq_zero_of_schurKilled {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.Limits.HasBinaryBiproducts A] (P : SchurPackage) (hone : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) {U : A} (hUU : CategoryTheory.MonoidalCategoryStruct.tensorObj U U ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit A) (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) (p q : ℕ) {lam : YoungDiagram} (hkill : SchurKilled P (sumPow (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) p ⊞ sumPow U q) lam) (c d : Fin lam.card → Fin (p + 1) ⊕ Fin (q + 1)) : colourSum mixedPar (P.e lam) c d = 0

Extraction in the ambient category: if the mixed sum is Schur-killed at a diagram, every colour sum of the block idempotent vanishes — a purely combinatorial consequence, shared with every other model.

Additive and linear monoidal structure of SuperVect

The graded tensor product is additive and ℂ-linear in each argument, componentwise.

instance RS.instMonoidalPreadditiveSuperVect : CategoryTheory.MonoidalPreadditive SuperVect

SuperVect is monoidal preadditive: whiskering is additive.

instance RS.instMonoidalLinearComplexSuperVect : CategoryTheory.MonoidalLinear ℂ SuperVect

SuperVect is monoidal ℂ-linear: whiskering is ℂ-linear.

The odd line of SuperVect

The standard super object ℂ^{0|1} self-braids by −1: its even component is the zero space, and the Koszul sign acts on the odd square.

theorem RS.stdSuper_braiding_neg : (β_ (stdSuper 0 1) (stdSuper 0 1)).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSuper 0 1) (stdSuper 0 1))

The odd line self-braids by −1.

The letter system of the standard super object

ℂ^{p+1|q+1} carries the evident letter system in SuperVect: unit letters along the even coordinates and odd-line letters along the odd coordinates. No biproducts are needed — the inclusions and projections are written down directly.

noncomputable def RS.unitIn (p q : ℕ) (i : Fin (p + 1)) : CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect ⟶ stdSuper (p + 1) (q + 1)

The inclusion of an even coordinate line.

Equations

• RS.unitIn p q i = { evenMap := LinearMap.single ℂ (fun (x : Fin (p + 1)) => ℂ) i, oddMap := 0 }

noncomputable def RS.unitPrj (p q : ℕ) (i : Fin (p + 1)) : stdSuper (p + 1) (q + 1) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect

The projection onto an even coordinate line.

Equations

• RS.unitPrj p q i = { evenMap := LinearMap.proj i, oddMap := 0 }

noncomputable def RS.oddIn (p q : ℕ) (j : Fin (q + 1)) : stdSuper 0 1 ⟶ stdSuper (p + 1) (q + 1)

The inclusion of an odd coordinate line.

Equations

• RS.oddIn p q j = { evenMap := 0, oddMap := LinearMap.single ℂ (fun (x : Fin (q + 1)) => ℂ) j ∘ₗ LinearMap.proj 0 }

noncomputable def RS.oddPrj (p q : ℕ) (j : Fin (q + 1)) : stdSuper (p + 1) (q + 1) ⟶ stdSuper 0 1

The projection onto an odd coordinate line.

Equations

• RS.oddPrj p q j = { evenMap := 0, oddMap := LinearMap.pi fun (x : Fin 1) => LinearMap.proj j }

noncomputable def RS.stdIns (p q : ℕ) (k : Fin (p + 1) ⊕ Fin (q + 1)) : letterObj (stdSuper 0 1) mixedPar k ⟶ stdSuper (p + 1) (q + 1)

The letter inclusions of the standard super object.

Equations

• RS.stdIns p q k = Sum.rec (fun (i : Fin (p + 1)) => RS.unitIn p q i) (fun (j : Fin (q + 1)) => RS.oddIn p q j) k

noncomputable def RS.stdPrj (p q : ℕ) (k : Fin (p + 1) ⊕ Fin (q + 1)) : stdSuper (p + 1) (q + 1) ⟶ letterObj (stdSuper 0 1) mixedPar k

The letter projections of the standard super object.

Equations

• RS.stdPrj p q k = Sum.rec (fun (i : Fin (p + 1)) => RS.unitPrj p q i) (fun (j : Fin (q + 1)) => RS.oddPrj p q j) k

noncomputable def RS.stdSuperLetters (p q : ℕ) : MixedLetters (Fin (p + 1) ⊕ Fin (q + 1)) mixedPar (stdSuper 0 1) (stdSuper (p + 1) (q + 1))

The letter system of the standard super object.

Equations

• RS.stdSuperLetters p q = { ins := RS.stdIns p q, prj := RS.stdPrj p q, ins_prj := ⋯, ins_prj_ne := ⋯, total := ⋯ }

theorem RS.schurKilled_stdSuper_of_colourSum (P₀ : SchurPackage) (p q : ℕ) {lam : YoungDiagram} (hcs : ∀ (c d : Fin lam.card → Fin (p + 1) ⊕ Fin (q + 1)), colourSum mixedPar (P₀.e lam) c d = 0) : SchurKilled P₀ (stdSuper (p + 1) (q + 1)) lam

Reconstruction in SuperVect: vanishing colour sums force the block idempotent to kill the standard super object.

The summit: nonvanishing of the mixed sum

The exact complement of schurKilled_unit_odd: at every diagram avoiding the cell (p + 1, q + 1), the mixed sum survives. The ambient extraction pins the colour sums of the block idempotent to zero, the reconstruction transports this into SuperVect, and the super trace computation of not_schurKilled_stdSuper refutes it. Both Schur packages have the Jacobi–Trudi character, so their block idempotents coincide and the two worlds speak about the same group-algebra element.

theorem RS.not_schurKilled_sum {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.Limits.HasBinaryBiproducts A] (P : SchurPackage) (P₀ : SchurPackage) (hone : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) {U : A} (hUU : CategoryTheory.MonoidalCategoryStruct.tensorObj U U ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit A) (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) (p q : ℕ) {lam : YoungDiagram} (hcell : (p + 1, q + 1) ∉ lam) : ¬SchurKilled P (sumPow (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) p ⊞ sumPow U q) lam

The nonvanishing half of Deligne 1.9, internally: in a nontrivial ambient category, a direct sum of p + 1 unit copies and q + 1 odd-line copies is not Schur-killed at any diagram avoiding the cell (p + 1, q + 1). Together with schurKilled_unit_odd this characterises the killed diagrams of the mixed sum exactly.