The monoid action on module powers and symmetric powers

Over an internal commutative monoid A and a left module X in a braided category, the tensor powers of X carry an A-action through their last factor, with A braided past the lower factors. This module descends that action through the coequalizers of SymAlg.lean, making every positive module power and every positive symmetric power a module again.

• braidPast A V T: the structural isomorphism carrying A across a context V, with naturality in both the context and the tail.
• actAcross/tensorLeftModObj: a module tensored with an object on the left is again a module, acting through the right factor — the braided mirror of tensorRightModObj.
• powTailAct: the induced action on tensorPow D X (n + 1).
• modPowAct/modPowModObj: over a commutative monoid the tail action descends to the module power; the slot relations away from the top factor pass by naturality alone, and the top slot passes by one slot relation together with commutativity.
• modPowAct_perm/modPowAct_alg: the descended action commutes with the permutation action and its ℂ-linear extension.
• symPowAct/symPowModObj: the action descends to the symmetric power, with symPowσ a module map.
• modPowMod/symPowMod: the bundled modules.

Braiding a monoid past a context

def RS.braidPast {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A V T : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj V T) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj V (CategoryTheory.MonoidalCategoryStruct.tensorObj A T)

Carry an object across a context: the isomorphism A ⊗ (V ⊗ T) ≅ V ⊗ (A ⊗ T) braiding A past V.

Equations

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

@[simp]

theorem RS.braidPast_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A V T : D) : (braidPast A V T).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A V T).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A V).hom T) (CategoryTheory.MonoidalCategoryStruct.associator V A T).hom)

theorem RS.braidPast_natural_tail {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A V : D) {T T' : D} (g : T ⟶ T') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V g)) (braidPast A V T').hom = CategoryTheory.CategoryStruct.comp (braidPast A V T).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g))

The carrying isomorphism is natural in the tail.

theorem RS.braidPast_natural_tail_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A V : D) {T T' : D} (g : T ⟶ T') {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj V (CategoryTheory.MonoidalCategoryStruct.tensorObj A T') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V g)) (CategoryTheory.CategoryStruct.comp (braidPast A V T').hom h) = CategoryTheory.CategoryStruct.comp (braidPast A V T).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g)) h)

The carrying isomorphism is natural in the tail.

theorem RS.braidPast_natural_context {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) {V V' : D} (f : V ⟶ V') (T : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight f T)) (braidPast A V' T).hom = CategoryTheory.CategoryStruct.comp (braidPast A V T).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj A T))

The carrying isomorphism is natural in the context.

theorem RS.braidPast_natural_context_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) {V V' : D} (f : V ⟶ V') (T : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj V' (CategoryTheory.MonoidalCategoryStruct.tensorObj A T) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight f T)) (CategoryTheory.CategoryStruct.comp (braidPast A V' T).hom h) = CategoryTheory.CategoryStruct.comp (braidPast A V T).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj A T)) h)

The carrying isomorphism is natural in the context.

theorem RS.braidPast_tensor_context {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A V₁ V₂ T : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (CategoryTheory.MonoidalCategoryStruct.tensorObj V₁ V₂) T).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A (CategoryTheory.MonoidalCategoryStruct.tensorObj V₁ V₂)).hom T) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj V₁ V₂) A T).hom (CategoryTheory.MonoidalCategoryStruct.associator V₁ V₂ (CategoryTheory.MonoidalCategoryStruct.tensorObj A T)).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator V₁ V₂ T).hom) (CategoryTheory.CategoryStruct.comp (braidPast A V₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj V₂ T)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V₁ (braidPast A V₂ T).hom))

Carrying past a tensor context is carrying past the factors in turn.

theorem RS.braidPast_tensor_first {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A₁ A₂ V T : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj A₁ A₂) V T).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj A₁ A₂) V).hom T) (CategoryTheory.MonoidalCategoryStruct.associator V (CategoryTheory.MonoidalCategoryStruct.tensorObj A₁ A₂) T).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A₁ A₂ (CategoryTheory.MonoidalCategoryStruct.tensorObj V T)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A₁ (braidPast A₂ V T).hom) (CategoryTheory.CategoryStruct.comp (braidPast A₁ V (CategoryTheory.MonoidalCategoryStruct.tensorObj A₂ T)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (CategoryTheory.MonoidalCategoryStruct.associator A₁ A₂ T).inv)))

Carrying a tensor pair past a context is carrying the factors past it in turn.

