The odd twist of a duality datum

A self-dual object of the ambient category makes the free module it generates self-dual over any commutative base: the duality datum over the trivial base is carried onto the free module and then base-changed, and both steps preserve the zigzag laws. For an odd line the self-duality is the square trivialisation, so tensoring a duality datum with the line datum and transporting along the twist shuffle gives the odd twist of a duality datum, zigzag laws included.

noncomputable def RS.unitFreeDatum {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)] (V : D) [CategoryTheory.ExactPairing V V] : ModDualityDatum (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (freeMod (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) V) (freeMod (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) V)

The self-duality datum over the trivial base, carried onto the free module of the trivial base.

Equations

• RS.unitFreeDatum V = RS.ModDualityDatum.transferIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (RS.unitBaseDatum V V) (RS.unitFreeIso V).symm (RS.unitFreeIso V).symm

theorem RS.unitFreeDatum_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)] (V : D) [CategoryTheory.ExactPairing V V] : ModZigzagDatum (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (unitFreeDatum V)

The carried datum satisfies the zigzag laws.

noncomputable def RS.freeSelfDatum {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] (V : D) [CategoryTheory.ExactPairing V V] : ModDualityDatum A (freeMod A V) (freeMod A V)

The free module on a self-dual object is self-dual over any commutative base.

Equations

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

theorem RS.freeSelfDatum_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] (V : D) [CategoryTheory.ExactPairing V V] : ModZigzagDatum A (freeSelfDatum A V)

The free self-duality datum satisfies the zigzag laws.

noncomputable def RS.lineDatum {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive 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] (L : OddLine D) : ModDualityDatum A (freeMod A L.obj) (freeMod A L.obj)

The line datum: the module generated by the odd line is self-dual over any commutative base.

Equations

• RS.lineDatum A L = RS.freeSelfDatum A L.obj

theorem RS.lineDatum_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] (L : OddLine D) : ModZigzagDatum A (lineDatum A L)

The line datum satisfies the zigzag laws.

noncomputable def RS.twistDatum {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive 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] (L : OddLine D) {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : ModDualityDatum A (tensorLeftMod A L.obj M) (tensorLeftMod A L.obj M')

The odd twist of a duality datum: tensor with the line datum and transport along the twist shuffle.

Equations

• RS.twistDatum A L d = RS.ModDualityDatum.transferIso A (RS.tensorDatum A (RS.lineDatum A L) d) (RS.freeTensorTwistIso A L.obj M).symm (RS.freeTensorTwistIso A L.obj M').symm

theorem RS.twistDatum_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] (L : OddLine D) {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) : ModZigzagDatum A (twistDatum A L d)

The odd twist preserves the zigzag laws.