The colimit algebra of the splitting chain

A chain of objects with one-step transitions has a filtered colimit over the v-small copy of ℕ. Given stagewise multiplications compatible with the transitions, the colimit carries a multiplication; given a bottom-stage unit with stagewise unit laws, it becomes a monoid object, commutative when the stagewise multiplication is commutative up to the index transport. The development is generic over any monoidal category in which tensoring preserves the chain colimits — the ind-category of a small monoidal category qualifies by RS.tensorLeft_ind_preservesColimitsOfShape and its right-hand twin — so the splitting chain of ChainDelta can be instantiated later with B n := chainStage A M M' n and δ n := chainDelta.

The multiplication is assembled in two passes of colimit.desc through the preservation isomorphisms, mirroring the merge pattern of BigTensor: first against a fixed stage in the second slot, then over the second slot. All colimit-level laws are cast-free because the stage inclusions absorb the index transports.

def RS.chainCast {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) {a b : ℕ} (h : a = b) : B a ⟶ B b

Transport of a chain object along an equality of indices.

Equations

• RS.chainCast B h = CategoryTheory.eqToHom ⋯

@[simp]

theorem RS.chainCast_rfl {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (a : ℕ) : chainCast B ⋯ = CategoryTheory.CategoryStruct.id (B a)

The trivial index transport is the identity.

@[simp]

theorem RS.chainCast_trans {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) {a b c : ℕ} (h : a = b) (h' : b = c) : CategoryTheory.CategoryStruct.comp (chainCast B h) (chainCast B h') = chainCast B ⋯

Index transports compose.

@[simp]

theorem RS.chainCast_trans_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) {a b c : ℕ} (h : a = b) (h' : b = c) {Z : E} (h✝ : B c ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainCast B h) (CategoryTheory.CategoryStruct.comp (chainCast B h') h✝) = CategoryTheory.CategoryStruct.comp (chainCast B ⋯) h✝

Index transports compose.

noncomputable def RS.chainDiagram {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) : CategoryTheory.Functor SmallNat E

The chain diagram over the v-small copy of ℕ, the shape at which the receiving category is assumed to have colimits.

Equations

• RS.chainDiagram B δ = RS.smallNatEquiv.inverse.comp (RS.chainFunctor B δ)

noncomputable def RS.chainColimit {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] : E

The colimit object of the chain.

Equations

• RS.chainColimit B δ = CategoryTheory.Limits.colimit (RS.chainDiagram B δ)

