Documentation

TauCeti.GroupTheory.Coxeter.Geometric.RankTwo

Positive rank-two geometric roots #

The image of a simple root under an alternating word has two explicit coefficients. Writing m = M i j, these are consecutive terms of the sequence S(n) = sin(n π / m) / sin(π / m) when m ≥ 2, and S(n) = n when m = 0 (an infinite Coxeter entry). Both coefficients are nonnegative before the braid length. This is the rank-two input to the sign/length theorem for the geometric representation; no finiteness or nondegeneracy is assumed.

We use Mathlib's Chebyshev polynomials Polynomial.Chebyshev.U to define the coefficients uniformly, including infinite entries, and consume their recurrence and trigonometric evaluation. The native CoxeterSystem.alternatingWord i j k ends in j: its image of the root at i has coefficients (S(k+1), S(k)) for even k, and (S(k), S(k+1)) for odd k.

Main results #

References #

source
noncomputable def CoxeterMatrix.dihedralCoeff {I : Type u_1} (M : CoxeterMatrix I) (i j : I) (n : ℕ) :
ℝ

The rank-two geometric coefficient S(n), defined by evaluating the Chebyshev polynomial U_(n-1) at cos(π / M i j). At an infinite entry it is n.

Instances For
    source
    theorem CoxeterMatrix.dihedralCoeff_comm {I : Type u_1} (M : CoxeterMatrix I) (i j : I) :
    M.dihedralCoeff j i = M.dihedralCoeff i j

    The rank-two coefficient sequence is symmetric in its two indices.

    source
    @[simp]
    theorem CoxeterMatrix.dihedralCoeff_zero {I : Type u_1} (M : CoxeterMatrix I) (i j : I) :
    M.dihedralCoeff i j 0 = 0
    source
    @[simp]
    theorem CoxeterMatrix.dihedralCoeff_one {I : Type u_1} (M : CoxeterMatrix I) (i j : I) :
    M.dihedralCoeff i j 1 = 1
    source
    theorem CoxeterMatrix.dihedralCoeff_add_two {I : Type u_1} (M : CoxeterMatrix I) (i j : I) (n : ℕ) :
    M.dihedralCoeff i j (n + 2) = 2 * Real.cos (Real.pi / ↑(M.M i j)) * M.dihedralCoeff i j (n + 1) - M.dihedralCoeff i j n

    The recurrence governing the two coefficients of successive alternating roots.

    source
    theorem CoxeterMatrix.dihedralCoeff_of_eq_zero {I : Type u_1} (M : CoxeterMatrix I) {i j : I} (hm : M.M i j = 0) (n : ℕ) :
    M.dihedralCoeff i j n = ↑n

    At an infinite Coxeter entry, the rank-two coefficients grow linearly.

    source
    theorem CoxeterMatrix.dihedralCoeff_eq_sin_div {I : Type u_1} (M : CoxeterMatrix I) {i j : I} (hm : 2 ≤ M.M i j) (n : ℕ) :
    M.dihedralCoeff i j n = Real.sin (↑n * (Real.pi / ↑(M.M i j))) / Real.sin (Real.pi / ↑(M.M i j))

    For a finite off-diagonal Coxeter entry the coefficients are sine quotients.

    source
    theorem CoxeterMatrix.dihedralCoeff_nonneg {I : Type u_1} (M : CoxeterMatrix I) (i j : I) {n : ℕ} (hn : n ≤ M.M i j ∨ M.M i j = 0) :
    0 ≤ M.dihedralCoeff i j n

    The coefficient is nonnegative up to and including the finite braid length, or at every index for an infinite entry.

    source
    theorem CoxeterSystem.geometricRepresentation_alternatingWord {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) (i j : I) (k : ℕ) :
    (cs.geometricRepresentation (cs.wordProd (alternatingWord i j k))) (Finsupp.single i 1) = if Even k then M.dihedralCoeff i j (k + 1) • Finsupp.single i 1 + M.dihedralCoeff i j k • Finsupp.single j 1 else M.dihedralCoeff i j k • Finsupp.single i 1 + M.dihedralCoeff i j (k + 1) • Finsupp.single j 1

    The exact image of a simple root under the native alternating word ending in the other index. The consecutive Chebyshev coefficients exchange places at each step.

    source
    theorem CoxeterSystem.rankTwo_nonnegative {I : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix I} (cs : CoxeterSystem M W) (i j : I) {k : ℕ} (hk : k < M.M i j ∨ M.M i j = 0) :
    ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ (cs.geometricRepresentation (cs.wordProd (alternatingWord i j k))) (Finsupp.single i 1) = a • Finsupp.single i 1 + b • Finsupp.single j 1

    Before the finite braid length, or at any length for an infinite entry, the alternating word sends the first simple root to a nonnegative combination of the two simple roots. The strict bound is necessary at finite entries.