Multiplication on symmetric module powers

The multiplication layer of Deligne (2002), §2.8: over an internal monoid A and a module X, the concatenation of tensor powers descends through the module-power coequalizers of SymAlg.lean to a multiplication modPow A X m ⊗ modPow A X n ⟶ modPow A X (m + n), and then, through the symmetrisers, to the symmetric powers.

• tensorPowConcat_assoc: the concatenation isomorphisms are associative up to the powCast of p + (q + r) = p + q + r.
• midConcatFst/midConcatSnd and modPowMul_rel_fst/snd: the slot relations of arity m (resp. n) embed across the concatenation boundary into slots of m + n.
• modPowMul: the raw multiplication, descended in two stages through whiskered coequalizers; its defining equation is (modPowπ ⊗ₘ modPowπ) ≫ modPowMul = concat ≫ modPowπ.
• modPowMul_perm/modPowMul_alg: equivariance for the block embedding of permutations and its ℂ-bilinear extension.
• symMul: the multiplication on symmetric powers, with defining equation (symPowπ ⊗ₘ symPowπ) ≫ symMul = modPowMul ≫ symPowπ, by absorption of the block-embedded symmetrisers.
• Laws: symPowZero, unit laws (symMul_zero_left/right), associativity (symMul_assoc) and commutativity (symMul_comm, through tensorPowConcat_braiding_exists: the braiding of two tensor powers is, across the concatenations, the action of a permutation, which the symmetriser absorbs).

Whiskered coequalizers are handled by an instance parameter asking that each tensorLeft Y preserve colimits of parallel pairs — in a braided category the tensorRight mirror follows — together with MonoidalPreadditive D for the biproduct legs; these hold in the intended consumers.

Associativity of the concatenation

theorem RS.tensorPowConcat_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (p q r : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (tensorPowConcat X p q).hom (tensorPow D X r)) (tensorPowConcat X (p + q) r).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (tensorPow D X p) (tensorPow D X q) (tensorPow D X r)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X p) (tensorPowConcat X q r).hom) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X p (q + r)).hom (powCast X ⋯)))

Associativity of the concatenation: concatenating the first two blocks and then the third agrees, up to the arity transport of p + (q + r) = p + q + r, with concatenating the last two blocks and then the first.

theorem RS.tensorPowConcat_zero_left {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (n : ℕ) : (tensorPowConcat X 0 n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (tensorPow D X n)).hom (powCast X ⋯)

Concatenation with an empty first block is the left unitor, up to the arity transport.

Transport of concatenation and projections along arities

theorem RS.powCast_whiskerRight_concat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) {k m : ℕ} (h : k = m) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (powCast X h) (tensorPow D X n)) (tensorPowConcat X m n).hom = CategoryTheory.CategoryStruct.comp (tensorPowConcat X k n).hom (powCast X ⋯)

An arity transport of the first block passes the concatenation.

theorem RS.powCast_whiskerLeft_concat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (m : ℕ) {k n : ℕ} (h : k = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X m) (powCast X h)) (tensorPowConcat X m n).hom = CategoryTheory.CategoryStruct.comp (tensorPowConcat X m k).hom (powCast X ⋯)

An arity transport of the second block passes the concatenation.

noncomputable def RS.modPowCast {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] {m n : ℕ} (h : m = n) : modPow A X m ⟶ modPow A X n

Transport of a module power along an equality of arities.

Equations

• RS.modPowCast A X h = CategoryTheory.eqToHom ⋯

@[simp]

theorem RS.modPowCast_rfl {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 : ℕ) : modPowCast A X ⋯ = CategoryTheory.CategoryStruct.id (modPow A X n)

theorem RS.modPowCast_irrel {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] {m n : ℕ} (h h' : m = n) : modPowCast A X h = modPowCast A X h'

Two module-power transports with the same endpoints agree.

theorem RS.modPowπ_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] {m n : ℕ} (h : m = n) : CategoryTheory.CategoryStruct.comp (modPowπ A X m) (modPowCast A X h) = CategoryTheory.CategoryStruct.comp (powCast X h) (modPowπ A X n)

