Permutations across the power pairing

The nested power pairing consumes the M'-power from the top and the M-power from the bottom, so it pairs slot j of the M'-power against slot n - 1 - j of the M-power. Moving a permutation of the M-slots across the pairing therefore turns it into the order-reversing adjoint permutation of the M'-slots.

• adjPerm: the adjoint σ ↦ rev ∘ σ⁻¹ ∘ rev. The convention is chosen so that the exchange law holds verbatim; it is an anti-homomorphism (adjPerm_mul) and an involution (adjPerm_adjPerm), and on transpositions it reverses the two slots (adjPerm_swap).
• swapTop_powPeel, powPeel_permMor_swap, powPeel_permMor_low: the head peel intertwines an adjacent braiding away from the bottom slot with the braiding one slot down, and resolves the bottom braiding into the braiding of the two exposed factors.
• pairStep_dbl_braid: the doubled generic step absorbs the braiding of its two consumed M'-factors as the braiding of its two consumed M-factors — the boundary of the exchange law.
• rawPair_perm: the exchange law — a permutation of the M-power slots crosses the raw pairing as the adjoint permutation of the M'-power slots.
• pairPow_perm, symPowIdem_pairPow: the exchange law descended to the module powers, and its average over the group — the symmetriser on either side of the descended pairing agree, the self-adjointness that transfers the power-level duality to the symmetric powers.

The order-reversing adjoint of a permutation

def RS.adjPerm {n : ℕ} (σ : Equiv.Perm (Fin n)) : Equiv.Perm (Fin n)

The order-reversing adjoint of a permutation: conjugate the inverse by the order reversal of the slots. The inverse makes it an anti-homomorphism, which is the direction in which permutations cross the power pairing.

Equations

• RS.adjPerm σ = Fin.revPerm * σ⁻¹ * Fin.revPerm

@[simp]

theorem RS.adjPerm_apply {n : ℕ} (σ : Equiv.Perm (Fin n)) (i : Fin n) : (adjPerm σ) i = (σ⁻¹ i.rev).rev

@[simp]

theorem RS.adjPerm_one {n : ℕ} : adjPerm 1 = 1

The adjoint of the identity is the identity.

theorem RS.adjPerm_mul {n : ℕ} (σ τ : Equiv.Perm (Fin n)) : adjPerm (σ * τ) = adjPerm τ * adjPerm σ

The adjoint is an anti-homomorphism.

@[simp]

theorem RS.adjPerm_adjPerm {n : ℕ} (σ : Equiv.Perm (Fin n)) : adjPerm (adjPerm σ) = σ

The adjoint is an involution.

theorem RS.adjPerm_swap {n : ℕ} (u v : Fin n) : adjPerm (Equiv.swap u v) = Equiv.swap u.rev v.rev

The adjoint of a transposition reverses its two slots.

theorem RS.adjPerm_swap_castSucc_succ {m : ℕ} (i : Fin (m + 1)) : adjPerm (Equiv.swap i.castSucc i.succ) = Equiv.swap i.rev.castSucc i.rev.succ

The adjoint of an adjacent transposition is the adjacent transposition at the reversed position.

Adjacent braidings across the head peel

The permutation action of Envelope/SymPerm.lean is built from the top of the power, while the pairing peels the bottom. The bridge is the head peel: an adjacent braiding that avoids the bottom slot passes the peel, dropping one slot; the braiding of the bottom two slots resolves, under the double peel, into the braiding of the two exposed factors.

theorem RS.swapTop_powPeel {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) (k : ℕ) : CategoryTheory.CategoryStruct.comp (swapTop X (k + 1)) (powPeel X (k + 2)).hom = CategoryTheory.CategoryStruct.comp (powPeel X (k + 2)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (swapTop X k))

The top braiding passes the head peel, dropping to the top braiding one arity down.

theorem RS.powPeel_permMor_swap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) (q a b : ℕ) (x✝ : a + 2 + b = q) : CategoryTheory.CategoryStruct.comp (permMor X (q + 1) (Equiv.swap ⟨a + 1, ⋯⟩ ⟨a + 2, ⋯⟩)) (powPeel X q).hom = CategoryTheory.CategoryStruct.comp (powPeel X q).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (permMor X q (Equiv.swap ⟨a, ⋯⟩ ⟨a + 1, ⋯⟩)))

An adjacent braiding above the bottom slot passes the head peel, dropping one slot.

theorem RS.powPeel_permMor_low {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) (n : ℕ) : CategoryTheory.CategoryStruct.comp (permMor X (n + 2) (Equiv.swap ⟨0, ⋯⟩ ⟨1, ⋯⟩)) (CategoryTheory.CategoryStruct.comp (powPeel X (n + 1)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (powPeel X n).hom)) = CategoryTheory.CategoryStruct.comp (powPeel X (n + 1)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (powPeel X n).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X (tensorPow D X n)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X X).hom (tensorPow D X n)) (CategoryTheory.MonoidalCategoryStruct.associator X X (tensorPow D X n)).hom)))

The bottom braiding resolves under the double peel into the braiding of the two exposed head factors.

The doubled step absorbs the boundary braiding

The recursion of the power pairing consumes the top M'-factor against the bottom M-factor; two consecutive steps consume the top two M'-factors against the bottom two M-factors. The boundary of the exchange law is that braiding the two consumed M'-factors equals braiding the two consumed M-factors, across the doubled step. Everything here is at general objects, over an opaque pairing u and continuation r; commutativity of the monoid enters exactly once, to exchange the two emitted scalars.

The exchange law

theorem RS.rawPair_perm {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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (n : ℕ) (σ : Equiv.Perm (Fin n)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (permMor M'.X n (adjPerm σ)) (tensorPow D M.X n)) (rawPair A M M' d n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X n) (permMor M.X n σ)) (rawPair A M M' d n)

The exchange law: a permutation of the M-power slots crosses the raw power pairing as the order-reversing adjoint permutation of the M'-power slots.

The descended exchange law and self-adjointness

theorem RS.pairPow_perm {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] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) (σ : Equiv.Perm (Fin n)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowPerm n (adjPerm σ)) (modPow A M.X n)) (pairPow A M M' d n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modPow A M'.X n) (modPowPerm n σ)) (pairPow A M M' d n)

The descended exchange law: a permutation of the module power crosses the descended pairing as its order-reversing adjoint.

theorem RS.symPowIdem_pairPow {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] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (symPowIdem A M'.X n) (modPow A M.X n)) (pairPow A M M' d n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modPow A M'.X n) (symPowIdem A M.X n)) (pairPow A M M' d n)

Self-adjointness of the symmetriser across the pairing: the symmetriser acting on either module power pairs equally. The adjoint is a bijection of the group, so the average over all permutations is invariant under the exchange law.

theorem RS.symPowIdem_pairPow_tensor {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] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowIdem A M'.X n) (CategoryTheory.CategoryStruct.id (modPow A M.X n))) (pairPow A M M' d n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id (modPow A M'.X n)) (symPowIdem A M.X n)) (pairPow A M M' d n)

Self-adjointness of the symmetriser, in tensor form.