The multi-tensor of internal modules over a monoid object

The replacement for associativity of the binary module tensor product of ModTensor.lean: for a list Xs of left modules over a monoid object A in a braided monoidal category, the multi-tensor X₁ ⊗_A ⋯ ⊗_A Xₙ is presented in one step, as the coequalizer of a single wide relation pair

`⊕ₛ mid s ⇉ X₁ ⊗ (X₂ ⊗ (⋯ ⊗ Xₙ))`

whose source is the finite biproduct, over the adjacent slots s of the list, of the relation objects obtained by inserting A between the two factors of the slot, and whose legs act on the slot through the braided right action and the left action respectively — the two legs of ModTensor.lean at the slot's window, in every adjacent slot at once.

• modList A Xs: the plain tensor fold of the underlying objects, with the monoidal unit as seed; modListCast transports it along equalities of lists.
• ModSlot Xs: an adjacent slot, recorded as a decomposition Xs = pre ++ M :: N :: post; modSlots Xs enumerates the slots and mem_modSlots shows the enumeration is complete.
• modMulti A Xs, modMultiπ, modMulti_rel, modMultiDesc, modMultiπ_desc, modMulti_hom_ext: the multi-tensor and its universal property, with the slot relations quantified over decompositions.
• modMultiNil/modMultiSingle: with this presentation the empty multi-tensor is the monoidal unit of the ambient category (not the regular module A, which is the unit of Mod A — consumers wanting that convention should treat the empty list separately), and the singleton multi-tensor is the module itself.
• modMultiPair: the two-element multi-tensor agrees with the binary modTensor, compatibly with the projections.
• modMultiWhiskerRDesc/modMultiWhiskerLDesc: descent along the whiskered projections, with the whiskered relation condition reduced to the slots through the biproduct distributors.
• modMultiConcatFst, modMultiConcat: the concatenation map modMulti A Xs ⊗ modMulti A Ys ⟶ modMulti A (Xs ++ Ys), by a two-stage descent through the whiskered coequalizers, with the defining equation tensorHom_modMultiπ_concat against the projections and the fold concatenation modListConcat.
• modMultiHeadAct, modMultiMod: for a commutative monoid the action on the head factor descends, making the multi-tensor of a non-empty list a module; the empty multi-tensor is the monoidal unit and carries no canonical A-action.

The further descent of modMultiConcat through the middle A-action — the comparison with modTensor of two multi-tensors — is outside this module's scope; its substrate (the head modules, the concatenation map, and the slot relations) is complete.

The underlying tensor fold

def RS.modList {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] : List (CategoryTheory.Mod D A) → D

The tensor fold of the underlying objects of a list of modules, folded to the right with the monoidal unit as seed.

Equations

• RS.modList A [] = CategoryTheory.MonoidalCategoryStruct.tensorUnit D
• RS.modList A (M :: l) = CategoryTheory.MonoidalCategoryStruct.tensorObj M.X (RS.modList A l)

@[simp]

theorem RS.modList_nil {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] : modList A [] = CategoryTheory.MonoidalCategoryStruct.tensorUnit D

@[simp]

theorem RS.modList_cons {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : modList A (M :: l) = CategoryTheory.MonoidalCategoryStruct.tensorObj M.X (modList A l)

def RS.modListCast {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {l₁ l₂ : List (CategoryTheory.Mod D A)} (h : l₁ = l₂) : modList A l₁ ⟶ modList A l₂

Transport of the tensor fold along an equality of lists. It is an eqToHom, so it composes and cancels by eqToHom simp lemmas.

Equations

• RS.modListCast A h = CategoryTheory.eqToHom ⋯

@[simp]

theorem RS.modListCast_rfl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (l : List (CategoryTheory.Mod D A)) : modListCast A ⋯ = CategoryTheory.CategoryStruct.id (modList A l)

@[simp]

theorem RS.modListCast_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {l₁ l₂ l₃ : List (CategoryTheory.Mod D A)} (h : l₁ = l₂) (h' : l₂ = l₃) : CategoryTheory.CategoryStruct.comp (modListCast A h) (modListCast A h') = modListCast A ⋯

@[simp]

theorem RS.modListCast_comp_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {l₁ l₂ l₃ : List (CategoryTheory.Mod D A)} (h : l₁ = l₂) (h' : l₂ = l₃) {Z : D} (h✝ : modList A l₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (modListCast A h) (CategoryTheory.CategoryStruct.comp (modListCast A h') h✝) = CategoryTheory.CategoryStruct.comp (modListCast A ⋯) h✝

theorem RS.modListCast_whiskerLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M : CategoryTheory.Mod D A) {l₁ l₂ : List (CategoryTheory.Mod D A)} (h : l₁ = l₂) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modListCast A h) = modListCast A ⋯

Whiskering a list transport is a list transport.

The slot relations

A slot of the list is a decomposition Xs = pre ++ M :: N :: post. Its relation object inserts A between the two factors of the slot, nested exactly as the ambient fold, so that the legs below are typed at the fold on the nose, with no transport.

def RS.modMultiMid {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] : List (CategoryTheory.Mod D A) → CategoryTheory.Mod D A → CategoryTheory.Mod D A → List (CategoryTheory.Mod D A) → D

The relation object of a slot: the ambient fold with the monoid inserted between the two factors of the slot.

Equations

• One or more equations did not get rendered due to their size.
• RS.modMultiMid A (P :: rest) x✝² x✝¹ x✝ = CategoryTheory.MonoidalCategoryStruct.tensorObj P.X (RS.modMultiMid A rest x✝² x✝¹ x✝)

@[simp]

theorem RS.modMultiMid_nil {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) : modMultiMid A [] M N post = CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X) (modList A post)

@[simp]