The projection intertwines the two arity transports.

theorem RS.modPowπ_cast_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.Limits.HasCoequalizers D] {m n : ℕ} (h : m = n) {Z : D} (h✝ : modPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowπ A X m) (CategoryTheory.CategoryStruct.comp (modPowCast A X h) h✝) = CategoryTheory.CategoryStruct.comp (powCast X h) (CategoryTheory.CategoryStruct.comp (modPowπ A X n) h✝)

The projection intertwines the two arity transports.

Embedding the slot relations across the concatenation

A relation slot of the left block, whiskered by the right block and concatenated, is a relation slot of the concatenated power; and mirrored for the right block. Each embedding is mediated by a structural bridge morphism that is independent of the relation leg, so both legs of a slot embed through the same bridge and the ambient relation applies.

noncomputable def RS.midConcatFst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) (a b n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPowMid A X a b) (tensorPow D X n) ⟶ modPowMid A X a (b + n)

The bridge carrying a left-block slot into the concatenated power: reassociate the right block onto the slot context and concatenate the contexts.

Equations

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

noncomputable def RS.midConcatSnd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) (m a b : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X m) (modPowMid A X a b) ⟶ modPowMid A X (m + a) b

The bridge carrying a right-block slot into the concatenated power: reassociate the left block onto the slot's lower context and concatenate.

Equations

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

theorem RS.modPowLeg_concat_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) (a b n : ℕ) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X a) w) (tensorPow D X b)) (modPowGlue X a b)) (tensorPow D X n)) (tensorPowConcat X (a + 2 + b) n).hom = CategoryTheory.CategoryStruct.comp (midConcatFst A X a b n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X a) w) (tensorPow D X (b + n))) (CategoryTheory.CategoryStruct.comp (modPowGlue X a (b + n)) (powCast X ⋯)))

A left-block slot leg embeds across the concatenation: the same computation for both legs, with the leg abstracted as w.

theorem RS.modPowLeg_concat_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) (m a b : ℕ) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X a) w) (tensorPow D X b)) (modPowGlue X a b))) (tensorPowConcat X m (a + 2 + b)).hom = CategoryTheory.CategoryStruct.comp (midConcatSnd A X m a b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X (m + a)) w) (tensorPow D X b)) (CategoryTheory.CategoryStruct.comp (modPowGlue X (m + a) b) (powCast X ⋯)))

A right-block slot leg embeds across the concatenation: the same computation for both legs, with the leg abstracted as w.

The slot relations across the concatenation boundary

theorem RS.modPowMul_rel_fst {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] {m : ℕ} (n a b : ℕ) (hab : a + 2 + b = m) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (powCast X hab)) (tensorPow D X n)) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X m n).hom (modPowπ A X (m + n))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (powCast X hab)) (tensorPow D X n)) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X m n).hom (modPowπ A X (m + n)))

Left-block slot relations embed: a relation slot of the left block, whiskered by the right block and concatenated into the ambient power of arity m + n, is absorbed by the projection.

theorem RS.modPowMul_rel_snd {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] (m : ℕ) {n : ℕ} (a b : ℕ) (hab : a + 2 + b = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X m) (CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (powCast X hab))) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X m n).hom (modPowπ A X (m + n))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X m) (CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (powCast X hab))) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X m n).hom (modPowπ A X (m + n)))

Right-block slot relations embed: a relation slot of the right block, whiskered by the left block and concatenated into the ambient power of arity m + n, is absorbed by the projection.

Whiskered coequalizers of the module power

The two-stage descent needs the module-power coequalizer to remain a colimit after whiskering on either side; this is exactly the preservation of parallel-pair colimits by tensorLeft/tensorRight, taken as instance parameters.

noncomputable def RS.modPowWhiskerLeftIsColimit {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) (n : ℕ) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modPowπ A X n)) ⋯)

