Module powers and symmetric powers over an internal monoid

The substrate of the Key Lemma: for an internal monoid A and a left module X in a symmetric monoidal category, the n-th module power X ^ ⊗_A n is presented in one step, with no associativity of a binary product anywhere — it is the coequalizer of a single pair

`⊕ᵢ Rᵢ ⇉ X ^ ⊗ n`

whose source is the finite biproduct, over the n − 1 adjacent slots, of the relation objects Rᵢ = X^⊗a ⊗ ((X ⊗ A) ⊗ X) ⊗ X^⊗b (a + 2 + b = n), and whose legs act on the slot through the braided right action and the left action respectively — identifying (x·c) ⊗ y with x ⊗ (c·y) in every adjacent slot at once.

• modPow A X n, modPowπ, modPowDesc, modPow_hom_ext: the power and its universal property. Slot conditions are quantified over decompositions a + 2 + b = n (with a powCast transport), so consumers never meet truncated subtraction.
• modPowZero, modPowOne: at n ≤ 1 there are no slots, the legs agree, and the projection is an isomorphism.
• modPowPerm: the permutation action of Envelope/SymPerm.lean descends to the module power; modPowPermHom, modPowAlg package it as a monoid homomorphism and a ℂ-algebra map. The descent is proved on the adjacent transpositions and extended by generation; commutativity of A is not needed, because the braided right action is by definition the left action through the braiding.
• symmetriser n: the trivial-character central idempotent (1/n!) • ∑ σ, σ of the group algebra, with absorption and idempotency.
• symPow A X n: the symmetric power, presented as the coequalizer of modPowAlg (symmetriser n) against the identity — the coinvariants — which the idempotent splits into a direct summand: symPowσ ≫ symPowπ = 𝟙 and symPowπ ≫ symPowσ is the symmetriser's action. This presentation is chosen because the consumers build morphisms out of symPow by descent along symPowπ and morphisms in through the section symPowσ. The multiplication maps between module powers of different arities are outside this module's scope; tensorPowConcat_peel and the frame machinery below are the concatenation substrate they will consume.

Transport along equal arities

def RS.powCast {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) {m n : ℕ} (h : m = n) : tensorPow D X m ⟶ tensorPow D X n

Transport of a tensor power along an equality of arities. It is an eqToHom, so it composes and cancels by eqToHom simp lemmas.

Equations

• RS.powCast X h = CategoryTheory.eqToHom ⋯

@[simp]

theorem RS.powCast_rfl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (n : ℕ) : powCast X ⋯ = CategoryTheory.CategoryStruct.id (tensorPow D X n)

@[simp]

theorem RS.powCast_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) {m n k : ℕ} (h : m = n) (h' : n = k) : CategoryTheory.CategoryStruct.comp (powCast X h) (powCast X h') = powCast X ⋯

@[simp]

theorem RS.powCast_comp_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) {m n k : ℕ} (h : m = n) (h' : n = k) {Z : D} (h✝ : tensorPow D X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (powCast X h) (CategoryTheory.CategoryStruct.comp (powCast X h') h✝) = CategoryTheory.CategoryStruct.comp (powCast X ⋯) h✝

theorem RS.powCast_irrel {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) {m n : ℕ} (h h' : m = n) : powCast X h = powCast X h'

Two arity transports with the same endpoints agree.

theorem RS.powCast_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) {m n : ℕ} (h : m = n) : CategoryTheory.MonoidalCategoryStruct.whiskerRight (powCast X h) X = powCast X ⋯

Whiskering an arity transport is an arity transport.

Peeling the first factor off a tensor power

The tensor power grows at the top, so the bottom factor is exposed by a recursion of its own; the peeling intertwines the two concatenation stages p + (q + 1) and (p + 1) + q, which is what lets a relation slot and an adjacent braiding that overlap in one module factor be compared in a common frame.