theorem RS.modMultiMid_cons {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (P : CategoryTheory.Mod D A) (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) : modMultiMid A (P :: pre) M N post = CategoryTheory.MonoidalCategoryStruct.tensorObj P.X (modMultiMid A pre M N post)

def RS.modMultiLegOf {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) (pre : List (CategoryTheory.Mod D A)) : modMultiMid A pre M N post ⟶ modList A (pre ++ M :: N :: post)

Assemble a window morphism on (M.X ⊗ A) ⊗ N.X into a relation leg over a prefix: resolve the window, reassociate the second factor onto the suffix, and whisker through the prefix.

Equations

• One or more equations did not get rendered due to their size.
• RS.modMultiLegOf A M N post w (M_1 :: l) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft M_1.X (RS.modMultiLegOf A M N post w l)

@[simp]

theorem RS.modMultiLegOf_nil {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) : modMultiLegOf A M N post w [] = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w (modList A post)) (CategoryTheory.MonoidalCategoryStruct.associator M.X N.X (modList A post)).hom

@[simp]

theorem RS.modMultiLegOf_cons {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) (P : CategoryTheory.Mod D A) (pre : List (CategoryTheory.Mod D A)) : modMultiLegOf A M N post w (P :: pre) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (modMultiLegOf A M N post w pre)

def RS.modMultiLegM {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) : modMultiMid A pre M N post ⟶ modList A (pre ++ M :: N :: post)

The first relation leg at a slot: act on the left factor of the window through the braided right action.

Equations

• RS.modMultiLegM A pre M N post = RS.modMultiLegOf A M N post (RS.modTensorLegM A M N) pre

def RS.modMultiLegN {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) : modMultiMid A pre M N post ⟶ modList A (pre ++ M :: N :: post)

The second relation leg at a slot: associate and act on the right factor of the window.

Equations

• RS.modMultiLegN A pre M N post = RS.modMultiLegOf A M N post (RS.modTensorLegN A M N) pre

Enumeration of the slots

structure RS.ModSlot {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A : D} [CategoryTheory.MonObj A] (Xs : List (CategoryTheory.Mod D A)) : Type (max u v)

An adjacent slot of a list of modules: a decomposition into a prefix, two adjacent factors, and a suffix.

• pre : List (CategoryTheory.Mod D A)

  The factors below the slot.

• fst : CategoryTheory.Mod D A

  The first factor of the slot.

• snd : CategoryTheory.Mod D A

  The second factor of the slot.

• post : List (CategoryTheory.Mod D A)

  The factors above the slot.

• eq : Xs = self.pre ++ self.fst :: self.snd :: self.post

  The decomposition of the ambient list.

def RS.ModSlot.consSlot {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A : D} [CategoryTheory.MonObj A] (P : CategoryTheory.Mod D A) {Xs : List (CategoryTheory.Mod D A)} (s : ModSlot Xs) : ModSlot (P :: Xs)

Extend a slot by one factor below.

Equations

• RS.ModSlot.consSlot P s = { pre := P :: s.pre, fst := s.fst, snd := s.snd, post := s.post, eq := ⋯ }

