The idempotent cut of module powers

The generic splitting that SymAlg.lean performs for the symmetriser and AltPow.lean for the antisymmetriser, done once for an arbitrary idempotent e of the symmetric-group algebra: the cut of the module power by e, presented as the coequalizer of the action modPowAlg e against the identity, which the idempotency splits off as a direct summand of the module power — together with the A-module structure descended through the splitting. This is the substrate for Schur functors of modules over an internal monoid; the Young idempotents of the Schur interface are plugged in elsewhere.

• modPowCut A X n e: the cut, with projection modPowCutπ, section modPowCutσ, the splitting identities, extensionality and descent. Idempotency e * e = e enters as an explicit hypothesis on exactly the declarations that need it.
• modPowAct_modPowCutIdem: the descended action commutes with the group-algebra action, by the linear extension of the permutation case.
• modPowCutAct/modPowCutModObj/modPowCutMod: the action on the cut, with modPowCutσ a module map.
• modPowCut_symmetriser/modPowCut_antisymmetriser: at the symmetriser and the antisymmetriser the cut is the symmetric and the alternating power, definitionally.

The cut of the module power by an idempotent

noncomputable def RS.modPowCutIdem {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] (n : ℕ) (e : SymGroupAlgebra n) : modPow A X n ⟶ modPow A X n

A group-algebra element acting on the module power.

Equations

• RS.modPowCutIdem A X n e = (RS.modPowAlg A X n) e

theorem RS.modPowCutIdem_idem {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] (n : ℕ) (e : SymGroupAlgebra n) (he : e * e = e) : CategoryTheory.CategoryStruct.comp (modPowCutIdem A X n e) (modPowCutIdem A X n e) = modPowCutIdem A X n e

An idempotent's action is idempotent.

noncomputable def RS.modPowCut {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] (n : ℕ) (e : SymGroupAlgebra n) : D

The cut of the module power by an idempotent: the coequalizer of the idempotent's action against the identity. The idempotency splits it off as a direct summand of the module power, with section modPowCutσ; this presentation is chosen because consumers build morphisms out of the cut by descent along modPowCutπ and morphisms into it through the section.

Equations

• RS.modPowCut A X n e = CategoryTheory.Limits.coequalizer (RS.modPowCutIdem A X n e) (CategoryTheory.CategoryStruct.id (RS.modPow A X n))

noncomputable def RS.modPowCutπ {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] (n : ℕ) (e : SymGroupAlgebra n) : modPow A X n ⟶ modPowCut A X n e

The projection onto the cut.

Equations

• RS.modPowCutπ A X n e = CategoryTheory.Limits.coequalizer.π (RS.modPowCutIdem A X n e) (CategoryTheory.CategoryStruct.id (RS.modPow A X n))

instance RS.instEpiModPowCutπ {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] (n : ℕ) (e : SymGroupAlgebra n) : CategoryTheory.Epi (modPowCutπ A X n e)

@[simp]

theorem RS.modPowCutIdem_π {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] (n : ℕ) (e : SymGroupAlgebra n) : CategoryTheory.CategoryStruct.comp (modPowCutIdem A X n e) (modPowCutπ A X n e) = modPowCutπ A X n e

The idempotent is absorbed by the projection.

@[simp]

theorem RS.modPowCutIdem_π_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.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (n : ℕ) (e : SymGroupAlgebra n) {Z : D} (h : modPowCut A X n e ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowCutIdem A X n e) (CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) h) = CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) h

The idempotent is absorbed by the projection.

noncomputable def RS.modPowCutσ {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] (n : ℕ) (e : SymGroupAlgebra n) (he : e * e = e) : modPowCut A X n e ⟶ modPow A X n

The section of the cut, from idempotency.

Equations

• RS.modPowCutσ A X n e he = CategoryTheory.Limits.coequalizer.desc (RS.modPowCutIdem A X n e) ⋯

@[simp]

theorem RS.modPowCutπ_σ {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] (n : ℕ) (e : SymGroupAlgebra n) (he : e * e = e) : CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) (modPowCutσ A X n e he) = modPowCutIdem A X n e

The section realises the idempotent as projection followed by inclusion.

@[simp]

theorem RS.modPowCutπ_σ_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.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (n : ℕ) (e : SymGroupAlgebra n) (he : e * e = e) {Z : D} (h : modPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) (CategoryTheory.CategoryStruct.comp (modPowCutσ A X n e he) h) = CategoryTheory.CategoryStruct.comp (modPowCutIdem A X n e) h

The section realises the idempotent as projection followed by inclusion.

theorem RS.modPowCut_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] {n : ℕ} {e : SymGroupAlgebra n} {W : D} {k l : modPowCut A X n e ⟶ W} (h : CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) k = CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) l) : k = l

