Commutativity and associativity of the chain multiplication

The chain multiplication braids and reassociates exactly as the symmetric multiplication it descends from. Both laws are proved by cancelling the jointly epimorphic stage projections and reducing to the corresponding symMul laws together with the coherence of the interchange tensorμ. Transports of chain stages along equalities of arities are packaged as chainStageCast.

Stage transports

noncomputable def RS.chainStageCast {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) {j k : ℕ} (h : j = k) : chainStage A M M' j ⟶ chainStage A M M' k

Transport of a chain stage along an equality of arities.

Equations

• RS.chainStageCast A M M' h = CategoryTheory.eqToHom ⋯

@[simp]

theorem RS.chainStageCast_rfl {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 : ℕ) : chainStageCast A M M' ⋯ = CategoryTheory.CategoryStruct.id (chainStage A M M' k)

The trivial transport is the identity.

@[simp]

theorem RS.chainStageCast_trans {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) {i j k : ℕ} (h : i = j) (h' : j = k) : CategoryTheory.CategoryStruct.comp (chainStageCast A M M' h) (chainStageCast A M M' h') = chainStageCast A M M' ⋯

Stage transports compose.

@[simp]

theorem RS.chainStageCast_trans_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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) {i j k : ℕ} (h : i = j) (h' : j = k) {Z : D} (h✝ : chainStage A M M' k ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainStageCast A M M' h) (CategoryTheory.CategoryStruct.comp (chainStageCast A M M' h') h✝) = CategoryTheory.CategoryStruct.comp (chainStageCast A M M' ⋯) h✝

Stage transports compose.

theorem RS.modTensorπ_chainStageCast {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) {j k : ℕ} (h : j = k) : CategoryTheory.CategoryStruct.comp (modTensorπ A (symPowMod A M'.X j) (symPowMod A M.X j)) (chainStageCast A M M' h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowCast A M'.X ⋯) (symPowCast A M.X ⋯)) (modTensorπ A (symPowMod A M'.X k) (symPowMod A M.X k))

The stage projection intertwines the symmetric-power and stage transports.

theorem RS.modTensorπ_chainStageCast_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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) {j k : ℕ} (h : j = k) {Z : D} (h✝ : chainStage A M M' k ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (modTensorπ A (symPowMod A M'.X j) (symPowMod A M.X j)) (chainStageCast A M M' h)) h✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowCast A M'.X ⋯) (symPowCast A M.X ⋯)) (modTensorπ A (symPowMod A M'.X k) (symPowMod A M.X k))) h✝

The stage projection intertwines the symmetric-power and stage transports.

Epimorphy of whiskered stage projections

instance RS.epi_modTensorπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (N P : CategoryTheory.Mod D A) : CategoryTheory.Epi (modTensorπ A N P)

The module-tensor projection is an epimorphism.

instance RS.epi_modTensorπ_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] (N P : CategoryTheory.Mod D A) (W : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N P) W)

The right-whiskered module-tensor projection is an epimorphism.

instance RS.epi_whiskerLeft_modTensorπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (N P : CategoryTheory.Mod D A) (Q : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (modTensorπ A N P))

The left-whiskered module-tensor projection is an epimorphism.

noncomputable def RS.modTensorWhiskerRLIsColimit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers 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] (N P : CategoryTheory.Mod D A) (W Q : D) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N P) W)) ⋯)

Whiskering the module-tensor coequalizer on the right and then on the left still yields a colimit cofork.

Equations

• RS.modTensorWhiskerRLIsColimit A N P W Q = CategoryTheory.Limits.isColimitCoforkMapOfIsColimit (CategoryTheory.MonoidalCategory.tensorLeft Q) ⋯ (RS.modTensorWhiskerRIsColimit A N P W)

instance RS.epi_whiskerLeft_modTensorπ_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers 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] (N P : CategoryTheory.Mod D A) (W Q : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N P) W))

The doubly whiskered module-tensor projection is an epimorphism.

instance RS.epi_modTensorπ_whiskerRight_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] (N P : CategoryTheory.Mod D A) (V W : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N P) V) W)

A projection whiskered on the right by two objects is an epimorphism.

instance RS.epi_whiskerLeft_modTensorπ_whiskerRight' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers 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] (N P : CategoryTheory.Mod D A) (Q W : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (modTensorπ A N P)) W)

A projection whiskered on the left and then on the right is an epimorphism.

instance RS.epi_whiskerLeft_whiskerLeft_modTensorπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (N P : CategoryTheory.Mod D A) (Q R : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (modTensorπ A N P)))

A projection whiskered on the left by two objects is an epimorphism.

instance RS.epi_modTensorπ_tensorHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers 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] (N P Q R : CategoryTheory.Mod D A) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.tensorHom (modTensorπ A N P) (modTensorπ A Q R))

The tensor product of two module-tensor projections is an epimorphism.

instance RS.epi_modTensorπ_tensorHom_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers 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] (N P Q R : CategoryTheory.Mod D A) (W : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom (modTensorπ A N P) (modTensorπ A Q R)) W)

The right-whiskered tensor product of two projections is an epimorphism.

instance RS.epi_modTensorπ_tensorHom_whiskerLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers 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] (N P Q R : CategoryTheory.Mod D A) (W : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.tensorHom (modTensorπ A N P) (modTensorπ A Q R)))

The left-whiskered tensor product of two projections is an epimorphism.

instance RS.epi_modTensorπ_tensorHom_tensorHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers 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] (N P Q R S T : CategoryTheory.Mod D A) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (modTensorπ A N P) (modTensorπ A Q R)) (modTensorπ A S T))

The tensored triple of module-tensor projections is an epimorphism.

Symmetric-power laws with transported arities

Commutativity of the chain multiplication

theorem RS.chainMul_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)] [∀ (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) (m n : ℕ) : CategoryTheory.CategoryStruct.comp (β_ (chainStage A M M' m) (chainStage A M M' n)).hom (CategoryTheory.CategoryStruct.comp (chainMul A M M' n m) (chainStageCast A M M' ⋯)) = chainMul A M M' m n

Commutativity of the chain multiplication, up to the stage transport of n + 1 + m = m + 1 + n.

Tensor surgery and the associativity core

Associativity of the chain multiplication

theorem RS.chainMul_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)] [∀ (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) (m n p : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainMul A M M' m n) (chainStage A M M' p)) (CategoryTheory.CategoryStruct.comp (chainMul A M M' (m + 1 + n) p) (chainStageCast A M M' ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (chainStage A M M' m) (chainStage A M M' n) (chainStage A M M' p)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainStage A M M' m) (chainMul A M M' n p)) (CategoryTheory.CategoryStruct.comp (chainMul A M M' m (n + 1 + p)) (chainStageCast A M M' ⋯)))

Associativity of the chain multiplication, up to the stage transports onto the common arity m + 1 + n + 1 + p.