def RS.modSlots {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (Xs : List (CategoryTheory.Mod D A)) : List (ModSlot Xs)

The list of all adjacent slots of a list of modules.

Equations

• RS.modSlots A [] = []
• RS.modSlots A [head] = []
• RS.modSlots A (M :: N :: post) = { pre := [], fst := M, snd := N, post := post, eq := ⋯ } :: List.map (RS.ModSlot.consSlot M) (RS.modSlots A (N :: post))

@[simp]

theorem RS.modSlots_nil {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] : modSlots A [] = []

@[simp]

theorem RS.modSlots_singleton {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M : CategoryTheory.Mod D A) : modSlots A [M] = []

theorem RS.ModSlot.consSlot_mem {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A : D} [CategoryTheory.MonObj A] (P : CategoryTheory.Mod D A) {Ys : List (CategoryTheory.Mod D A)} (s : ModSlot Ys) : s ∈ modSlots A Ys → consSlot P s ∈ modSlots A (P :: Ys)

Extension by a factor preserves membership in the slot list.

theorem RS.mem_modSlots {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A : D} [CategoryTheory.MonObj A] {Xs : List (CategoryTheory.Mod D A)} (s : ModSlot Xs) : s ∈ modSlots A Xs

The slot enumeration is complete: every decomposition of the list occurs among its slots.

The relation pair of the multi-tensor

@[reducible, inline]

abbrev RS.ModSlot.mid {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A : D} [CategoryTheory.MonObj A] {Xs : List (CategoryTheory.Mod D A)} (s : ModSlot Xs) : D

The relation object of a slot, in slot form.

Equations

• s.mid = RS.modMultiMid A s.pre s.fst s.snd s.post

def RS.ModSlot.legM {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A : D} [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] {Xs : List (CategoryTheory.Mod D A)} (s : ModSlot Xs) : s.mid ⟶ modList A Xs

The first relation leg of a slot, transported to the ambient list.

Equations

• s.legM = CategoryTheory.CategoryStruct.comp (RS.modMultiLegM A s.pre s.fst s.snd s.post) (RS.modListCast A ⋯)

def RS.ModSlot.legN {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A : D} [CategoryTheory.MonObj A] {Xs : List (CategoryTheory.Mod D A)} (s : ModSlot Xs) : s.mid ⟶ modList A Xs

The second relation leg of a slot, transported to the ambient list.

Equations

• s.legN = CategoryTheory.CategoryStruct.comp (RS.modMultiLegN A s.pre s.fst s.snd s.post) (RS.modListCast A ⋯)

@[reducible, inline]

noncomputable abbrev RS.modMultiSrc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (Xs : List (CategoryTheory.Mod D A)) : D

The source of the relation pair: the biproduct of the relation objects over all adjacent slots. An abbreviation, so that the biproduct API applies to the legs without unfolding.

Equations

• RS.modMultiSrc A Xs = ⨁ fun (i : Fin (RS.modSlots A Xs).length) => (RS.modSlots A Xs)[↑i].mid

noncomputable def RS.modMultiLegFst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (Xs : List (CategoryTheory.Mod D A)) : modMultiSrc A Xs ⟶ modList A Xs

The first leg of the relation pair, assembled over all slots.

Equations

• RS.modMultiLegFst A Xs = CategoryTheory.Limits.biproduct.desc fun (i : Fin (RS.modSlots A Xs).length) => (RS.modSlots A Xs)[↑i].legM

noncomputable def RS.modMultiLegSnd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (Xs : List (CategoryTheory.Mod D A)) : modMultiSrc A Xs ⟶ modList A Xs

The second leg of the relation pair, assembled over all slots.

Equations

• RS.modMultiLegSnd A Xs = CategoryTheory.Limits.biproduct.desc fun (i : Fin (RS.modSlots A Xs).length) => (RS.modSlots A Xs)[↑i].legN

The multi-tensor and its universal property

noncomputable def RS.modMulti {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (Xs : List (CategoryTheory.Mod D A)) : D

The multi-tensor of a list of modules over A: the coequalizer of the wide relation pair, identifying (x·c) ⊗ y ~ x ⊗ (c·y) in every adjacent slot simultaneously. No binary module tensor product and no associativity enter.

Equations

• RS.modMulti A Xs = CategoryTheory.Limits.coequalizer (RS.modMultiLegFst A Xs) (RS.modMultiLegSnd A Xs)

noncomputable def RS.modMultiπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (Xs : List (CategoryTheory.Mod D A)) : modList A Xs ⟶ modMulti A Xs

The projection of the ambient fold onto the multi-tensor.

Equations

• RS.modMultiπ A Xs = CategoryTheory.Limits.coequalizer.π (RS.modMultiLegFst A Xs) (RS.modMultiLegSnd A Xs)

instance RS.instEpiModMultiπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (Xs : List (CategoryTheory.Mod D A)) : CategoryTheory.Epi (modMultiπ A Xs)

theorem RS.modMulti_condition {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (Xs : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (modMultiLegFst A Xs) (modMultiπ A Xs) = CategoryTheory.CategoryStruct.comp (modMultiLegSnd A Xs) (modMultiπ A Xs)

The two assembled legs agree after the projection.

theorem RS.modMulti_condition_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (Xs : List (CategoryTheory.Mod D A)) {Z : D} (h : modMulti A Xs ⟶ Z) : CategoryTheory.CategoryStruct.comp (modMultiLegFst A Xs) (CategoryTheory.CategoryStruct.comp (modMultiπ A Xs) h) = CategoryTheory.CategoryStruct.comp (modMultiLegSnd A Xs) (CategoryTheory.CategoryStruct.comp (modMultiπ A Xs) h)

The two assembled legs agree after the projection.

theorem RS.modMulti_rel {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {Xs : List (CategoryTheory.Mod D A)} (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (h : Xs = pre ++ M :: N :: post) : CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) (modMultiπ A Xs)) = CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) (modMultiπ A Xs))

The slot relation in the multi-tensor: at every decomposition Xs = pre ++ M :: N :: post the two slot legs agree after the projection.

theorem RS.modMulti_rel_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {Xs : List (CategoryTheory.Mod D A)} (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (h : Xs = pre ++ M :: N :: post) {Z : D} (h✝ : modMulti A Xs ⟶ Z) : CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) (CategoryTheory.CategoryStruct.comp (modMultiπ A Xs) h✝)) = CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) (CategoryTheory.CategoryStruct.comp (modMultiπ A Xs) h✝))

The slot relation in the multi-tensor: at every decomposition Xs = pre ++ M :: N :: post the two slot legs agree after the projection.

theorem RS.modMulti_hom_ext {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {Xs : List (CategoryTheory.Mod D A)} {W : D} {k l : modMulti A Xs ⟶ W} (h : CategoryTheory.CategoryStruct.comp (modMultiπ A Xs) k = CategoryTheory.CategoryStruct.comp (modMultiπ A Xs) l) : k = l

Morphisms out of the multi-tensor are determined by their composite with the projection.

noncomputable def RS.modMultiDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {Xs : List (CategoryTheory.Mod D A)} {W : D} (k : modList A Xs ⟶ W) (h : ∀ (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (hd : Xs = pre ++ M :: N :: post), CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) k) = CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) k)) : modMulti A Xs ⟶ W

Descend a morphism that coequalizes every slot relation to the multi-tensor.

Equations

• RS.modMultiDesc A k h = CategoryTheory.Limits.coequalizer.desc k ⋯

@[simp]

theorem RS.modMultiπ_desc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {Xs : List (CategoryTheory.Mod D A)} {W : D} (k : modList A Xs ⟶ W) (h : ∀ (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (hd : Xs = pre ++ M :: N :: post), CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) k) = CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) k)) : CategoryTheory.CategoryStruct.comp (modMultiπ A Xs) (modMultiDesc A k h) = k

The descent factors the given morphism through the projection.

@[simp]

theorem RS.modMultiπ_desc_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {Xs : List (CategoryTheory.Mod D A)} {W : D} (k : modList A Xs ⟶ W) (h : ∀ (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (hd : Xs = pre ++ M :: N :: post), CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) k) = CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) k)) {Z : D} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (modMultiπ A Xs) (CategoryTheory.CategoryStruct.comp (modMultiDesc A k h) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The descent factors the given morphism through the projection.

The empty and singleton multi-tensors

Below two factors there are no adjacent slots: the relation source is the empty biproduct, the legs agree, and the projection is an isomorphism.

noncomputable def RS.modMultiTriv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {Xs : List (CategoryTheory.Mod D A)} (h : modSlots A Xs = []) : modMulti A Xs ≅ modList A Xs

On a slot-free list the projection is an isomorphism.

Equations

• RS.modMultiTriv A h = { hom := RS.modMultiDesc A (CategoryTheory.CategoryStruct.id (RS.modList A Xs)) ⋯, inv := RS.modMultiπ A Xs, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.modMultiNil {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] : modMulti A [] ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

The empty multi-tensor is the monoidal unit of the ambient category. With this presentation the empty fold is 𝟙_ D, not the regular module: consumers wanting A as the empty product — the unit of the module category — should treat the empty list as a separate case.

Equations

• RS.modMultiNil A = RS.modMultiTriv A ⋯

noncomputable def RS.modMultiSingle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X : CategoryTheory.Mod D A) : modMulti A [X] ≅ X.X

The singleton multi-tensor is the module.

Equations

• RS.modMultiSingle A X = RS.modMultiTriv A ⋯ ≪≫ CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X

Comparison with the binary module tensor product

For a two-element list the wide relation pair has a single slot, whose window legs are exactly the parallel pair of ModTensor.lean; the two coequalizer presentations agree, up to the right unitor absorbing the unit seed of the fold.

theorem RS.pair_decomp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {X Y M N : CategoryTheory.Mod D A} {pre post : List (CategoryTheory.Mod D A)} (h : [X, Y] = pre ++ M :: N :: post) : pre = [] ∧ X = M ∧ Y = N ∧ post = []

The only slot of a two-element list is the full decomposition.

def RS.pairResolve {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) : modList A [X, Y] ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X

The resolution of the two-element fold onto the plain tensor product: absorb the unit seed. A bridge morphism with a modList-typed source, so that statements through it stay type-correct at low transparency.

Equations

• RS.pairResolve A X Y = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y.X).hom