Morphisms out of the cut are determined by their composite with the projection.

@[simp]

theorem RS.modPowCutσ_π {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] (n : ℕ) (e : SymGroupAlgebra n) (he : e * e = e) : CategoryTheory.CategoryStruct.comp (modPowCutσ A X n e he) (modPowCutπ A X n e) = CategoryTheory.CategoryStruct.id (modPowCut A X n e)

The cut is a direct summand: the section followed by the projection is the identity.

@[simp]

theorem RS.modPowCutσ_π_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.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (n : ℕ) (e : SymGroupAlgebra n) (he : e * e = e) {Z : D} (h : modPowCut A X n e ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowCutσ A X n e he) (CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) h) = h

The cut is a direct summand: the section followed by the projection is the identity.

noncomputable def RS.modPowCutDesc {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] {n : ℕ} {e : SymGroupAlgebra n} {W : D} (k : modPow A X n ⟶ W) (h : CategoryTheory.CategoryStruct.comp (modPowCutIdem A X n e) k = k) : modPowCut A X n e ⟶ W

Descend a morphism absorbed by the idempotent to the cut.

Equations

• RS.modPowCutDesc A X k h = CategoryTheory.Limits.coequalizer.desc k ⋯

@[simp]

theorem RS.modPowCutπ_desc {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] {n : ℕ} {e : SymGroupAlgebra n} {W : D} (k : modPow A X n ⟶ W) (h : CategoryTheory.CategoryStruct.comp (modPowCutIdem A X n e) k = k) : CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) (modPowCutDesc A X k h) = k

The descent factors the given morphism through the projection.

@[simp]

theorem RS.modPowCutπ_desc_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.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] {n : ℕ} {e : SymGroupAlgebra n} {W : D} (k : modPow A X n ⟶ W) (h : CategoryTheory.CategoryStruct.comp (modPowCutIdem A X n e) k = k) {Z : D} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) (CategoryTheory.CategoryStruct.comp (modPowCutDesc A X k h) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The descent factors the given morphism through the projection.

Compatibility with the symmetric and alternating powers

theorem RS.modPowCut_symmetriser {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] (n : ℕ) : modPowCut A X n (symmetriser n) = symPow A X n

At the symmetriser the cut is the symmetric power, definitionally.

theorem RS.modPowCut_antisymmetriser {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] (n : ℕ) : modPowCut A X n (antisymmetriser n) = altPow A X n

At the antisymmetriser the cut is the alternating power, definitionally.

Whiskered extensionality for the cut

theorem RS.modPowCut_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 : ℕ) (e : SymGroupAlgebra n) (he : e * e = e) {Z : D} {k l : CategoryTheory.MonoidalCategoryStruct.tensorObj P (modPowCut A X n e) ⟶ Z} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modPowCutπ A X n e)) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modPowCutπ A X n e)) l) : k = l

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

The cut as a module

theorem RS.modPowAct_modPowCutIdem {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 : ℕ) (e : SymGroupAlgebra (n + 1)) : CategoryTheory.CategoryStruct.comp (modPowAct A X n) (modPowCutIdem A X (n + 1) e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowCutIdem A X (n + 1) e)) (modPowAct A X n)

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

noncomputable def RS.modPowCutAct {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 : ℕ) (e : SymGroupAlgebra (n + 1)) (he : e * e = e) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (modPowCut A X (n + 1) e) ⟶ modPowCut A X (n + 1) e

The monoid action on the cut, through the section and the descended action.

Equations

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

@[simp]

theorem RS.whiskerLeft_modPowCutπ_modPowCutAct {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 : ℕ) (e : SymGroupAlgebra (n + 1)) (he : e * e = e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowCutπ A X (n + 1) e)) (modPowCutAct A X n e he) = CategoryTheory.CategoryStruct.comp (modPowAct A X n) (modPowCutπ A X (n + 1) e)

Defining equation of the cut action.

@[simp]

theorem RS.whiskerLeft_modPowCutπ_modPowCutAct_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 : ℕ) (e : SymGroupAlgebra (n + 1)) (he : e * e = e) {Z : D} (h : modPowCut A X (n + 1) e ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowCutπ A X (n + 1) e)) (CategoryTheory.CategoryStruct.comp (modPowCutAct A X n e he) h) = CategoryTheory.CategoryStruct.comp (modPowAct A X n) (CategoryTheory.CategoryStruct.comp (modPowCutπ A X (n + 1) e) h)

Defining equation of the cut action.

theorem RS.modPowCutAct_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 : ℕ) (e : SymGroupAlgebra (n + 1)) (he : e * e = e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (modPowCut A X (n + 1) e)) (modPowCutAct A X n e he) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (modPowCut A X (n + 1) e)).hom

Unitality of the cut action.

