The tensor product of an arbitrary family of monoid objects

Infrastructure for Deligne's 2.11: in a braided monoidal category D with filtered colimits, an arbitrary family B : ι → D of (commutative) monoid objects has a tensor product, defined as the filtered colimit of the tensor products of its finite subfamilies.

The index type carries a linear order, which fixes the ordering of the tensor slots: the finite sub-tensor-product over s : Finset ι is the fold of B over the sorted list of s. For s ⊆ t there is an insertion morphism which places the unit of the missing factors into the extra slots; these are the transition maps of a Finset ι-shaped diagram, and the big tensor product is its colimit.

Finite tensor products

def RS.listTensor {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) : List ι → D

The tensor product of the factors B i over a list of indices, folded to the right with the unit object as seed.

Equations

• RS.listTensor B [] = CategoryTheory.MonoidalCategoryStruct.tensorUnit D
• RS.listTensor B (i :: l) = CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (RS.listTensor B l)

@[simp]

theorem RS.listTensor_nil {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) : listTensor B [] = CategoryTheory.MonoidalCategoryStruct.tensorUnit D

@[simp]

theorem RS.listTensor_cons {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) (i : ι) (l : List ι) : listTensor B (i :: l) = CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (listTensor B l)

def RS.finTensor {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) (s : Finset ι) : D

The tensor product of the factors B i over a finite set of indices, in the slot order given by the linear order on ι.

Equations

• RS.finTensor B s = RS.listTensor B (s.sort fun (x1 x2 : ι) => x1 ≤ x2)

@[simp]

theorem RS.finTensor_empty {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) : finTensor B ∅ = CategoryTheory.MonoidalCategoryStruct.tensorUnit D

@[simp]

theorem RS.finTensor_singleton {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) (i : ι) : finTensor B {i} = CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

@[instance_reducible]