Whiskering the module-power coequalizer on the left yields a colimit cofork.

Equations

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

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

Morphisms out of a left-whiskered module power are determined by their composite with the whiskered projection.

noncomputable def RS.modPowWhiskerLeftDesc {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) (n : ℕ) {Z : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj P (tensorPow D X n) ⟶ Z) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modPowLegFst A X n)) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modPowLegSnd A X n)) k) : CategoryTheory.MonoidalCategoryStruct.tensorObj P (modPow A X n) ⟶ Z

Descend a morphism along the left-whiskered projection.

Equations

• RS.modPowWhiskerLeftDesc A X P n k h = CategoryTheory.Limits.Cofork.IsColimit.desc (RS.modPowWhiskerLeftIsColimit A X P n) k h

@[simp]

theorem RS.modPowπ_whiskerLeft_desc {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) (n : ℕ) {Z : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj P (tensorPow D X n) ⟶ Z) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modPowLegFst A X n)) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modPowLegSnd A X n)) k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modPowπ A X n)) (modPowWhiskerLeftDesc A X P n k h) = k

The left-whiskered descent factors through the whiskered projection.

@[simp]

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

The left-whiskered descent factors through the whiskered projection.

noncomputable def RS.modPowWhiskerRightLeftIsColimit {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)] (n : ℕ) (W P : D) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X n) W)) ⋯)

A doubly whiskered projection is still a colimit cofork.

Equations

• RS.modPowWhiskerRightLeftIsColimit A X n W P = CategoryTheory.Limits.isColimitCoforkMapOfIsColimit (CategoryTheory.MonoidalCategory.tensorLeft P) ⋯ (RS.modPowWhiskerRightIsColimit A X n W)

instance RS.epi_whiskerLeft_modPowπ {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) (n : ℕ) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modPowπ A X n))

The left-whiskered projection is an epimorphism.

instance RS.epi_whiskerLeft_modPowπ_whiskerRight {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)] (n : ℕ) (W P : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X n) W))

The doubly whiskered projection is an epimorphism.

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

Morphisms out of a tensor product of module powers are determined by their composite with the tensored projections.

The raw multiplication

noncomputable def RS.modPowMulStage {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] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A X m) (tensorPow D X n) ⟶ modPow A X (m + n)

The first stage of the multiplication: the concatenation descends through the left factor against an ambient right factor.

Equations

• RS.modPowMulStage A X m n = RS.modPowWhiskerRightDesc A X m (RS.tensorPow D X n) (CategoryTheory.CategoryStruct.comp (RS.tensorPowConcat X m n).hom (RS.modPowπ A X (m + n))) ⋯

@[simp]

theorem RS.modPowπ_whiskerRight_mulStage {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] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X m) (tensorPow D X n)) (modPowMulStage A X m n) = CategoryTheory.CategoryStruct.comp (tensorPowConcat X m n).hom (modPowπ A X (m + n))

Defining equation of the first stage.

@[simp]

theorem RS.modPowπ_whiskerRight_mulStage_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.Limits.HasCoequalizers D] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) {Z : D} (h : modPow A X (m + n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X m) (tensorPow D X n)) (CategoryTheory.CategoryStruct.comp (modPowMulStage A X m n) h) = CategoryTheory.CategoryStruct.comp (tensorPowConcat X m n).hom (CategoryTheory.CategoryStruct.comp (modPowπ A X (m + n)) h)

Defining equation of the first stage.

theorem RS.modPowMulStage_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.Limits.HasCoequalizers D] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modPow A X m) (modPowLegFst A X n)) (modPowMulStage A X m n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modPow A X m) (modPowLegSnd A X n)) (modPowMulStage A X m n)

The first stage coequalizes the left-whiskered legs of the right factor.

noncomputable def RS.modPowMul {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] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A X m) (modPow A X n) ⟶ modPow A X (m + n)

The raw multiplication on module powers, descended from the concatenation of the ambient tensor powers in two stages.

