Crossing the monoid over a block of the multi-tensor

The endgame of ModMulti.lean: the braided crossing of the monoid A over a whole first block of modules factors through the slot relations of the multi-tensor. From it, the concatenation map descends through the binary modTensor of two bundled multi-tensor modules, and the braiding of two adjacent factors descends to the two-element multi-tensor.

• modCrossMid, modCrossLegOf: the boundary-insertion carrier — the monoid seated between two blocks, under a prefix — and its assembly of a boundary window into a prefix-whiskered leg.
• modCrossHeadWin/modCrossYWin: the two boundary windows — the monoid crosses the whole first block and acts on its head, or acts on the head of the second block.
• modCross_rel: the fold-level crossing relation — the two boundary legs agree after the projection, at every prefix; the crossing is consumed one factor at a time, one slot relation per factor.
• modListCross: the prefix-free crossing relation, in the typed form consumed by the modTensor descent.
• modTensorMulti: the concatenation map descended through the binary module tensor product of two bundled multi-tensors, with its defining equation modTensorπ_multi.
• modWinSwap, modMultiSwapPair: the braiding of the two factors of a two-element multi-tensor, by descent through the single slot relation, with its defining equation modMultiπ_swapPair.

The boundary-insertion carrier

The monoid seated at the boundary between two blocks, under a prefix. The prefix enters by recursion, exactly as in modMultiMid, so that slot-relation consumption below can match prefixes on the nose.

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

The boundary-insertion object: the monoid between the folds of two blocks, whiskered under a prefix.

Equations

• RS.modCrossMid A Xs Ys [] = CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (RS.modList A Xs) A) (RS.modList A Ys)
• RS.modCrossMid A Xs Ys (P :: rest) = CategoryTheory.MonoidalCategoryStruct.tensorObj P.X (RS.modCrossMid A Xs Ys rest)

@[simp]

theorem RS.modCrossMid_nil {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (Xs Ys : List (CategoryTheory.Mod D A)) : modCrossMid A Xs Ys [] = CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (modList A Xs) A) (modList A Ys)

@[simp]

theorem RS.modCrossMid_cons {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (Xs Ys : List (CategoryTheory.Mod D A)) (P : CategoryTheory.Mod D A) (pre : List (CategoryTheory.Mod D A)) : modCrossMid A Xs Ys (P :: pre) = CategoryTheory.MonoidalCategoryStruct.tensorObj P.X (modCrossMid A Xs Ys pre)

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

Assemble a boundary window into a prefix-whiskered leg.

Equations

• RS.modCrossLegOf A Xs Ys w [] = w
• RS.modCrossLegOf A Xs Ys w (P :: rest) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (RS.modCrossLegOf A Xs Ys w rest)

@[simp]

theorem RS.modCrossLegOf_nil {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (Xs Ys : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (modList A Xs) A) (modList A Ys) ⟶ modList A (Xs ++ Ys)) : modCrossLegOf A Xs Ys w [] = w

@[simp]

theorem RS.modCrossLegOf_cons {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (Xs Ys : List (CategoryTheory.Mod D A)) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (modList A Xs) A) (modList A Ys) ⟶ modList A (Xs ++ Ys)) (P : CategoryTheory.Mod D A) (pre : List (CategoryTheory.Mod D A)) : modCrossLegOf A Xs Ys w (P :: pre) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (modCrossLegOf A Xs Ys w pre)

The two boundary windows

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

The crossing window: the monoid braids over the whole first block and acts on its head.

Equations

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

def RS.modCrossYWin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (Xs : List (CategoryTheory.Mod D A)) (Y : CategoryTheory.Mod D A) (m : List (CategoryTheory.Mod D A)) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (modList A Xs) A) (modList A (Y :: m)) ⟶ modList A (Xs ++ Y :: m)

The stationary window: the monoid acts on the head of the second block.

Equations

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

The singleton first block

For a one-module first block the two boundary windows are the two relation legs of the head slot, up to the unit seed of the fold. The bridge below absorbs the seed and retypes the boundary carrier at the relation object of the slot.

def RS.modCrossBridge {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) (m pre : List (CategoryTheory.Mod D A)) : modCrossMid A [X] (Y :: m) pre ⟶ modMultiMid A pre X Y m

The base bridge: absorb the unit seed of a singleton first block and reassociate onto the relation window of the head slot.

Equations

• One or more equations did not get rendered due to their size.
• RS.modCrossBridge A X Y m (P :: rest) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (RS.modCrossBridge A X Y m rest)

