The objects split by a fixed algebra

An object is split by an algebra when its free module is isomorphic to the free module on a mixed sum of copies of the unit and of the odd line. This file collects the closure properties of that class: the unit and the odd line are split, and split objects are closed under zero objects, finite biproducts and tensor products.

The bookkeeping is entirely at the level of the mixed sums: the free module functor carries binary biproducts to module biproducts (RS.freeModBiprodIso) and tensor products to relative tensor products (RS.freeModTensorIso), so each closure statement reduces to an isomorphism of mixed sums in the ambient category, and those are proved by peeling summands with RS.OddLine.mixSuccIso and RS.OddLine.mixLineSuccIso.

The payoff is RS.splitsOn_of_generator: an algebra splitting a tensor generator and its dual splits every embedded object, once subquotients of split objects are known to be split.

theorem RS.isZero_biproductFinZero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (g : Fin 0 → D) : CategoryTheory.Limits.IsZero (⨁ g)

The empty biproduct vanishes.

theorem RS.biproductFin_ι_zero_lift {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {k : ℕ} (g : Fin (k + 1) → D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι g 0) (CategoryTheory.Limits.biproduct.lift fun (i : Fin k) => CategoryTheory.Limits.biproduct.π g i.succ) = 0

The first inclusion misses the shifted projections.

theorem RS.biproductFin_ι_zero_lift_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {k : ℕ} (g : Fin (k + 1) → D) {Z : D} (h : (⨁ fun (i : Fin k) => g i.succ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι g 0) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift fun (i : Fin k) => CategoryTheory.Limits.biproduct.π g i.succ) h) = CategoryTheory.CategoryStruct.comp 0 h

The first inclusion misses the shifted projections.

theorem RS.biproductFin_ι_succ_lift {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {k : ℕ} (g : Fin (k + 1) → D) (i : Fin k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι g i.succ) (CategoryTheory.Limits.biproduct.lift fun (i' : Fin k) => CategoryTheory.Limits.biproduct.π g i'.succ) = CategoryTheory.Limits.biproduct.ι (fun (i : Fin k) => g i.succ) i

A shifted inclusion meets the shifted projections diagonally.

theorem RS.biproductFin_ι_succ_lift_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {k : ℕ} (g : Fin (k + 1) → D) (i : Fin k) {Z : D} (h : (⨁ fun (i' : Fin k) => g i'.succ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι g i.succ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift fun (i' : Fin k) => CategoryTheory.Limits.biproduct.π g i'.succ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : Fin k) => g i.succ) i) h

A shifted inclusion meets the shifted projections diagonally.

noncomputable def RS.biprodPeelFinIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {k : ℕ} (g : Fin (k + 1) → D) : ⨁ g ≅ g 0 ⊞ ⨁ fun (i : Fin k) => g i.succ

Peeling the first summand off a biproduct indexed by Fin (k + 1).

Equations

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

Mixed sums are closed under biproducts and tensors

noncomputable def RS.OddLine.mixOneZeroIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) : L.mix 1 0 ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

The mixed sum of one unit and no line is the unit.

Equations

• L.mixOneZeroIso = L.mixSuccIso 0 0 ≪≫ (CategoryTheory.Limits.isoBiprodZero ⋯).symm

noncomputable def RS.OddLine.mixZeroOneIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) : L.mix 0 1 ≅ L.obj

The mixed sum of no unit and one line is the line.

Equations

• L.mixZeroOneIso = L.mixLineSuccIso 0 0 ≪≫ (CategoryTheory.Limits.isoBiprodZero ⋯).symm

theorem RS.OddLine.exists_mix_biprod {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 p' q' : ℕ) : ∃ (a : ℕ) (b : ℕ), Nonempty (L.mix p q ⊞ L.mix p' q' ≅ L.mix a b)

A biproduct of mixed sums is a mixed sum.

theorem RS.OddLine.exists_mix_line_tensor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) : ∃ (a : ℕ) (b : ℕ), Nonempty (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj (L.mix p q) ≅ L.mix a b)

The line times a mixed sum is a mixed sum: the line exchanges the unit summands with the line summands.

theorem RS.OddLine.exists_mix_tensor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q p' q' : ℕ) : ∃ (a : ℕ) (b : ℕ), Nonempty (CategoryTheory.MonoidalCategoryStruct.tensorObj (L.mix p q) (L.mix p' q') ≅ L.mix a b)