instance RS.listTensorMon {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (l : List ι) : CategoryTheory.MonObj (listTensor B l)

The finite tensor products of a family of monoid objects are monoid objects, by folding the binary braided instance.

Equations

• One or more equations did not get rendered due to their size.
• RS.listTensorMon B [] = { one := RS.listTensorMon._aux_1 B, mul := RS.listTensorMon._aux_3 B, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

@[instance_reducible]

instance RS.finTensorMon {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (s : Finset ι) : CategoryTheory.MonObj (finTensor B s)

Equations

• RS.finTensorMon B s = RS.finTensorMon._aux_1 B s

instance RS.listTensorCommMon {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [∀ (i : ι), CategoryTheory.IsCommMonObj (B i)] (l : List ι) : CategoryTheory.IsCommMonObj (listTensor B l)

Finite tensor products of commutative monoid objects are commutative, by folding the binary instance of the symmetric category.

instance RS.finTensorCommMon {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [∀ (i : ι), CategoryTheory.IsCommMonObj (B i)] (s : Finset ι) : CategoryTheory.IsCommMonObj (finTensor B s)

Insertion of units

instance RS.isMonHom_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (M : D) [CategoryTheory.MonObj M] : CategoryTheory.IsMonHom CategoryTheory.MonObj.one

The unit η[M] : 𝟙_ D ⟶ M is a morphism of monoid objects from the trivial monoid.

def RS.unitIncl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (M X : D) [CategoryTheory.MonObj M] : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M X

Insertion of the unit of the monoid M in the front slot.

Equations

• RS.unitIncl M X = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)

theorem RS.unitIncl_eq_tensorHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (M X : D) [CategoryTheory.MonObj M] : unitIncl M X = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.id X))

theorem RS.unitIncl_naturality {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (M : D) [CategoryTheory.MonObj M] {X Y : D} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (unitIncl M Y) = CategoryTheory.CategoryStruct.comp (unitIncl M X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f)

theorem RS.unitIncl_naturality_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (M : D) [CategoryTheory.MonObj M] {X Y : D} (f : X ⟶ Y) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (unitIncl M Y) h) = CategoryTheory.CategoryStruct.comp (unitIncl M X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f) h)

instance RS.isMonHom_unitIncl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (M X : D) [CategoryTheory.MonObj M] [CategoryTheory.MonObj X] : CategoryTheory.IsMonHom (unitIncl M X)

Inclusions of finite tensor products

The inclusion of a sub-tensor-product is defined at the level of lists: for a Boolean predicate p, the tensor product over l.filter p maps into the tensor product over l by inserting the unit of each factor whose index fails p.

def RS.inclFilter {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (p : ι → Bool) (l : List ι) : listTensor B (List.filter p l) ⟶ listTensor B l

Insertion morphism from the tensor product over the filtered list into the tensor product over the full list, placing units in the slots dropped by the filter.

Convention: all stated morphisms have listTensor-form endpoints; the tensor-shaped intermediate objects appear only between explicit eqToHom guards, so that every composition in the subsequent lemmas is well typed on the nose.

Equations

• One or more equations did not get rendered due to their size.
• RS.inclFilter B p [] = CategoryTheory.CategoryStruct.id (RS.listTensor B (List.filter p []))

@[simp]

theorem RS.inclFilter_nil {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (p : ι → Bool) : inclFilter B p [] = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

theorem RS.inclFilter_cons_pos {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (p : ι → Bool) {i : ι} (l : List ι) (h : p i = true) : inclFilter B p (i :: l) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (B i) (inclFilter B p l)) (CategoryTheory.eqToHom ⋯))

theorem RS.inclFilter_cons_neg {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (p : ι → Bool) {i : ι} (l : List ι) (h : ¬p i = true) : inclFilter B p (i :: l) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (inclFilter B p l) (CategoryTheory.CategoryStruct.comp (unitIncl (B i) (listTensor B l)) (CategoryTheory.eqToHom ⋯)))

theorem RS.inclFilter_congr {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (p : ι → Bool) {l₁ l₂ : List ι} (h : l₁ = l₂) : inclFilter B p l₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (inclFilter B p l₂) (CategoryTheory.eqToHom ⋯))

Equal index lists give equal (conjugated) insertions.

theorem RS.inclFilter_congr_pred {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] {p q : ι → Bool} (h : p = q) (l : List ι) : inclFilter B p l = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (inclFilter B q l)

Equal predicates give equal (transported) insertions.

theorem RS.isMonHom_eqToHom {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.BraidedCategory D] {l₁ l₂ : List ι} (h : l₁ = l₂) (q : listTensor B l₁ = listTensor B l₂) : CategoryTheory.IsMonHom (CategoryTheory.eqToHom q)

Transporting along an equality of index lists is a morphism of monoid objects.

instance RS.isMonHom_inclFilter {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.BraidedCategory D] (p : ι → Bool) (l : List ι) : CategoryTheory.IsMonHom (inclFilter B p l)

The insertions are morphisms of monoid objects.

theorem RS.inclFilter_of_forall {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (p : ι → Bool) (l : List ι) (h : ∀ i ∈ l, p i = true) : inclFilter B p l = CategoryTheory.eqToHom ⋯

Inserting nothing: if every index passes the filter, the insertion is the transport of the identity.

theorem RS.inclFilter_inclFilter {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (p q : ι → Bool) (l : List ι) : CategoryTheory.CategoryStruct.comp (inclFilter B p (List.filter q l)) (inclFilter B q l) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (inclFilter B (fun (i : ι) => p i && q i) l)

The composition law for insertions: inserting the units of l.filter q past p and then those of l past q is the insertion past the conjunction. This is the coherence heart of the transition maps of the big tensor product.

Bridging lemmas for the units of the fold monoids.

theorem RS.listTensor_one_eq {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.BraidedCategory D] {l : List ι} (h : l = []) : CategoryTheory.MonObj.one = CategoryTheory.eqToHom ⋯

On a vanishing index list, the unit of the fold monoid is the canonical identification with the monoidal unit.

Inclusions between finite sub-tensor-products

theorem RS.sort_filter_of_subset {ι : Type v} [LinearOrder ι] {s t : Finset ι} (h : s ⊆ t) : List.filter (fun (i : ι) => decide (i ∈ s)) (t.sort fun (x1 x2 : ι) => x1 ≤ x2) = s.sort fun (x1 x2 : ι) => x1 ≤ x2

Sorting commutes with restriction: the sorted list of a subset of t is the filtering of the sorted list of t.

def RS.finTensorIncl {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] {s t : Finset ι} (h : s ⊆ t) : finTensor B s ⟶ finTensor B t

The inclusion of the finite sub-tensor-product over s ⊆ t, inserting the units of the factors missing from s.

Equations

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

@[simp]

theorem RS.finTensorIncl_refl {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (s : Finset ι) : finTensorIncl B ⋯ = CategoryTheory.CategoryStruct.id (finTensor B s)

theorem RS.finTensorIncl_trans {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] {s t u : Finset ι} (hst : s ⊆ t) (htu : t ⊆ u) : CategoryTheory.CategoryStruct.comp (finTensorIncl B hst) (finTensorIncl B htu) = finTensorIncl B ⋯

Functoriality of the inclusions of sub-tensor-products.

theorem RS.finTensorIncl_trans_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] {s t u : Finset ι} (hst : s ⊆ t) (htu : t ⊆ u) {Z : D} (h : finTensor B u ⟶ Z) : CategoryTheory.CategoryStruct.comp (finTensorIncl B hst) (CategoryTheory.CategoryStruct.comp (finTensorIncl B htu) h) = CategoryTheory.CategoryStruct.comp (finTensorIncl B ⋯) h

Functoriality of the inclusions of sub-tensor-products.

instance RS.isMonHom_finTensorIncl {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.BraidedCategory D] {s t : Finset ι} (h : s ⊆ t) : CategoryTheory.IsMonHom (finTensorIncl B h)

The inclusions of sub-tensor-products are morphisms of monoid objects.

The big tensor product as a filtered colimit

def RS.finTensorDiagram {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] : CategoryTheory.Functor (Finset ι) D

The Finset ι-shaped diagram of finite sub-tensor-products, with the unit insertions as transition maps.

Equations

• RS.finTensorDiagram B = { obj := fun (s : Finset ι) => RS.finTensor B s, map := fun {X Y : Finset ι} (f : X ⟶ Y) => RS.finTensorIncl B ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem RS.finTensorDiagram_map {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] {X✝ Y✝ : Finset ι} (f : X✝ ⟶ Y✝) : (finTensorDiagram B).map f = finTensorIncl B ⋯

@[simp]

theorem RS.finTensorDiagram_obj {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (s : Finset ι) : (finTensorDiagram B).obj s = finTensor B s

noncomputable def RS.bigTensor {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] : D

The tensor product of the whole family B, as the filtered colimit of its finite sub-tensor-products.

Equations

• RS.bigTensor B = CategoryTheory.Limits.colimit (RS.finTensorDiagram B)

noncomputable def RS.bigTensorStage {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] (s : Finset ι) : finTensor B s ⟶ bigTensor B

The stage inclusion of a finite sub-tensor-product into the big tensor product.

Equations

• RS.bigTensorStage B s = CategoryTheory.Limits.colimit.ι (RS.finTensorDiagram B) s

@[simp]

theorem RS.finTensorIncl_bigTensorStage {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] {s t : Finset ι} (h : s ⊆ t) : CategoryTheory.CategoryStruct.comp (finTensorIncl B h) (bigTensorStage B t) = bigTensorStage B s

Stage inclusions are compatible with the insertions.

@[simp]

theorem RS.finTensorIncl_bigTensorStage_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] {s t : Finset ι} (h : s ⊆ t) {Z : D} (h✝ : bigTensor B ⟶ Z) : CategoryTheory.CategoryStruct.comp (finTensorIncl B h) (CategoryTheory.CategoryStruct.comp (bigTensorStage B t) h✝) = CategoryTheory.CategoryStruct.comp (bigTensorStage B s) h✝

Stage inclusions are compatible with the insertions.

noncomputable def RS.bigTensorUnit {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ bigTensor B

The unit of the big tensor product: the empty stage.

Equations

• RS.bigTensorUnit B = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (RS.bigTensorStage B ∅)

noncomputable def RS.bigTensorOf {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] (i : ι) : B i ⟶ bigTensor B

The inclusion of a single factor, through the stage at the singleton.

Equations

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

The unit against the stages

theorem RS.finTensor_one_def {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (s : Finset ι) : CategoryTheory.MonObj.one = CategoryTheory.MonObj.one

theorem RS.finTensor_one_empty {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] : CategoryTheory.MonObj.one = CategoryTheory.eqToHom ⋯

The unit of the empty stage is the canonical identification with the monoidal unit.

theorem RS.bigTensorUnit_stage {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] (s : Finset ι) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (bigTensorStage B s) = bigTensorUnit B

The unit of the big tensor product is reached from the unit of any finite stage.

Merge maps

The multiplication of the big tensor product is presented on the finite stages by the merge maps: include both stages into their union, then multiply there. This section provides the merge maps together with their coherence squares.

theorem RS.finTensorIncl_empty {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (u : Finset ι) : finTensorIncl B ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) CategoryTheory.MonObj.one

The inclusion of the empty stage is the unit.

def RS.finTensorMul {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (s t : Finset ι) : CategoryTheory.MonoidalCategoryStruct.tensorObj (finTensor B s) (finTensor B t) ⟶ finTensor B (s ∪ t)

The merge map of two finite stages: include both into the union stage and multiply there.

Equations

• RS.finTensorMul B s t = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (RS.finTensorIncl B ⋯) (RS.finTensorIncl B ⋯)) CategoryTheory.MonObj.mul

theorem RS.finTensorMul_incl {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] {s t v : Finset ι} (hs : s ⊆ v) (ht : t ⊆ v) (huv : s ∪ t ⊆ v) : CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (finTensorIncl B huv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (finTensorIncl B hs) (finTensorIncl B ht)) CategoryTheory.MonObj.mul

Include-then-multiply is independent of the receiving stage: merging and then including into any common superset is inclusion into the superset followed by its multiplication.

theorem RS.finTensorMul_natural {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] {s s' t t' : Finset ι} (hs : s ⊆ s') (ht : t ⊆ t') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (finTensorIncl B hs) (finTensorIncl B ht)) (finTensorMul B s' t') = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (finTensorIncl B ⋯)

Naturality of the merge maps in both stages.

theorem RS.finTensorMul_natural_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] {s s' t t' : Finset ι} (hs : s ⊆ s') (ht : t ⊆ t') {Z : D} (h : finTensor B (s' ∪ t') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (finTensorIncl B hs) (finTensorIncl B ht)) (CategoryTheory.CategoryStruct.comp (finTensorMul B s' t') h) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (CategoryTheory.CategoryStruct.comp (finTensorIncl B ⋯) h)

Naturality of the merge maps in both stages.

theorem RS.finTensorMul_stage {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] {s s' t t' : Finset ι} (hs : s ⊆ s') (ht : t ⊆ t') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (finTensorIncl B hs) (finTensorIncl B ht)) (CategoryTheory.CategoryStruct.comp (finTensorMul B s' t') (bigTensorStage B (s' ∪ t'))) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (bigTensorStage B (s ∪ t))

The merge maps composed with the stage inclusions form a cocone in each variable: the square defining the multiplication of the big tensor product commutes.

theorem RS.eqToHom_eq_finTensorIncl {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] {s t : Finset ι} (e : s = t) (h : s ⊆ t) : CategoryTheory.eqToHom ⋯ = finTensorIncl B h

The stage identification along an equality of finite sets is an inclusion.

theorem RS.finTensorMul_empty_left {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (t : Finset ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eqToHom ⋯) (finTensor B t)) (finTensorMul B ∅ t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (finTensor B t)).hom (finTensorIncl B ⋯)

Unit square: merging with the empty stage on the left is the left unitor followed by the inclusion.

theorem RS.finTensorMul_empty_right {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (t : Finset ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (finTensor B t) (CategoryTheory.eqToHom ⋯)) (finTensorMul B t ∅) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (finTensor B t)).hom (finTensorIncl B ⋯)

Unit square: merging with the empty stage on the right is the right unitor followed by the inclusion.

theorem RS.tensor_mul_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {M X Y Z : D} [CategoryTheory.MonObj M] (a : X ⟶ M) (b : Y ⟶ M) (c : Z ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a b) CategoryTheory.MonObj.mul) c) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom b c) CategoryTheory.MonObj.mul)) CategoryTheory.MonObj.mul)