theorem RS.modCrossBridge_legM {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : CategoryTheory.Mod D A) (m pre : List (CategoryTheory.Mod D A)) : modCrossLegOf A [X] (Y :: m) (modCrossHeadWin A X [] (Y :: m)) pre = CategoryTheory.CategoryStruct.comp (modCrossBridge A X Y m pre) (modMultiLegM A pre X Y m)

The crossing window of a singleton block is the first relation leg of the head slot, through the bridge.

theorem RS.modCrossBridge_legN {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : CategoryTheory.Mod D A) (m pre : List (CategoryTheory.Mod D A)) : modCrossLegOf A [X] (Y :: m) (modCrossYWin A [X] Y m) pre = CategoryTheory.CategoryStruct.comp (modCrossBridge A X Y m pre) (modMultiLegN A pre X Y m)

The stationary window of a singleton block is the second relation leg of the head slot, through the bridge.

The step of the crossing

For a first block of two or more modules, the crossing decomposes by the hexagon: the monoid braids over the tail of the block first, reaching the relation window of the head slot; the slot relation walks it past the head, and what remains is the crossing of the tail block under a prefix extended by the head.

def RS.modCrossPeel {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : CategoryTheory.Mod D A) (Xs' Ys pre : List (CategoryTheory.Mod D A)) : modCrossMid A (X :: Xs') Ys pre ⟶ modCrossMid A Xs' Ys (pre ++ [X])

Peel the head of the first block into the prefix.

Equations

• One or more equations did not get rendered due to their size.
• RS.modCrossPeel A X Xs' Ys (P :: rest) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (RS.modCrossPeel A X Xs' Ys rest)

theorem RS.modCrossPeel_yWin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : CategoryTheory.Mod D A) (Xs' : List (CategoryTheory.Mod D A)) (Y : CategoryTheory.Mod D A) (m pre : List (CategoryTheory.Mod D A)) (h : pre ++ [X] ++ (Xs' ++ Y :: m) = pre ++ (X :: Xs' ++ Y :: m)) : CategoryTheory.CategoryStruct.comp (modCrossPeel A X Xs' (Y :: m) pre) (CategoryTheory.CategoryStruct.comp (modCrossLegOf A Xs' (Y :: m) (modCrossYWin A Xs' Y m) (pre ++ [X])) (modListCast A h)) = modCrossLegOf A (X :: Xs') (Y :: m) (modCrossYWin A (X :: Xs') Y m) pre

Peeling passes the stationary window: the stationary window of the extended block is the peel followed by the whiskered stationary window of the tail block.

def RS.modCrossStepBridge {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X P : CategoryTheory.Mod D A) (l' Ys pre : List (CategoryTheory.Mod D A)) : modCrossMid A (X :: P :: l') Ys pre ⟶ modMultiMid A pre X P (l' ++ Ys)

The step bridge: braid the monoid over the tail of the first block and retype at the relation window of the head slot.

Equations

• One or more equations did not get rendered due to their size.
• RS.modCrossStepBridge A X P l' Ys (P_1 :: rest) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft P_1.X (RS.modCrossStepBridge A X P l' Ys rest)

theorem RS.modCrossStepBridge_legM {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X P : CategoryTheory.Mod D A) (l' Ys pre : List (CategoryTheory.Mod D A)) : modCrossLegOf A (X :: P :: l') Ys (modCrossHeadWin A X (P :: l') Ys) pre = CategoryTheory.CategoryStruct.comp (modCrossStepBridge A X P l' Ys pre) (modMultiLegM A pre X P (l' ++ Ys))

The crossing window decomposes over the head slot: by the hexagon, the full crossing is the step bridge followed by the first relation leg of the head slot.

theorem RS.modCrossStepBridge_legN {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X P : CategoryTheory.Mod D A) (l' Ys pre : List (CategoryTheory.Mod D A)) (h : pre ++ [X] ++ (P :: l' ++ Ys) = pre ++ (X :: P :: l' ++ Ys)) : CategoryTheory.CategoryStruct.comp (modCrossStepBridge A X P l' Ys pre) (modMultiLegN A pre X P (l' ++ Ys)) = CategoryTheory.CategoryStruct.comp (modCrossPeel A X (P :: l') Ys pre) (CategoryTheory.CategoryStruct.comp (modCrossLegOf A (P :: l') Ys (modCrossHeadWin A P l' Ys) (pre ++ [X])) (modListCast A h))

The step bridge against the second relation leg: past the head slot, what remains is the crossing of the tail block, under the prefix extended by the head.

The crossing relation

theorem RS.modCross_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] (Y : CategoryTheory.Mod D A) (m l : List (CategoryTheory.Mod D A)) (X : CategoryTheory.Mod D A) (pr Zs : List (CategoryTheory.Mod D A)) (h : Zs = pr ++ (X :: l ++ Y :: m)) : CategoryTheory.CategoryStruct.comp (modCrossLegOf A (X :: l) (Y :: m) (modCrossHeadWin A X l (Y :: m)) pr) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) (modMultiπ A Zs)) = CategoryTheory.CategoryStruct.comp (modCrossLegOf A (X :: l) (Y :: m) (modCrossYWin A (X :: l) Y m) pr) (CategoryTheory.CategoryStruct.comp (modListCast A ⋯) (modMultiπ A Zs))