def RS.pairResolveInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X ⟶ modList A [X, Y]

The inverse resolution: reinstate the unit seed.

Equations

• RS.pairResolveInv A X Y = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y.X).inv

@[simp]

theorem RS.pairResolve_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (pairResolve A X Y) (pairResolveInv A X Y) = CategoryTheory.CategoryStruct.id (modList A [X, Y])

@[simp]

theorem RS.pairResolve_inv_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) {Z : D} (h : modList A [X, Y] ⟶ Z) : CategoryTheory.CategoryStruct.comp (pairResolve A X Y) (CategoryTheory.CategoryStruct.comp (pairResolveInv A X Y) h) = h

@[simp]

theorem RS.pairResolveInv_resolve {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (pairResolveInv A X Y) (pairResolve A X Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)

@[simp]

theorem RS.pairResolveInv_resolve_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (pairResolveInv A X Y) (CategoryTheory.CategoryStruct.comp (pairResolve A X Y) h) = h

def RS.pairSeed {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) : modMultiMid A [] X Y [] ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X

The window seed of the pair: the right unitor of the single relation object, retyped at modMultiMid.

Equations

• RS.pairSeed A X Y = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X)).hom

def RS.pairSeedInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X ⟶ modMultiMid A [] X Y []

The inverse window seed of the pair.

Equations

• RS.pairSeedInv A X Y = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X)).inv

theorem RS.modMultiLeg_pair_resolve {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X) (h : [] ++ [X, Y] = [X, Y]) : CategoryTheory.CategoryStruct.comp (modMultiLegOf A X Y [] w []) (CategoryTheory.CategoryStruct.comp (modListCast A h) (pairResolve A X Y)) = CategoryTheory.CategoryStruct.comp (pairSeed A X Y) w

The single relation leg of the pair against the resolution: the unit seed is absorbed and the window morphism remains.

theorem RS.modMultiLeg_pair_resolve_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X) (h : [] ++ [X, Y] = [X, Y]) {Z : D} (h✝ : CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (modMultiLegOf A X Y [] w []) (CategoryTheory.CategoryStruct.comp (modListCast A h) (CategoryTheory.CategoryStruct.comp (pairResolve A X Y) h✝)) = CategoryTheory.CategoryStruct.comp (pairSeed A X Y) (CategoryTheory.CategoryStruct.comp w h✝)

The single relation leg of the pair against the resolution: the unit seed is absorbed and the window morphism remains.

theorem RS.modMultiLeg_pair_resolveInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X) (h : [] ++ [X, Y] = [X, Y]) : CategoryTheory.CategoryStruct.comp w (pairResolveInv A X Y) = CategoryTheory.CategoryStruct.comp (pairSeedInv A X Y) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A X Y [] w []) (modListCast A h))

A window morphism against the inverse resolution, in leg form.

theorem RS.modMultiLeg_pair_resolveInv_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X) (h : [] ++ [X, Y] = [X, Y]) {Z : D} (h✝ : modList A [X, Y] ⟶ Z) : CategoryTheory.CategoryStruct.comp w (CategoryTheory.CategoryStruct.comp (pairResolveInv A X Y) h✝) = CategoryTheory.CategoryStruct.comp (pairSeedInv A X Y) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A X Y [] w []) (CategoryTheory.CategoryStruct.comp (modListCast A h) h✝))

A window morphism against the inverse resolution, in leg form.

noncomputable def RS.modMultiPairHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X Y : CategoryTheory.Mod D A) : modMulti A [X, Y] ⟶ modTensor A X Y

Comparison with the binary tensor product: the forward direction, descending the binary projection.

Equations

• RS.modMultiPairHom A X Y = RS.modMultiDesc A (CategoryTheory.CategoryStruct.comp (RS.pairResolve A X Y) (RS.modTensorπ A X Y)) ⋯

@[simp]

theorem RS.modMultiπ_pairMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X Y : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modMultiπ A [X, Y]) (modMultiPairHom A X Y) = CategoryTheory.CategoryStruct.comp (pairResolve A X Y) (modTensorπ A X Y)

Defining equation of the forward comparison.

@[simp]

theorem RS.modMultiπ_pairMod_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X Y : CategoryTheory.Mod D A) {Z : D} (h : modTensor A X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (modMultiπ A [X, Y]) (CategoryTheory.CategoryStruct.comp (modMultiPairHom A X Y) h) = CategoryTheory.CategoryStruct.comp (pairResolve A X Y) (CategoryTheory.CategoryStruct.comp (modTensorπ A X Y) h)

Defining equation of the forward comparison.

noncomputable def RS.modMultiPairInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X Y : CategoryTheory.Mod D A) : modTensor A X Y ⟶ modMulti A [X, Y]

Comparison with the binary tensor product: the backward direction, descending the wide projection.

Equations