The action through the right tensor factor

def RS.actAcross {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V X : D) [CategoryTheory.ModObj A X] : CategoryTheory.MonoidalCategoryStruct.tensorObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj V X) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V X

The action of a monoid on V ⊗ X through the right factor: braid A past V, then act on X.

Equations

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

theorem RS.actAcross_eq_braidPast {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V X : D) [CategoryTheory.ModObj A X] : actAcross A V X = CategoryTheory.CategoryStruct.comp (braidPast A V X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (actLeft A X))

The action through the right factor, through the carrying isomorphism.

theorem RS.actAcross_natural {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] {V V' : D} (f : V ⟶ V') (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)) (actAcross A V' X) = CategoryTheory.CategoryStruct.comp (actAcross A V X) (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)

The action through the right factor is natural in the context.

theorem RS.actAcross_natural_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] {V V' : D} (f : V ⟶ V') (X : D) [CategoryTheory.ModObj A X] {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj V' X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)) (CategoryTheory.CategoryStruct.comp (actAcross A V' X) h) = CategoryTheory.CategoryStruct.comp (actAcross A V X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) h)

The action through the right factor is natural in the context.

theorem RS.one_actAcross {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (CategoryTheory.MonoidalCategoryStruct.tensorObj V X)) (actAcross A V X) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj V X)).hom

Unitality of the action through the right factor.

theorem RS.mul_actAcross {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj V X)) (actAcross A V X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.MonoidalCategoryStruct.tensorObj V X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (actAcross A V X)) (actAcross A V X))

Associativity of the action through the right factor.

@[implicit_reducible]

def RS.tensorLeftModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V X : D) [CategoryTheory.ModObj A X] : CategoryTheory.ModObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj V X)

A left module tensored with an object on the left: the action of A on V ⊗ X through the right factor.

Equations

• RS.tensorLeftModObj A V X = { smul := RS.actAcross A V X, one_smul := ⋯, mul_smul := ⋯ }

@[simp]

theorem RS.tensorLeftModObj_smul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V X : D) [CategoryTheory.ModObj A X] : CategoryTheory.ModObj.smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A V X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A V).hom X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V A X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (actLeft A X))))

theorem RS.actAcross_context_split {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V₁ V₂ X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (actAcross A (CategoryTheory.MonoidalCategoryStruct.tensorObj V₁ V₂) X) (CategoryTheory.MonoidalCategoryStruct.associator V₁ V₂ X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator V₁ V₂ X).hom) (CategoryTheory.CategoryStruct.comp (braidPast A V₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj V₂ X)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V₁ (actAcross A V₂ X)))

The action through the right factor decomposes over a tensor context: braid past the outer factor, then act through the inner one.

theorem RS.actAcross_context_split_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V₁ V₂ X : D) [CategoryTheory.ModObj A X] {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj V₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj V₂ X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (actAcross A (CategoryTheory.MonoidalCategoryStruct.tensorObj V₁ V₂) X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V₁ V₂ X).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator V₁ V₂ X).hom) (CategoryTheory.CategoryStruct.comp (braidPast A V₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj V₂ X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V₁ (actAcross A V₂ X)) h))

The action through the right factor decomposes over a tensor context: braid past the outer factor, then act through the inner one.

theorem RS.actAcross_split_last {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (V X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator V X X).inv) (actAcross A (CategoryTheory.MonoidalCategoryStruct.tensorObj V X) X) = CategoryTheory.CategoryStruct.comp (braidPast A V (CategoryTheory.MonoidalCategoryStruct.tensorObj X X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (actAcross A X X)) (CategoryTheory.MonoidalCategoryStruct.associator V X X).inv)

The action through the right factor of a two-step context, conjugated by the associator: braid past the outer factor, act inside the last two.

theorem RS.whiskerLeft_associator_inv_actAcross {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] {P₁ P₂ Q : D} (g : CategoryTheory.MonoidalCategoryStruct.tensorObj P₁ P₂ ⟶ Q) (X : D) [CategoryTheory.ModObj A X] {Z : D} (p : CategoryTheory.MonoidalCategoryStruct.tensorObj Q X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P₁ P₂ X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight g X))) (CategoryTheory.CategoryStruct.comp (actAcross A Q X) p) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator P₁ P₂ X).inv) (CategoryTheory.CategoryStruct.comp (actAcross A (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁ P₂) X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g X) p))

