Carrier-level zigzag identities

The zigzag laws of a Mod-internal duality datum are stated at the multi-tensor level, where the wide-coequalizer presentation keeps them associativity-free. Their consumers work on the carriers M.X and M'.X, through the binary relative tensor alone: insert the copairing beside the carrier, contract the crossing pair through the descended pairing, and let the resulting scalar act on the inserted half. This file identifies both triangle composites with their carrier forms, unconditionally, and derives the carrier-level triangle identities from the multi-level laws and conversely.

• zigContract, zagContract: the carrier contractions, morphisms out of modTensor A M M' ⊗ M.X and M'.X ⊗ modTensor A M M' descended along the whiskered module-tensor coequalizers, with defining equations isolating modTensorπ A M' M ≫ p.
• zigComposite_eq_carrier, zagComposite_eq_carrier: the multi-level triangle composites are the singleton conjugates of the carrier words. No zigzag hypothesis enters.
• zigzag_carrier_zig, zigzag_carrier_zag: the carrier triangle identities of a zigzag datum, with quantified variants for any solution of the contraction's defining equation.
• modZigzagDatum_of_carrier: the converse packaging, producing the multi-level laws from the carrier-level identities.

theorem RS.iso_conj_id_iff {D : Type u} [CategoryTheory.Category.{v, u} D] {X Y : D} (i : X ≅ Y) {g : Y ⟶ Y} : CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.CategoryStruct.comp g i.inv) = CategoryTheory.CategoryStruct.id X ↔ g = CategoryTheory.CategoryStruct.id Y

Conjugation by an isomorphism preserves and reflects the identity.

The singleton comparison as a conjugation

theorem RS.modMultiπ_single {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] (X : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modMultiπ A [X]) (modMultiSingle A X).hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).hom

The singleton projection against the comparison iso: the right unitor of the carrier.

theorem RS.modMultiπ_single_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] (A : D) [CategoryTheory.MonObj A] (X : CategoryTheory.Mod D A) {Z : D} (h : X.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (modMultiπ A [X]) (CategoryTheory.CategoryStruct.comp (modMultiSingle A X).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).hom h

The singleton projection against the comparison iso: the right unitor of the carrier.

theorem RS.eq_single_conj {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] {X Y : CategoryTheory.Mod D A} {f : modMulti A [X] ⟶ modMulti A [Y]} {g : X.X ⟶ Y.X} (h : CategoryTheory.CategoryStruct.comp (modMultiπ A [X]) (CategoryTheory.CategoryStruct.comp f (modMultiSingle A Y).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).hom g) : f = CategoryTheory.CategoryStruct.comp (modMultiSingle A X).hom (CategoryTheory.CategoryStruct.comp g (modMultiSingle A Y).inv)

Recognise a singleton conjugate: a multi-level morphism whose projection matches a carrier morphism through the unitor is the conjugate of that morphism.

The zig triangle on the carrier

theorem RS.contract3Fold_single {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) : CategoryTheory.CategoryStruct.comp (contract3Fold A p M) (modMultiSingle A M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X).hom) (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p))) (actRight A M.X)

The trailing contraction fold against the singleton comparison: pair the trailing window, act on the head from the right.

theorem RS.window_contract3Fold_carrier {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) (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.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) M'.X) (CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w (modList A [M])) (CategoryTheory.MonoidalCategoryStruct.associator M.X M'.X (modList A [M])).hom)) (CategoryTheory.CategoryStruct.comp (contract3Fold A p M) (modMultiSingle A M).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X M'.X M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p)) (actRight A M.X)))

A trailing window against the resolved contraction: stripping the unit seed of the fold, the window meets the carrier contraction word.

theorem RS.zigContract_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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegM A M M') M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X M'.X M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p)) (actRight A M.X))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegN A M M') M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X M'.X M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p)) (actRight A M.X)))

The descent condition of the trailing carrier contraction: the two legs of the crossing pair agree, through the boundary condition of the fold-level contraction.

noncomputable def RS.zigContract {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)] [∀ (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} (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) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A M M') M.X ⟶ M.X

The carrier contraction of the zig triangle: on modTensor A M M' ⊗ M.X, the inserted M'-half pairs against the trailing carrier through the descended pairing and the resulting scalar acts on the inserted M-half from the right. Descended along the right-whiskered module-tensor coequalizer.

Equations

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

@[simp]

theorem RS.whiskerRight_modTensorπ_zigContract {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)] [∀ (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} (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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M M') M.X) (zigContract A p hp) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X M'.X M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p)) (actRight A M.X))