• RS.modMultiPairInv A X Y = RS.modTensorDesc A X Y (CategoryTheory.CategoryStruct.comp (RS.pairResolveInv A X Y) (RS.modMultiπ A [X, Y])) ⋯

@[simp]

theorem RS.modTensorπ_pairInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X Y : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorπ A X Y) (modMultiPairInv A X Y) = CategoryTheory.CategoryStruct.comp (pairResolveInv A X Y) (modMultiπ A [X, Y])

Defining equation of the backward comparison.

@[simp]

theorem RS.modTensorπ_pairInv_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X Y : CategoryTheory.Mod D A) {Z : D} (h : modMulti A [X, Y] ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A X Y) (CategoryTheory.CategoryStruct.comp (modMultiPairInv A X Y) h) = CategoryTheory.CategoryStruct.comp (pairResolveInv A X Y) (CategoryTheory.CategoryStruct.comp (modMultiπ A [X, Y]) h)

Defining equation of the backward comparison.

noncomputable def RS.modMultiPair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X Y : CategoryTheory.Mod D A) : modMulti A [X, Y] ≅ modTensor A X Y

The two-element multi-tensor is the binary module tensor product: the one-slot wide presentation and the parallel-pair presentation coequalize the same relations.

Equations

• RS.modMultiPair A X Y = { hom := RS.modMultiPairHom A X Y, inv := RS.modMultiPairInv A X Y, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Concatenation of folds

The fold of a concatenated list against the tensor product of the two folds, with the bridges that carry a relation slot of one block into the concatenated list. Casts are quantified, as in the slot relations, so consumers never meet a transported proof they cannot name.

def RS.modListConcat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (Xs Ys : List (CategoryTheory.Mod D A)) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modList A Xs) (modList A Ys) ≅ modList A (Xs ++ Ys)

Concatenation of tensor folds: the two-block fold reassociates onto the fold of the concatenated list.

Equations

• One or more equations did not get rendered due to their size.
• RS.modListConcat A [] x✝ = CategoryTheory.MonoidalCategoryStruct.leftUnitor (RS.modList A x✝)

theorem RS.modListConcat_cons_whisker {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (P : CategoryTheory.Mod D A) {S : D} {T Ys : List (CategoryTheory.Mod D A)} (u : S ⟶ modList A T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X u) (modList A Ys)) (modListConcat A (P :: T) Ys).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S (modList A Ys)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u (modList A Ys)) (modListConcat A T Ys).hom))

A morphism whiskered under a cons prefix passes the concatenation: the step case of every prefix induction below.

theorem RS.modListConcat_whiskerLeft_cons {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (P : CategoryTheory.Mod D A) (Xs : List (CategoryTheory.Mod D A)) {S : D} {T : List (CategoryTheory.Mod D A)} (u : S ⟶ modList A T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modList A (P :: Xs)) u) (modListConcat A (P :: Xs) T).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X (modList A Xs) S).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modList A Xs) u) (modListConcat A Xs T).hom))

A morphism whiskered on the right of a cons prefix passes the concatenation.

theorem RS.modListConcat_cast_right {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (Xs : List (CategoryTheory.Mod D A)) {l₁ l₂ : List (CategoryTheory.Mod D A)} (h : l₁ = l₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modList A Xs) (modListCast A h)) (modListConcat A Xs l₂).hom = CategoryTheory.CategoryStruct.comp (modListConcat A Xs l₁).hom (modListCast A ⋯)

A transport in the second block passes the concatenation.

theorem RS.modListConcat_cast_right_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (Xs : List (CategoryTheory.Mod D A)) {l₁ l₂ : List (CategoryTheory.Mod D A)} (h : l₁ = l₂) {Z : D} (h✝ : modList A (Xs ++ l₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modList A Xs) (modListCast A h)) (CategoryTheory.CategoryStruct.comp (modListConcat A Xs l₂).hom h✝) = CategoryTheory.CategoryStruct.comp (modListConcat A Xs l₁).hom (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) h✝)

A transport in the second block passes the concatenation.

def RS.modMultiMidConcat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post Ys pre : List (CategoryTheory.Mod D A)) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modMultiMid A pre M N post) (modList A Ys) ⟶ modMultiMid A pre M N (post ++ Ys)

The relation object of a slot, concatenated on the right: the suffix grows by the second block.

Equations

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

theorem RS.modMultiLegOf_concat_nil {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post Ys : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiLegOf A M N post w []) (modList A Ys)) (modListConcat A (M :: N :: post) Ys).hom = CategoryTheory.CategoryStruct.comp (modMultiMidConcat A M N post Ys []) (modMultiLegOf A M N (post ++ Ys) w [])

The base of the right leg-concatenation: the window against the concatenation, by the pentagon.

theorem RS.modMultiLegOf_concat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post Ys : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) (pre : List (CategoryTheory.Mod D A)) (h : pre ++ M :: N :: (post ++ Ys) = pre ++ M :: N :: post ++ Ys) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiLegOf A M N post w pre) (modList A Ys)) (modListConcat A (pre ++ M :: N :: post) Ys).hom = CategoryTheory.CategoryStruct.comp (modMultiMidConcat A M N post Ys pre) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A M N (post ++ Ys) w pre) (modListCast A h))

The right leg-concatenation: a slot leg of the first block, whiskered by the second block, is the slot leg of the concatenated list at the widened suffix.

theorem RS.modMultiLegOf_concat_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post Ys : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) (pre : List (CategoryTheory.Mod D A)) (h : pre ++ M :: N :: (post ++ Ys) = pre ++ M :: N :: post ++ Ys) {Z : D} (h✝ : modList A (pre ++ M :: N :: post ++ Ys) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiLegOf A M N post w pre) (modList A Ys)) (CategoryTheory.CategoryStruct.comp (modListConcat A (pre ++ M :: N :: post) Ys).hom h✝) = CategoryTheory.CategoryStruct.comp (modMultiMidConcat A M N post Ys pre) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A M N (post ++ Ys) w pre) (CategoryTheory.CategoryStruct.comp (modListCast A h) h✝))

