The duality datum over the trivial base

An exact pairing of the ambient category induces a duality datum between the corresponding modules over the tensor unit: the relative tensor collapses to the plain tensor, and the pairing and copairing pass through the collapse.

noncomputable def RS.unitBasePair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (X Y : D) [CategoryTheory.ExactPairing X Y] : modTensor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (unitMod Y) (unitMod X) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

The pairing over the trivial base: collapse and evaluate.

Equations

• RS.unitBasePair X Y = CategoryTheory.CategoryStruct.comp (RS.modTensorUnitBase (RS.unitMod Y) (RS.unitMod X)).hom (ε_ X Y)

noncomputable def RS.unitBaseCopair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (X Y : D) [CategoryTheory.ExactPairing X Y] : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ modTensor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (unitMod X) (unitMod Y)

The copairing over the trivial base: coevaluate and embed.

Equations

• RS.unitBaseCopair X Y = CategoryTheory.CategoryStruct.comp (η_ X Y) (RS.modTensorUnitBase (RS.unitMod X) (RS.unitMod Y)).inv

theorem RS.unitBasePair_linear {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)] (X Y : D) [CategoryTheory.ExactPairing X Y] : CategoryTheory.CategoryStruct.comp (actLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (modTensor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (unitMod Y) (unitMod X))) (unitBasePair X Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (unitBasePair X Y)) CategoryTheory.MonObj.mul

The pairing is linear over the trivial base.

theorem RS.unitBaseCopair_linear {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)] (X Y : D) [CategoryTheory.ExactPairing X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (unitBaseCopair X Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (unitBaseCopair X Y)) (actLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (modTensor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (unitMod X) (unitMod Y)))

The copairing is linear over the trivial base.

noncomputable def RS.unitBaseDatum {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)] (X Y : D) [CategoryTheory.ExactPairing X Y] : ModDualityDatum (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (unitMod X) (unitMod Y)

The duality datum over the trivial base attached to an exact pairing of the ambient category.

Equations

• RS.unitBaseDatum X Y = { pair := RS.unitBasePair X Y, copair := RS.unitBaseCopair X Y, pair_linear := ⋯, copair_linear := ⋯ }

theorem RS.unitBaseDatum_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)] (X Y : D) [CategoryTheory.ExactPairing X Y] : ModZigzagDatum (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (unitBaseDatum X Y)

The trivial-base datum satisfies the zigzag laws: through the collapse they are the zigzag identities of the exact pairing.