noncomputable def RS.chainColimitι {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (n : ℕ) : B n ⟶ chainColimit B δ

The stage inclusion into the chain colimit.

Equations

• RS.chainColimitι B δ n = CategoryTheory.Limits.colimit.ι (RS.chainDiagram B δ) (RS.smallNatEquiv.functor.obj n)

@[simp]

theorem RS.chainMap_chainColimitι {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {a b : ℕ} (h : a ≤ b) : CategoryTheory.CategoryStruct.comp (chainMap B δ h) (chainColimitι B δ b) = chainColimitι B δ a

The chain morphisms are absorbed by the stage inclusions.

@[simp]

theorem RS.chainMap_chainColimitι_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {a b : ℕ} (h : a ≤ b) {Z : E} (h✝ : chainColimit B δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainMap B δ h) (CategoryTheory.CategoryStruct.comp (chainColimitι B δ b) h✝) = CategoryTheory.CategoryStruct.comp (chainColimitι B δ a) h✝

The chain morphisms are absorbed by the stage inclusions.

@[simp]

theorem RS.delta_chainColimitι {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (n : ℕ) : CategoryTheory.CategoryStruct.comp (δ n) (chainColimitι B δ (n + 1)) = chainColimitι B δ n

The transitions are absorbed by the stage inclusions.

@[simp]

theorem RS.delta_chainColimitι_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (n : ℕ) {Z : E} (h : chainColimit B δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ n) (CategoryTheory.CategoryStruct.comp (chainColimitι B δ (n + 1)) h) = CategoryTheory.CategoryStruct.comp (chainColimitι B δ n) h

The transitions are absorbed by the stage inclusions.

@[simp]

theorem RS.chainCast_chainColimitι {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {a b : ℕ} (h : a = b) : CategoryTheory.CategoryStruct.comp (chainCast B h) (chainColimitι B δ b) = chainColimitι B δ a

The index transports are absorbed by the stage inclusions.

@[simp]

theorem RS.chainCast_chainColimitι_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {a b : ℕ} (h : a = b) {Z : E} (h✝ : chainColimit B δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainCast B h) (CategoryTheory.CategoryStruct.comp (chainColimitι B δ b) h✝) = CategoryTheory.CategoryStruct.comp (chainColimitι B δ a) h✝

The index transports are absorbed by the stage inclusions.

theorem RS.chainColimit_hom_ext {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] {Z : E} {f g : chainColimit B δ ⟶ Z} (w : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (chainColimitι B δ n) f = CategoryTheory.CategoryStruct.comp (chainColimitι B δ n) g) : f = g

Maps out of the chain colimit agree once they agree on all stages.

The colimit multiplication

Stagewise multiplications compatible with the transitions assemble into a multiplication on the chain colimit. The two compatibility squares are taken as hypotheses; only the left one needs an index transport, since (i + 1) + 1 + j is not definitionally (i + 1 + j) + 1.

theorem RS.mul_chainMap_ι_left {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) {i i' : ℕ} (h : i ≤ i') (j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainMap B δ h) (B j)) (CategoryTheory.CategoryStruct.comp (mu i' j) (chainColimitι B δ (i' + 1 + j))) = CategoryTheory.CategoryStruct.comp (mu i j) (chainColimitι B δ (i + 1 + j))

Multiplying after a chain morphism in the first slot agrees with multiplying first, once both land in the colimit.

theorem RS.mul_chainMap_ι_right {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) (i : ℕ) {j j' : ℕ} (h : j ≤ j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (chainMap B δ h)) (CategoryTheory.CategoryStruct.comp (mu i j') (chainColimitι B δ (i + 1 + j'))) = CategoryTheory.CategoryStruct.comp (mu i j) (chainColimitι B δ (i + 1 + j))

Multiplying after a chain morphism in the second slot agrees with multiplying first, once both land in the colimit.

noncomputable def RS.chainMulCocone {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (j : ℕ) : CategoryTheory.Limits.Cocone ((chainDiagram B δ).comp (CategoryTheory.MonoidalCategory.tensorRight (B j)))

The multiply-then-include maps against a fixed stage in the second slot form a cocone on the chain diagram tensored on the right with that stage.

Equations

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

noncomputable def RS.chainMulStage {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] (j : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainColimit B δ) (B j) ⟶ chainColimit B δ

Partial multiplication of the chain colimit against a fixed stage in the second slot.

Equations

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

theorem RS.ι_chainMulStage {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitι B δ i) (B j)) (chainMulStage B δ mu hδl j) = CategoryTheory.CategoryStruct.comp (mu i j) (chainColimitι B δ (i + 1 + j))

On a stage, the partial multiplication is multiply-then-include.

theorem RS.ι_chainMulStage_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] (i j : ℕ) {Z : E} (h : chainColimit B δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitι B δ i) (B j)) (CategoryTheory.CategoryStruct.comp (chainMulStage B δ mu hδl j) h) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (chainColimitι B δ (i + 1 + j)) h)

On a stage, the partial multiplication is multiply-then-include.

theorem RS.chainColimit_tensorRight_hom_ext {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] {X Z : E} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainColimit B δ) X ⟶ Z} (w : ∀ (i : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitι B δ i) X) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitι B δ i) X) g) : f = g

Maps out of the chain colimit tensored on the right are determined by their restrictions to the stages.

theorem RS.chainMulStage_natural {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] {j j' : ℕ} (h : j ≤ j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainColimit B δ) (chainMap B δ h)) (chainMulStage B δ mu hδl j') = chainMulStage B δ mu hδl j

The partial multiplications are natural in the stage.