Defining equation of the zig carrier contraction: the pairing occurrence is isolated as modTensorπ A M' M ≫ p.

@[simp]

theorem RS.whiskerRight_modTensorπ_zigContract_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)] [∀ (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} (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) {Z : D} (h : M.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M M') M.X) (CategoryTheory.CategoryStruct.comp (zigContract A p hp) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X M'.X M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p)) (CategoryTheory.CategoryStruct.comp (actRight A M.X) h))

Defining equation of the zig carrier contraction: the pairing occurrence is isolated as modTensorπ A M' M ≫ p.

theorem RS.zigContract_unique {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)] [∀ (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} (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) {e : CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A M M') M.X ⟶ M.X} (he : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A M M') M.X) e = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X M'.X M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p)) (actRight A M.X))) : e = zigContract A p hp

The zig carrier contraction is the unique solution of its defining equation.

theorem RS.pairInv_concat_contract3_single {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} (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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiPairInv A M M') (modList A [M])) (CategoryTheory.CategoryStruct.comp (modMultiConcatFst A [M, M'] [M]) (CategoryTheory.CategoryStruct.comp (modMultiContract3 A p hp M) (modMultiSingle A M).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor A M M') (CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X).hom) (zigContract A p hp)

The inserted pair against the concatenation and trailing contraction: the multi-level word collapses to the carrier contraction.

theorem RS.copairImage_eq {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') : copairImage A c = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one c) (modMultiPairInv A M M')

The image of a copairing splits into the copairing and the pair comparison.

theorem RS.zigComposite_eq_carrier {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) : zigComposite A c p hp = CategoryTheory.CategoryStruct.comp (modMultiSingle A M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one c) M.X) (zigContract A p hp))) (modMultiSingle A M).inv)

The zig composite in carrier form: conjugated by the singleton comparison, the multi-level zig composite is the carrier insertion of the copairing followed by the carrier contraction. No zigzag law enters.

theorem RS.zig_carrier_of_multi {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) (h : zigComposite A c p hp = CategoryTheory.CategoryStruct.id (modMulti A [M])) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one c) M.X) (zigContract A p hp)) = CategoryTheory.CategoryStruct.id M.X

The carrier zig identity from the multi-level zig law.

theorem RS.multi_of_zig_carrier {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) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one c) M.X) (zigContract A p hp)) = CategoryTheory.CategoryStruct.id M.X) : zigComposite A c p hp = CategoryTheory.CategoryStruct.id (modMulti A [M])

The multi-level zig law from the carrier zig identity.

The zag triangle on the carrier

theorem RS.contract3LFold_single {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) : CategoryTheory.CategoryStruct.comp (contract3LFold A p M') (modMultiSingle A M').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X (CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p) (CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.rightUnitor M'.X).hom) (actLeft A M'.X)))

The leading contraction fold against the singleton comparison: pair the leading window, act on the remainder from the left.

theorem RS.window_contract3LFold_carrier {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) (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 M'.X (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X A) M'.X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w (modList A [])) (CategoryTheory.MonoidalCategoryStruct.associator M.X M'.X (modList A [])).hom))) (CategoryTheory.CategoryStruct.comp (contract3LFold A p M') (modMultiSingle A M').hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p) M'.X) (actLeft A M'.X)))

A leading window against the resolved contraction: stripping the unit seed of the fold, the window meets the carrier contraction word.

theorem RS.zagContract_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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (modTensorLegM A M M')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p) M'.X) (actLeft A M'.X))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (modTensorLegN A M M')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p) M'.X) (actLeft A M'.X)))

The descent condition of the leading carrier contraction: the two legs of the crossing pair agree, through the boundary condition of the fold-level contraction.

noncomputable def RS.zagContract {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) : CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X (modTensor A M M') ⟶ M'.X

The carrier contraction of the zag triangle: on M'.X ⊗ modTensor A M M', the leading carrier pairs against the inserted M-half through the descended pairing and the resulting scalar acts on the inserted M'-half from the left. Descended along the left-whiskered module-tensor coequalizer.

Equations

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

@[simp]

theorem RS.whiskerLeft_modTensorπ_zagContract {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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (modTensorπ A M M')) (zagContract A p hp) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p) M'.X) (actLeft A M'.X))

Defining equation of the zag carrier contraction: the pairing occurrence is isolated as modTensorπ A M' M ≫ p.

@[simp]

theorem RS.whiskerLeft_modTensorπ_zagContract_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) {Z : D} (h : M'.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (modTensorπ A M M')) (CategoryTheory.CategoryStruct.comp (zagContract A p hp) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p) M'.X) (CategoryTheory.CategoryStruct.comp (actLeft A M'.X) h))

