The bridge from the power chain to the splitting chain

The symmetriser projection carries the power-chain units to the splitting-chain units. Stagewise, a power stage maps to the matching splitting-chain stage by swapping the pair into copairing order and projecting both slots onto the symmetric powers; this projection carries the seed to the seed and intertwines the transitions, hence transports every power-chain unit to the corresponding splitting-chain unit. This is the wiring that connects the copairing powers of the duality datum to the stage units that the colimit detection speaks about.

Interchange coherence in a symmetric category

theorem RS.tensorμ_tensorμ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (a b c d : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ a b c d) (CategoryTheory.MonoidalCategory.tensorμ a c b d) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) (CategoryTheory.MonoidalCategoryStruct.tensorObj c d))

The interchange of the crossed middle pair undoes the interchange, in a symmetric category.

theorem RS.tensorμ_tensorμ_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (a b c d : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) (CategoryTheory.MonoidalCategoryStruct.tensorObj c d) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ a b c d) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ a c b d) h) = h

The interchange of the crossed middle pair undoes the interchange, in a symmetric category.

theorem RS.tensorμ_braiding_right {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (a b c d : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ a b c d) (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj a c) (CategoryTheory.MonoidalCategoryStruct.tensorObj b d)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (β_ a b).hom (β_ c d).hom) (CategoryTheory.MonoidalCategory.tensorμ b a d c)

The mirror of tensorμ_braiding: interchanging and then braiding the two blocks equals braiding slotwise and then interchanging in the exchanged order.

theorem RS.tensorμ_braiding_right_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (a b c d : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj b d) (CategoryTheory.MonoidalCategoryStruct.tensorObj a c) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ a b c d) (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj a c) (CategoryTheory.MonoidalCategoryStruct.tensorObj b d)).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (β_ a b).hom (β_ c d).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ b a d c) h)

The mirror of tensorμ_braiding: interchanging and then braiding the two blocks equals braiding slotwise and then interchanging in the exchanged order.

Commutativity of the projected power multiplication

theorem RS.braid_modPowMul_cast_symPowπ {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)] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) {c : ℕ} (h : b + a = c) (h' : a + b = c) : CategoryTheory.CategoryStruct.comp (β_ (modPow A X a) (modPow A X b)).hom (CategoryTheory.CategoryStruct.comp (modPowMul A X b a) (CategoryTheory.CategoryStruct.comp (modPowCast A X h) (symPowπ A X c))) = CategoryTheory.CategoryStruct.comp (modPowMul A X a b) (CategoryTheory.CategoryStruct.comp (modPowCast A X h') (symPowπ A X c))

The projected power multiplication is commutative: after the symmetriser projection, multiplying in the braided order and transporting the arity agrees with multiplying directly.

The stage projection

noncomputable def RS.projStage {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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (k : ℕ) : powStage A M M' k ⟶ chainStage A M M' k

The stage projection: a power stage maps to the matching splitting-chain stage by swapping the pair into copairing order and projecting both slots onto the symmetric powers.

Equations

• RS.projStage A M M' k = CategoryTheory.CategoryStruct.comp (RS.modTensorSwap A (RS.modPowMod A M.X k) (RS.modPowMod A M'.X k)) (RS.modTensorMap A (RS.symPowπMod A k) (RS.symPowπMod A k))

theorem RS.modTensorπ_projStage {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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (k : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modPowMod A M.X k) (modPowMod A M'.X k)) (projStage A M M' k) = CategoryTheory.CategoryStruct.comp (β_ (modPow A M.X (k + 1)) (modPow A M'.X (k + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowπ A M'.X (k + 1)) (symPowπ A M.X (k + 1))) (modTensorπ A (symPowMod A M'.X k) (symPowMod A M.X k)))

The stage projection under the stage projections of the coequalizers: the braiding of the factors followed by the symmetriser projections.

The zero stages

theorem RS.toModPowModZero_symPowπMod {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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (toModPowModZero A M) (symPowπMod A 0) = toSymPowModZero A M

The symmetriser projection carries the singleton power stage of a module to its singleton symmetric-power stage.

theorem RS.powSeed_projStage {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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (powSeed A M M' d) (projStage A M M' 0) = chainSeed A M M' d

The seed bridge: the stage projection carries the seed of the power chain to the seed of the splitting chain.

The multiplication bridge

theorem RS.powMulDesc_symPowπ {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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (powMulDesc A X m n) (symPowπ A X (m + 1 + n + 1)) = CategoryTheory.CategoryStruct.comp (modTensorMap A (symPowπMod A m) (symPowπMod A n)) (symMulDesc A X m n)

The multiplication bridge, at the carriers: the descended power multiplication followed by the symmetriser projection is the slotwise projection followed by the descended symmetric multiplication.

The transition bridge

theorem RS.projStage_mul {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) (k : ℕ) : CategoryTheory.CategoryStruct.comp (interchange A (modPowMod A M.X k) (modPowMod A M'.X k) (modPowMod A M.X 0) (modPowMod A M'.X 0)) (CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.comp (modTensorSwapMod A (modPowMod A M.X k) (modPowMod A M.X 0)) (CategoryTheory.CategoryStruct.comp (powMulMod A M.X 0 k) (modPowCastMod A M.X ⋯))) (powMulMod A M'.X k 0)) (projStage A M M' (k + 1))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (projStage A M M' k) (projStage A M M' 0)) (chainMul A M M' k 0)

The transition core: the interchange followed by the power multiplications and the stage projection is the slotwise stage projection followed by the chain multiplication.

theorem RS.powDelta_projStage {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') (k : ℕ) : CategoryTheory.CategoryStruct.comp (powDelta A M M' d k) (projStage A M M' (k + 1)) = CategoryTheory.CategoryStruct.comp (projStage A M M' k) (chainDelta A M M' d k)

The transition bridge: the stage projection intertwines the power-chain transition with the splitting-chain transition.

The unit bridge

theorem RS.powUnitStage_projStage {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') (k : ℕ) : CategoryTheory.CategoryStruct.comp (powUnitStage A M M' d k) (projStage A M M' k) = chainUnitStage A M M' d k

The unit bridge: the stage projection carries every power-chain unit to the corresponding splitting-chain unit. Together with the identification of the copairing powers as the power-chain units, this transports the copair element of the power datum to the stage units of the splitting chain.