An action through the right factor, precomposed with a reassociated whiskered morphism into the context.

theorem RS.actAcross_actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (actAcross A A X) (actLeft A X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (actLeft A X)) (actLeft A X)

Over a commutative monoid the braided self-crossing of the action agrees with the plain iterated action.

theorem RS.actAcross_winLegN {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (actAcross A (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X) (winLegN A X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (winLegN A X)) (actAcross A X X)

The key commutation: over a commutative monoid the external action slides across a slot leg acting on the inner factor.

The tail action on tensor powers

def RS.powTailAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (tensorPow D X (n + 1)) ⟶ tensorPow D X (n + 1)

The raw tail action on a positive tensor power: the monoid acts on the last factor, braided past the lower power.

Equations

• RS.powTailAct A X n = CategoryTheory.ModObj.smul

theorem RS.powTailAct_eq {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) : powTailAct A X n = actAcross A (tensorPow D X n) X

The tail action is the action through the right factor at the definitional fold of the tensor power.

theorem RS.powTailAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (tensorPow D X (n + 1))) (powTailAct A X n) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (tensorPow D X (n + 1))).hom

Unitality of the tail action.

theorem RS.powTailAct_one_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) {Z : D} (h : tensorPow D X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (tensorPow D X (n + 1))) (CategoryTheory.CategoryStruct.comp (powTailAct A X n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (tensorPow D X (n + 1))).hom h

Unitality of the tail action.

theorem RS.powTailAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (tensorPow D X (n + 1))) (powTailAct A X n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (tensorPow D X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (powTailAct A X n)) (powTailAct A X n))

Associativity of the tail action.

theorem RS.powTailAct_mul_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) {Z : D} (h : tensorPow D X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (tensorPow D X (n + 1))) (CategoryTheory.CategoryStruct.comp (powTailAct A X n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (tensorPow D X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (powTailAct A X n)) (CategoryTheory.CategoryStruct.comp (powTailAct A X n) h))

Associativity of the tail action.

Descent of the tail action to the module power

The tail action coequalizes the whiskered relation legs: at a slot away from the top factor the action and the leg touch disjoint factors and pass one another by naturality, and at the top slot one slot relation together with commutativity of the monoid closes the square. Every equation crossing the definitional fold tensorPow D X (n + 1) = tensorPow D X n ⊗ X is applied by exact term-level composition, never by rewriting inside a foreign frame.

noncomputable def RS.modPowActRaw {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (tensorPow D X (n + 1)) ⟶ modPow A X (n + 1)

The raw action on the ambient power of the module power.

Equations

• RS.modPowActRaw A X n = CategoryTheory.CategoryStruct.comp (RS.powTailAct A X n) (RS.modPowπ A X (n + 1))

theorem RS.modPowActRaw_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowLegFst A X (n + 1))) (modPowActRaw A X n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowLegSnd A X (n + 1))) (modPowActRaw A X n)

The raw action coequalizes the whiskered relation legs.

noncomputable def RS.modPowAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (modPow A X (n + 1)) ⟶ modPow A X (n + 1)

The monoid action on the module power, descended from the tail action through the whiskered coequalizer.

Equations

• RS.modPowAct A X n = RS.modPowWhiskerLeftDesc A X A (n + 1) (RS.modPowActRaw A X n) ⋯

@[simp]

theorem RS.whiskerLeft_modPowπ_modPowAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowπ A X (n + 1))) (modPowAct A X n) = CategoryTheory.CategoryStruct.comp (powTailAct A X n) (modPowπ A X (n + 1))

Defining equation of the descended action.

@[simp]

theorem RS.whiskerLeft_modPowπ_modPowAct_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) {Z : D} (h : modPow A X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowπ A X (n + 1))) (CategoryTheory.CategoryStruct.comp (modPowAct A X n) h) = CategoryTheory.CategoryStruct.comp (powTailAct A X n) (CategoryTheory.CategoryStruct.comp (modPowπ A X (n + 1)) h)

Defining equation of the descended action.

theorem RS.modPowAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (modPow A X (n + 1))) (modPowAct A X n) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (modPow A X (n + 1))).hom

Unitality of the descended action.

theorem RS.modPowAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (modPow A X (n + 1))) (modPowAct A X n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (modPow A X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowAct A X n)) (modPowAct A X n))

Associativity of the descended action.

@[implicit_reducible]

noncomputable def RS.modPowModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.ModObj A (modPow A X (n + 1))

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

