Transfer of the zigzag laws along retractions

The zigzag laws pass from a duality datum to its transfer along a section–retraction pair, given the self-adjointness of the composite idempotent across the pairing. The transferred zig factors as section, original zig, retraction: the idempotent slides across the pairing once and then dissolves into the retraction. Instantiated at the symmetriser section and projection, this gives the zigzag laws of the symmetric-power datum from those of the power datum — Deligne's 1.15.1.

theorem RS.map_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] {P P' Q Q' : CategoryTheory.Mod D A} (d₀ : ModDualityDatum A P P') (s : Q ⟶ P) (s' : Q' ⟶ P') (r : P ⟶ Q) (r' : P' ⟶ Q') (hsr : CategoryTheory.CategoryStruct.comp s r = CategoryTheory.CategoryStruct.id Q) (hadj : CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.comp r' s') (CategoryTheory.CategoryStruct.id P)) d₀.pair = CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.id P') (CategoryTheory.CategoryStruct.comp r s)) d₀.pair) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorMap A r r') Q.X) (zigContract A (ModDualityDatum.transfer A d₀ s s' r r').pair ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor A P P') s.hom) (CategoryTheory.CategoryStruct.comp (zigContract A d₀.pair ⋯) r.hom)

Retraction images contract through the transferred contraction: precomposing the transferred zig contraction with the retraction image is the section, the original contraction, and the retraction — the idempotent slides across the pairing and dissolves into the retraction.

theorem RS.transfer_carrier_zig {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] {P P' Q Q' : CategoryTheory.Mod D A} (d₀ : ModDualityDatum A P P') (s : Q ⟶ P) (s' : Q' ⟶ P') (r : P ⟶ Q) (r' : P' ⟶ Q') (hz₀ : ModZigzagDatum A d₀) (hsr : CategoryTheory.CategoryStruct.comp s r = CategoryTheory.CategoryStruct.id Q) (hadj : CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.comp r' s') (CategoryTheory.CategoryStruct.id P)) d₀.pair = CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.id P') (CategoryTheory.CategoryStruct.comp r s)) d₀.pair) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Q.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (ModDualityDatum.transfer A d₀ s s' r r').copair) Q.X) (zigContract A (ModDualityDatum.transfer A d₀ s s' r r').pair ⋯)) = CategoryTheory.CategoryStruct.id Q.X

The transferred carrier zig identity: the zig of the transferred datum factors as section, original zig, retraction.

theorem RS.map_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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {P P' Q Q' : CategoryTheory.Mod D A} (d₀ : ModDualityDatum A P P') (s : Q ⟶ P) (s' : Q' ⟶ P') (r : P ⟶ Q) (r' : P' ⟶ Q') (hsr' : CategoryTheory.CategoryStruct.comp s' r' = CategoryTheory.CategoryStruct.id Q') (hadj : CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.comp r' s') (CategoryTheory.CategoryStruct.id P)) d₀.pair = CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.id P') (CategoryTheory.CategoryStruct.comp r s)) d₀.pair) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q'.X (modTensorMap A r r')) (zagContract A (ModDualityDatum.transfer A d₀ s s' r r').pair ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight s'.hom (modTensor A P P')) (CategoryTheory.CategoryStruct.comp (zagContract A d₀.pair ⋯) r'.hom)

Retraction images contract through the transferred zag contraction: the mirror of map_zigContract.

theorem RS.transfer_carrier_zag {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] {P P' Q Q' : CategoryTheory.Mod D A} (d₀ : ModDualityDatum A P P') (s : Q ⟶ P) (s' : Q' ⟶ P') (r : P ⟶ Q) (r' : P' ⟶ Q') (hz₀ : ModZigzagDatum A d₀) (hsr' : CategoryTheory.CategoryStruct.comp s' r' = CategoryTheory.CategoryStruct.id Q') (hadj : CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.comp r' s') (CategoryTheory.CategoryStruct.id P)) d₀.pair = CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.id P') (CategoryTheory.CategoryStruct.comp r s)) d₀.pair) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Q'.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q'.X (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (ModDualityDatum.transfer A d₀ s s' r r').copair)) (zagContract A (ModDualityDatum.transfer A d₀ s s' r r').pair ⋯)) = CategoryTheory.CategoryStruct.id Q'.X

The transferred carrier zag identity: the mirror factorization through the dual-side section and retraction.

theorem RS.modZigzagDatum_transfer {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] {P P' Q Q' : CategoryTheory.Mod D A} (d₀ : ModDualityDatum A P P') (s : Q ⟶ P) (s' : Q' ⟶ P') (r : P ⟶ Q) (r' : P' ⟶ Q') (hz₀ : ModZigzagDatum A d₀) (hsr : CategoryTheory.CategoryStruct.comp s r = CategoryTheory.CategoryStruct.id Q) (hsr' : CategoryTheory.CategoryStruct.comp s' r' = CategoryTheory.CategoryStruct.id Q') (hadj : CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.comp r' s') (CategoryTheory.CategoryStruct.id P)) d₀.pair = CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.id P') (CategoryTheory.CategoryStruct.comp r s)) d₀.pair) : ModZigzagDatum A (ModDualityDatum.transfer A d₀ s s' r r')

The zigzag laws transfer along retractions: given the self-adjointness of the composite idempotents across the pairing, the transferred datum satisfies the zigzag laws.

theorem RS.symDualityDatum_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] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (d : ModDualityDatum A M M') (n : ℕ) (hz : ModZigzagDatum A (powDualityDatum A M M' d n)) : ModZigzagDatum A (symDualityDatum A M M' d n)

The symmetric-power datum inherits the zigzag laws (Deligne 1.15.1): the transfer along the symmetriser section and projection, with the self-adjointness of the symmetriser across the nested pairing as the idempotent-slide input.