noncomputable def RS.powPeel {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (q : ℕ) : tensorPow D X (q + 1) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj X (tensorPow D X q)

Peel the first factor off a non-empty tensor power.

Equations

• RS.powPeel X 0 = CategoryTheory.MonoidalCategoryStruct.leftUnitor X ≪≫ (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).symm
• RS.powPeel X q.succ = CategoryTheory.MonoidalCategory.whiskerRightIso (RS.powPeel X q) X ≪≫ CategoryTheory.MonoidalCategoryStruct.associator X (RS.tensorPow D X q) X

theorem RS.powPeel_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) : powPeel X 0 = CategoryTheory.MonoidalCategoryStruct.leftUnitor X ≪≫ (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).symm

The base case of the peeling.

noncomputable def RS.powAttach {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X p) (CategoryTheory.MonoidalCategoryStruct.tensorObj X (tensorPow D X q)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X (p + 1)) (tensorPow D X q)

Attach a peeled factor to the power below it. The associator, retyped so that its target is stated through the tensor power — this keeps every statement about it type-correct at low transparency.

Equations

• RS.powAttach X p q = (CategoryTheory.MonoidalCategoryStruct.associator (RS.tensorPow D X p) X (RS.tensorPow D X q)).inv

noncomputable def RS.powExpose {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X p) (tensorPow D X (q + 1)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X p) (tensorPow D X q)) X

Expose the top factor of the second block of a pair of powers. The associator, retyped so that its source is stated through the tensor power.

Equations

• RS.powExpose X p q = (CategoryTheory.MonoidalCategoryStruct.associator (RS.tensorPow D X p) (RS.tensorPow D X q) X).inv

theorem RS.tensorPowConcat_succ_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (p q : ℕ) : (tensorPowConcat X p (q + 1)).hom = CategoryTheory.CategoryStruct.comp (powExpose X p q) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (tensorPowConcat X p q).hom X)

The successor stage of the concatenation, through the exposed top factor; definitional.

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

The concatenation shift: concatenating p with q + 1 factors is peeling the first of the q + 1, attaching it to the p, and concatenating p + 1 with q.

The slot relation

The local shape of one relation slot: on (X ⊗ A) ⊗ X, either the monoid acts on the left factor through the braided right action, or it associates and acts on the right factor. These are the legs of ModTensor.lean at the module X itself, unbundled.

noncomputable def RS.winLegM {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.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X X

The slot leg acting on the left factor, through the braided right action.

Equations

• RS.winLegM A X = CategoryTheory.MonoidalCategoryStruct.whiskerRight (RS.actRight A X) X

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

The slot leg acting on the right factor: associate, then act.

Equations

• RS.winLegN A X = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X A X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (RS.actLeft A X))

The relation pair of the module power

@[reducible, inline]

abbrev RS.modPowMid {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) (a b : ℕ) : D

The relation object of the slot a + 2 + b = n: the ambient power with the monoid inserted between the module factors in slots a and a + 1. An abbreviation, so that statements about it stay type-correct at low transparency.

Equations

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

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

Glue a resolved slot back into the ambient power: reassociate the two exposed factors onto the lower power and concatenate.

Equations

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

noncomputable def RS.modPowLegM {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 : ℕ) : modPowMid A X a b ⟶ tensorPow D X (a + 2 + b)

The first relation leg at slot (a, b): act on the left module factor through the braided right action, then glue.

Equations

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

noncomputable def RS.modPowLegN {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) : modPowMid A X a b ⟶ tensorPow D X (a + 2 + b)

The second relation leg at slot (a, b): associate and act on the right module factor, then glue.

Equations

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

theorem RS.slot_decomp {n : ℕ} (i : Fin (n - 1)) : ↑i + 2 + (n - 2 - ↑i) = n

Each slot index of arity n decomposes it.

@[reducible, inline]

noncomputable abbrev RS.modPowSrc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (n : ℕ) : D

The source of the relation pair: the biproduct of the relation objects over all n − 1 adjacent slots. An abbreviation, so that the biproduct API applies to the legs without unfolding.

Equations

• RS.modPowSrc A X n = ⨁ fun (i : Fin (n - 1)) => RS.modPowMid A X (↑i) (n - 2 - ↑i)

noncomputable def RS.modPowLegFst {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] (n : ℕ) : modPowSrc A X n ⟶ tensorPow D X n

The first leg of the relation pair, assembled over all slots.