Equations

• RS.modPowModObj A X n = { smul := RS.modPowAct A X n, one_smul := ⋯, mul_smul := ⋯ }

noncomputable def RS.modPowMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : CategoryTheory.Mod D A

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

Equations

• RS.modPowMod A X n = { X := RS.modPow A X (n + 1), mod := RS.modPowModObj A X n }

@[simp]

theorem RS.modPowMod_X {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) : (modPowMod A X n).X = modPow A X (n + 1)

Permutation equivariance of the descended action

The descended action commutes with the permutation action: for a top-fixing generator by naturality alone, and for the top transposition by carrying the acting monoid into the top slot and applying the slot relation there — the same slot the descent itself used. Generation by the adjacent transpositions extends both to the full symmetric group, and linearity to the group algebra.

def RS.winShuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A X : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj X X) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X

The window shuffle carrying the acting monoid into the top slot: d ⊗ (y ⊗ z) ↦ (z ⊗ d) ⊗ y.

Equations

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

theorem RS.actAcross_braiding {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.CategoryStruct.comp (actAcross A X X) (β_ X X).hom = CategoryTheory.CategoryStruct.comp (winShuffle A X) (winLegM A X)

The braided window identity for the first leg: acting on the top factor and braiding is shuffling and acting through the braided right action.

theorem RS.winShuffle_winLegN {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.CategoryStruct.comp (winShuffle A X) (winLegN A X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (β_ X X).hom) (actAcross A X X)

The braided window identity for the second leg: the shuffle followed by the second leg is braiding first, then acting on the top factor.

theorem RS.modPowAct_perm {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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (n : ℕ) (σ : Equiv.Perm (Fin (n + 1))) : CategoryTheory.CategoryStruct.comp (modPowAct A X n) (modPowPerm (n + 1) σ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowPerm (n + 1) σ)) (modPowAct A X n)

The descended action commutes with every permutation.

theorem RS.modPowAct_alg {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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (n : ℕ) (z : SymGroupAlgebra (n + 1)) : CategoryTheory.CategoryStruct.comp (modPowAct A X n) ((modPowAlg A X (n + 1)) z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A ((modPowAlg A X (n + 1)) z)) (modPowAct A X n)

The descended action commutes with the group-algebra action, by linear extension of the permutation case.

The symmetric power as a module

noncomputable def RS.symPowAct {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 (symPow A X (n + 1)) ⟶ symPow A X (n + 1)

The monoid action on the symmetric 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_symPowπ_symPowAct {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 (symPowπ A X (n + 1))) (symPowAct A X n) = CategoryTheory.CategoryStruct.comp (modPowAct A X n) (symPowπ A X (n + 1))

Defining equation of the symmetric-power action.

@[simp]

theorem RS.whiskerLeft_symPowπ_symPowAct_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 : symPow A X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (symPowπ A X (n + 1))) (CategoryTheory.CategoryStruct.comp (symPowAct A X n) h) = CategoryTheory.CategoryStruct.comp (modPowAct A X n) (CategoryTheory.CategoryStruct.comp (symPowπ A X (n + 1)) h)

Defining equation of the symmetric-power action.

theorem RS.symPowAct_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 (symPow A X (n + 1))) (symPowAct A X n) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (symPow A X (n + 1))).hom

Unitality of the symmetric-power action.

theorem RS.symPowAct_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 (symPow A X (n + 1))) (symPowAct A X n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (symPow A X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (symPowAct A X n)) (symPowAct A X n))

Associativity of the symmetric-power action.

@[implicit_reducible]

noncomputable def RS.symPowModObj {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 (symPow A X (n + 1))

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

Equations

• RS.symPowModObj A X n = { smul := RS.symPowAct A X n, one_smul := ⋯, mul_smul := ⋯ }

theorem RS.symPowσ_modPowAct {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 (symPowσ A X (n + 1))) (modPowAct A X n) = CategoryTheory.CategoryStruct.comp (symPowAct A X n) (symPowσ A X (n + 1))

The section of the symmetric power is a module map.

noncomputable def RS.symPowMod {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 symmetric power of a module, bundled as a module.

Equations

• RS.symPowMod A X n = { X := RS.symPow A X (n + 1), mod := RS.symPowModObj A X n }

@[simp]

theorem RS.symPowMod_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 : ℕ) : (symPowMod A X n).X = symPow A X (n + 1)