Mixed sums as folded biproduct powers

The mixed sum L.mix (p + 1) (q + 1) of the dévissage is indexed by a Sum of two Fin types. Splitting the biproduct along the two injections and folding each constant family into the iterated binary sum sumPow identifies the mixed sum with the object sumPow (𝟙_ D) p ⊞ sumPow L.obj q of the 1.9 layer. The nonvanishing of the mixed sum at every diagram avoiding the cell (p + 1, q + 1) then transports across the isomorphism.

noncomputable def RS.OddLine.mixSplitHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) : ⨁ L.mixFun (p + 1) (q + 1) ⟶ (⨁ fun (x : Fin (p + 1)) => CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⊞ ⨁ fun (x : Fin (q + 1)) => L.obj

Split a mixed sum into its unit part and its line part.

Equations

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

noncomputable def RS.OddLine.mixSplitInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) : ((⨁ fun (x : Fin (p + 1)) => CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⊞ ⨁ fun (x : Fin (q + 1)) => L.obj) ⟶ ⨁ L.mixFun (p + 1) (q + 1)

Rebuild a mixed sum from its unit part and its line part.

Equations

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

theorem RS.OddLine.ι_inl_mixSplitHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) (i : Fin (p + 1)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun (p + 1) (q + 1)) (Sum.inl i)) (L.mixSplitHom p q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (x : Fin (p + 1)) => CategoryTheory.MonoidalCategoryStruct.tensorUnit D) i) CategoryTheory.Limits.biprod.inl)

The splitting map restricted to a unit summand is the matching inclusion into the unit part.

theorem RS.OddLine.ι_inl_mixSplitHom_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) (i : Fin (p + 1)) {Z : D} (h : ((⨁ fun (x : Fin (p + 1)) => CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⊞ ⨁ fun (x : Fin (q + 1)) => L.obj) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun (p + 1) (q + 1)) (Sum.inl i)) (CategoryTheory.CategoryStruct.comp (L.mixSplitHom p q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (x : Fin (p + 1)) => CategoryTheory.MonoidalCategoryStruct.tensorUnit D) i) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h))

The splitting map restricted to a unit summand is the matching inclusion into the unit part.

theorem RS.OddLine.ι_inr_mixSplitHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) (j : Fin (q + 1)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun (p + 1) (q + 1)) (Sum.inr j)) (L.mixSplitHom p q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (x : Fin (q + 1)) => L.obj) j) CategoryTheory.Limits.biprod.inr)

The splitting map restricted to a line summand is the matching inclusion into the line part.

theorem RS.OddLine.ι_inr_mixSplitHom_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) (j : Fin (q + 1)) {Z : D} (h : ((⨁ fun (x : Fin (p + 1)) => CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⊞ ⨁ fun (x : Fin (q + 1)) => L.obj) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun (p + 1) (q + 1)) (Sum.inr j)) (CategoryTheory.CategoryStruct.comp (L.mixSplitHom p q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (x : Fin (q + 1)) => L.obj) j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h))

The splitting map restricted to a line summand is the matching inclusion into the line part.

theorem RS.OddLine.mixSplit_hom_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) : CategoryTheory.CategoryStruct.comp (L.mixSplitHom p q) (L.mixSplitInv p q) = CategoryTheory.CategoryStruct.id (⨁ L.mixFun (p + 1) (q + 1))

Splitting then rebuilding is the identity on the mixed sum.

theorem RS.OddLine.mixSplit_inv_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) : CategoryTheory.CategoryStruct.comp (L.mixSplitInv p q) (L.mixSplitHom p q) = CategoryTheory.CategoryStruct.id ((⨁ fun (x : Fin (p + 1)) => CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⊞ ⨁ fun (x : Fin (q + 1)) => L.obj)

Rebuilding then splitting is the identity on the split form.

noncomputable def RS.OddLine.mixSplitIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) : L.mix (p + 1) (q + 1) ≅ (⨁ fun (x : Fin (p + 1)) => CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⊞ ⨁ fun (x : Fin (q + 1)) => L.obj

A mixed sum is the biproduct of its unit part and its line part.

Equations

• L.mixSplitIso p q = { hom := L.mixSplitHom p q, inv := L.mixSplitInv p q, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.constSumIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (X : D) (k : ℕ) : (⨁ fun (x : Fin (k + 1)) => X) ≅ sumPow X k

Folding a constant biproduct into the iterated binary sum.

Equations

• RS.constSumIso X k = { hom := CategoryTheory.Limits.biproduct.desc (RS.sumPowIns X k), inv := CategoryTheory.Limits.biproduct.lift (RS.sumPowPrj X k), hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.OddLine.mixSumPowIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) : L.mix (p + 1) (q + 1) ≅ sumPow (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) p ⊞ sumPow L.obj q

The mixed sum in fold form: the mixed sum of p + 1 units and q + 1 lines is the biproduct of the folded unit power and the folded line power.

Equations

• L.mixSumPowIso p q = L.mixSplitIso p q ≪≫ CategoryTheory.Limits.biprod.mapIso (RS.constSumIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) p) (RS.constSumIso L.obj q)

theorem RS.OddLine.not_schurKilled_mix {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.MonoidalLinear ℂ D] (P : SchurPackage) (P₀ : SchurPackage) (hone : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (L : OddLine D) (p q : ℕ) {lam : YoungDiagram} (hcell : (p + 1, q + 1) ∉ lam) : ¬SchurKilled P (L.mix (p + 1) (q + 1)) lam

Nonvanishing of the mixed sum: in a nontrivial ambient category, the mixed sum of p + 1 units and q + 1 odd lines is not Schur-killed at any diagram avoiding the cell (p + 1, q + 1).