Insertion and contraction on the multi-tensor

The two workhorses of the Key Lemma's pairing calculus: inserting a copairing's image at a boundary of the multi-tensor, and contracting a pairing across one. Insertion needs no descent — it lands in the larger multi-tensor through the concatenation; contraction descends through the coequalizer using the pairing's linearity.

noncomputable def RS.modListPairFold {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) : modList A [M', M] ⟶ A

The pairing evaluated on the two-element fold.

Equations

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

theorem RS.append_pair_slot_cases {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {Xs pre post : List (CategoryTheory.Mod D A)} {M M' P Q : CategoryTheory.Mod D A} (hd : Xs ++ [M', M] = pre ++ P :: Q :: post) : (∃ (post' : List (CategoryTheory.Mod D A)), post = post' ++ [M', M] ∧ Xs = pre ++ P :: Q :: post') ∨ post = [M] ∧ Q = M' ∧ Xs = pre ++ [P] ∨ post = [] ∧ P = M' ∧ Q = M ∧ Xs = pre

Case analysis for decompositions of Xs ++ [M', M]: a slot lies inside Xs, at the boundary, or inside the pair.

noncomputable def RS.contract3Fold {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) (N : CategoryTheory.Mod D A) : modList A [N, M', M] ⟶ modMulti A [N]

The fold-level three-window contraction: pair off the trailing window, act on the head with the resulting scalar.

Equations

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

theorem RS.window_contract3Fold {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) (N : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X A) M.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X M.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft N.X (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w (modList A [])) (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X (modList A [])).hom)) (contract3Fold A p N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft N.X (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X A) M.X)).hom (CategoryTheory.CategoryStruct.comp w (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p)))) (CategoryTheory.CategoryStruct.comp (actRight A N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor N.X).inv (modMultiπ A [N])))

The window morphism of the trailing pair passes to the pairing through the projection.

theorem RS.contract3Fold_boundary_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) (hp : CategoryTheory.CategoryStruct.comp (actLeft A (modTensor A M' M)) p = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A p) CategoryTheory.MonObj.mul) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modMultiLegM A [] N M' [M]) (contract3Fold A p N) = CategoryTheory.CategoryStruct.comp (modMultiLegN A [] N M' [M]) (contract3Fold A p N)

The boundary-slot condition of the three-window contraction: the two window legs of the head--dual boundary agree after the contraction, through the linearity of the pairing.

noncomputable def RS.modMultiContract3 {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) (hp : CategoryTheory.CategoryStruct.comp (actLeft A (modTensor A M' M)) p = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A p) CategoryTheory.MonObj.mul) (N : CategoryTheory.Mod D A) : modMulti A [N, M', M] ⟶ modMulti A [N]

The multi-level contraction at a three-element window: a linear pairing contracts the trailing pair of the multi-tensor, the scalar acting on the head.

Equations

• RS.modMultiContract3 A p hp N = RS.modMultiDesc A (RS.contract3Fold A p N) ⋯

@[simp]

theorem RS.modMultiπ_contract3 {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) (hp : CategoryTheory.CategoryStruct.comp (actLeft A (modTensor A M' M)) p = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A p) CategoryTheory.MonObj.mul) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modMultiπ A [N, M', M]) (modMultiContract3 A p hp N) = contract3Fold A p N

Defining equation of the three-window contraction.

@[simp]

theorem RS.modMultiπ_contract3_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) (hp : CategoryTheory.CategoryStruct.comp (actLeft A (modTensor A M' M)) p = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A p) CategoryTheory.MonObj.mul) (N : CategoryTheory.Mod D A) {Z : D} (h : modMulti A [N] ⟶ Z) : CategoryTheory.CategoryStruct.comp (modMultiπ A [N, M', M]) (CategoryTheory.CategoryStruct.comp (modMultiContract3 A p hp N) h) = CategoryTheory.CategoryStruct.comp (contract3Fold A p N) h

Defining equation of the three-window contraction.

noncomputable def RS.copairImage {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] {M M' : CategoryTheory.Mod D A} (c : A ⟶ modTensor A M M') : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ modMulti A [M, M']

The image of a copairing at the two-element multi-tensor.

Equations

• RS.copairImage A c = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp c (RS.modMultiPair A M M').inv)

noncomputable def RS.zigComposite {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (c : A ⟶ modTensor A M M') (p : modTensor A M' M ⟶ A) (hp : CategoryTheory.CategoryStruct.comp (actLeft A (modTensor A M' M)) p = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A p) CategoryTheory.MonObj.mul) : modMulti A [M] ⟶ modMulti A [M]

The zig composite of a copairing and a linear pairing: insert the copairing on the left, concatenate, and contract the trailing pair. The zigzag law of a duality datum states that this composite is the identity.

Equations

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