The module power, one letter at a time

The relative tensor power modPow A X n of SymAlg.lean is presented in a single step, over all adjacent slots at once. The arities are nevertheless joined by one letter at a time, and this file supplies that stage map: the projection at arity n + 1 factors through the projection at arity n whiskered by one further letter.

• modPowGlue_succ, modPowLegM_succ, modPowLegN_succ: a relation slot with one further letter of tail is that slot with the shorter tail, whiskered by the letter, after the associator that exposes it.
• modPowStage A X n : modPow A X n ⊗ X ⟶ modPow A X (n + 1), descended along the whiskered presentation of SymAlg.lean, with modPowπ_whiskerRight_stage the factorisation itself.
• modPow_invisible_succ: an ambient endomorphism invisible to the projection at one arity is invisible at the next.

One further letter of tail

Every relation leg is a local morphism whiskered by the tail and then glued. Lengthening the tail by one letter therefore only reassociates: at general objects this is a single application of whiskerRight_tensor, and each arity-bearing instance is obtained from it by exact, so that no tensor-power arity enters the rewriting.

theorem RS.modPowGlue_succ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (a b : ℕ) : modPowGlue X a (b + 1) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X a) (CategoryTheory.MonoidalCategoryStruct.tensorObj X X)) (tensorPow D X b) X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowGlue X a b) X)

Gluing a longer tail: the glue at tail length b + 1 is the glue at tail length b, whiskered by the extra letter.

theorem RS.modPowLegM_succ {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] (a b : ℕ) : modPowLegM A X a (b + 1) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X a) (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X)) (tensorPow D X b) X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegM A X a b) X)

The first leg with a longer tail: acting on the left module factor over a tail of length b + 1 is doing so over a tail of length b, whiskered by the extra letter.

theorem RS.modPowLegN_succ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) : modPowLegN A X a (b + 1) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X a) (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X)) (tensorPow D X b) X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegN A X a b) X)

The second leg with a longer tail: acting on the right module factor over a tail of length b + 1 is doing so over a tail of length b, whiskered by the extra letter.

The stage map

The whiskered relation pair still coequalizes the projection one arity up: tensoring on the right is additive, so the assembled legs split into their slots, and each slot is the slot relation of the longer arity with one more letter of tail.

theorem RS.modPow_condition_succ {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.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegFst A X n) X) (modPowπ A X (n + 1)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegSnd A X n) X) (modPowπ A X (n + 1))

The whiskered relation pair coequalizes one arity up: the assembled legs at arity n, whiskered by one letter, agree after the projection at arity n + 1.

noncomputable def RS.modPowStage {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.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A X n) X ⟶ modPow A X (n + 1)

The stage map: the projection at arity n + 1 factors through the projection at arity n whiskered by one letter.

Equations

• RS.modPowStage A X n = RS.modPowWhiskerRightDesc A X n X (RS.modPowπ A X (n + 1)) ⋯

@[simp]

theorem RS.modPowπ_whiskerRight_stage {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.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X n) X) (modPowStage A X n) = modPowπ A X (n + 1)

The stage map is the factorisation of the projection at arity n + 1 through the whiskered projection at arity n.

@[simp]

theorem RS.modPowπ_whiskerRight_stage_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.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (n : ℕ) {Z : D} (h : modPow A X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X n) X) (CategoryTheory.CategoryStruct.comp (modPowStage A X n) h) = CategoryTheory.CategoryStruct.comp (modPowπ A X (n + 1)) h

The stage map is the factorisation of the projection at arity n + 1 through the whiskered projection at arity n.

theorem RS.modPow_invisible_succ {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.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (n : ℕ) {g : tensorPow D X n ⟶ tensorPow D X n} (hg : CategoryTheory.CategoryStruct.comp g (modPowπ A X n) = modPowπ A X n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g X) (modPowπ A X (n + 1)) = modPowπ A X (n + 1)

An identity invisible at one arity is invisible at the next: whiskering by a further letter keeps it invisible.