theorem RS.chainMulStage_natural_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] {j j' : ℕ} (h : j ≤ j') {Z : E} (h✝ : chainColimit B δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainColimit B δ) (chainMap B δ h)) (CategoryTheory.CategoryStruct.comp (chainMulStage B δ mu hδl j') h✝) = CategoryTheory.CategoryStruct.comp (chainMulStage B δ mu hδl j) h✝

The partial multiplications are natural in the stage.

theorem RS.tensorLeft_chainColimit_hom_ext {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] {X Z : E} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X (chainColimit B δ) ⟶ Z} (w : ∀ (j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (chainColimitι B δ j)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (chainColimitι B δ j)) g) : f = g

Maps out of the chain colimit tensored on the left are determined by their restrictions to the stages.

noncomputable def RS.chainMulTotalCocone {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.Limits.Cocone ((chainDiagram B δ).comp (CategoryTheory.MonoidalCategory.tensorLeft (chainColimit B δ)))

The partial multiplications form a cocone on the chain diagram tensored on the left with the chain colimit.

Equations

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

noncomputable def RS.chainColimitMul {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainColimit B δ) (chainColimit B δ) ⟶ chainColimit B δ

The colimit multiplication: the partial multiplications assembled over the second slot.

Equations

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

theorem RS.whiskerLeft_ι_chainColimitMul {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainColimit B δ) (chainColimitι B δ j)) (chainColimitMul B δ mu hδl hδr) = chainMulStage B δ mu hδl j

On a stage in the second slot, the colimit multiplication is the partial multiplication.

theorem RS.whiskerLeft_ι_chainColimitMul_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (j : ℕ) {Z : E} (h : chainColimit B δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainColimit B δ) (chainColimitι B δ j)) (CategoryTheory.CategoryStruct.comp (chainColimitMul B δ mu hδl hδr) h) = CategoryTheory.CategoryStruct.comp (chainMulStage B δ mu hδl j) h

On a stage in the second slot, the colimit multiplication is the partial multiplication.

theorem RS.ι_tensorHom_chainColimitMul {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δ i) (chainColimitι B δ j)) (chainColimitMul B δ mu hδl hδr) = CategoryTheory.CategoryStruct.comp (mu i j) (chainColimitι B δ (i + 1 + j))

Defining equation of the colimit multiplication: on a pair of stages it is multiply-then-include.

theorem RS.ι_tensorHom_chainColimitMul_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (i j : ℕ) {Z : E} (h : chainColimit B δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δ i) (chainColimitι B δ j)) (CategoryTheory.CategoryStruct.comp (chainColimitMul B δ mu hδl hδr) h) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (chainColimitι B δ (i + 1 + j)) h)

Defining equation of the colimit multiplication: on a pair of stages it is multiply-then-include.

noncomputable def RS.chainMulLCocone {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) (i : ℕ) : CategoryTheory.Limits.Cocone ((chainDiagram B δ).comp (CategoryTheory.MonoidalCategory.tensorLeft (B i)))

The multiply-then-include maps against a fixed stage in the first slot form a cocone on the chain diagram tensored on the left with that stage.

Equations

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

noncomputable def RS.chainMulStageL {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (i : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (chainColimit B δ) ⟶ chainColimit B δ

Partial multiplication of a fixed stage in the first slot against the chain colimit.

Equations

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

theorem RS.ι_chainMulStageL {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (chainColimitι B δ j)) (chainMulStageL B δ mu hδr i) = CategoryTheory.CategoryStruct.comp (mu i j) (chainColimitι B δ (i + 1 + j))

On a stage, the left partial multiplication is multiply-then-include.

theorem RS.ι_chainMulStageL_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (i j : ℕ) {Z : E} (h : chainColimit B δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (chainColimitι B δ j)) (CategoryTheory.CategoryStruct.comp (chainMulStageL B δ mu hδr i) h) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (chainColimitι B δ (i + 1 + j)) h)

On a stage, the left partial multiplication is multiply-then-include.

theorem RS.ι_whiskerRight_chainColimitMul {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (i : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitι B δ i) (chainColimit B δ)) (chainColimitMul B δ mu hδl hδr) = chainMulStageL B δ mu hδr i

On a stage in the first slot, the colimit multiplication is the left partial multiplication.

theorem RS.ι_whiskerRight_chainColimitMul_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (i : ℕ) {Z : E} (h : chainColimit B δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitι B δ i) (chainColimit B δ)) (CategoryTheory.CategoryStruct.comp (chainColimitMul B δ mu hδl hδr) h) = CategoryTheory.CategoryStruct.comp (chainMulStageL B δ mu hδr i) h

