The zigzag laws as a sandwich retract #

The triangle identities of a Mod-internal duality datum are carrier-level statements about insertion and contraction. This file rewrites them inside the monoidal structure of the category of modules: the zig triangle says exactly that the sandwich insertion followed by the sandwich contraction is the identity, where both legs are built from the module unitors, the module associator and the relative tensor of morphisms.

That form is what a strong monoidal functor transports, so it is the shape in which base change consumes the zigzag laws.

source

theorem RS.modTensorπ_sandwichCon {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] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') :

CategoryTheory.CategoryStruct.comp (modTensorπ A (modTensorMod A M M') M) (sandwichCon A d).hom = zigContract A d.pair ⋯

The sandwich contraction descends the carrier contraction: reassociating, contracting the trailing pair and collapsing the regular factor is the carrier contraction of the zig triangle.

source

Naming a map out of the regular module: inserting the name of a module map beside the carrier and projecting is the relative tensor of the map with the identity.

source

The sandwich insertion is the copairing insertion: on carriers, expanding the unit and inserting the copairing is naming the copairing beside the carrier.

source

theorem RS.sandwich_zig_carrier {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] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') :

(CategoryTheory.CategoryStruct.comp (sandwichIns A d) (sandwichCon A d)).hom = 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 ⋯))

The sandwich composite is the zig composite: the retract word of the double-dual sandwich has the carrier zig triangle as its underlying morphism.

source

theorem RS.sandwich_zig_iff {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] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') :

The zig triangle is the sandwich retract identity: a duality datum satisfies the carrier zig law exactly when the module is a retract of its double-dual sandwich through the canonical insertion and contraction.

source