The right leg-concatenation: a slot leg of the first block, whiskered by the second block, is the slot leg of the concatenated list at the widened suffix.

def RS.modMultiMidConcatL {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post Xs : List (CategoryTheory.Mod D A)) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modList A Xs) (modMultiMid A pre M N post) ⟶ modMultiMid A (Xs ++ pre) M N post

The relation object of a slot, concatenated on the left: the prefix grows by the first block.

Equations

• One or more equations did not get rendered due to their size.
• RS.modMultiMidConcatL A pre M N post [] = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (RS.modMultiMid A pre M N post)).hom

theorem RS.modMultiLegOf_concatL {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) (Xs : List (CategoryTheory.Mod D A)) (h : Xs ++ pre ++ M :: N :: post = Xs ++ (pre ++ M :: N :: post)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modList A Xs) (modMultiLegOf A M N post w pre)) (modListConcat A Xs (pre ++ M :: N :: post)).hom = CategoryTheory.CategoryStruct.comp (modMultiMidConcatL A pre M N post Xs) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A M N post w (Xs ++ pre)) (modListCast A h))

The left leg-concatenation: a slot leg of the second block, whiskered by the first block, is the slot leg of the concatenated list at the widened prefix.

theorem RS.modMultiLegOf_concatL_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) (Xs : List (CategoryTheory.Mod D A)) (h : Xs ++ pre ++ M :: N :: post = Xs ++ (pre ++ M :: N :: post)) {Z : D} (h✝ : modList A (Xs ++ (pre ++ M :: N :: post)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modList A Xs) (modMultiLegOf A M N post w pre)) (CategoryTheory.CategoryStruct.comp (modListConcat A Xs (pre ++ M :: N :: post)).hom h✝) = CategoryTheory.CategoryStruct.comp (modMultiMidConcatL A pre M N post Xs) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A M N post w (Xs ++ pre)) (CategoryTheory.CategoryStruct.comp (modListCast A h) h✝))

The left leg-concatenation: a slot leg of the second block, whiskered by the first block, is the slot leg of the concatenated list at the widened prefix.

Whiskered descent

Morphisms out of a whiskered multi-tensor, by descent along the whiskered projection. The relation source is a biproduct, so the whiskered relation condition reduces to the slots through the distributors of the monoidal preadditive structure.

theorem RS.biproduct_whiskerRight_hom_ext {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {J : Type} [Finite J] (f : J → D) (P : D) {W : D} {u v : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) P ⟶ W} (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) P) u = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) P) v) : u = v

Maps out of a right-whiskered biproduct are determined by the whiskered injections.

theorem RS.biproduct_whiskerLeft_hom_ext {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {J : Type} [Finite J] (f : J → D) (P : D) {W : D} {u v : CategoryTheory.MonoidalCategoryStruct.tensorObj P (⨁ f) ⟶ W} (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.Limits.biproduct.ι f j)) u = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.Limits.biproduct.ι f j)) v) : u = v

Maps out of a left-whiskered biproduct are determined by the whiskered injections.

noncomputable def RS.modMultiWhiskerRIsColimit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] (Xs : List (CategoryTheory.Mod D A)) (P : D) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiπ A Xs) P) ⋯)

Whiskering the multi-tensor coequalizer by tensorRight P yields a colimit cofork.

Equations

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

theorem RS.modMulti_whiskerR_hom_ext {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] (Xs : List (CategoryTheory.Mod D A)) (P : D) {W : D} {k l : CategoryTheory.MonoidalCategoryStruct.tensorObj (modMulti A Xs) P ⟶ W} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiπ A Xs) P) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiπ A Xs) P) l) : k = l

Morphisms out of a right-whiskered multi-tensor are determined by their composite with the whiskered projection.

noncomputable def RS.modMultiWhiskerRDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] (Xs : List (CategoryTheory.Mod D A)) (P : D) {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj (modList A Xs) P ⟶ W) (h : ∀ (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (hd : Xs = pre ++ M :: N :: post), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (modListCast A ⋯)) P) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (modListCast A ⋯)) P) k) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modMulti A Xs) P ⟶ W

Descend a morphism coequalizing every right-whiskered slot relation along the right-whiskered projection.

Equations

• RS.modMultiWhiskerRDesc A Xs P k h = CategoryTheory.Limits.Cofork.IsColimit.desc (RS.modMultiWhiskerRIsColimit A Xs P) k ⋯

@[simp]

theorem RS.whiskerRight_modMultiπ_whiskerRDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] (Xs : List (CategoryTheory.Mod D A)) (P : D) {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj (modList A Xs) P ⟶ W) (h : ∀ (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (hd : Xs = pre ++ M :: N :: post), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (modListCast A ⋯)) P) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (modListCast A ⋯)) P) k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiπ A Xs) P) (modMultiWhiskerRDesc A Xs P k h) = k

The right-whiskered descent factors the given morphism through the whiskered projection.

@[simp]

theorem RS.whiskerRight_modMultiπ_whiskerRDesc_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] (Xs : List (CategoryTheory.Mod D A)) (P : D) {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj (modList A Xs) P ⟶ W) (h : ∀ (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (hd : Xs = pre ++ M :: N :: post), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (modListCast A ⋯)) P) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (modListCast A ⋯)) P) k) {Z : D} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiπ A Xs) P) (CategoryTheory.CategoryStruct.comp (modMultiWhiskerRDesc A Xs P k h) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The right-whiskered descent factors the given morphism through the whiskered projection.

noncomputable def RS.modMultiWhiskerLIsColimit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (Xs : List (CategoryTheory.Mod D A)) (P : D) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modMultiπ A Xs)) ⋯)

Whiskering the multi-tensor coequalizer by tensorLeft P yields a colimit cofork.

Equations

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

theorem RS.modMulti_whiskerL_hom_ext {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (Xs : List (CategoryTheory.Mod D A)) (P : D) {W : D} {k l : CategoryTheory.MonoidalCategoryStruct.tensorObj P (modMulti A Xs) ⟶ W} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modMultiπ A Xs)) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modMultiπ A Xs)) l) : k = l