Equations

• RS.modPowLegFst A X n = CategoryTheory.Limits.biproduct.desc fun (i : Fin (n - 1)) => CategoryTheory.CategoryStruct.comp (RS.modPowLegM A X (↑i) (n - 2 - ↑i)) (RS.powCast X ⋯)

noncomputable def RS.modPowLegSnd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (n : ℕ) : modPowSrc A X n ⟶ tensorPow D X n

The second leg of the relation pair, assembled over all slots.

Equations

• RS.modPowLegSnd A X n = CategoryTheory.Limits.biproduct.desc fun (i : Fin (n - 1)) => CategoryTheory.CategoryStruct.comp (RS.modPowLegN A X (↑i) (n - 2 - ↑i)) (RS.powCast X ⋯)

The module power and its universal property

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

The n-th module power of X over A: the coequalizer of the wide relation pair, identifying (x·c) ⊗ y ~ x ⊗ (c·y) in every adjacent slot simultaneously. No binary module tensor product and no associativity enter.

Equations

• RS.modPow A X n = CategoryTheory.Limits.coequalizer (RS.modPowLegFst A X n) (RS.modPowLegSnd A X n)

noncomputable def RS.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] (n : ℕ) : tensorPow D X n ⟶ modPow A X n

The projection of the ambient power onto the module power.

Equations

• RS.modPowπ A X n = CategoryTheory.Limits.coequalizer.π (RS.modPowLegFst A X n) (RS.modPowLegSnd A X n)

instance RS.instEpiModPowπ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (n : ℕ) : CategoryTheory.Epi (modPowπ A X n)

theorem RS.modPow_condition {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (n : ℕ) : CategoryTheory.CategoryStruct.comp (modPowLegFst A X n) (modPowπ A X n) = CategoryTheory.CategoryStruct.comp (modPowLegSnd A X n) (modPowπ A X n)

The two assembled legs agree after the projection.

theorem RS.modPow_condition_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] (n : ℕ) {Z : D} (h : modPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowLegFst A X n) (CategoryTheory.CategoryStruct.comp (modPowπ A X n) h) = CategoryTheory.CategoryStruct.comp (modPowLegSnd A X n) (CategoryTheory.CategoryStruct.comp (modPowπ A X n) h)

The two assembled legs agree after the projection.

theorem RS.modPow_rel {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 : ℕ} (a b : ℕ) (h : a + 2 + b = n) : CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (CategoryTheory.CategoryStruct.comp (powCast X h) (modPowπ A X n)) = CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (CategoryTheory.CategoryStruct.comp (powCast X h) (modPowπ A X n))

The slot relation in the module power: at every decomposition a + 2 + b = n the two slot legs agree after the projection.

theorem RS.modPow_rel_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] {n : ℕ} (a b : ℕ) (h : a + 2 + b = n) {Z : D} (h✝ : modPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (CategoryTheory.CategoryStruct.comp (powCast X h) (CategoryTheory.CategoryStruct.comp (modPowπ A X n) h✝)) = CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (CategoryTheory.CategoryStruct.comp (powCast X h) (CategoryTheory.CategoryStruct.comp (modPowπ A X n) h✝))

The slot relation in the module power: at every decomposition a + 2 + b = n the two slot legs agree after the projection.

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

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

noncomputable def RS.modPowDesc {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 : ℕ} {W : D} (k : tensorPow D X n ⟶ W) (h : ∀ (a b : ℕ) (hab : a + 2 + b = n), CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (CategoryTheory.CategoryStruct.comp (powCast X hab) k) = CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (CategoryTheory.CategoryStruct.comp (powCast X hab) k)) : modPow A X n ⟶ W

Descend a morphism that coequalizes every slot relation to the module power.

Equations

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

@[simp]

theorem RS.modPowπ_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] {n : ℕ} {W : D} (k : tensorPow D X n ⟶ W) (h : ∀ (a b : ℕ) (hab : a + 2 + b = n), CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (CategoryTheory.CategoryStruct.comp (powCast X hab) k) = CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (CategoryTheory.CategoryStruct.comp (powCast X hab) k)) : CategoryTheory.CategoryStruct.comp (modPowπ A X n) (modPowDesc A X k h) = k

