Peeling a unit summand off a mixed sum

The mixed sum L.mix (p + 1) q of p + 1 copies of the unit and q copies of an odd line decomposes as a binary biproduct of one unit summand and the smaller mixed sum L.mix p q. The isomorphism is pure index bookkeeping: the first unit index is peeled off and the remaining indices are shifted down by one.

def RS.mixShift (p q : ℕ) : Fin p ⊕ Fin q → Fin (p + 1) ⊕ Fin q

Shift the unit indices of a mixed sum up by one, leaving the line indices unchanged.

Equations

• RS.mixShift p q = Sum.elim (fun (i : Fin p) => Sum.inl i.succ) Sum.inr

@[reducible, inline]

abbrev RS.OddLine.mixFun {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (p q : ℕ) (i : Fin p ⊕ Fin q) : D

The summand family of the mixed sum: the unit at each Fin p index, the line at each Fin q index.

Equations

• L.mixFun p q i = Sum.elim (fun (x : Fin p) => CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (fun (x : Fin q) => L.obj) i

theorem RS.OddLine.mixShift_summand {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (p q : ℕ) (j : Fin p ⊕ Fin q) : L.mixFun (p + 1) q (mixShift p q j) = L.mixFun p q j

Shifting an index does not change the associated summand.

theorem RS.mixShift_ne_inl_zero (p q : ℕ) (j : Fin p ⊕ Fin q) : mixShift p q j ≠ Sum.inl 0

The shift never produces the first unit index.

theorem RS.mixShift_injective (p q : ℕ) : Function.Injective (mixShift p q)

The index shift is injective.

theorem RS.OddLine.mixFun_inl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (p q : ℕ) (i : Fin p) : L.mixFun p q (Sum.inl i) = CategoryTheory.MonoidalCategoryStruct.tensorUnit D

Every unit summand of a mixed sum is the unit.

theorem RS.OddLine.mixFun_inr {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (p q : ℕ) (j : Fin q) : L.mixFun p q (Sum.inr j) = L.obj

Every line summand of a mixed sum is the line.

noncomputable def RS.OddLine.mixSuccHom {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 ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⊞ ⨁ L.mixFun p q

Project a mixed sum onto its first unit summand together with the remaining, downshifted, mixed sum.

Equations

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

noncomputable def RS.OddLine.mixSuccInv {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.MonoidalCategoryStruct.tensorUnit D ⊞ ⨁ L.mixFun p q ⟶ ⨁ L.mixFun (p + 1) q

Rebuild a mixed sum from its first unit summand and the remaining, downshifted, mixed sum.

Equations

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

theorem RS.OddLine.ι_zero_mixSuccHom {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 (CategoryTheory.Limits.biproduct.ι (L.mixFun (p + 1) q) (Sum.inl 0)) (L.mixSuccHom p q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) CategoryTheory.Limits.biprod.inl

The peeling map restricted to the first unit summand is the left biproduct inclusion.

theorem RS.OddLine.ι_zero_mixSuccHom_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 : ℕ) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⊞ ⨁ L.mixFun p q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun (p + 1) q) (Sum.inl 0)) (CategoryTheory.CategoryStruct.comp (L.mixSuccHom p q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h)

The peeling map restricted to the first unit summand is the left biproduct inclusion.

theorem RS.OddLine.ι_mixShift_mixSuccHom {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 p ⊕ Fin q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun (p + 1) q) (mixShift p q j)) (L.mixSuccHom p q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun p q) j) CategoryTheory.Limits.biprod.inr)

The peeling map restricted to a shifted summand is the right inclusion of the corresponding summand of the smaller sum.

theorem RS.OddLine.ι_mixShift_mixSuccHom_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 p ⊕ Fin q) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⊞ ⨁ L.mixFun p q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun (p + 1) q) (mixShift p q j)) (CategoryTheory.CategoryStruct.comp (L.mixSuccHom p q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun p q) j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h))

The peeling map restricted to a shifted summand is the right inclusion of the corresponding summand of the smaller sum.

theorem RS.mixShift_cases (p q : ℕ) (i : Fin (p + 1) ⊕ Fin q) : i = Sum.inl 0 ∨ ∃ (j : Fin p ⊕ Fin q), i = mixShift p q j

Every index of the longer mixed sum is either the first unit index or a shifted index.

theorem RS.OddLine.mixSucc_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.mixSuccHom p q) (L.mixSuccInv p q) = CategoryTheory.CategoryStruct.id (⨁ L.mixFun (p + 1) q)

The peeling map followed by the rebuilding map is the identity on the longer mixed sum.

theorem RS.OddLine.mixSucc_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.mixSuccInv p q) (L.mixSuccHom p q) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⊞ ⨁ L.mixFun p q)

The rebuilding map followed by the peeling map is the identity on the peeled form.

noncomputable def RS.OddLine.mixSuccIso {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 ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⊞ L.mix p q

Peeling one unit summand off a mixed sum: the mixed sum of p + 1 units and q lines is a unit plus the mixed sum of p units and q lines.

Equations

• L.mixSuccIso p q = { hom := L.mixSuccHom p q, inv := L.mixSuccInv p q, hom_inv_id := ⋯, inv_hom_id := ⋯ }