Conjugating the permutation action through the twisted power

identification

Over the plain covers the twisted power identification is the shuffle followed by the projection, so the descended permutation action on the powers of a twisted module conjugates to the simultaneous action: the plain action on the twisting powers alongside the descended action on the module powers.

theorem RS.twistPow_perm_conj {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] (V : D) (R : CategoryTheory.Mod D A) (k : ℕ) (σ : Equiv.Perm (Fin (k + 1))) : CategoryTheory.CategoryStruct.comp (modPowPerm (k + 1) σ) (twistPowModIso A V R k).hom.hom = CategoryTheory.CategoryStruct.comp (twistPowModIso A V R k).hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (permMor V (k + 1) σ) (modPowPerm (k + 1) σ))

The conjugated permutation action: through the twisted power identification, the descended action on the powers of a twisted module is the simultaneous action on the twisting powers and the module powers.

noncomputable def RS.twistPowCarrierIso {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] (V : D) (R : CategoryTheory.Mod D A) (k : ℕ) : modPow A (tensorLeftMod A V R).X (k + 1) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D V (k + 1)) (modPow A R.X (k + 1))

The carrier of the twisted power identification.

Equations

• RS.twistPowCarrierIso A V R k = { hom := (RS.twistPowModIso A V R k).hom.hom, inv := (RS.twistPowModIso A V R k).inv.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem RS.twistPow_perm_conj_oddLine {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] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : CategoryTheory.Mod D A) (k : ℕ) (σ : Equiv.Perm (Fin (k + 1))) : CategoryTheory.CategoryStruct.comp (modPowPerm (k + 1) σ) (twistPowModIso A L.obj R k).hom.hom = ↑↑(Equiv.Perm.sign σ) • CategoryTheory.CategoryStruct.comp (twistPowModIso A L.obj R k).hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D L.obj (k + 1)) (modPowPerm (k + 1) σ))

Each conjugated permutation over an odd line is the sign times the whiskered module action.

theorem RS.twistPow_symIdem_conj {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] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : CategoryTheory.Mod D A) (k : ℕ) : CategoryTheory.CategoryStruct.comp (symPowIdem A (tensorLeftMod A L.obj R).X (k + 1)) (twistPowModIso A L.obj R k).hom.hom = CategoryTheory.CategoryStruct.comp (twistPowModIso A L.obj R k).hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D L.obj (k + 1)) (altPowIdem A R.X (k + 1)))

The symmetriser collapses over an odd line: through the twisted power identification, the symmetriser of the twisted module powers is the whiskered antisymmetriser of the module powers.

noncomputable def RS.symPowOddTwistIso {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] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : CategoryTheory.Mod D A) (k : ℕ) : symPow A (tensorLeftMod A L.obj R).X (k + 1) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D L.obj (k + 1)) (altPow A R.X (k + 1))

The symmetric powers of an odd twist are the twisted alternating powers: the coequalizer transports along the identification through the symmetriser collapse, and the twist passes out of the colimit.

Equations

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

theorem RS.OddLine.isZero_tensorPow_tensor_iff {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) (n : ℕ) (Z : D) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D L.obj n) Z) ↔ CategoryTheory.Limits.IsZero Z

Tensor powers of the odd line reflect vanishing.

theorem RS.symPowOddTwist_isZero_iff {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] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : CategoryTheory.Mod D A) (k : ℕ) : CategoryTheory.Limits.IsZero (symPow A (tensorLeftMod A L.obj R).X (k + 1)) ↔ CategoryTheory.Limits.IsZero (altPow A R.X (k + 1))

The vanishing criterion for symmetric powers of an odd twist: they vanish exactly when the alternating powers of the module do.