The descent factors the given morphism through the projection.

@[simp]

theorem RS.modPowπ_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] {n : ℕ} {W : D} (k : tensorPow D X n ⟶ W) (h : ∀ (a b : ℕ) (hab : a + 2 + b = n), CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (CategoryTheory.CategoryStruct.comp (powCast X hab) k) = CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (CategoryTheory.CategoryStruct.comp (powCast X hab) k)) {Z : D} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowπ A X n) (CategoryTheory.CategoryStruct.comp (modPowDesc A X k h) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The descent factors the given morphism through the projection.

The empty and singleton powers

At n ≤ 1 there are no adjacent slots: the relation source is the empty biproduct, the legs agree, and the projection is an isomorphism.

noncomputable def RS.modPowTriv {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 : ℕ} (h : n ≤ 1) : modPow A X n ≅ tensorPow D X n

Below two factors the projection is an isomorphism.

Equations

• RS.modPowTriv A X h = { hom := RS.modPowDesc A X (CategoryTheory.CategoryStruct.id (RS.tensorPow D X n)) ⋯, inv := RS.modPowπ A X n, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

The empty module power is the unit.

Equations

• RS.modPowZero A X = RS.modPowTriv A X RS.modPowZero._proof_2

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

The singleton module power is the module.

Equations

• RS.modPowOne A X = RS.modPowTriv A X RS.modPowOne._proof_2 ≪≫ CategoryTheory.MonoidalCategoryStruct.leftUnitor X

Whiskering the presentation on the right

Tensoring on the right by a fixed object carries the coequalizer presenting the module power to a coequalizer, so a morphism out of the whiskered module power is a morphism out of the whiskered ambient power that respects the whiskered relation. The hypothesis is the exact colimit preservation needed, so that the kit applies both where tensoring on the left is assumed exact and where tensoring on the right is.

noncomputable def RS.modPowWhiskerRightIsColimit {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 : ℕ) (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (modPowLegFst A X n) (modPowLegSnd A X n)) (CategoryTheory.MonoidalCategory.tensorRight W)] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X n) W) ⋯)

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

Equations

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

theorem RS.modPow_whiskerRight_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] (n : ℕ) (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (modPowLegFst A X n) (modPowLegSnd A X n)) (CategoryTheory.MonoidalCategory.tensorRight W)] {Z : D} {k l : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A X n) W ⟶ Z} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X n) W) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X n) W) l) : k = l

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

instance RS.epi_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] (n : ℕ) (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (modPowLegFst A X n) (modPowLegSnd A X n)) (CategoryTheory.MonoidalCategory.tensorRight W)] : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X n) W)

The right-whiskered projection is an epimorphism.

noncomputable def RS.modPowWhiskerRightDesc {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 : ℕ) (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (modPowLegFst A X n) (modPowLegSnd A X n)) (CategoryTheory.MonoidalCategory.tensorRight W)] {Z : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X n) W ⟶ Z) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegFst A X n) W) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegSnd A X n) W) k) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A X n) W ⟶ Z

Descend a morphism along the right-whiskered projection.

Equations

• RS.modPowWhiskerRightDesc A X n W k h = CategoryTheory.Limits.Cofork.IsColimit.desc (RS.modPowWhiskerRightIsColimit A X n W) k h

@[simp]

theorem RS.modPowπ_whiskerRight_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] (n : ℕ) (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (modPowLegFst A X n) (modPowLegSnd A X n)) (CategoryTheory.MonoidalCategory.tensorRight W)] {Z : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X n) W ⟶ Z) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegFst A X n) W) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegSnd A X n) W) k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X n) W) (modPowWhiskerRightDesc A X n W k h) = k

The right-whiskered descent factors through the whiskered projection.

@[simp]

