The tensor datum inherits the zigzag laws

Deligne's 1.15 tensor part, the verification "left to the reader": the zigzag laws of two duality data pass to their tensor. The tensor copair element is the interchange of the two copair elements, and the tensor contraction against a pure tensor of carriers is the tensor of the component contractions; nesting the two component triangles closes the tensor triangle.

theorem RS.tensorCopair_point {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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] {N₁ N₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (tensorCopair A d₁ d₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d₁.copair) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d₂.copair)) (interchange A N₁ N₁' N₂ N₂'))

The tensor copair element is the interchange of the copair elements.

theorem RS.tensorHom_actRight_π {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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] (N₁ N₂ : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (actRight A N₁.X) (actRight A N₂.X)) (modTensorπ A N₁ N₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ N₁.X A N₂.X A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X N₂.X) CategoryTheory.MonObj.mul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N₁ N₂) A) (CategoryTheory.CategoryStruct.comp (β_ (modTensor A N₁ N₂) A).hom (modTensorAct A N₁ N₂))))

Paired right actions descend to the joint action: acting on both carriers and projecting is multiplying the scalars and acting on the projected pair — the quotient relation of the relative tensor.

theorem RS.interchange_zigContract {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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] {N₁ N₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A N₁ N₁') (modTensor A N₂ N₂')) (modTensorπ A N₁ N₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (interchange A N₁ N₁' N₂ N₂') (modTensor A N₁ N₂)) (zigContract A (tensorDatum A d₁ d₂).pair ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (modTensor A N₁ N₁') (modTensor A N₂ N₂') N₁.X N₂.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (zigContract A d₁.pair ⋯) (zigContract A d₂.pair ⋯)) (modTensorπ A N₁ N₂))

The tensor contraction against the interchange is the tensor of the component contractions: the crossing seats each dual half against its own carrier.

theorem RS.interchange_zagContract {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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] {N₁ N₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N₁' N₂') (CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A N₁ N₁') (modTensor A N₂ N₂'))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor A N₁' N₂') (interchange A N₁ N₁' N₂ N₂')) (zagContract A (tensorDatum A d₁ d₂).pair ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ N₁'.X N₂'.X (modTensor A N₁ N₁') (modTensor A N₂ N₂')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (zagContract A d₁.pair ⋯) (zagContract A d₂.pair ⋯)) (modTensorπ A N₁' N₂'))

The tensor contraction against the interchange is the tensor of the component contractions, zag side: the crossing seats each dual half against its own carrier.

theorem RS.tensorDatum_carrier_zig {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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] {N₁ N₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') (hz₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor N₁.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d₁.copair) N₁.X) (zigContract A d₁.pair ⋯)) = CategoryTheory.CategoryStruct.id N₁.X) (hz₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor N₂.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d₂.copair) N₂.X) (zigContract A d₂.pair ⋯)) = CategoryTheory.CategoryStruct.id N₂.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (modTensor A N₁ N₂)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (tensorDatum A d₁ d₂).copair) (modTensor A N₁ N₂)) (zigContract A (tensorDatum A d₁ d₂).pair ⋯)) = CategoryTheory.CategoryStruct.id (modTensor A N₁ N₂)

The tensor datum inherits the carrier zig identity.

theorem RS.tensorDatum_carrier_zag {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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] {N₁ N₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') (hz₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor N₁'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft N₁'.X (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d₁.copair)) (zagContract A d₁.pair ⋯)) = CategoryTheory.CategoryStruct.id N₁'.X) (hz₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor N₂'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft N₂'.X (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d₂.copair)) (zagContract A d₂.pair ⋯)) = CategoryTheory.CategoryStruct.id N₂'.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (modTensor A N₁' N₂')).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor A N₁' N₂') (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (tensorDatum A d₁ d₂).copair)) (zagContract A (tensorDatum A d₁ d₂).pair ⋯)) = CategoryTheory.CategoryStruct.id (modTensor A N₁' N₂')

The tensor datum inherits the carrier zag identity.

theorem RS.tensorDatum_zigzag {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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] {N₁ N₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') (hz₁ : ModZigzagDatum A d₁) (hz₂ : ModZigzagDatum A d₂) : ModZigzagDatum A (tensorDatum A d₁ d₂)

The tensor of zigzag data is a zigzag datum (Deligne 1.15, tensor part, in triangle form).