Contraction of a leading dual pair on the multi-tensor

The mirror image of the three-window contraction of ModIns.lean: a linear pairing contracts the leading pair of the multi-tensor, its scalar acting on the head of the remainder from the left, so no braid is needed at the fold level. The zag composite inserts a copairing's image on the right and contracts the leading pair.

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

Case analysis for decompositions of the three-element list [M', M, N]: a slot is the leading pair or the boundary.

noncomputable def RS.contract3LFold {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 [M', M, N] ⟶ modMulti A [N]

The fold-level three-window contraction of a leading pair: pair off the leading window, act on the head of the remainder with the resulting scalar from the left.

Equations

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

theorem RS.window_contract3LFold {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.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w (modList A [N])) (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X (modList A [N])).hom) (contract3LFold A p N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp w (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p)) (CategoryTheory.MonoidalCategoryStruct.tensorObj N.X (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))) (CategoryTheory.CategoryStruct.comp (modListHeadAct A N []) (modMultiπ A [N]))

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

theorem RS.contract3LFold_pair_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] (A : D) [CategoryTheory.MonObj A] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modMultiLegM A [] M' M [N]) (contract3LFold A p N) = CategoryTheory.CategoryStruct.comp (modMultiLegN A [] M' M [N]) (contract3LFold A p N)

The pair-slot condition of the leading three-window contraction: the two window legs of the leading pair agree after the contraction.

theorem RS.contract3LFold_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 [M'] M N []) (contract3LFold A p N) = CategoryTheory.CategoryStruct.comp (modMultiLegN A [M'] M N []) (contract3LFold A p N)

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

noncomputable def RS.modMultiContract3L {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 [M', M, N] ⟶ modMulti A [N]

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

Equations

• RS.modMultiContract3L A p hp N = RS.modMultiDesc A (RS.contract3LFold A p N) ⋯

@[simp]

theorem RS.modMultiπ_contract3L {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 [M', M, N]) (modMultiContract3L A p hp N) = contract3LFold A p N

Defining equation of the leading three-window contraction.

@[simp]

theorem RS.modMultiπ_contract3L_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 [M', M, N]) (CategoryTheory.CategoryStruct.comp (modMultiContract3L A p hp N) h) = CategoryTheory.CategoryStruct.comp (contract3LFold A p N) h

Defining equation of the leading three-window contraction.

noncomputable def RS.zagComposite {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 zag composite of a copairing and a linear pairing: insert the copairing on the right, concatenate, and contract the leading pair. The zagzig 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.