Equations

• RS.modPowMul A X m n = RS.modPowWhiskerLeftDesc A X (RS.modPow A X m) n (RS.modPowMulStage A X m n) ⋯

@[simp]

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

The second-stage defining equation.

@[simp]

theorem RS.modPow_whiskerLeft_modPowMul_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.Limits.HasCoequalizers D] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) {Z : D} (h : modPow A X (m + n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modPow A X m) (modPowπ A X n)) (CategoryTheory.CategoryStruct.comp (modPowMul A X m n) h) = CategoryTheory.CategoryStruct.comp (modPowMulStage A X m n) h

The second-stage defining equation.

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

Defining equation of the raw multiplication: on the ambient tensor powers it is the concatenation followed by the projection.

theorem RS.modPowπ_tensor_modPowMul_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.Limits.HasCoequalizers D] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) {Z : D} (h : modPow A X (m + n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X m) (modPowπ A X n)) (CategoryTheory.CategoryStruct.comp (modPowMul A X m n) h) = CategoryTheory.CategoryStruct.comp (tensorPowConcat X m n).hom (CategoryTheory.CategoryStruct.comp (modPowπ A X (m + n)) h)

Defining equation of the raw multiplication: on the ambient tensor powers it is the concatenation followed by the projection.

Bilinear glue for the algebra intertwining

Equivariance of the raw multiplication

theorem RS.modPowMul_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.Limits.HasCoequalizers D] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) (σ : Equiv.Perm (Fin m)) (τ : Equiv.Perm (Fin n)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowPerm m σ) (modPowPerm n τ)) (modPowMul A X m n) = CategoryTheory.CategoryStruct.comp (modPowMul A X m n) (modPowPerm (m + n) (blockEmbed σ τ))

Equivariance: the raw multiplication intertwines the pair of permutation actions with the block-embedded action.

theorem RS.modPowMul_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.Limits.HasCoequalizers D] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (m n : ℕ) (x : SymGroupAlgebra m) (y : SymGroupAlgebra n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((modPowAlg A X m) x) ((modPowAlg A X n) y)) (modPowMul A X m n) = CategoryTheory.CategoryStruct.comp (modPowMul A X m n) ((modPowAlg A X (m + n)) (blockAlgEmbed x y))

Linear equivariance: the raw multiplication intertwines the group-algebra actions with the block embedding of group algebras, by bilinear extension of the permutation case.

Absorption of embedded symmetrisers

theorem RS.symmetriser_mul_mapDomain {k N : ℕ} (f : Equiv.Perm (Fin k) →* Equiv.Perm (Fin N)) : symmetriser N * (MonoidAlgebra.mapDomainAlgHom ℂ ℂ f) (symmetriser k) = symmetriser N

The full symmetriser absorbs the image of any mass-one average: pushing a symmetriser forward along any group homomorphism into the larger symmetric group leaves the larger symmetriser fixed.

theorem RS.symmetriser_mul_blockAlgEmbed (m n : ℕ) : symmetriser (m + n) * blockAlgEmbed (symmetriser m) (symmetriser n) = symmetriser (m + n)

The coset identity: the block embedding of the two symmetrisers is absorbed by the full symmetriser.

theorem RS.blockAlgEmbed_one_left {m n : ℕ} (y : SymGroupAlgebra n) : blockAlgEmbed 1 y = (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (blockEmbedSndHom m n)) y

The block embedding of a one-sided unit is one-sided.

theorem RS.blockAlgEmbed_one_right {m n : ℕ} (x : SymGroupAlgebra m) : blockAlgEmbed x 1 = (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (blockEmbedFstHom m n)) x

The block embedding of a one-sided unit is one-sided.

theorem RS.modPowAlg_absorb {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 : ℕ} (z : SymGroupAlgebra N) (hz : symmetriser N * z = symmetriser N) : CategoryTheory.CategoryStruct.comp ((modPowAlg A X N) z) (symPowπ A X N) = symPowπ A X N

