The stage units of the local splitting chain are point powers

The bridge between the chain and the nonvanishing substrate: the stage units of the local splitting chain are the symmetrised point powers, so for a monic point in a rigid category with nonzero unit no stage unit vanishes. The class of the object in the splitting algebra restricts on the point to the unit.

theorem RS.tensorPowPoint_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (Y : D) (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) : tensorPowPoint pt 1 = CategoryTheory.CategoryStruct.comp pt (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv

The singleton point in the tensor power, as the point against the unitor.

theorem RS.splitSeed_eq {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (Y : D) (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) : splitSeed Y pt = CategoryTheory.CategoryStruct.comp (tensorPowPoint pt 1) (CategoryTheory.CategoryStruct.comp (modPowπ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) Y 1) (symPowπ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) Y 1))

The seed is the symmetrised singleton point.

theorem RS.splitUnitStage_eq {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (Y : D) (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) (n : ℕ) : splitUnitStage Y pt n = CategoryTheory.CategoryStruct.comp (tensorPowPoint pt (n + 1)) (CategoryTheory.CategoryStruct.comp (modPowπ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) Y (n + 1)) (symPowπ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) Y (n + 1)))

The stage units are the symmetrised point powers.

theorem RS.splitUnitStage_ne_zero' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (Y : D) (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) [∀ (Z : D), (CategoryTheory.MonoidalCategory.tensorLeft Z).PreservesMonomorphisms] [∀ (Z : D), (CategoryTheory.MonoidalCategory.tensorRight Z).PreservesMonomorphisms] [CategoryTheory.Mono pt] (h1 : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (n : ℕ) : splitUnitStage Y pt n ≠ 0

The stage-unit nonvanishing, from mono preservation of the tensor factors alone — the form consumed over an ind-completion.

noncomputable def RS.splitCls {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (Y : D) (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] : Y ⟶ splitAlgebra Y pt

The class of the object in the splitting algebra: the singleton power, included at the bottom stage.

Equations

• RS.splitCls Y pt = CategoryTheory.CategoryStruct.comp (RS.symPowOne (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) Y).inv (RS.chainColimitι (RS.splitStage Y) (RS.splitDelta Y pt) 0)

theorem RS.splitCls_point {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (Y : D) (pt : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Y) [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] : CategoryTheory.CategoryStruct.comp pt (splitCls Y pt) = splitAlgebraUnit Y pt

The class restricts on the point to the unit.