On a stage in the first slot, the colimit multiplication is the left partial multiplication.

theorem RS.chainColimit_pair_hom_ext {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] {Z : E} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainColimit B δ) (chainColimit B δ) ⟶ Z} (w : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δ i) (chainColimitι B δ j)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δ i) (chainColimitι B δ j)) g) : f = g

Maps out of the tensor square of the chain colimit are determined by pairs of stages.

theorem RS.chainColimit_sandwich_hom_ext {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (X Y : E) {Z : E} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj (chainColimit B δ) Y) ⟶ Z} (w : ∀ (j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitι B δ j) Y)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitι B δ j) Y)) g) : f = g

Sandwich extensionality: maps out of a tensor product with the chain colimit in the middle slot are determined by the stages there.

The unit and the monoid laws

The colimit unit is the bottom-stage unit followed by the stage inclusion. The monoid laws hold on the colimit whenever their stagewise forms hold; the index transports disappear into the stage inclusions.

noncomputable def RS.chainColimitUnit {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit E ⟶ B 0) : CategoryTheory.MonoidalCategoryStruct.tensorUnit E ⟶ chainColimit B δ

The colimit unit: the bottom-stage unit followed by the stage inclusion.

Equations

• RS.chainColimitUnit B δ u = CategoryTheory.CategoryStruct.comp u (RS.chainColimitι B δ 0)

theorem RS.chainColimit_one_mul {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit E ⟶ B 0) (hul : ∀ (j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u (B j)) (mu 0 j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (B j)).hom (chainMap B δ ⋯)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitUnit B δ u) (chainColimit B δ)) (chainColimitMul B δ mu hδl hδr) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (chainColimit B δ)).hom

Left unit law of the colimit multiplication, from the stagewise left unit law.

theorem RS.chainColimit_mul_one {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit E ⟶ B 0) (hur : ∀ (i : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) u) (mu i 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (B i)).hom (δ i)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainColimit B δ) (chainColimitUnit B δ u)) (chainColimitMul B δ mu hδl hδr) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (chainColimit B δ)).hom

Right unit law of the colimit multiplication, from the stagewise right unit law.

theorem RS.mul_assoc_ι {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hassoc : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mu i j) (B k)) (mu (i + 1 + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (B i) (B j) (B k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (mu j k)) (CategoryTheory.CategoryStruct.comp (mu i (j + 1 + k)) (chainCast B ⋯)))) (i j k : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mu i j) (B k)) (CategoryTheory.CategoryStruct.comp (mu (i + 1 + j) k) (chainColimitι B δ (i + 1 + j + 1 + k))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (B i) (B j) (B k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (mu j k)) (CategoryTheory.CategoryStruct.comp (mu i (j + 1 + k)) (chainColimitι B δ (i + 1 + (j + 1 + k)))))

Stagewise associativity, pushed into the colimit: the index transport is absorbed by the stage inclusion.

theorem RS.chainColimit_mul_assoc {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (hassoc : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mu i j) (B k)) (mu (i + 1 + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (B i) (B j) (B k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (mu j k)) (CategoryTheory.CategoryStruct.comp (mu i (j + 1 + k)) (chainCast B ⋯)))) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainColimitMul B δ mu hδl hδr) (chainColimit B δ)) (chainColimitMul B δ mu hδl hδr) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (chainColimit B δ) (chainColimit B δ) (chainColimit B δ)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainColimit B δ) (chainColimitMul B δ mu hδl hδr)) (chainColimitMul B δ mu hδl hδr))

Associativity of the colimit multiplication, from stagewise associativity.

@[reducible]