theorem RS.modPowπ_whiskerRight_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] (n : ℕ) (W : D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (modPowLegFst A X n) (modPowLegSnd A X n)) (CategoryTheory.MonoidalCategory.tensorRight W)] {Z : D} (k : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X n) W ⟶ Z) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegFst A X n) W) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegSnd A X n) W) k) {Z✝ : D} (h✝ : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X n) W) (CategoryTheory.CategoryStruct.comp (modPowWhiskerRightDesc A X n W k h) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The right-whiskered descent factors through the whiskered projection.

The adjacent transposition on the ambient power

The permutation action descends to the module power once it descends on the adjacent transpositions, which act by a braiding of two adjacent slots — the top braiding of the first a + 2 factors, conjugated into the ambient power by the concatenation.

noncomputable def RS.adjSwapMor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) (a b : ℕ) : tensorPow D X (a + 2 + b) ⟶ tensorPow D X (a + 2 + b)

The braiding of slots a and a + 1 of the ambient power: the top braiding of the first a + 2 factors, in block form.

Equations

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

theorem RS.adjSwapMor_eq_permMor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) (a b : ℕ) : adjSwapMor X a b = permMor X (a + 2 + b) (Equiv.swap ⟨a, ⋯⟩ ⟨a + 1, ⋯⟩)

The adjacent braiding is the action of the adjacent transposition.

theorem RS.powCast_permMor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) {m n : ℕ} (h : m = n) (σ : Equiv.Perm (Fin m)) : CategoryTheory.CategoryStruct.comp (powCast X h) (permMor X n ((finCongr h).permCongr σ)) = CategoryTheory.CategoryStruct.comp (permMor X m σ) (powCast X h)

Transport of a permutation action along an equality of arities.

theorem RS.powCast_permMor_swap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) {m n : ℕ} (h : m = n) (u v : Fin m) : CategoryTheory.CategoryStruct.comp (powCast X h) (permMor X n (Equiv.swap (Fin.cast h u) (Fin.cast h v))) = CategoryTheory.CategoryStruct.comp (permMor X m (Equiv.swap u v)) (powCast X h)

Transport of a transposition action along an equality of arities.

The braiding at a relation slot

The braiding of the two module factors of a slot carries the monoid along; the relation legs intertwine it with the plain braiding on the resolved slot. No commutativity of the monoid is needed: the braided right action is by definition the left action through the braiding, so the exchanged slot acts by the same morphism.

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

Exchange of the two module factors of a relation slot, carrying the monoid along: (x ⊗ c) ⊗ y ↦ (y ⊗ c) ⊗ x.

Equations

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

@[simp]

theorem RS.winSwap_winSwap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A X : D) : CategoryTheory.CategoryStruct.comp (winSwap A X) (winSwap A X) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X)

The slot exchange is an involution.

@[simp]

theorem RS.winSwap_winSwap_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A X : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X ⟶ Z) : CategoryTheory.CategoryStruct.comp (winSwap A X) (CategoryTheory.CategoryStruct.comp (winSwap A X) h) = h

The slot exchange is an involution.