The fold-level crossing relation: after the projection of the multi-tensor, braiding the monoid over the whole first block and acting on its head agrees with acting on the head of the second block, at every ambient prefix. The crossing is consumed one factor at a time, one slot relation per factor.

theorem RS.modListCross {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) (l m : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (β_ (modList A (X :: l)) A).hom (modListHeadAct A X l)) (modList A (Y :: m))) (CategoryTheory.CategoryStruct.comp (modListConcat A (X :: l) (Y :: m)).hom (modMultiπ A (X :: l ++ Y :: m))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (modList A (X :: l)) A (modList A (Y :: m))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modList A (X :: l)) (modListHeadAct A Y m)) (CategoryTheory.CategoryStruct.comp (modListConcat A (X :: l) (Y :: m)).hom (modMultiπ A (X :: l ++ Y :: m))))

The crossing relation, prefix-free: braiding the monoid over the first block and acting on its head agrees, after the projection, with acting on the head of the second block. This is the typed form consumed by the modTensor descent below.

Descent of the concatenation through the module tensor

For a commutative monoid the two bundled multi-tensor modules have a binary modTensor; the concatenation map coequalizes its two legs — by the crossing relation — and so descends.

theorem RS.modTensorLeg_multi {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.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X Y : CategoryTheory.Mod D A) (l m : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (modTensorLegM A (modMultiMod A X l) (modMultiMod A Y m)) (modMultiConcat A (X :: l) (Y :: m)) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (modMultiMod A X l) (modMultiMod A Y m)) (modMultiConcat A (X :: l) (Y :: m))

The concatenation coequalizes the binary module-tensor legs of two bundled multi-tensors: the crossing relation, lifted through the projections.

noncomputable def RS.modTensorMulti {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.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X Y : CategoryTheory.Mod D A) (l m : List (CategoryTheory.Mod D A)) : modTensor A (modMultiMod A X l) (modMultiMod A Y m) ⟶ modMulti A (X :: l ++ Y :: m)

The concatenation descends to the binary module tensor product of two multi-tensors.

Equations

• RS.modTensorMulti A X Y l m = RS.modTensorDesc A (RS.modMultiMod A X l) (RS.modMultiMod A Y m) (RS.modMultiConcat A (X :: l) (Y :: m)) ⋯

@[simp]

theorem RS.modTensorπ_multi {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.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X Y : CategoryTheory.Mod D A) (l m : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modMultiMod A X l) (modMultiMod A Y m)) (modTensorMulti A X Y l m) = modMultiConcat A (X :: l) (Y :: m)

Defining equation of the descended concatenation against the module-tensor projection.

@[simp]

theorem RS.modTensorπ_multi_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.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X Y : CategoryTheory.Mod D A) (l m : List (CategoryTheory.Mod D A)) {Z : D} (h : modMulti A (X :: l ++ Y :: m) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modMultiMod A X l) (modMultiMod A Y m)) (CategoryTheory.CategoryStruct.comp (modTensorMulti A X Y l m) h) = CategoryTheory.CategoryStruct.comp (modMultiConcat A (X :: l) (Y :: m)) h

Defining equation of the descended concatenation against the module-tensor projection.

theorem RS.tensorHom_modTensorπ_multi {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.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X Y : CategoryTheory.Mod D A) (l m : List (CategoryTheory.Mod D A)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modMultiπ A (X :: l)) (modMultiπ A (Y :: m))) (CategoryTheory.CategoryStruct.comp (modTensorπ A (modMultiMod A X l) (modMultiMod A Y m)) (modTensorMulti A X Y l m)) = CategoryTheory.CategoryStruct.comp (modListConcat A (X :: l) (Y :: m)).hom (modMultiπ A (X :: l ++ Y :: m))

Defining equation of the descended concatenation against the multi-tensor projections: on the folds it is the fold concatenation.