Three-fold multiplication of a monoid object is associative, in the folded form used by the merge maps.

theorem RS.finTensorMul_def {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (s t : Finset ι) : finTensorMul B s t = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (finTensorIncl B ⋯) (finTensorIncl B ⋯)) CategoryTheory.MonObj.mul

Definitional unfolding of the merge map, for targeted rewriting.

theorem RS.finTensorMul_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (s t u : Finset ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (finTensorMul B s t) (finTensor B u)) (finTensorMul B (s ∪ t) u) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (finTensor B s) (finTensor B t) (finTensor B u)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (finTensor B s) (finTensorMul B t u)) (CategoryTheory.CategoryStruct.comp (finTensorMul B s (t ∪ u)) (CategoryTheory.eqToHom ⋯)))

Associativity square of the merge maps.

theorem RS.finTensorMul_assoc_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] (s t u : Finset ι) {Z : D} (h : finTensor B (s ∪ t ∪ u) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (finTensorMul B s t) (finTensor B u)) (CategoryTheory.CategoryStruct.comp (finTensorMul B (s ∪ t) u) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (finTensor B s) (finTensor B t) (finTensor B u)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (finTensor B s) (finTensorMul B t u)) (CategoryTheory.CategoryStruct.comp (finTensorMul B s (t ∪ u)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)))

