Compatibility of the module-power action with the multiplication

Over an internal commutative monoid A and a module X, the module powers and symmetric powers carry both a multiplication (SymMul.lean) and an A-action (PowAct.lean). This module proves the two structures compatible: the multiplications are module maps, in both factors — the statements that make the power algebras into A-module algebras.

• powTailAct_concat: on the ambient tensor powers, routing the monoid to the tail of the second block and concatenating equals concatenating and acting on the tail of the product. Because the concatenation folds on the right, this is a naturality of the concatenation against the action through the right factor.
• modPowMul_actRight/symMul_actRight: acting on the right factor, with the monoid carried past the left factor, equals multiplying and acting on the product.
• modPowMul_braiding_exists: the braiding of two module powers is, across the multiplications, the action of a block permutation — the descent of tensorPowConcat_braiding_exists.
• modPowMul_actLeft/symMul_actLeft: acting on the left factor equals multiplying and acting on the product; proved from the right version by braiding the factors, sliding the action across the braiding, and absorbing the block permutation through the equivariance of the descended action.

The action through the right factor against a concatenation

theorem RS.actAcross_split_pair {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 (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.associator V₁ V₂ X).inv) (actAcross A (CategoryTheory.MonoidalCategoryStruct.tensorObj V₁ V₂) X) = CategoryTheory.CategoryStruct.comp (braidPast A V₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj V₂ X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V₁ (actAcross A V₂ X)) (CategoryTheory.MonoidalCategoryStruct.associator V₁ V₂ X).inv)

The action through the right factor of a tensor pair, with the pair reassociated: carry the monoid past the first factor and act through the second.

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

Naturality of a fold-and-collapse against the action: acting through the second factor of a pair and collapsing the pair onto a codomain equals collapsing first and acting through the right factor of the codomain.

theorem RS.powTailAct_concat {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] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (braidPast A (tensorPow D X (m + 1)) (tensorPow D X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X (m + 1)) (powTailAct A X n)) (tensorPowConcat X (m + 1) (n + 1)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (tensorPowConcat X (m + 1) (n + 1)).hom) (powTailAct A X (m + 1 + n))

The tail action passes the concatenation: carrying the monoid to the tail of the second block and concatenating equals concatenating and acting on the tail of the product. The concatenation folds on the right, so the tail of the product is the tail of the second block and no arity transport is needed.

The multiplication as a module map, right factor

theorem RS.modPowTensorLeft_hom_ext {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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (P : D) (m n : ℕ) {Z : D} {k l : CategoryTheory.MonoidalCategoryStruct.tensorObj P (CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A X m) (modPow A X n)) ⟶ Z} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X m) (modPowπ A X n))) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X m) (modPowπ A X n))) l) : k = l

Morphisms out of a whiskered tensor pair of module powers are determined by their composites with the tensored projections.

theorem RS.modPowAct_cast {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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.IsCommMonObj A] {a b : ℕ} (h : a + 1 = b + 1) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowCast A X h)) (modPowAct A X b) = CategoryTheory.CategoryStruct.comp (modPowAct A X a) (modPowCast A X h)

The descended action passes an arity transport.

theorem RS.modPowMul_actRight {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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.IsCommMonObj A] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (braidPast A (modPow A X (m + 1)) (modPow A X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modPow A X (m + 1)) (modPowAct A X n)) (modPowMul A X (m + 1) (n + 1))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowMul A X (m + 1) (n + 1))) (modPowAct A X (m + 1 + n))

The raw multiplication is a module map in the right factor: acting on the right factor, with the monoid carried past the left factor, equals multiplying and acting on the product.

Braiding the monoid out of a braided pair

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

Braiding a pair with the monoid attached to its first factor, then carrying the monoid back out of the second factor, is braiding the bare pair under the monoid.

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

Braiding a pair with the monoid attached to its first factor, then carrying the monoid back out of the second factor, is braiding the bare pair under the monoid.

The multiplication as a module map, left factor

theorem RS.modPowMul_braiding_exists {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.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) : ∃ (σ : Equiv.Perm (Fin (n + m))), CategoryTheory.CategoryStruct.comp (β_ (modPow A X m) (modPow A X n)).hom (modPowMul A X n m) = CategoryTheory.CategoryStruct.comp (modPowMul A X m n) (CategoryTheory.CategoryStruct.comp (modPowCast A X ⋯) (modPowPerm (n + m) σ))

The braiding of module powers is a block permutation across the multiplications: the descent of tensorPowConcat_braiding_exists through the projections.

theorem RS.modPowMul_actLeft {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.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] [CategoryTheory.IsCommMonObj A] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (modPow A X (m + 1)) (modPow A X (n + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowAct A X m) (modPow A X (n + 1))) (modPowMul A X (m + 1) (n + 1))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowMul A X (m + 1) (n + 1))) (modPowAct A X (m + 1 + n))

The raw multiplication is a module map in the left factor: acting on the left factor equals multiplying and acting on the product, with no braiding of the monoid past anything. The action slides from the tail of the left block to the tail of the product; the slide is packaged through the braiding of the blocks, the right-factor statement, and the equivariance of the descended action.

The symmetric multiplication as a module map

theorem RS.symPowTensorLeft_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) (m n : ℕ) {Z : D} {k l : CategoryTheory.MonoidalCategoryStruct.tensorObj P (CategoryTheory.MonoidalCategoryStruct.tensorObj (symPow A X m) (symPow A X n)) ⟶ Z} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowπ A X m) (symPowπ A X n))) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowπ A X m) (symPowπ A X n))) l) : k = l

Morphisms out of a whiskered tensor pair of symmetric powers are determined by their composites with the tensored projections, which are jointly split epi.

theorem RS.symMul_actRight {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.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] [CategoryTheory.IsCommMonObj A] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (braidPast A (symPow A X (m + 1)) (symPow A X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (symPow A X (m + 1)) (symPowAct A X n)) (symMul A X (m + 1) (n + 1))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (symMul A X (m + 1) (n + 1))) (symPowAct A X (m + 1 + n))

The symmetric multiplication is a module map in the right factor: acting on the right factor, with the monoid carried past the left factor, equals multiplying and acting on the product.

theorem RS.symMul_actLeft {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.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] [CategoryTheory.IsCommMonObj A] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (symPow A X (m + 1)) (symPow A X (n + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (symPowAct A X m) (symPow A X (n + 1))) (symMul A X (m + 1) (n + 1))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (symMul A X (m + 1) (n + 1))) (symPowAct A X (m + 1 + n))

The symmetric multiplication is a module map in the left factor: acting on the left factor equals multiplying and acting on the product, with no braiding of the monoid past anything.