theorem RS.tensorHom_modTensorπ_multi_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.tensorRight Y)] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (X Y : CategoryTheory.Mod D A) (l m : List (CategoryTheory.Mod D A)) {Z : D} (h : modMulti A (X :: l ++ Y :: m) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modMultiπ A (X :: l)) (modMultiπ A (Y :: m))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (modTensorπ A (modMultiMod A X l) (modMultiMod A Y m)) (modTensorMulti A X Y l m)) h) = CategoryTheory.CategoryStruct.comp (modListConcat A (X :: l) (Y :: m)).hom (CategoryTheory.CategoryStruct.comp (modMultiπ A (X :: l ++ Y :: m)) h)

Defining equation of the descended concatenation against the multi-tensor projections: on the folds it is the fold concatenation.

The braiding at a relation window

In a symmetric category the braiding of the two module factors of a relation window carries the monoid along; the window legs intertwine it with the plain braiding of the factors, exchanging the two legs. This mirrors the treatment of the symmetric-power slot exchange, at two distinct modules.

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

Exchange of the two module factors of a relation window, carrying the monoid along: (x ⊗ c) ⊗ y ↦ (y ⊗ c) ⊗ x.

Equations

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

@[simp]

theorem RS.modWinSwap_modWinSwap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modWinSwap A M N) (modWinSwap A N M) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X)

The window exchange is an involution.

@[simp]

theorem RS.modWinSwap_modWinSwap_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (modWinSwap A M N) (CategoryTheory.CategoryStruct.comp (modWinSwap A N M) h) = h

The window exchange is an involution.

theorem RS.modWinSwap_legM {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorLegM A M N) (β_ M.X N.X).hom = CategoryTheory.CategoryStruct.comp (modWinSwap A M N) (modTensorLegN A N M)

The first leg intertwines the window exchange with the braiding: acting on the first factor and braiding is exchanging and acting on the second factor.

theorem RS.modWinSwap_legM_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj N.X M.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorLegM A M N) (CategoryTheory.CategoryStruct.comp (β_ M.X N.X).hom h) = CategoryTheory.CategoryStruct.comp (modWinSwap A M N) (CategoryTheory.CategoryStruct.comp (modTensorLegN A N M) h)

The first leg intertwines the window exchange with the braiding: acting on the first factor and braiding is exchanging and acting on the second factor.

theorem RS.modWinSwap_legN {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorLegN A M N) (β_ M.X N.X).hom = CategoryTheory.CategoryStruct.comp (modWinSwap A M N) (modTensorLegM A N M)

The second leg intertwines the window exchange with the braiding, by the involutivity of both.

theorem RS.modWinSwap_legN_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj N.X M.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorLegN A M N) (CategoryTheory.CategoryStruct.comp (β_ M.X N.X).hom h) = CategoryTheory.CategoryStruct.comp (modWinSwap A M N) (CategoryTheory.CategoryStruct.comp (modTensorLegM A N M) h)

The second leg intertwines the window exchange with the braiding, by the involutivity of both.

The two-element swap

noncomputable def RS.modMultiSwapPair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (M N : CategoryTheory.Mod D A) : modMulti A [M, N] ⟶ modMulti A [N, M]

The braiding of a two-element multi-tensor: the exchange of the two factors descends, the single slot relation consumed through the window exchange.

Equations

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

@[simp]

theorem RS.modMultiπ_swapPair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modMultiπ A [M, N]) (modMultiSwapPair A M N) = CategoryTheory.CategoryStruct.comp (pairResolve A M N) (CategoryTheory.CategoryStruct.comp (β_ M.X N.X).hom (CategoryTheory.CategoryStruct.comp (pairResolveInv A N M) (modMultiπ A [N, M])))

Defining equation of the two-element swap: on the fold it is the braiding of the factors, conjugated by the unit seeds.

@[simp]

theorem RS.modMultiπ_swapPair_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (M N : CategoryTheory.Mod D A) {Z : D} (h : modMulti A [N, M] ⟶ Z) : CategoryTheory.CategoryStruct.comp (modMultiπ A [M, N]) (CategoryTheory.CategoryStruct.comp (modMultiSwapPair A M N) h) = CategoryTheory.CategoryStruct.comp (pairResolve A M N) (CategoryTheory.CategoryStruct.comp (β_ M.X N.X).hom (CategoryTheory.CategoryStruct.comp (pairResolveInv A N M) (CategoryTheory.CategoryStruct.comp (modMultiπ A [N, M]) h)))

Defining equation of the two-element swap: on the fold it is the braiding of the factors, conjugated by the unit seeds.