theorem RS.winLegM_braiding {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (winLegM A X) (β_ X X).hom = CategoryTheory.CategoryStruct.comp (winSwap A X) (winLegN A X)

The first leg intertwines the slot exchange with the braiding: acting on the left factor and braiding is exchanging and acting on the right factor.

theorem RS.winLegN_braiding {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (winLegN A X) (β_ X X).hom = CategoryTheory.CategoryStruct.comp (winSwap A X) (winLegM A X)

The second leg intertwines the slot exchange with the braiding, by the involutivity of both.

Descent of the slot relations under the adjacent braiding

theorem RS.modPow_rel_self {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] (a b : ℕ) : CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (modPowπ A X (a + 2 + b)) = CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (modPowπ A X (a + 2 + b))

The slot relation with no arity transport.

theorem RS.modPow_rel_self_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] (a b : ℕ) {Z : D} (h : modPow A X (a + 2 + b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (CategoryTheory.CategoryStruct.comp (modPowπ A X (a + 2 + b)) h) = CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (CategoryTheory.CategoryStruct.comp (modPowπ A X (a + 2 + b)) h)

The slot relation with no arity transport.

def RS.modPowDescends {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] (n : ℕ) (f : tensorPow D X n ⟶ tensorPow D X n) : Prop

Descent along the projection: the property that an ambient endomorphism carries every slot relation into the kernel of the projection again.

Equations

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

The disjoint cases

When the braided pair lies entirely inside the upper or lower context of the relation slot, the braiding passes the legs by the exchange law, through the block form of the embedded permutation.

The three-slot window

The two overlapping cases — the braided pair sharing one module factor with the relation slot — are compared inside a window of three module factors. The window morphisms below are stated on ((X ⊗ A) ⊗ X) ⊗ X and X ⊗ ((X ⊗ A) ⊗ X), with the monoid carried along; their identities against the slot legs are the local content of the two cases.

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

The braiding of the two upper factors of the resolved window.

Equations

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

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

The braiding of the two lower factors of the resolved window.

Equations

• RS.winLow X = CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X X).hom X

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

Exchange of the two pure module factors of a lower-relation window, carrying nothing else along.

Equations

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

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

From a lower-relation window to an upper-relation window: the top module factor moves down past the flanked pair, by the braiding against the pair.

Equations

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

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

From an upper-relation window to a lower-relation window: the bottom module factor moves up past the flanked pair.

Equations

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

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

Exchange of the two lower module factors of an upper-relation window, across the monoid.

Equations

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

The three-slot frame

Both overlap cases are compared in a frame (Xᵃ ⊗ V) ⊗ X^q around a three-slot window V, glued into the ambient power through the assembled window and the concatenation.

noncomputable def RS.winAssemble {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (a : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X a) (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X X) X) ⟶ tensorPow D X (a + 3)

Assemble a resolved three-slot window onto the power below.

Equations

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

noncomputable def RS.winFrame {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (a q : ℕ) {n : ℕ} (h : a + 3 + q = n) {V : D} (u : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X X) X) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X a) V) (tensorPow D X q) ⟶ tensorPow D X n

The framed window morphism: act inside the window, assemble, concatenate, and transport.

Equations

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

theorem RS.winFrame_pre {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (a q : ℕ) {n : ℕ} (h : a + 3 + q = n) {V V' : D} (m : V' ⟶ V) (u : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X X) X) : winFrame X a q h (CategoryTheory.CategoryStruct.comp m u) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X a) m) (tensorPow D X q)) (winFrame X a q h u)

Precomposition inside the frame.

noncomputable def RS.winFromLower {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) (a q : ℕ) : modPowMid A X a (q + 1) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X a) (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X) X)) (tensorPow D X q)

The lower-relation mid object entering the frame.

Equations

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

noncomputable def RS.winFromUpper {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) (a q : ℕ) : modPowMid A X (a + 1) q ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X a) (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) X))) (tensorPow D X q)

The upper-relation mid object entering the frame.

Equations

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

theorem RS.modPowDescends_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] {n₁ n₂ : ℕ} (h : n₁ = n₂) {f₁ : tensorPow D X n₁ ⟶ tensorPow D X n₁} {f₂ : tensorPow D X n₂ ⟶ tensorPow D X n₂} (hf : CategoryTheory.CategoryStruct.comp (powCast X h) f₂ = CategoryTheory.CategoryStruct.comp f₁ (powCast X h)) (hd : modPowDescends A X n₁ f₁) : modPowDescends A X n₂ f₂

Descent transports along an equality of arities.

theorem RS.modPowDescends_adjSwap {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] (a₀ b₀ : ℕ) : modPowDescends A X (a₀ + 2 + b₀) (adjSwapMor X a₀ b₀)

Descent of the adjacent braiding: every slot relation passes every adjacent braiding, by the same-slot, disjoint and overlap cases.

theorem RS.modPowDescends_permMor {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] (n : ℕ) (σ : Equiv.Perm (Fin n)) : modPowDescends A X n (permMor X n σ)

Descent of the permutation action: every slot relation passes the action of every permutation — on the adjacent transpositions by the case analysis, and in general by generation and multiplicativity, exactly as the ambient action itself was assembled.

noncomputable def RS.modPowPerm {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] (n : ℕ) (σ : Equiv.Perm (Fin n)) : modPow A X n ⟶ modPow A X n

The permutation action descends to the module power.

Equations