theorem RS.modPowCutAct_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 : ℕ) (e : SymGroupAlgebra (n + 1)) (he : e * e = e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (modPowCut A X (n + 1) e)) (modPowCutAct A X n e he) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (modPowCut A X (n + 1) e)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowCutAct A X n e he)) (modPowCutAct A X n e he))

Associativity of the cut action.

@[implicit_reducible]

noncomputable def RS.modPowCutModObj {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 : ℕ) (e : SymGroupAlgebra (n + 1)) (he : e * e = e) : CategoryTheory.ModObj A (modPowCut A X (n + 1) e)

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

Equations

• RS.modPowCutModObj A X n e he = { smul := RS.modPowCutAct A X n e he, one_smul := ⋯, mul_smul := ⋯ }

noncomputable def RS.modPowCutMod {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 : ℕ) (e : SymGroupAlgebra (n + 1)) (he : e * e = e) : CategoryTheory.Mod D A

The cut of a module, bundled as a module.

Equations

• RS.modPowCutMod A X n e he = { X := RS.modPowCut A X (n + 1) e, mod := RS.modPowCutModObj A X n e he }

@[simp]

theorem RS.modPowCutMod_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 : ℕ) (e : SymGroupAlgebra (n + 1)) (he : e * e = e) : (modPowCutMod A X n e he).X = modPowCut A X (n + 1) e

Naturality substrate: module maps on powers

The transport kit for the cut: a module map f : X ⟶ Y induces a map of module powers and of their cuts, functorially, and killing the cut transports along retracts and isomorphisms.

theorem RS.powCast_tensorPowMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {X Y : D} (f : X ⟶ Y) {m n : ℕ} (h : m = n) : CategoryTheory.CategoryStruct.comp (powCast X h) (tensorPowMap f n) = CategoryTheory.CategoryStruct.comp (tensorPowMap f m) (powCast Y h)

Arity transports pass tensor powers of a morphism.

theorem RS.tensorPowMap_concat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {X Y : D} (f : X ⟶ Y) (a b : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f a) (tensorPowMap f b)) (tensorPowConcat Y a b).hom = CategoryTheory.CategoryStruct.comp (tensorPowConcat X a b).hom (tensorPowMap f (a + b))

The concatenation isomorphism is natural in tensor powers of a morphism.

theorem RS.winLegM_natural {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id A)) f) (winLegM A Y) = CategoryTheory.CategoryStruct.comp (winLegM A X) (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)

The first window leg is natural in module maps.

theorem RS.winLegN_natural {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id A)) f) (winLegN A Y) = CategoryTheory.CategoryStruct.comp (winLegN A X) (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)

The second window leg is natural in module maps.

theorem RS.modPowGlue_natural {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {X Y : D} (f : X ⟶ Y) (a b : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f a) (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)) (tensorPowMap f b)) (modPowGlue Y a b) = CategoryTheory.CategoryStruct.comp (modPowGlue X a b) (tensorPowMap f (a + 2 + b))

The slot gluing is natural in tensor powers of a morphism.

theorem RS.modPowLegM_natural {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (a b : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f a) (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id A)) f)) (tensorPowMap f b)) (modPowLegM A Y a b) = CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (tensorPowMap f (a + 2 + b))

The first slot leg is natural in module maps.

theorem RS.modPowLegN_natural {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (a b : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (tensorPowMap f a) (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id A)) f)) (tensorPowMap f b)) (modPowLegN A Y a b) = CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (tensorPowMap f (a + 2 + b))

The second slot leg is natural in module maps.

noncomputable def RS.modPowMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (n : ℕ) : modPow A X n ⟶ modPow A Y n

The module power of a module map: the tensor power of the map descends to the module powers, since it carries every slot relation of the source into a slot relation of the target.

Equations

• RS.modPowMap A f n = RS.modPowDesc A X (CategoryTheory.CategoryStruct.comp (RS.tensorPowMap f n) (RS.modPowπ A Y n)) ⋯

@[simp]

theorem RS.modPowπ_map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (n : ℕ) : CategoryTheory.CategoryStruct.comp (modPowπ A X n) (modPowMap A f n) = CategoryTheory.CategoryStruct.comp (tensorPowMap f n) (modPowπ A Y n)

Defining square of the module-power map.

@[simp]

theorem RS.modPowπ_map_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (n : ℕ) {Z : D} (h : modPow A Y n ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowπ A X n) (CategoryTheory.CategoryStruct.comp (modPowMap A f n) h) = CategoryTheory.CategoryStruct.comp (tensorPowMap f n) (CategoryTheory.CategoryStruct.comp (modPowπ A Y n) h)

Defining square of the module-power map.

@[simp]

theorem RS.modPowMap_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {X : D} [CategoryTheory.ModObj A X] (n : ℕ) : modPowMap A (CategoryTheory.CategoryStruct.id X) n = CategoryTheory.CategoryStruct.id (modPow A X n)