Defining equation of the zag carrier contraction: the pairing occurrence is isolated as modTensorπ A M' M ≫ p.

theorem RS.zagContract_unique {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) {e : CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X (modTensor A M M') ⟶ M'.X} (he : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (modTensorπ A M M')) e = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p) M'.X) (actLeft A M'.X))) : e = zagContract A p hp

The zag carrier contraction is the unique solution of its defining equation.

theorem RS.pairInv_concat_contract3L_single {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} (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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modList A [M']) (modMultiPairInv A M M')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modMultiπ A [M']) (modMulti A [M, M'])) (CategoryTheory.CategoryStruct.comp (modMultiConcat A [M'] [M, M']) (CategoryTheory.CategoryStruct.comp (modMultiContract3L A p hp M') (modMultiSingle A M').hom))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor M'.X).hom (modTensor A M M')) (zagContract A p hp)

The inserted pair against the concatenation and leading contraction: the multi-level word collapses to the carrier contraction.

theorem RS.zagComposite_eq_carrier {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) : zagComposite A c p hp = CategoryTheory.CategoryStruct.comp (modMultiSingle A M').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one c)) (zagContract A p hp))) (modMultiSingle A M').inv)

The zag composite in carrier form: conjugated by the singleton comparison, the multi-level zag composite is the carrier insertion of the copairing followed by the carrier contraction. No zigzag law enters.

theorem RS.zag_carrier_of_multi {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) (h : zagComposite A c p hp = CategoryTheory.CategoryStruct.id (modMulti A [M'])) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one c)) (zagContract A p hp)) = CategoryTheory.CategoryStruct.id M'.X

The carrier zag identity from the multi-level zag law.

theorem RS.multi_of_zag_carrier {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) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one c)) (zagContract A p hp)) = CategoryTheory.CategoryStruct.id M'.X) : zagComposite A c p hp = CategoryTheory.CategoryStruct.id (modMulti A [M'])

The multi-level zag law from the carrier zag identity.

The carrier identities of a zigzag datum

theorem RS.zigzag_carrier_zig {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} {d : ModDualityDatum A M M'} (hz : ModZigzagDatum A d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d.copair) M.X) (zigContract A d.pair ⋯)) = CategoryTheory.CategoryStruct.id M.X

The carrier zig identity of a zigzag datum: insert the copairing on the left of the carrier and contract; the composite is the identity of M.X.

theorem RS.zigzag_carrier_zig_assoc {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} {d : ModDualityDatum A M M'} (hz : ModZigzagDatum A d) {Z : D} (h : M.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d.copair) M.X) (CategoryTheory.CategoryStruct.comp (zigContract A d.pair ⋯) h)) = h

The carrier zig identity of a zigzag datum: insert the copairing on the left of the carrier and contract; the composite is the identity of M.X.

theorem RS.zigzag_carrier_zag {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} {d : ModDualityDatum A M M'} (hz : ModZigzagDatum A d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d.copair)) (zagContract A d.pair ⋯)) = CategoryTheory.CategoryStruct.id M'.X

The carrier zag identity of a zigzag datum: insert the copairing on the right of the dual carrier and contract; the composite is the identity of M'.X.

theorem RS.zigzag_carrier_zag_assoc {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} {d : ModDualityDatum A M M'} (hz : ModZigzagDatum A d) {Z : D} (h : M'.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d.copair)) (CategoryTheory.CategoryStruct.comp (zagContract A d.pair ⋯) h)) = h

The carrier zag identity of a zigzag datum: insert the copairing on the right of the dual carrier and contract; the composite is the identity of M'.X.

theorem RS.modZigzagDatum_of_carrier {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} {d : ModDualityDatum A M M'} (hzig : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d.copair) M.X) (zigContract A d.pair ⋯)) = CategoryTheory.CategoryStruct.id M.X) (hzag : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor M'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d.copair)) (zagContract A d.pair ⋯)) = CategoryTheory.CategoryStruct.id M'.X) : ModZigzagDatum A d

The converse packaging: the multi-level zigzag laws from the carrier-level triangle identities.