The monoid action on alternating powers

The antisymmetric counterpart of the symmetric-power module structure of PowAct.lean: over an internal commutative monoid A and a left module X in a symmetric monoidal category, the descended action on the module power commutes with the antisymmetriser's action — the antisymmetriser is a ℂ-linear combination of permutations, each of which the action passes — so the action descends through the splitting of AltPow.lean, making every positive alternating power a module.

• altPow_whiskerLeft_hom_ext: morphisms out of a left-whiskered alternating power are determined by the whiskered projection, which is split epi.
• modPowAct_altPowIdem: the descended action commutes with the antisymmetriser's action.
• altPowAct/altPowModObj: the action on the alternating power, with altPowσ a module map.
• altPowMod: the bundled module.

Whiskered extensionality for the alternating power

theorem RS.altPow_whiskerLeft_hom_ext {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (P : D) (n : ℕ) {Z : D} {k l : CategoryTheory.MonoidalCategoryStruct.tensorObj P (altPow A X n) ⟶ Z} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (altPowπ A X n)) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (altPowπ A X n)) l) : k = l

Morphisms out of a left-whiskered alternating power are determined by the whiskered projection, which is split epi.

The alternating power as a module

theorem RS.modPowAct_altPowIdem {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (modPowAct A X n) (altPowIdem A X (n + 1)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (altPowIdem A X (n + 1))) (modPowAct A X n)

The descended action commutes with the antisymmetriser's action: the antisymmetriser is a ℂ-linear combination of permutations, each of which the action passes.

noncomputable def RS.altPowAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Linear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (altPow A X (n + 1)) ⟶ altPow A X (n + 1)

The monoid action on the alternating power, through the section and the descended action.

Equations

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

@[simp]

theorem RS.whiskerLeft_altPowπ_altPowAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (altPowπ A X (n + 1))) (altPowAct A X n) = CategoryTheory.CategoryStruct.comp (modPowAct A X n) (altPowπ A X (n + 1))

Defining equation of the alternating-power action.

@[simp]

theorem RS.whiskerLeft_altPowπ_altPowAct_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) {Z : D} (h : altPow A X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (altPowπ A X (n + 1))) (CategoryTheory.CategoryStruct.comp (altPowAct A X n) h) = CategoryTheory.CategoryStruct.comp (modPowAct A X n) (CategoryTheory.CategoryStruct.comp (altPowπ A X (n + 1)) h)

Defining equation of the alternating-power action.

theorem RS.altPowAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (altPow A X (n + 1))) (altPowAct A X n) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (altPow A X (n + 1))).hom

Unitality of the alternating-power action.

theorem RS.altPowAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (altPow A X (n + 1))) (altPowAct A X n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (altPow A X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (altPowAct A X n)) (altPowAct A X n))

Associativity of the alternating-power action.

@[implicit_reducible]

noncomputable def RS.altPowModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.ModObj A (altPow A X (n + 1))

The alternating power of a module is a module, in every positive arity.

Equations

• RS.altPowModObj A X n = { smul := RS.altPowAct A X n, one_smul := ⋯, mul_smul := ⋯ }

noncomputable def RS.altPowMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.Mod D A

The alternating power of a module, bundled as a module.

Equations

• RS.altPowMod A X n = { X := RS.altPow A X (n + 1), mod := RS.altPowModObj A X n }

@[simp]

theorem RS.altPowMod_X {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : (altPowMod A X n).X = altPow A X (n + 1)