Associativity square of the merge maps.

The multiplication of the big tensor product

With tensoring preserving Finset ι-colimits, bigTensor B ⊗ X and X ⊗ bigTensor B are colimits of the corresponding stage diagrams; maps out of them are determined by the stages, and the merge maps assemble into the multiplication.

theorem RS.bigTensor_tensorRight_hom_ext {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] {X Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (bigTensor B) X ⟶ Z} (w : ∀ (s : Finset ι), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bigTensorStage B s) X) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bigTensorStage B s) X) g) : f = g

Maps out of bigTensor B ⊗ X are determined by their restrictions to the stages.

theorem RS.tensorLeft_bigTensor_hom_ext {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] {X Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X (bigTensor B) ⟶ Z} (w : ∀ (t : Finset ι), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (bigTensorStage B t)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (bigTensorStage B t)) g) : f = g

Maps out of X ⊗ bigTensor B are determined by their restrictions to the stages.

theorem RS.finTensorMul_stage_left {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] {s s' t : Finset ι} (hs : s ⊆ s') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (finTensorIncl B hs) (finTensor B t)) (CategoryTheory.CategoryStruct.comp (finTensorMul B s' t) (bigTensorStage B (s' ∪ t))) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (bigTensorStage B (s ∪ t))

Left compatibility of the merge-then-stage maps.