The module power of the identity is the identity.

theorem RS.modPowMap_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] {Z : D} [CategoryTheory.ModObj A Z] (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsModHom A f] [CategoryTheory.IsModHom A g] (n : ℕ) : modPowMap A (CategoryTheory.CategoryStruct.comp f g) n = CategoryTheory.CategoryStruct.comp (modPowMap A f n) (modPowMap A g n)

The module power is functorial in module maps.

theorem RS.modPowMap_perm {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (n : ℕ) (σ : Equiv.Perm (Fin n)) : CategoryTheory.CategoryStruct.comp (modPowMap A f n) (modPowPerm n σ) = CategoryTheory.CategoryStruct.comp (modPowPerm n σ) (modPowMap A f n)

The module-power map passes the descended permutation action.

theorem RS.modPowMap_alg {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (n : ℕ) (z : SymGroupAlgebra n) : CategoryTheory.CategoryStruct.comp (modPowMap A f n) ((modPowAlg A Y n) z) = CategoryTheory.CategoryStruct.comp ((modPowAlg A X n) z) (modPowMap A f n)

The module-power map passes the group-algebra action, by linear extension of the permutation case.

theorem RS.modPowMap_cutIdem {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (n : ℕ) (e : SymGroupAlgebra n) : CategoryTheory.CategoryStruct.comp (modPowCutIdem A X n e) (modPowMap A f n) = CategoryTheory.CategoryStruct.comp (modPowMap A f n) (modPowCutIdem A Y n e)

The module-power map passes the idempotent's action.

noncomputable def RS.modPowCutMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (n : ℕ) (e : SymGroupAlgebra n) : modPowCut A X n e ⟶ modPowCut A Y n e

The cut of a module map: the module-power map descends to the cuts by an idempotent.

Equations

• RS.modPowCutMap A f n e = RS.modPowCutDesc A X (CategoryTheory.CategoryStruct.comp (RS.modPowMap A f n) (RS.modPowCutπ A Y n e)) ⋯

@[simp]

theorem RS.modPowCutπ_map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (n : ℕ) (e : SymGroupAlgebra n) : CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) (modPowCutMap A f n e) = CategoryTheory.CategoryStruct.comp (modPowMap A f n) (modPowCutπ A Y n e)

Defining square of the cut map.

@[simp]

theorem RS.modPowCutπ_map_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (f : X ⟶ Y) [CategoryTheory.IsModHom A f] (n : ℕ) (e : SymGroupAlgebra n) {Z : D} (h : modPowCut A Y n e ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowCutπ A X n e) (CategoryTheory.CategoryStruct.comp (modPowCutMap A f n e) h) = CategoryTheory.CategoryStruct.comp (modPowMap A f n) (CategoryTheory.CategoryStruct.comp (modPowCutπ A Y n e) h)

Defining square of the cut map.

@[simp]

theorem RS.modPowCutMap_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] {X : D} [CategoryTheory.ModObj A X] (n : ℕ) (e : SymGroupAlgebra n) : modPowCutMap A (CategoryTheory.CategoryStruct.id X) n e = CategoryTheory.CategoryStruct.id (modPowCut A X n e)

The cut of the identity is the identity.

theorem RS.modPowCutMap_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] {Z : D} [CategoryTheory.ModObj A Z] (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsModHom A f] [CategoryTheory.IsModHom A g] (n : ℕ) (e : SymGroupAlgebra n) : modPowCutMap A (CategoryTheory.CategoryStruct.comp f g) n e = CategoryTheory.CategoryStruct.comp (modPowCutMap A f n e) (modPowCutMap A g n e)

The cut map is functorial in module maps.

Killing the cut transports along retracts

theorem RS.modPowCutMap_congr {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] {f g : X ⟶ Y} [CategoryTheory.IsModHom A f] [CategoryTheory.IsModHom A g] (h : f = g) (n : ℕ) (e : SymGroupAlgebra n) : modPowCutMap A f n e = modPowCutMap A g n e

The cut map depends only on the underlying morphism, not on the module-map witness.

theorem RS.modPowCut_isZero_of_retract {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (r : X ⟶ Y) (s : Y ⟶ X) [CategoryTheory.IsModHom A r] [CategoryTheory.IsModHom A s] (hs : CategoryTheory.CategoryStruct.comp s r = CategoryTheory.CategoryStruct.id Y) (n : ℕ) (e : SymGroupAlgebra n) (hX : CategoryTheory.Limits.IsZero (modPowCut A X n e)) : CategoryTheory.Limits.IsZero (modPowCut A Y n e)

The cut of a retract is a retract of the cut: if the cut of X vanishes, so does the cut of a module retract of X.