Morphisms out of a left-whiskered multi-tensor are determined by their composite with the whiskered projection.

noncomputable def RS.modMultiWhiskerLDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (Xs : List (CategoryTheory.Mod D A)) (P : D) {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj P (modList A Xs) ⟶ W) (h : ∀ (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (hd : Xs = pre ++ M :: N :: post), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (modListCast A ⋯))) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (modListCast A ⋯))) k) : CategoryTheory.MonoidalCategoryStruct.tensorObj P (modMulti A Xs) ⟶ W

Descend a morphism coequalizing every left-whiskered slot relation along the left-whiskered projection.

Equations

• RS.modMultiWhiskerLDesc A Xs P k h = CategoryTheory.Limits.Cofork.IsColimit.desc (RS.modMultiWhiskerLIsColimit A Xs P) k ⋯

@[simp]

theorem RS.whiskerLeft_modMultiπ_whiskerLDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (Xs : List (CategoryTheory.Mod D A)) (P : D) {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj P (modList A Xs) ⟶ W) (h : ∀ (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (hd : Xs = pre ++ M :: N :: post), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (modListCast A ⋯))) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (modListCast A ⋯))) k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modMultiπ A Xs)) (modMultiWhiskerLDesc A Xs P k h) = k

The left-whiskered descent factors the given morphism through the whiskered projection.

@[simp]

theorem RS.whiskerLeft_modMultiπ_whiskerLDesc_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (Xs : List (CategoryTheory.Mod D A)) (P : D) {W : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj P (modList A Xs) ⟶ W) (h : ∀ (pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (hd : Xs = pre ++ M :: N :: post), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (modListCast A ⋯))) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (modListCast A ⋯))) k) {Z : D} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modMultiπ A Xs)) (CategoryTheory.CategoryStruct.comp (modMultiWhiskerLDesc A Xs P k h) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The left-whiskered descent factors the given morphism through the whiskered projection.

The concatenation map

The projection of the concatenated list descends through the tensor product of the two multi-tensors, one block at a time: first the relations of the first block through the right-whiskered coequalizer, then those of the second block through the left-whiskered coequalizer.

noncomputable def RS.modMultiConcatFst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] (Xs Ys : List (CategoryTheory.Mod D A)) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modMulti A Xs) (modList A Ys) ⟶ modMulti A (Xs ++ Ys)

First stage of the concatenation: the relations of the first block descend, the second block still at the fold.

Equations

• RS.modMultiConcatFst A Xs Ys = RS.modMultiWhiskerRDesc A Xs (RS.modList A Ys) (CategoryTheory.CategoryStruct.comp (RS.modListConcat A Xs Ys).hom (RS.modMultiπ A (Xs ++ Ys))) ⋯

@[simp]

theorem RS.whiskerRight_modMultiπ_concatFst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] (Xs Ys : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiπ A Xs) (modList A Ys)) (modMultiConcatFst A Xs Ys) = CategoryTheory.CategoryStruct.comp (modListConcat A Xs Ys).hom (modMultiπ A (Xs ++ Ys))

Defining equation of the first stage.

@[simp]

theorem RS.whiskerRight_modMultiπ_concatFst_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] (Xs Ys : List (CategoryTheory.Mod D A)) {Z : D} (h : modMulti A (Xs ++ Ys) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiπ A Xs) (modList A Ys)) (CategoryTheory.CategoryStruct.comp (modMultiConcatFst A Xs Ys) h) = CategoryTheory.CategoryStruct.comp (modListConcat A Xs Ys).hom (CategoryTheory.CategoryStruct.comp (modMultiπ A (Xs ++ Ys)) h)

Defining equation of the first stage.

noncomputable def RS.modMultiConcat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (Xs Ys : List (CategoryTheory.Mod D A)) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modMulti A Xs) (modMulti A Ys) ⟶ modMulti A (Xs ++ Ys)

The concatenation map: the multi-tensor of a concatenated list receives the tensor product of the two multi-tensors.

Equations

• RS.modMultiConcat A Xs Ys = RS.modMultiWhiskerLDesc A Ys (RS.modMulti A Xs) (RS.modMultiConcatFst A Xs Ys) ⋯

@[simp]

theorem RS.whiskerLeft_modMultiπ_concat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (Xs Ys : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modMulti A Xs) (modMultiπ A Ys)) (modMultiConcat A Xs Ys) = modMultiConcatFst A Xs Ys

Defining equation of the concatenation against the projection of the second block.

@[simp]

theorem RS.whiskerLeft_modMultiπ_concat_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (Xs Ys : List (CategoryTheory.Mod D A)) {Z : D} (h : modMulti A (Xs ++ Ys) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modMulti A Xs) (modMultiπ A Ys)) (CategoryTheory.CategoryStruct.comp (modMultiConcat A Xs Ys) h) = CategoryTheory.CategoryStruct.comp (modMultiConcatFst A Xs Ys) h

Defining equation of the concatenation against the projection of the second block.

theorem RS.tensorHom_modMultiπ_concat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (Xs Ys : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modMultiπ A Xs) (modMultiπ A Ys)) (modMultiConcat A Xs Ys) = CategoryTheory.CategoryStruct.comp (modListConcat A Xs Ys).hom (modMultiπ A (Xs ++ Ys))

Defining equation of the concatenation: on the two projections it is the fold concatenation followed by the projection of the concatenated list.

theorem RS.tensorHom_modMultiπ_concat_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (Xs Ys : List (CategoryTheory.Mod D A)) {Z : D} (h : modMulti A (Xs ++ Ys) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modMultiπ A Xs) (modMultiπ A Ys)) (CategoryTheory.CategoryStruct.comp (modMultiConcat A Xs Ys) h) = CategoryTheory.CategoryStruct.comp (modListConcat A Xs Ys).hom (CategoryTheory.CategoryStruct.comp (modMultiπ A (Xs ++ Ys)) h)