noncomputable def RS.chainColimitMonObj {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit E ⟶ B 0) (hul : ∀ (j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u (B j)) (mu 0 j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (B j)).hom (chainMap B δ ⋯)) (hur : ∀ (i : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) u) (mu i 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (B i)).hom (δ i)) (hassoc : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mu i j) (B k)) (mu (i + 1 + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (B i) (B j) (B k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (mu j k)) (CategoryTheory.CategoryStruct.comp (mu i (j + 1 + k)) (chainCast B ⋯)))) : CategoryTheory.MonObj (chainColimit B δ)

The chain colimit as a monoid object: the unit is the included bottom-stage unit and the multiplication is assembled from the stagewise multiplications.

Equations

• RS.chainColimitMonObj B δ mu hδl hδr u hul hur hassoc = { one := RS.chainColimitUnit B δ u, mul := RS.chainColimitMul B δ mu hδl hδr, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

Commutativity

theorem RS.mul_comm_ι {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) [CategoryTheory.BraidedCategory E] (hcomm : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (β_ (B i) (B j)).hom (CategoryTheory.CategoryStruct.comp (mu j i) (chainCast B ⋯)) = mu i j) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (β_ (B i) (B j)).hom (CategoryTheory.CategoryStruct.comp (mu j i) (chainColimitι B δ (j + 1 + i))) = CategoryTheory.CategoryStruct.comp (mu i j) (chainColimitι B δ (i + 1 + j))

Stagewise commutativity, pushed into the colimit: the index transport is absorbed by the stage inclusion.

theorem RS.chainColimitMul_comm {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.BraidedCategory E] (hcomm : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (β_ (B i) (B j)).hom (CategoryTheory.CategoryStruct.comp (mu j i) (chainCast B ⋯)) = mu i j) : CategoryTheory.CategoryStruct.comp (β_ (chainColimit B δ) (chainColimit B δ)).hom (chainColimitMul B δ mu hδl hδr) = chainColimitMul B δ mu hδl hδr

Commutativity of the colimit multiplication, from stagewise commutativity up to the index transport.

theorem RS.chainColimit_isCommMonObj {E : Type u} [CategoryTheory.Category.{v, u} E] (B : ℕ → E) (δ : (n : ℕ) → B n ⟶ B (n + 1)) [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] [CategoryTheory.MonoidalCategory E] (mu : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + 1 + j)) (hδl : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (δ i) (B j)) (mu (i + 1) j) = CategoryTheory.CategoryStruct.comp (mu i j) (CategoryTheory.CategoryStruct.comp (δ (i + 1 + j)) (chainCast B ⋯))) (hδr : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (δ j)) (mu i (j + 1)) = CategoryTheory.CategoryStruct.comp (mu i j) (δ (i + 1 + j))) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit E ⟶ B 0) [CategoryTheory.BraidedCategory E] (hul : ∀ (j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u (B j)) (mu 0 j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (B j)).hom (chainMap B δ ⋯)) (hur : ∀ (i : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) u) (mu i 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (B i)).hom (δ i)) (hassoc : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mu i j) (B k)) (mu (i + 1 + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (B i) (B j) (B k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (mu j k)) (CategoryTheory.CategoryStruct.comp (mu i (j + 1 + k)) (chainCast B ⋯)))) (hcomm : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (β_ (B i) (B j)).hom (CategoryTheory.CategoryStruct.comp (mu j i) (chainCast B ⋯)) = mu i j) : CategoryTheory.IsCommMonObj (chainColimit B δ)

The chain colimit as a commutative monoid object: stagewise commutativity makes the packaged monoid structure commutative.

The ind-category instantiation

Over the ind-category of a small monoidal category the generic development applies verbatim: the shape has colimits, tensoring preserves them (IndTensorExact), and the generic chain diagram is the chain functor of ChainUnit, so the nonvanishing criterion for the colimit unit transfers to the packaged unit.

theorem RS.chainColimitUnit_eq_zero_iff {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] (B : ℕ → CategoryTheory.Ind C) (δ : (n : ℕ) → B n ⟶ B (n + 1)) (u : (n : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ B n) (hu : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (u n) (δ n) = u (n + 1)) : chainColimitUnit B δ (u 0) = 0 ↔ ∃ (n : ℕ), u n = 0

Nonvanishing of the colimit unit: over the ind-category, the colimit unit built from a compatible family of stage units vanishes exactly when the family dies at a finite stage.