• RS.modPowPerm n σ = RS.modPowDesc A X (CategoryTheory.CategoryStruct.comp (RS.permMor X n σ) (RS.modPowπ A X n)) ⋯

@[simp]

theorem RS.modPowπ_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] (n : ℕ) (σ : Equiv.Perm (Fin n)) : CategoryTheory.CategoryStruct.comp (modPowπ A X n) (modPowPerm n σ) = CategoryTheory.CategoryStruct.comp (permMor X n σ) (modPowπ A X n)

Defining square of the descended action.

@[simp]

theorem RS.modPowπ_perm_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] (n : ℕ) (σ : Equiv.Perm (Fin n)) {Z : D} (h : modPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowπ A X n) (CategoryTheory.CategoryStruct.comp (modPowPerm n σ) h) = CategoryTheory.CategoryStruct.comp (permMor X n σ) (CategoryTheory.CategoryStruct.comp (modPowπ A X n) h)

Defining square of the descended action.

theorem RS.modPowPerm_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] (n : ℕ) : modPowPerm n 1 = CategoryTheory.CategoryStruct.id (modPow A X n)

The identity acts as the identity on the module power.

theorem RS.modPowPerm_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.Limits.HasCoequalizers D] (n : ℕ) (σ τ : Equiv.Perm (Fin n)) : modPowPerm n (σ * τ) = CategoryTheory.CategoryStruct.comp (modPowPerm n τ) (modPowPerm n σ)

The descended action is functorial.

noncomputable def RS.modPowPermHom {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] (n : ℕ) : Equiv.Perm (Fin n) →* CategoryTheory.End (modPow A X n)

The symmetric group acting on the module power, as a monoid homomorphism.

Equations

• RS.modPowPermHom A X n = { toFun := RS.modPowPerm n, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem RS.modPowPermHom_apply {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] (n : ℕ) (σ : Equiv.Perm (Fin n)) : (modPowPermHom A X n) σ = modPowPerm n σ

The symmetriser

The trivial-character central idempotent of the group algebra ℂ[Sₙ] — the charIdempotent 1 (fun _ => 1) of the Schur interface, written directly.

noncomputable def RS.symmetriser (n : ℕ) : SymGroupAlgebra n

The symmetriser (1/n!) • ∑ σ, σ of the symmetric-group algebra.

Equations

• RS.symmetriser n = (↑n.factorial)⁻¹ • ∑ σ : Equiv.Perm (Fin n), MonoidAlgebra.single σ 1

@[simp]

theorem RS.symmetriser_mul_single (n : ℕ) (τ : Equiv.Perm (Fin n)) : symmetriser n * MonoidAlgebra.single τ 1 = symmetriser n

The symmetriser absorbs every group element on the right.

@[simp]

theorem RS.single_mul_symmetriser (n : ℕ) (τ : Equiv.Perm (Fin n)) : MonoidAlgebra.single τ 1 * symmetriser n = symmetriser n

The symmetriser absorbs every group element on the left.

theorem RS.symmetriser_idem (n : ℕ) : symmetriser n * symmetriser n = symmetriser n

The symmetriser is idempotent.

The group algebra on the module power, and the symmetric

power

noncomputable def RS.modPowAlg {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 : ℕ) : SymGroupAlgebra n →ₐ[ℂ] CategoryTheory.End (modPow A X n)

The symmetric-group algebra acting on the module power, the ℂ-linear extension of the descended action.

Equations

• RS.modPowAlg A X n = (MonoidAlgebra.lift ℂ (CategoryTheory.End (RS.modPow A X n)) (Equiv.Perm (Fin n))) (RS.modPowPermHom A X n)

@[simp]

theorem RS.modPowAlg_single {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)) : (modPowAlg A X n) (MonoidAlgebra.single σ 1) = modPowPerm n σ

The algebra map sends a group element to its action.

noncomputable def RS.symPowIdem {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 : ℕ) : modPow A X n ⟶ modPow A X n

The symmetriser acting on the module power.

Equations

• RS.symPowIdem A X n = (RS.modPowAlg A X n) (RS.symmetriser n)