Defining equation of the concatenation: on the two projections it is the fold concatenation followed by the projection of the concatenated list.

The head action

On a non-empty list the monoid acts through the head factor; the action descends to the multi-tensor, making it a module. The slot compatibilities are the two cases: the slot at the head, through the binary window compatibilities of ModTensor.lean, and a slot in the tail, disjoint from the action.

def RS.modListHeadAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (modList A (X :: l)) ⟶ modList A (X :: l)

The head action on the fold of a non-empty list: act on the head factor.

Equations

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

theorem RS.modListHeadAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (modList A (X :: l))) (modListHeadAct A X l) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (modList A (X :: l))).hom

Unitality of the head action.

theorem RS.modListHeadAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (modList A (X :: l))) (modListHeadAct A X l) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (modList A (X :: l))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modListHeadAct A X l)) (modListHeadAct A X l))

Associativity of the head action.

def RS.modMultiHeadShuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (modMultiMid A [] M N post) ⟶ modMultiMid A [] M N post

The shuffle of the head slot: the monoid moves inside the window and acts on the left module factor there.

Equations

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

theorem RS.modListHeadAct_window {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) (hw : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M.X N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A M.X) N.X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M.X A).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A M.X) A)) N.X)) w) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modMultiLegOf A M N post w [])) (modListHeadAct A M (N :: post)) = CategoryTheory.CategoryStruct.comp (modMultiHeadShuffle A M N post) (modMultiLegOf A M N post w [])

The head-slot compatibility: a window morphism compatible with the binary action commutes the head action past the head slot's leg.

theorem RS.modListHeadAct_window_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) (hw : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M.X N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A M.X) N.X)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M.X A).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A M.X) A)) N.X)) w) {Z : D} (h : modList A (M :: N :: post) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modMultiLegOf A M N post w [])) (CategoryTheory.CategoryStruct.comp (modListHeadAct A M (N :: post)) h) = CategoryTheory.CategoryStruct.comp (modMultiHeadShuffle A M N post) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A M N post w []) h)

The head-slot compatibility: a window morphism compatible with the binary action commutes the head action past the head slot's leg.

theorem RS.modListHeadAct_tail {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : CategoryTheory.Mod D A) {S : D} {T : List (CategoryTheory.Mod D A)} (u : S ⟶ modList A T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X u)) (modListHeadAct A X T) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X.X S).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A X.X) S)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X u)

The tail-slot compatibility: the head action is disjoint from any morphism whiskered under the head factor.

theorem RS.modListHeadAct_tail_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : CategoryTheory.Mod D A) {S : D} {T : List (CategoryTheory.Mod D A)} (u : S ⟶ modList A T) {Z : D} (h : modList A (X :: T) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X u)) (modListHeadAct A X T)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X.X S).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A X.X) S) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X u))) h

The tail-slot compatibility: the head action is disjoint from any morphism whiskered under the head factor.

Descent of the head action

theorem RS.modListHeadAct_slotwise {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (X : CategoryTheory.Mod D A) (l pre : List (CategoryTheory.Mod D A)) (M N : CategoryTheory.Mod D A) (post : List (CategoryTheory.Mod D A)) (hd : X :: l = pre ++ M :: N :: post) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp (modMultiLegM A pre M N post) (modListCast A ⋯))) (CategoryTheory.CategoryStruct.comp (modListHeadAct A X l) (modMultiπ A (X :: l))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp (modMultiLegN A pre M N post) (modListCast A ⋯))) (CategoryTheory.CategoryStruct.comp (modListHeadAct A X l) (modMultiπ A (X :: l)))

The head action carries every slot relation into the kernel of the projection.

noncomputable def RS.modMultiHeadAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (modMulti A (X :: l)) ⟶ modMulti A (X :: l)

The head action on the multi-tensor, by descent.

Equations

• RS.modMultiHeadAct A X l = RS.modMultiWhiskerLDesc A (X :: l) A (CategoryTheory.CategoryStruct.comp (RS.modListHeadAct A X l) (RS.modMultiπ A (X :: l))) ⋯

@[simp]

theorem RS.whiskerLeft_modMultiπ_headAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modMultiπ A (X :: l))) (modMultiHeadAct A X l) = CategoryTheory.CategoryStruct.comp (modListHeadAct A X l) (modMultiπ A (X :: l))

Defining equation of the descended head action.

@[simp]

theorem RS.whiskerLeft_modMultiπ_headAct_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) {Z : D} (h : modMulti A (X :: l) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modMultiπ A (X :: l))) (CategoryTheory.CategoryStruct.comp (modMultiHeadAct A X l) h) = CategoryTheory.CategoryStruct.comp (modListHeadAct A X l) (CategoryTheory.CategoryStruct.comp (modMultiπ A (X :: l)) h)

Defining equation of the descended head action.

theorem RS.modMultiHeadAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (modMulti A (X :: l))) (modMultiHeadAct A X l) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (modMulti A (X :: l))).hom

Unitality of the descended head action.

theorem RS.modMultiHeadAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (modMulti A (X :: l))) (modMultiHeadAct A X l) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (modMulti A (X :: l))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modMultiHeadAct A X l)) (modMultiHeadAct A X l))

Associativity of the descended head action.

@[implicit_reducible]

noncomputable def RS.modMultiModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : CategoryTheory.ModObj A (modMulti A (X :: l))

The multi-tensor of a non-empty list is a module over A.

Equations

• RS.modMultiModObj A X l = { smul := RS.modMultiHeadAct A X l, one_smul := ⋯, mul_smul := ⋯ }

noncomputable def RS.modMultiMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : CategoryTheory.Mod D A

The multi-tensor of a non-empty list, bundled as a module.

Equations

• RS.modMultiMod A X l = { X := RS.modMulti A (X :: l), mod := RS.modMultiModObj A X l }

@[simp]

theorem RS.modMultiMod_X {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X : CategoryTheory.Mod D A) (l : List (CategoryTheory.Mod D A)) : (modMultiMod A X l).X = modMulti A (X :: l)