Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.RowColIdem

The one-row and one-column idempotents #

The central idempotent of the single-row shape of size n is the symmetriser of ℂ[S_n], and that of the single-column shape is the antisymmetriser: Shape.e P (rowShape n) = symmetriser n and Shape.e P (colShape n) = antisymmetriser n.

The route runs through the Frobenius field of the package. The Schur specialisation of the single-row shape is the complete homogeneous value newtonH t n (a one-by-one Jacobi–Trudi determinant), and that of the single-column shape is the elementary value (-1)^n · newtonH (-t) n (an n × n determinant, evaluated by clearing with the unitriangular matrix of newtonHZ (-t) through the convolution identity of NewtonConv.lean). The cycle-sum identity of SchurTheory/CycleSum.lean expresses the same two specialisations as the Frobenius pairings of the constant and the sign character, so the determination theorem of RegularSum.lean pins the package's characters on these shapes; idempotency then forces dimension one, and the idempotents coincide with the symmetriser and antisymmetriser on the nose.

Complete homogeneous values: the zero and alternating #

sequences

source
theorem RS.newtonH_zero_fun (m : ℕ) :
newtonH (fun (x : ℕ) => 0) (m + 1) = 0

The complete homogeneous values of the zero sequence vanish in positive degree.

source
theorem RS.newtonH_alt (t : ℕ → ℂ) (m : ℕ) :
newtonH (fun (c : ℕ) => (-1) ^ (c + 1) * t c) m = (-1) ^ m * newtonH (fun (c : ℕ) => -t c) m

The complete homogeneous values of the alternating twist of a sequence are, up to sign, those of its negation.

The row lengths of the one-row and one-column shapes #

source
theorem RS.rowShape_rowLens_zero :
(↑(rowShape 0)).rowLens = []

The single-row shape of size zero has no rows.

source
theorem RS.rowShape_rowLens_pos {n : ℕ} (hn : 0 < n) :
(↑(rowShape n)).rowLens = [n]

The single-row shape of positive size has row-length list [n].

source
theorem RS.diagramSchur_rowShape (n : ℕ) (t : ℕ → ℂ) :
diagramSchur (↑(rowShape n)) t = newtonH t n

The Schur specialisation of the single-row shape is the complete homogeneous value.

source
theorem RS.colShape_colLen_zero (n : ℕ) :
(↑(colShape n)).colLen 0 = n

The first column of the single-column shape has length n.

source
theorem RS.colShape_rowLens (n : ℕ) :
(↑(colShape n)).rowLens = List.replicate n 1

The single-column shape has row-length list [1, …, 1].

The single-column Jacobi–Trudi determinant #

source
noncomputable def RS.colJTMat (t : ℕ → ℂ) (n : ℕ) :
Matrix (Fin n) (Fin n) ℂ

The Jacobi–Trudi matrix of the single-column shape of size n.