theorem RS.symPowIdem_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 : ℕ) : CategoryTheory.CategoryStruct.comp (symPowIdem A X n) (symPowIdem A X n) = symPowIdem A X n

The symmetriser's action is idempotent.

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

The symmetric power: the coinvariants of the symmetriser's action — the coequalizer of the action against the identity. The idempotency splits it off as a direct summand of the module power, with section symPowσ; this presentation is chosen because the consumers of the Key Lemma build morphisms out of the symmetric power by descent along symPowπ and morphisms into it through the section.

Equations

• RS.symPow A X n = CategoryTheory.Limits.coequalizer (RS.symPowIdem A X n) (CategoryTheory.CategoryStruct.id (RS.modPow A X n))

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

The projection onto the symmetric power.

Equations

• RS.symPowπ A X n = CategoryTheory.Limits.coequalizer.π (RS.symPowIdem A X n) (CategoryTheory.CategoryStruct.id (RS.modPow A X n))

instance RS.instEpiSymPowπ {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 : ℕ) : CategoryTheory.Epi (symPowπ A X n)

@[simp]

theorem RS.symPowIdem_π {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 : ℕ) : CategoryTheory.CategoryStruct.comp (symPowIdem A X n) (symPowπ A X n) = symPowπ A X n

The symmetriser is absorbed by the projection.

@[simp]

theorem RS.symPowIdem_π_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 : ℕ) {Z : D} (h : symPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (symPowIdem A X n) (CategoryTheory.CategoryStruct.comp (symPowπ A X n) h) = CategoryTheory.CategoryStruct.comp (symPowπ A X n) h

The symmetriser is absorbed by the projection.

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

The section of the symmetric power, from idempotency.

Equations

• RS.symPowσ A X n = CategoryTheory.Limits.coequalizer.desc (RS.symPowIdem A X n) ⋯

@[simp]

theorem RS.symPowπ_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] (n : ℕ) : CategoryTheory.CategoryStruct.comp (symPowπ A X n) (symPowσ A X n) = symPowIdem A X n

The section realises the symmetriser as projection followed by inclusion.

@[simp]

theorem RS.symPowπ_symPowσ_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 : ℕ) {Z : D} (h : modPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (symPowπ A X n) (CategoryTheory.CategoryStruct.comp (symPowσ A X n) h) = CategoryTheory.CategoryStruct.comp (symPowIdem A X n) h

The section realises the symmetriser as projection followed by inclusion.

theorem RS.symPow_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} {k l : symPow A X n ⟶ W} (h : CategoryTheory.CategoryStruct.comp (symPowπ A X n) k = CategoryTheory.CategoryStruct.comp (symPowπ A X n) l) : k = l

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

@[simp]

theorem RS.symPowσ_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] (n : ℕ) : CategoryTheory.CategoryStruct.comp (symPowσ A X n) (symPowπ A X n) = CategoryTheory.CategoryStruct.id (symPow A X n)

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

@[simp]

theorem RS.symPowσ_symPowπ_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 : ℕ) {Z : D} (h : symPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (symPowσ A X n) (CategoryTheory.CategoryStruct.comp (symPowπ A X n) h) = h

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

noncomputable def RS.symPowDesc {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} (k : modPow A X n ⟶ W) (h : CategoryTheory.CategoryStruct.comp (symPowIdem A X n) k = k) : symPow A X n ⟶ W

Descend a morphism absorbed by the symmetriser to the symmetric power.

Equations

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

@[simp]

theorem RS.symPowπ_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 : ℕ} {W : D} (k : modPow A X n ⟶ W) (h : CategoryTheory.CategoryStruct.comp (symPowIdem A X n) k = k) : CategoryTheory.CategoryStruct.comp (symPowπ A X n) (symPowDesc A X k h) = k

The descent factors the given morphism through the projection.

@[simp]

theorem RS.symPowπ_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 : ℕ} {W : D} (k : modPow A X n ⟶ W) (h : CategoryTheory.CategoryStruct.comp (symPowIdem A X n) k = k) {Z : D} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (symPowπ A X n) (CategoryTheory.CategoryStruct.comp (symPowDesc A X k h) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The descent factors the given morphism through the projection.