theorem RS.finTensorMul_stage_left_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] {s s' t : Finset ι} (hs : s ⊆ s') {Z : D} (h : bigTensor B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (finTensorIncl B hs) (finTensor B t)) (CategoryTheory.CategoryStruct.comp (finTensorMul B s' t) (CategoryTheory.CategoryStruct.comp (bigTensorStage B (s' ∪ t)) h)) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (CategoryTheory.CategoryStruct.comp (bigTensorStage B (s ∪ t)) h)

Left compatibility of the merge-then-stage maps.

theorem RS.finTensorMul_stage_right {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] {s t t' : Finset ι} (ht : t ⊆ t') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (finTensor B s) (finTensorIncl B ht)) (CategoryTheory.CategoryStruct.comp (finTensorMul B s t') (bigTensorStage B (s ∪ t'))) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (bigTensorStage B (s ∪ t))

Right compatibility of the merge-then-stage maps.

theorem RS.finTensorMul_stage_right_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] {s t t' : Finset ι} (ht : t ⊆ t') {Z : D} (h : bigTensor B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (finTensor B s) (finTensorIncl B ht)) (CategoryTheory.CategoryStruct.comp (finTensorMul B s t') (CategoryTheory.CategoryStruct.comp (bigTensorStage B (s ∪ t')) h)) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (CategoryTheory.CategoryStruct.comp (bigTensorStage B (s ∪ t)) h)

Right compatibility of the merge-then-stage maps.

noncomputable def RS.bigTensorMulCocone {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] (t : Finset ι) : CategoryTheory.Limits.Cocone ((finTensorDiagram B).comp (CategoryTheory.MonoidalCategory.tensorRight (finTensor B t)))

The merge maps into the big tensor product form a cocone on the stage diagram tensored with a fixed finite stage.

Equations

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

