Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.CharSplit

Character splitting of the completed cycle product #

The completed cycle product cycleFun is multiplicative in the scalar sequence and expands over the Jacobi–Trudi characters with Schur coefficients — the inverse Frobenius formula. Pairing the expansion against a third character produces the Kronecker multiplicities, which are nonnegative integers by the equivariant Hom-space count, and yields the splitting of the Schur specialisation at a pointwise product of scalar sequences over pairs of shapes.

The completed cycle product #

source
noncomputable def RS.cycleFun {n : ℕ} (t : ℕ → ℂ) (π : Equiv.Perm (Fin n)) :
ℂ

The completed cycle product of a prospective power-sum sequence: the product of t over the cycle type, completed by t 1 over the fixed points.

Equations
Instances For
    source
    theorem RS.cycleFun_eq_cycleProd {n : ℕ} (t : ℕ → ℂ) (π : Equiv.Perm (Fin n)) :
    cycleFun t π = cycleProd t π

    cycleFun is the completed cycle-type product of the orbit-factorization development.

    source
    theorem RS.cycleFun_mul {n : ℕ} (t t' : ℕ → ℂ) (π : Equiv.Perm (Fin n)) :
    cycleFun (fun (c : ℕ) => t c * t' c) π = cycleFun t π * cycleFun t' π

    Multiplicativity of the completed cycle product in the scalar sequence.

    source
    theorem RS.cycleFun_conj {n : ℕ} (t : ℕ → ℂ) (σ π : Equiv.Perm (Fin n)) :
    cycleFun t (σ * π * σ⁻¹) = cycleFun t π

    The completed cycle product is a class function.

    source
    theorem RS.cycleFun_permCast {m n : ℕ} (h : m = n) (t : ℕ → ℂ) (π : Equiv.Perm (Fin m)) :
    cycleFun t ((permCast h) π) = cycleFun t π

    The completed cycle product is invariant under relabelling along an equality of sizes.

    Shape-level Frobenius and orthonormality #

    The Frobenius formula and the orthonormality of the Jacobi–Trudi characters, reindexed along permCast to the group S_n shared by all shapes of size n.

    source
    theorem RS.jtChar_shape_frobenius {n : ℕ} (μ : Shape n) (t : ℕ → ℂ) :
    (↑n.factorial)⁻¹ * ∑ π : Equiv.Perm (Fin n), jtChar (↑μ) ((permCast ⋯) π) * cycleFun t π = diagramSchur (↑μ) t

    The Frobenius formula at a shape: the normalized pairing of the recast Jacobi–Trudi character with the completed cycle product is the Schur specialisation.

    source
    theorem RS.jtChar_shape_orthonormal {n : ℕ} (μ : Shape n) :
    (↑n.factorial)⁻¹ * ∑ π : Equiv.Perm (Fin n), jtChar (↑μ) ((permCast ⋯) π) * jtChar (↑μ) ((permCast ⋯) π) = 1

    Orthonormality at a shape: the recast Jacobi–Trudi character has unit norm for the class pairing of S_n.

    Cross-shape orthogonality #

    Distinct shapes of one size have orthogonal recast characters: a common irreducible constituent would force the two Schur specialisations to agree, contradicting the separation theorem.

    source
    theorem RS.jtChar_orthogonal {n : ℕ} (μ ν : Shape n) (hne : μ ≠ ν) :
    (↑n.factorial)⁻¹ * ∑ π : Equiv.Perm (Fin n), jtChar (↑μ) ((permCast ⋯) π) * jtChar (↑ν) ((permCast ⋯) π) = 0

    Orthogonality of the recast characters: the class pairing of the Jacobi–Trudi characters of distinct shapes of size n vanishes.

    The character expansion of the completed cycle product #

    The recast idempotents of a Schur package span the class elements of ℂ[S_n]; expanding the class element of the completed cycle product over them and pairing against each character determines the coefficients as Schur specialisations — the inverse Frobenius formula.

    source
    theorem RS.shape_e_coeff (P : SchurPackage) {n : ℕ} (μ : Shape n) (π : Equiv.Perm (Fin n)) :
    (Shape.e P μ).coeff π = ↑(P.dim ↑μ) / ↑n.factorial * jtChar (↑μ) ((permCast ⋯) π)

    The coefficients of a recast idempotent: the normalized recast Jacobi–Trudi character.

    source
    theorem RS.classElem_eq_sum_shape_e (P : SchurPackage) {n : ℕ} (c : Equiv.Perm (Fin n) → ℂ) (hc : ∀ (g k : Equiv.Perm (Fin n)), c (k * g * k⁻¹) = c g) :
    ∃ (a : Shape n → ℂ), classElem c = ∑ μ : Shape n, a μ • Shape.e P μ

    The recast idempotents span the class elements: every conjugation-invariant coefficient function's class element is a linear combination of the Shape.e P μ.

    source
    theorem RS.cycleFun_expand {n : ℕ} (t : ℕ → ℂ) (π : Equiv.Perm (Fin n)) :
    cycleFun t π = ∑ μ : Shape n, diagramSchur (↑μ) t * jtChar (↑μ) ((permCast ⋯) π)

    The character expansion of the completed cycle product — the inverse Frobenius formula: the completed cycle product expands over the recast Jacobi–Trudi characters with the Schur specialisations as coefficients.

    Kronecker multiplicities #

    The triple class pairing of three recast characters counts, by the equivariant Hom-space dimension against a tensor product of pullback representations, a nonnegative integer.

    source
    noncomputable def RS.kronMult {n : ℕ} (lam μ ν : Shape n) :
    ℂ

    The Kronecker multiplicity of three shapes of one size: the normalized triple class pairing of their recast Jacobi–Trudi characters.

    Equations
    Instances For
      source
      theorem RS.kronMult_exists_nat {n : ℕ} (lam μ ν : Shape n) :
      ∃ (m : ℕ), kronMult lam μ ν = ↑m

      Kronecker multiplicities are nonnegative integers: the triple pairing is the dimension of an equivariant Hom space.

      The Kronecker splitting identity #

      The Schur specialisation at a pointwise product of scalar sequences splits over pairs of shapes with Kronecker multiplicities: Frobenius at the product, multiplicativity of the completed cycle product, and the character expansion of each factor.

      source
      theorem RS.diagramSchur_pointwise_mul (lam : YoungDiagram) (t t' : ℕ → ℂ) :
      (diagramSchur lam fun (c : ℕ) => t c * t' c) = ∑ μ : Shape lam.card, ∑ ν : Shape lam.card, kronMult ⟨lam, ⋯⟩ μ ν * diagramSchur (↑μ) t * diagramSchur (↑ν) t'

      The Kronecker splitting identity: the Schur specialisation at a pointwise product of scalar sequences is the Kronecker-weighted sum of products of Schur specialisations.