Equations
Instances For
    source
    theorem RS.schurDet_replicate_one (t : ℕ → ℂ) (n : ℕ) :
    schurDet t (List.replicate n 1) = (colJTMat t n).det

    The Schur specialisation of the single-column shape is the determinant of colJTMat.

    source
    noncomputable def RS.negHMat (t : ℕ → ℂ) (n : ℕ) :
    Matrix (Fin n) (Fin n) ℂ

    The unitriangular convolution matrix of the negated sequence.

    Equations
    Instances For
      source
      theorem RS.negHMat_det (t : ℕ → ℂ) (n : ℕ) :
      (negHMat t n).det = 1

      The convolution matrix is unitriangular: determinant one.

      source
      theorem RS.colJT_mul_negH_pos (t : ℕ → ℂ) {n : ℕ} (i k : Fin n) (hi : 0 < ↑i) :
      (colJTMat t n * negHMat t n) i k = if ↑k + 1 = ↑i then 1 else 0

      The positive-index rows of the cleared Jacobi–Trudi matrix form a shifted identity.

      source
      theorem RS.colJT_mul_negH_zero (t : ℕ → ℂ) {n : ℕ} (i k : Fin n) (hi : ↑i = 0) :
      (colJTMat t n * negHMat t n) i k = -newtonH (fun (c : ℕ) => -t c) (↑k + 1)

      The top row of the cleared Jacobi–Trudi matrix carries the negated elementary values.

      source
      theorem RS.colJTMat_det (t : ℕ → ℂ) (n : ℕ) :
      (colJTMat t n).det = (-1) ^ n * newtonH (fun (c : ℕ) => -t c) n

      The single-column determinant: the Jacobi–Trudi determinant of the one-column shape is the elementary value (-1)^n · newtonH (-t) n.

      source
      theorem RS.diagramSchur_colShape (n : ℕ) (t : ℕ → ℂ) :
      diagramSchur (↑(colShape n)) t = (-1) ^ n * newtonH (fun (c : ℕ) => -t c) n

      The Schur specialisation of the single-column shape is the elementary value.

      The signed cycle sum #

      source
      theorem RS.sign_mul_cycleProd (t : ℕ → ℂ) {n : ℕ} (π : Equiv.Perm (Fin n)) :
      ↑↑(Equiv.Perm.sign π) * cycleProd t π = cycleProd (fun (c : ℕ) => (-1) ^ (c + 1) * t c) π

      The sign of a permutation times its completed cycle product is the completed cycle product of the alternating twist.

      source
      theorem RS.signed_cycleSum (t : ℕ → ℂ) (n : ℕ) :
      ∑ π : Equiv.Perm (Fin n), ↑↑(Equiv.Perm.sign π) * cycleProd t π = ↑n.factorial * ((-1) ^ n * newtonH (fun (c : ℕ) => -t c) n)

      The signed cycle sum: the sign-weighted completed cycle products of all permutations sum to n! times the elementary value.

      Pinning the characters of the one-row and one-column #

      shapes

      source
      theorem RS.SchurPackage.char_eq_of_frobenius (P : SchurPackage) (μ : YoungDiagram) (χ : Equiv.Perm (Fin μ.card) → ℂ) (hconj : ∀ (g c : Equiv.Perm (Fin μ.card)), χ (c * g * c⁻¹) = χ g) (hsum : ∀ (t : ℕ → ℂ), ∑ π : Equiv.Perm (Fin μ.card), χ π * cycleProd t π = ↑μ.card.factorial * diagramSchur μ t) (π : Equiv.Perm (Fin μ.card)) :
      P.char μ π = χ π

      A package character agreeing with a class function in all Frobenius pairings is that class function.

      source
      theorem RS.SchurPackage.char_rowShape (P : SchurPackage) (n : ℕ) (π : Equiv.Perm (Fin (↑(rowShape n)).card)) :
      P.char (↑(rowShape n)) π = 1

      The character of the single-row shape is constant one.

      source
      theorem RS.SchurPackage.char_colShape (P : SchurPackage) (n : ℕ) (π : Equiv.Perm (Fin (↑(colShape n)).card)) :
      P.char (↑(colShape n)) π = ↑↑(Equiv.Perm.sign π)

      The character of the single-column shape is the sign.

      The idempotents #

      source
      theorem RS.SchurPackage.dim_rowShape (P : SchurPackage) (n : ℕ) :
      P.dim ↑(rowShape n) = 1

      The single-row dimension is one.

      source
      theorem RS.SchurPackage.dim_colShape (P : SchurPackage) (n : ℕ) :
      P.dim ↑(colShape n) = 1

      The single-column dimension is one.

      source
      theorem RS.charIdempotent_const_one (n : ℕ) :
      (charIdempotent 1 fun (x : Equiv.Perm (Fin n)) => 1) = symmetriser n

      charIdempotent at dimension one and the constant character: the symmetriser.

      source
      theorem RS.charIdempotent_sign (n : ℕ) :
      (charIdempotent 1 fun (π : Equiv.Perm (Fin n)) => ↑↑(Equiv.Perm.sign π)) = antisymmetriser n

      charIdempotent at dimension one and the sign character: the antisymmetriser.

      source
      theorem RS.SchurPackage.e_rowShape (P : SchurPackage) (n : ℕ) :
      P.e ↑(rowShape n) = symmetriser (↑(rowShape n)).card

      The package idempotent of the single-row shape is the symmetriser, at the native size.

      source
      theorem RS.SchurPackage.e_colShape (P : SchurPackage) (n : ℕ) :
      P.e ↑(colShape n) = antisymmetriser (↑(colShape n)).card

      The package idempotent of the single-column shape is the antisymmetriser, at the native size.

      source
      theorem RS.symCast_symmetriser {m n : ℕ} (h : m = n) :
      (symCast ⋯) (symmetriser m) = symmetriser n

      Recasting the symmetriser along an equality of sizes.

      source
      theorem RS.symCast_antisymmetriser {m n : ℕ} (h : m = n) :
      (symCast ⋯) (antisymmetriser m) = antisymmetriser n

      Recasting the antisymmetriser along an equality of sizes.