The power datum inherits the zigzag laws

Deligne's 1.15 tensor part, in chain form: the zigzag laws of a duality datum pass to its tensor powers. The bottom stage is the transfer of the datum along the arity-one comparison isomorphisms — the transfer theorem applies with trivial idempotents. The step peels one inserted couple off the onion-aligned copairing power against the outermost ring of the nested pairing.

theorem RS.modPowPairing_zero {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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') : modPowPairing A M M' d 0 = CategoryTheory.CategoryStruct.comp (modTensorMap A (fromModPowModZero A M') (fromModPowModZero A M)) d.pair

The arity-one power pairing is the pairing, through the comparison isomorphisms.

theorem RS.ModDualityDatum.ext' {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} {x y : ModDualityDatum A N N'} (hp : x.pair = y.pair) (hc : x.copair = y.copair) : x = y

Duality data with equal pairings and copairings are equal.

theorem RS.powDualityDatum_zero {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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') : powDualityDatum A M M' d 0 = ModDualityDatum.transfer A d (fromModPowModZero A M) (fromModPowModZero A M') (toModPowModZero A M) (toModPowModZero A M')

The bottom power datum is the transferred datum: the arity-one comparison isomorphisms carry the datum to its zeroth power.

theorem RS.powDualityDatum_zigzag_zero {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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (hz : ModZigzagDatum A d) : ModZigzagDatum A (powDualityDatum A M M' d 0)

The bottom power datum satisfies the zigzag laws.