noncomputable def RS.bigTensorMulStage {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (t : Finset ι) : CategoryTheory.MonoidalCategoryStruct.tensorObj (bigTensor B) (finTensor B t) ⟶ bigTensor B

Multiplication of the big tensor product against a fixed finite stage.

Equations

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

theorem RS.stage_bigTensorMulStage {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (s t : Finset ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bigTensorStage B s) (finTensor B t)) (bigTensorMulStage B t) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (bigTensorStage B (s ∪ t))

On a stage, the partial multiplication is merge-then-stage.

theorem RS.stage_bigTensorMulStage_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (s t : Finset ι) {Z : D} (h : bigTensor B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bigTensorStage B s) (finTensor B t)) (CategoryTheory.CategoryStruct.comp (bigTensorMulStage B t) h) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (CategoryTheory.CategoryStruct.comp (bigTensorStage B (s ∪ t)) h)

On a stage, the partial multiplication is merge-then-stage.

theorem RS.bigTensorMulStage_natural {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] {t t' : Finset ι} (ht : t ⊆ t') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (bigTensor B) (finTensorIncl B ht)) (bigTensorMulStage B t') = bigTensorMulStage B t

The partial multiplications are natural in the stage.

theorem RS.bigTensorMulStage_natural_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] {t t' : Finset ι} (ht : t ⊆ t') {Z : D} (h : bigTensor B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (bigTensor B) (finTensorIncl B ht)) (CategoryTheory.CategoryStruct.comp (bigTensorMulStage B t') h) = CategoryTheory.CategoryStruct.comp (bigTensorMulStage B t) h

The partial multiplications are natural in the stage.

noncomputable def RS.bigTensorMulTotalCocone {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.Limits.Cocone ((finTensorDiagram B).comp (CategoryTheory.MonoidalCategory.tensorLeft (bigTensor B)))

The partial multiplications form a cocone on the stage diagram tensored on the left with the big tensor product.

Equations

• RS.bigTensorMulTotalCocone B = { pt := RS.bigTensor B, ι := { app := fun (t : Finset ι) => RS.bigTensorMulStage B t, naturality := ⋯ } }

noncomputable def RS.bigTensorMul {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.MonoidalCategoryStruct.tensorObj (bigTensor B) (bigTensor B) ⟶ bigTensor B

The multiplication of the big tensor product.

Equations

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

theorem RS.stage_bigTensorMul_right {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (t : Finset ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (bigTensor B) (bigTensorStage B t)) (bigTensorMul B) = bigTensorMulStage B t

On a stage in the second variable, the multiplication is the partial multiplication.

theorem RS.stage_bigTensorMul_right_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (t : Finset ι) {Z : D} (h : bigTensor B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (bigTensor B) (bigTensorStage B t)) (CategoryTheory.CategoryStruct.comp (bigTensorMul B) h) = CategoryTheory.CategoryStruct.comp (bigTensorMulStage B t) h

On a stage in the second variable, the multiplication is the partial multiplication.

theorem RS.stage_bigTensorMul {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (s t : Finset ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (bigTensorStage B s) (bigTensorStage B t)) (bigTensorMul B) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (bigTensorStage B (s ∪ t))

The multiplication restricted to a pair of stages is the merge map followed by the union stage: the presentation of the multiplication over pairs of finite stages.

theorem RS.stage_bigTensorMul_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (s t : Finset ι) {Z : D} (h : bigTensor B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (bigTensorStage B s) (bigTensorStage B t)) (CategoryTheory.CategoryStruct.comp (bigTensorMul B) h) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (CategoryTheory.CategoryStruct.comp (bigTensorStage B (s ∪ t)) h)

The multiplication restricted to a pair of stages is the merge map followed by the union stage: the presentation of the multiplication over pairs of finite stages.

theorem RS.bigTensor_sandwich_hom_ext {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (X Y : D) {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj (bigTensor B) Y) ⟶ Z} (w : ∀ (t : Finset ι), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bigTensorStage B t) Y)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bigTensorStage B t) Y)) g) : f = g

Sandwich extension: maps out of X ⊗ (bigTensor B ⊗ Y) are determined by the stages in the middle slot.

theorem RS.bigTensor_pair_hom_ext {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (bigTensor B) (bigTensor B) ⟶ Z} (w : ∀ (s t : Finset ι), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (bigTensorStage B s) (bigTensorStage B t)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (bigTensorStage B s) (bigTensorStage B t)) g) : f = g

Maps out of bigTensor B ⊗ bigTensor B are determined by pairs of stages.

noncomputable def RS.bigTensorMulLCocone {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] (s : Finset ι) : CategoryTheory.Limits.Cocone ((finTensorDiagram B).comp (CategoryTheory.MonoidalCategory.tensorLeft (finTensor B s)))

