Mixed sums with degenerate counts

The nonvanishing half of Deligne 1.9 was established for mixed sums L.mix (p + 1) (q + 1) with both counts strictly positive. Nothing in the argument needs that. The letter framework of MixedLetters is stated at an arbitrary finite label type, the super-trace computation behind not_schurKilled_stdSuper holds at every pair of dimensions, and the only trace of positivity in the existing chain is the shape of the objects carrying the letter systems: an iterated binary sum sumPow X k has k + 1 summands, and the standard super object was equipped with letters only in the form stdSuper (p + 1) (q + 1).

Both are avoidable. Here the ambient letter system is read off directly from the indexed biproduct defining L.mix r s, whose label type Fin r ⊕ Fin s is allowed to be empty, and the SuperVect letter system is rebuilt on stdSuper r s at arbitrary dimensions. The two sides are joined exactly as before, giving the nonvanishing statement for all counts r s : ℕ.

@[reducible, inline]

abbrev RS.mixParity (r s : ℕ) : Fin r ⊕ Fin s → Bool

The parity of a mixed letter label at arbitrary counts: even on the unit summands, odd on the line summands.

Equations

• RS.mixParity r s k = Sum.rec (fun (x : Fin r) => false) (fun (x : Fin s) => true) k

The letter system of a mixed sum

noncomputable def RS.OddLine.mixLetters {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.SymmetricCategory D] (L : OddLine D) (r s : ℕ) : MixedLetters (Fin r ⊕ Fin s) (mixParity r s) L.obj (L.mix r s)

The letter system of a mixed sum, read off from the indexed biproduct: the inclusions and projections of the summands, with the unit summands even and the line summands odd. No positivity of the counts is involved.

Equations

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

The letter system of the standard super object

The same letters on stdSuper r s, at arbitrary dimensions: unit letters along the even coordinates, odd-line letters along the odd coordinates.

noncomputable def RS.evenIn (r s : ℕ) (i : Fin r) : CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect ⟶ stdSuper r s

The inclusion of an even coordinate line.

Equations

• RS.evenIn r s i = { evenMap := LinearMap.single ℂ (fun (x : Fin r) => ℂ) i, oddMap := 0 }

noncomputable def RS.evenOut (r s : ℕ) (i : Fin r) : stdSuper r s ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect

The projection onto an even coordinate line.

Equations

• RS.evenOut r s i = { evenMap := LinearMap.proj i, oddMap := 0 }

noncomputable def RS.oddInto (r s : ℕ) (j : Fin s) : stdSuper 0 1 ⟶ stdSuper r s

The inclusion of an odd coordinate line.

Equations

• RS.oddInto r s j = { evenMap := 0, oddMap := LinearMap.single ℂ (fun (x : Fin s) => ℂ) j ∘ₗ LinearMap.proj 0 }

noncomputable def RS.oddOut (r s : ℕ) (j : Fin s) : stdSuper r s ⟶ stdSuper 0 1

The projection onto an odd coordinate line.

Equations

• RS.oddOut r s j = { evenMap := 0, oddMap := LinearMap.pi fun (x : Fin 1) => LinearMap.proj j }

noncomputable def RS.superIns (r s : ℕ) (k : Fin r ⊕ Fin s) : letterObj (stdSuper 0 1) (mixParity r s) k ⟶ stdSuper r s

The letter inclusions of the standard super object.

Equations

• RS.superIns r s k = Sum.rec (fun (i : Fin r) => RS.evenIn r s i) (fun (j : Fin s) => RS.oddInto r s j) k

noncomputable def RS.superPrj (r s : ℕ) (k : Fin r ⊕ Fin s) : stdSuper r s ⟶ letterObj (stdSuper 0 1) (mixParity r s) k

The letter projections of the standard super object.

Equations

• RS.superPrj r s k = Sum.rec (fun (i : Fin r) => RS.evenOut r s i) (fun (j : Fin s) => RS.oddOut r s j) k

noncomputable def RS.superLetters (r s : ℕ) : MixedLetters (Fin r ⊕ Fin s) (mixParity r s) (stdSuper 0 1) (stdSuper r s)

The letter system of the standard super object at arbitrary dimensions.

Equations

• RS.superLetters r s = { ins := RS.superIns r s, prj := RS.superPrj r s, ins_prj := ⋯, ins_prj_ne := ⋯, total := ⋯ }