Any element absorbed by the symmetriser acts trivially after the symmetric-power projection.

The multiplication on symmetric powers

noncomputable def RS.symMul {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] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (symPow A X m) (symPow A X n) ⟶ symPow A X (m + n)

The multiplication on symmetric powers, through the sections and the raw multiplication.

Equations

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

theorem RS.symPowπ_tensor_symMul {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)] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowπ A X m) (symPowπ A X n)) (symMul A X m n) = CategoryTheory.CategoryStruct.comp (modPowMul A X m n) (symPowπ A X (m + n))

Defining equation of the symmetric multiplication: the two projections carry the raw multiplication to symMul. The two factor symmetrisers introduced by the sections are absorbed by the full symmetriser through equivariance and the coset identity.

theorem RS.symPowπ_tensor_symMul_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.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n : ℕ) {Z : D} (h : symPow A X (m + n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowπ A X m) (symPowπ A X n)) (CategoryTheory.CategoryStruct.comp (symMul A X m n) h) = CategoryTheory.CategoryStruct.comp (modPowMul A X m n) (CategoryTheory.CategoryStruct.comp (symPowπ A X (m + n)) h)

Defining equation of the symmetric multiplication: the two projections carry the raw multiplication to symMul. The two factor symmetrisers introduced by the sections are absorbed by the full symmetriser through equivariance and the coset identity.

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

Morphisms out of a tensor product of symmetric powers are determined by their composites with the tensored projections.

The empty symmetric power

theorem RS.symmetriser_zero : symmetriser 0 = 1

At arity zero the symmetriser is the unit of the group algebra.

theorem RS.symPowIdem_zero {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] : symPowIdem A X 0 = CategoryTheory.CategoryStruct.id (modPow A X 0)

At arity zero the symmetriser acts as the identity.

noncomputable def RS.symPowZero {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] : symPow A X 0 ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

The empty symmetric power is the unit object.

Equations

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

theorem RS.symmetriser_one : symmetriser 1 = 1

At arity one the symmetriser is the unit of the group algebra.

theorem RS.symPowIdem_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.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] : symPowIdem A X 1 = CategoryTheory.CategoryStruct.id (modPow A X 1)

At arity one the symmetriser acts as the identity.

noncomputable def RS.symPowOne {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] : symPow A X 1 ≅ X

The singleton symmetric power is the module.

Equations

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

noncomputable def RS.symPowCast {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] {m n : ℕ} (h : m = n) : symPow A X m ⟶ symPow A X n

Transport of a symmetric power along an equality of arities.

Equations

• RS.symPowCast A X h = CategoryTheory.eqToHom ⋯

@[simp]

theorem RS.symPowCast_rfl {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 : ℕ) : symPowCast A X ⋯ = CategoryTheory.CategoryStruct.id (symPow A X n)

theorem RS.symPowπ_cast {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] {m n : ℕ} (h : m = n) : CategoryTheory.CategoryStruct.comp (symPowπ A X m) (symPowCast A X h) = CategoryTheory.CategoryStruct.comp (modPowCast A X h) (symPowπ A X n)

The projection intertwines the module- and symmetric-power transports.

theorem RS.symPowπ_cast_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] {m n : ℕ} (h : m = n) {Z : D} (h✝ : symPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (symPowπ A X m) (CategoryTheory.CategoryStruct.comp (symPowCast A X h) h✝) = CategoryTheory.CategoryStruct.comp (modPowCast A X h) (CategoryTheory.CategoryStruct.comp (symPowπ A X n) h✝)

The projection intertwines the module- and symmetric-power transports.

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

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

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

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

Unit laws

theorem RS.modPowMul_zero_left {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)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowZero A X).inv (modPow A X n)) (modPowMul A X 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (modPow A X n)).hom (modPowCast A X ⋯)

Left unit law at the module-power level: multiplying by the empty power is the left unitor, up to the arity transport.