The merge maps against a fixed first stage form a cocone.

Equations

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

noncomputable def RS.bigTensorMulStageL {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (s : Finset ι) : CategoryTheory.MonoidalCategoryStruct.tensorObj (finTensor B s) (bigTensor B) ⟶ bigTensor B

Multiplication of a fixed finite stage against the big tensor product.

Equations

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

theorem RS.stage_bigTensorMulStageL {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (s t : Finset ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (finTensor B s) (bigTensorStage B t)) (bigTensorMulStageL B s) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (bigTensorStage B (s ∪ t))

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

theorem RS.stage_bigTensorMulStageL_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (s t : Finset ι) {Z : D} (h : bigTensor B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (finTensor B s) (bigTensorStage B t)) (CategoryTheory.CategoryStruct.comp (bigTensorMulStageL B s) h) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (CategoryTheory.CategoryStruct.comp (bigTensorStage B (s ∪ t)) h)

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

theorem RS.stage_bigTensorMul_left {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (s : Finset ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bigTensorStage B s) (bigTensor B)) (bigTensorMul B) = bigTensorMulStageL B s

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

theorem RS.stage_bigTensorMul_left_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (s : Finset ι) {Z : D} (h : bigTensor B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bigTensorStage B s) (bigTensor B)) (CategoryTheory.CategoryStruct.comp (bigTensorMul B) h) = CategoryTheory.CategoryStruct.comp (bigTensorMulStageL B s) h

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

The monoid structure on the big tensor product

theorem RS.bigTensor_one_mul {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bigTensorUnit B) (bigTensor B)) (bigTensorMul B) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (bigTensor B)).hom

Left unit law of the big tensor product.

theorem RS.bigTensor_mul_one {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (bigTensor B) (bigTensorUnit B)) (bigTensorMul B) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (bigTensor B)).hom

Right unit law of the big tensor product.

theorem RS.bigTensor_mul_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bigTensorMul B) (bigTensor B)) (bigTensorMul B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (bigTensor B) (bigTensor B) (bigTensor B)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (bigTensor B) (bigTensorMul B)) (bigTensorMul B))

Associativity of the big tensor product multiplication.

@[instance_reducible]

noncomputable instance RS.bigTensorMon {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.MonObj (bigTensor B)

The big tensor product of a family of monoid objects is a monoid object: the unit is the empty stage and the multiplication is assembled from the merge maps.

Equations

• RS.bigTensorMon B = { one := RS.bigTensorUnit B, mul := RS.bigTensorMul B, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

instance RS.isMonHom_bigTensorStage {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (s : Finset ι) : CategoryTheory.IsMonHom (bigTensorStage B s)

The stage inclusions are morphisms of monoid objects.

instance RS.isMonHom_bigTensorOf {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.BraidedCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] (i : ι) : CategoryTheory.IsMonHom (bigTensorOf B i)

The single-factor inclusions are morphisms of monoid objects.

Commutativity

theorem RS.finTensorMul_comm {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.SymmetricCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [∀ (i : ι), CategoryTheory.IsCommMonObj (B i)] (s t : Finset ι) : CategoryTheory.CategoryStruct.comp (β_ (finTensor B s) (finTensor B t)).hom (finTensorMul B t s) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (CategoryTheory.eqToHom ⋯)

Commutativity square of the merge maps.

theorem RS.finTensorMul_comm_assoc {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.SymmetricCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [∀ (i : ι), CategoryTheory.IsCommMonObj (B i)] (s t : Finset ι) {Z : D} (h : finTensor B (t ∪ s) ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ (finTensor B s) (finTensor B t)).hom (CategoryTheory.CategoryStruct.comp (finTensorMul B t s) h) = CategoryTheory.CategoryStruct.comp (finTensorMul B s t) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

Commutativity square of the merge maps.

instance RS.bigTensorCommMon {ι : Type v} {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [LinearOrder ι] [CategoryTheory.SymmetricCategory D] (B : ι → D) [(i : ι) → CategoryTheory.MonObj (B i)] [∀ (i : ι), CategoryTheory.IsCommMonObj (B i)] [CategoryTheory.Limits.HasColimitsOfShape (Finset ι) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (Finset ι) (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.IsCommMonObj (bigTensor B)

The big tensor product of commutative monoid objects is commutative.