The local splitting chain

The algebra of Deligne's 2.10: for a point of an object, the chain of plain symmetric powers with transitions multiplication by the point. The colimit is the quotient of the symmetric algebra identifying the point with the unit; the stages, the seed, the stage multiplication, and the stage units are pinned here, and the laws assemble the colimit into a commutative algebra through the generic chain kit.

noncomputable def RS.splitStage {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) (n : ℕ) : D

The stages of the local splitting chain: the plain symmetric powers, one letter up.

Equations

• RS.splitStage Y n = RS.symPow (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) Y (n + 1)

noncomputable def RS.splitSeed {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) : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ splitStage Y 0

The seed of the local splitting chain: the point, in the singleton power.

Equations

• RS.splitSeed Y pt = CategoryTheory.CategoryStruct.comp pt (RS.symPowOne (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) Y).inv

noncomputable def RS.splitDelta {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) (n : ℕ) : splitStage Y n ⟶ splitStage Y (n + 1)

The transition of the local splitting chain: multiplication by the seed.

Equations

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

noncomputable def RS.splitMu {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) (i j : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (splitStage Y i) (splitStage Y j) ⟶ splitStage Y (i + 1 + j)

The stage multiplication of the local splitting chain.

Equations

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

noncomputable def RS.splitUnitStage {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) (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ splitStage Y n

The stage units of the local splitting chain: the powers of the point.

Equations

• RS.splitUnitStage Y pt 0 = RS.splitSeed Y pt
• RS.splitUnitStage Y pt n.succ = CategoryTheory.CategoryStruct.comp (RS.splitUnitStage Y pt n) (RS.splitDelta Y pt n)

theorem RS.splitUnitStage_succ {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) (n : ℕ) : CategoryTheory.CategoryStruct.comp (splitUnitStage Y pt n) (splitDelta Y pt n) = splitUnitStage Y pt (n + 1)

The stage units ride along the transitions.

Stage laws

The transitions, the stage multiplication and the seed satisfy the five stagewise laws consumed by the chain kit, derived from the symmetric-multiplication laws one letter up. The arity transports over definitionally equal indices collapse to identities.

theorem RS.splitDelta_mu_right {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) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (splitStage Y i) (splitDelta Y pt j)) (splitMu Y i (j + 1)) = CategoryTheory.CategoryStruct.comp (splitMu Y i j) (splitDelta Y pt (i + 1 + j))

Right transition law: transitioning the second factor and multiplying is multiplying and transitioning, since the transition is right multiplication by the seed.

theorem RS.splitSeed_mu_right {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) (i : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (splitStage Y i) (splitSeed Y pt)) (splitMu Y i 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (splitStage Y i)).hom (splitDelta Y pt i)

Right seed law: multiplying by the seed on the right is the transition, through the right unitor.

theorem RS.splitMu_assoc {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) (i j k : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (splitMu Y i j) (splitStage Y k)) (splitMu Y (i + 1 + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (splitStage Y i) (splitStage Y j) (splitStage Y k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (splitStage Y i) (splitMu Y j k)) (CategoryTheory.CategoryStruct.comp (splitMu Y i (j + 1 + k)) (chainCast (splitStage Y) ⋯)))

Associativity of the stage multiplication, up to the index transport of i + 1 + (j + 1 + k) = i + 1 + j + 1 + k.

theorem RS.splitMu_comm {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) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (β_ (splitStage Y i) (splitStage Y j)).hom (CategoryTheory.CategoryStruct.comp (splitMu Y j i) (chainCast (splitStage Y) ⋯)) = splitMu Y i j

Commutativity of the stage multiplication, up to the index transport of j + 1 + i = i + 1 + j.

theorem RS.splitDelta_mu_left {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) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (splitDelta Y pt i) (splitStage Y j)) (splitMu Y (i + 1) j) = CategoryTheory.CategoryStruct.comp (splitMu Y i j) (CategoryTheory.CategoryStruct.comp (splitDelta Y pt (i + 1 + j)) (chainCast (splitStage Y) ⋯))

Left transition law: transitioning the first factor and multiplying is multiplying and transitioning, up to the index transport, through the braiding and the right transition law.

theorem RS.splitSeed_mu_left {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) (j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (splitSeed Y pt) (splitStage Y j)) (splitMu Y 0 j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (splitStage Y j)).hom (chainMap (splitStage Y) (splitDelta Y pt) ⋯)

Left seed law: multiplying by the seed on the left is the one-step chain morphism, through the braiding of the unit.

noncomputable def RS.splitAlgebra {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] : D

The local splitting algebra: the colimit of the chain of symmetric powers along multiplication by the point.

Equations

• RS.splitAlgebra Y pt = RS.chainColimit (RS.splitStage Y) (RS.splitDelta Y pt)

noncomputable def RS.splitAlgebraUnit {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.MonoidalCategoryStruct.tensorUnit D ⟶ splitAlgebra Y pt

The unit of the local splitting algebra: the included seed.

Equations

• RS.splitAlgebraUnit Y pt = RS.chainColimitUnit (RS.splitStage Y) (RS.splitDelta Y pt) (RS.splitSeed Y pt)

@[reducible]

noncomputable def RS.splitAlgebraMonObj {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) [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft Z)] : CategoryTheory.MonObj (splitAlgebra Y pt)

The local splitting algebra as a monoid object: the unit is the included seed and the multiplication is assembled from the stage multiplications through the chain kit.

Equations

• RS.splitAlgebraMonObj Y pt = RS.chainColimitMonObj (RS.splitStage Y) (RS.splitDelta Y pt) (RS.splitMu Y) ⋯ ⋯ (RS.splitSeed Y pt) ⋯ ⋯ ⋯

theorem RS.splitAlgebra_isCommMonObj {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) [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft Z)] : CategoryTheory.IsCommMonObj (splitAlgebra Y pt)

The local splitting algebra is commutative.