A tensor product of mixed sums is a mixed sum.

Split objects

def RS.IsSplit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] (Y : D) : Prop

An object is split by R when its free module is a mixed sum: a sum of copies of the unit and of the odd line.

Equations

• RS.IsSplit L R Y = ∃ (p : ℕ) (q : ℕ), Nonempty (RS.freeMod R Y ≅ RS.freeMod R (L.mix p q))

theorem RS.IsSplit.of_iso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] {Y Z : D} (e : Y ≅ Z) (h : IsSplit L R Y) : IsSplit L R Z

Splitness transports along an isomorphism.

theorem RS.isSplit_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] : IsSplit L R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

The unit is split: it is the mixed sum of a single unit.

theorem RS.isSplit_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] {Y : D} (h : CategoryTheory.Limits.IsZero Y) : IsSplit L R Y

A zero object is split: it is the empty mixed sum.

theorem RS.IsSplit.biprod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.MonoidalPreadditive D] {Y Z : D} (hY : IsSplit L R Y) (hZ : IsSplit L R Z) : IsSplit L R (Y ⊞ Z)

Split objects are closed under binary biproducts, the ranks adding.

theorem RS.IsSplit.biproduct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.MonoidalPreadditive D] (k : ℕ) (g : Fin k → D) : (∀ (t : Fin k), IsSplit L R (g t)) → IsSplit L R (⨁ g)

Split objects are closed under finite biproducts.

theorem RS.IsSplit.tensor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj R] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] {Y Z : D} (hY : IsSplit L R Y) (hZ : IsSplit L R Z) : IsSplit L R (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)

Split objects are closed under tensor products: the free module functor carries the tensor product to the relative tensor product, and a tensor product of mixed sums is a mixed sum.

theorem RS.IsSplit.tensorPow {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj R] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] {Y : D} (h : IsSplit L R Y) (n : ℕ) : IsSplit L R (RS.tensorPow D Y n)

Split objects are closed under tensor powers.

The generator splits the embedded category

theorem RS.isSplit_indOf_tensorPow {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive (CategoryTheory.Ind C)] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] [CategoryTheory.Limits.HasCoequalizers (CategoryTheory.Ind C)] [∀ (Z : CategoryTheory.Ind C), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (X : C) (hX : IsSplit L 𝔸 (indOf.obj X)) (n : ℕ) : IsSplit L 𝔸 (indOf.obj (tensorPow C X n))

The embedded tensor powers of a split object are split: the embedding is strong monoidal, so it carries the tensor power downstairs to the tensor power upstairs.

theorem RS.isSplit_indOf_mixedPow {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive (CategoryTheory.Ind C)] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] [CategoryTheory.Limits.HasCoequalizers (CategoryTheory.Ind C)] [∀ (Z : CategoryTheory.Ind C), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (X : C) (hX : IsSplit L 𝔸 (indOf.obj X)) (hXd : IsSplit L 𝔸 (indOf.obj Xᘁ)) (a b : ℕ) : IsSplit L 𝔸 (indOf.obj (mixedPow C X a b))

The embedded mixed tensor powers of a generator are split, given that the generator and its dual are.

theorem RS.splitsOn_of_generator {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive (CategoryTheory.Ind C)] [CategoryTheory.SymmetricCategory (CategoryTheory.Ind C)] [CategoryTheory.Limits.HasCoequalizers (CategoryTheory.Ind C)] [∀ (Z : CategoryTheory.Ind C), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Ind C)] (L : OddLine (CategoryTheory.Ind C)) (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (X : C) (hX : IsSplit L 𝔸 (indOf.obj X)) (hXd : IsSplit L 𝔸 (indOf.obj Xᘁ)) (hsub : ∀ (Y Z : C), IsSubquotientOf Y Z → IsSplit L 𝔸 (indOf.obj Z) → IsSplit L 𝔸 (indOf.obj Y)) (hgen : TensorGeneratedBy C X) : SplitsOn L 𝔸 indOf

A splitting generator splits the whole embedded category. Every object of C is a subquotient of a finite biproduct of mixed tensor powers of the generator; the embedding is additive, so it carries that biproduct into Ind C, where the closure properties above make it split, and the subquotient hypothesis finishes.

The subquotient hypothesis is phrased downstairs: for objects Y and Z of C with Y a subquotient of Z, splitness of the embedded Z implies splitness of the embedded Y.