theorem RS.modPowMul_zero_right {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)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modPow A X n) (modPowZero A X).inv) (modPowMul A X n 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (modPow A X n)).hom (modPowCast A X ⋯)

Right unit law at the module-power level: multiplying by the empty power is the right unitor, up to the arity transport.

Unit laws for the symmetric multiplication

theorem RS.symPowZero_inv_symPowσ {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] : CategoryTheory.CategoryStruct.comp (symPowZero A X).inv (symPowσ A X 0) = (modPowZero A X).inv

The unit section of the empty symmetric power lifts to the empty module power.

theorem RS.symMul_zero_left {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)] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (symPowZero A X).inv (symPow A X n)) (symMul A X 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (symPow A X n)).hom (symPowCast A X ⋯)

Left unit law: multiplying by the empty symmetric power is the left unitor, up to the arity transport.

Associativity

instance RS.instEpiTensorHomModPowπOfPreservesColimitsOfShapeWalkingParallelPairTensorLeft {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)] (m n : ℕ) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X m) (modPowπ A X n))

instance RS.instEpiWhiskerRightTensorHomModPowπTensorPowOfPreservesColimitsOfShapeWalkingParallelPairTensorLeft {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)] (m n r : ℕ) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X m) (modPowπ A X n)) (tensorPow D X r))

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

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

theorem RS.modPowMul_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.Limits.HasCoequalizers D] [CategoryTheory.MonoidalPreadditive D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (m n r : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowMul A X m n) (modPow A X r)) (modPowMul A X (m + n) r) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (modPow A X m) (modPow A X n) (modPow A X r)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modPow A X m) (modPowMul A X n r)) (CategoryTheory.CategoryStruct.comp (modPowMul A X m (n + r)) (modPowCast A X ⋯)))

Associativity of the raw multiplication, up to the arity transport of m + (n + r) = m + n + r.

Associativity of the symmetric multiplication

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

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

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

Associativity of the symmetric multiplication, up to the arity transport of m + (n + r) = m + n + r.

Commutativity

The braiding of two tensor powers is, through the concatenations, a permutation action; commutativity of symMul then follows because the symmetriser absorbs every permutation. The permutation itself is never computed: each intertwining is established with an existentially quantified permutation, assembled by the same recursion as the concatenation.

theorem RS.braiding_one_pow_exists {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) (n : ℕ) : ∃ (τ : Equiv.Perm (Fin (n + 1))), CategoryTheory.CategoryStruct.comp (powPeel X n).hom (β_ X (tensorPow D X n)).hom = permMor X (n + 1) τ

The peeled braiding of one factor with a power acts by a permutation, assembled by the recursion of the power itself.

theorem RS.tensorPowConcat_braiding_exists {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) (n m : ℕ) : ∃ (σ : Equiv.Perm (Fin (n + m))), CategoryTheory.CategoryStruct.comp (β_ (tensorPow D X m) (tensorPow D X n)).hom (tensorPowConcat X n m).hom = CategoryTheory.CategoryStruct.comp (tensorPowConcat X m n).hom (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (permMor X (n + m) σ))

The braiding of tensor powers is a permutation across the concatenations: for some permutation σ of the slots.

Commutativity of the symmetric multiplication

theorem RS.permMor_π_absorb {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 : ℕ) (τ : Equiv.Perm (Fin N)) : CategoryTheory.CategoryStruct.comp (permMor X N τ) (CategoryTheory.CategoryStruct.comp (modPowπ A X N) (symPowπ A X N)) = CategoryTheory.CategoryStruct.comp (modPowπ A X N) (symPowπ A X N)

Every permutation action on the ambient power is absorbed by the two projections: the symmetriser eats it.

theorem RS.symMul_comm {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)] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (β_ (symPow A X m) (symPow A X n)).hom (symMul A X n m) = CategoryTheory.CategoryStruct.comp (symMul A X m n) (symPowCast A X ⋯)

Commutativity of the symmetric multiplication, up to the arity transport of m + n = n + m.