The transition squares of the splitting chain

The chain transitions are multiplication by the seed, so they commute with the chain multiplication: multiplying after an insertion is inserting after multiplying. These are the compatibility squares consumed by the colimit algebra.

theorem RS.chainDelta_mul_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainStage A M M' i) (chainDelta A M M' d j)) (chainMul A M M' i (j + 1)) = CategoryTheory.CategoryStruct.comp (chainMul A M M' i j) (chainDelta A M M' d (i + 1 + j))

The right transition square: inserting the seed in the second factor and multiplying is multiplying and then inserting the seed.

theorem RS.chainStageCast_delta {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') {a b : ℕ} (h : a = b) : CategoryTheory.CategoryStruct.comp (chainStageCast A M M' h) (chainDelta A M M' d b) = CategoryTheory.CategoryStruct.comp (chainDelta A M M' d a) (chainStageCast A M M' ⋯)

Transitions transport along index casts.

theorem RS.chainDelta_mul_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainDelta A M M' d i) (chainStage A M M' j)) (chainMul A M M' (i + 1) j) = CategoryTheory.CategoryStruct.comp (chainMul A M M' i j) (CategoryTheory.CategoryStruct.comp (chainDelta A M M' d (i + 1 + j)) (chainStageCast A M M' ⋯))

The left transition square: inserting the seed in the first factor and multiplying is multiplying and then inserting the seed, up to the index transport.

theorem RS.chainSeed_mul_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (i : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainStage A M M' i) (chainSeed A M M' d)) (chainMul A M M' i 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (chainStage A M M' i)).hom (chainDelta A M M' d i)

The right unit law of the seed: multiplying by the seed on the right is the transition.

theorem RS.chainSeed_mul_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainSeed A M M' d) (chainStage A M M' j)) (chainMul A M M' 0 j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (chainStage A M M' j)).hom (CategoryTheory.CategoryStruct.comp (chainDelta A M M' d j) (chainStageCast A M M' ⋯))

The left unit law of the seed: multiplying by the seed on the left is the transition, through the unit braiding.

theorem RS.chainMap_eq_cast {D : Type u} [CategoryTheory.Category.{v, u} D] (B : ℕ → D) (δ : (n : ℕ) → B n ⟶ B (n + 1)) {m n n' : ℕ} (h : m ≤ n) (hn : n = n') (h' : m ≤ n') : chainMap B δ h' = CategoryTheory.CategoryStruct.comp (chainMap B δ h) (chainCast B hn)

A chain map to a transported index is the chain map followed by the transport.

theorem RS.chainSeed_mul_left_chainMap {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainSeed A M M' d) (chainStage A M M' j)) (chainMul A M M' 0 j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (chainStage A M M' j)).hom (chainMap (chainStage A M M') (chainDelta A M M' d) ⋯)

The left seed law in chain-map form.

noncomputable def RS.chainB {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] (d : ModDualityDatum A M M') : D

The algebra of the splitting chain: the colimit of the symmetric stages along the seed transitions.

Equations

• RS.chainB A M M' d = RS.chainColimit (RS.chainStage A M M') (RS.chainDelta A M M' d)

@[reducible]

noncomputable def RS.chainBMonObj {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.MonObj (chainB A M M' d)

The splitting-chain algebra is a commutative monoid: the stage laws transport to the colimit.

Equations

• RS.chainBMonObj A M M' d = RS.chainColimitMonObj (RS.chainStage A M M') (RS.chainDelta A M M' d) (RS.chainMul A M M') ⋯ ⋯ (RS.chainSeed A M M' d) ⋯ ⋯ ⋯

theorem RS.chainB_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.IsCommMonObj (chainB A M M' d)

The splitting-chain algebra is commutative.

noncomputable def RS.chainBUnit {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] (d : ModDualityDatum A M M') : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ chainB A M M' d

The unit of the splitting-chain algebra: the seed at the bottom stage.

Equations

• RS.chainBUnit A M M' d = RS.chainColimitUnit (RS.chainStage A M M') (RS.chainDelta A M M' d) (RS.chainSeed A M M' d)