Peeling a line summand off a mixed sum

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

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

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

Equations

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

theorem RS.OddLine.mixShiftL_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 (q + 1) (mixShiftL p q j) = L.mixFun p q j

Shifting an index does not change the associated summand.

theorem RS.mixShiftL_ne_inr_zero (p q : ℕ) (j : Fin p ⊕ Fin q) : mixShiftL p q j ≠ Sum.inr 0

The shift never produces the first line index.

theorem RS.mixShiftL_injective (p q : ℕ) : Function.Injective (mixShiftL p q)

The index shift is injective.

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

Project a mixed sum onto its first line 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.mixLineSuccInv {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.obj ⊞ ⨁ L.mixFun p q ⟶ ⨁ L.mixFun p (q + 1)

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

Equations

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

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

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

theorem RS.OddLine.ι_inr_zero_mixLineSuccHom_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 : L.obj ⊞ ⨁ L.mixFun p q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun p (q + 1)) (Sum.inr 0)) (CategoryTheory.CategoryStruct.comp (L.mixLineSuccHom p q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h)

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

theorem RS.OddLine.ι_mixShiftL_mixLineSuccHom {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 (q + 1)) (mixShiftL p q j)) (L.mixLineSuccHom 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.ι_mixShiftL_mixLineSuccHom_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 : L.obj ⊞ ⨁ L.mixFun p q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (L.mixFun p (q + 1)) (mixShiftL p q j)) (CategoryTheory.CategoryStruct.comp (L.mixLineSuccHom 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.mixShiftL_cases (p q : ℕ) (i : Fin p ⊕ Fin (q + 1)) : i = Sum.inr 0 ∨ ∃ (j : Fin p ⊕ Fin q), i = mixShiftL p q j

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

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

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

theorem RS.OddLine.mixLineSucc_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.mixLineSuccInv p q) (L.mixLineSuccHom p q) = CategoryTheory.CategoryStruct.id (L.obj ⊞ ⨁ L.mixFun p q)

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

noncomputable def RS.OddLine.mixLineSuccIso {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 (q + 1) ≅ L.obj ⊞ L.mix p q

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

Equations

• L.mixLineSuccIso p q = { hom := L.mixLineSuccHom p q, inv := L.mixLineSuccInv p q, hom_inv_id := ⋯, inv_hom_id := ⋯ }