Alternating powers over an internal monoid

The antisymmetric counterpart of the symmetric-power interface of SymAlg.lean: the sign-character central idempotent of the group algebra ℂ[Sₙ] — the antisymmetriser — and the alternating power of a module over an internal monoid, presented as the coequalizer of the antisymmetriser's action on the module power against the identity.

• antisymmetriser n: the sign-character central idempotent (1/n!) • ∑ σ, sign σ • σ of the group algebra, with signed absorption and idempotency.
• altPow A X n: the alternating power, presented as the coequalizer of modPowAlg (antisymmetriser n) against the identity — which the idempotent splits into a direct summand: altPowσ ≫ altPowπ = 𝟙 and altPowπ ≫ altPowσ is the antisymmetriser's action. Morphisms out of the alternating power descend along altPowπ; morphisms in arrive through the section altPowσ.

The A-module structure on the alternating power is outside this module's scope, exactly as its symmetric counterpart lives in PowAct.lean rather than in SymAlg.lean.

The antisymmetriser

The sign-character central idempotent of the group algebra ℂ[Sₙ] — the charIdempotent 1 sign of the Schur interface, written directly.

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

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

Equations

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

theorem RS.sign_coe_mul_self {n : ℕ} (σ : Equiv.Perm (Fin n)) : ↑↑(Equiv.Perm.sign σ) * ↑↑(Equiv.Perm.sign σ) = 1

The square of a sign, cast to ℂ, is one.

@[simp]

theorem RS.antisymmetriser_mul_single (n : ℕ) (τ : Equiv.Perm (Fin n)) : antisymmetriser n * MonoidAlgebra.single τ 1 = ↑↑(Equiv.Perm.sign τ) • antisymmetriser n

The antisymmetriser absorbs every group element on the right, up to its sign.

@[simp]

theorem RS.single_mul_antisymmetriser (n : ℕ) (τ : Equiv.Perm (Fin n)) : MonoidAlgebra.single τ 1 * antisymmetriser n = ↑↑(Equiv.Perm.sign τ) • antisymmetriser n

The antisymmetriser absorbs every group element on the left, up to its sign.

theorem RS.antisymmetriser_mul_sign_single (n : ℕ) (τ : Equiv.Perm (Fin n)) : antisymmetriser n * MonoidAlgebra.single τ ↑↑(Equiv.Perm.sign τ) = antisymmetriser n

The antisymmetriser absorbs a sign-weighted group element on the right, exactly.

theorem RS.antisymmetriser_idem (n : ℕ) : antisymmetriser n * antisymmetriser n = antisymmetriser n

The antisymmetriser is idempotent.

The alternating power

noncomputable def RS.altPowIdem {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 antisymmetriser acting on the module power.

Equations

• RS.altPowIdem A X n = (RS.modPowAlg A X n) (RS.antisymmetriser n)

theorem RS.altPowIdem_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 (altPowIdem A X n) (altPowIdem A X n) = altPowIdem A X n

The antisymmetriser's action is idempotent.

noncomputable def RS.altPow {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 alternating power: the coinvariants of the antisymmetriser'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 altPowσ; this presentation is chosen because consumers build morphisms out of the alternating power by descent along altPowπ and morphisms into it through the section.

Equations

• RS.altPow A X n = CategoryTheory.Limits.coequalizer (RS.altPowIdem A X n) (CategoryTheory.CategoryStruct.id (RS.modPow A X n))

noncomputable def RS.altPowπ {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 ⟶ altPow A X n

The projection onto the alternating power.

Equations

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

instance RS.instEpiAltPowπ {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 (altPowπ A X n)

@[simp]

theorem RS.altPowIdem_π {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 (altPowIdem A X n) (altPowπ A X n) = altPowπ A X n

The antisymmetriser is absorbed by the projection.

@[simp]

theorem RS.altPowIdem_π_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 : altPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (altPowIdem A X n) (CategoryTheory.CategoryStruct.comp (altPowπ A X n) h) = CategoryTheory.CategoryStruct.comp (altPowπ A X n) h

The antisymmetriser is absorbed by the projection.

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

The section of the alternating power, from idempotency.

Equations

• RS.altPowσ A X n = CategoryTheory.Limits.coequalizer.desc (RS.altPowIdem A X n) ⋯

@[simp]

theorem RS.altPowπ_altPowσ {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 (altPowπ A X n) (altPowσ A X n) = altPowIdem A X n

The section realises the antisymmetriser as projection followed by inclusion.

@[simp]

theorem RS.altPowπ_altPowσ_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 (altPowπ A X n) (CategoryTheory.CategoryStruct.comp (altPowσ A X n) h) = CategoryTheory.CategoryStruct.comp (altPowIdem A X n) h

The section realises the antisymmetriser as projection followed by inclusion.

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

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

@[simp]

theorem RS.altPowσ_altPowπ {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 (altPowσ A X n) (altPowπ A X n) = CategoryTheory.CategoryStruct.id (altPow A X n)

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

@[simp]

theorem RS.altPowσ_altPowπ_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 : altPow A X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (altPowσ A X n) (CategoryTheory.CategoryStruct.comp (altPowπ A X n) h) = h

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

noncomputable def RS.altPowDesc {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 (altPowIdem A X n) k = k) : altPow A X n ⟶ W

Descend a morphism absorbed by the antisymmetriser to the alternating power.

Equations

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

@[simp]

theorem RS.altPowπ_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 (altPowIdem A X n) k = k) : CategoryTheory.CategoryStruct.comp (altPowπ A X n) (altPowDesc A X k h) = k

The descent factors the given morphism through the projection.

@[simp]

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

The descent factors the given morphism through the projection.