The symplectic alphabet of a power of the Kostant element

For zeta a primitive t-th root of unity in a field, t = 2m+2, k a natural number, d = gcd(k,t) and q = t/d, the multiset A = {zeta^(jk), zeta^(-jk) : 1 <= j <= m} (counted with multiplicity) equals d times the multiset of q-th roots of unity minus two copies of 1 (d even) or minus {1} and {-1} (d odd). Equality is of multisets with multiplicities. The ambient field is arbitrary (the paper works over C); no characteristic hypothesis is needed. The additive forms A + 2{1} = d.mu_q and A + {1} + {-1} = d.mu_q are also proved. Nothing about Lie theory or characters is formalized.

Main results

• KostantAlphabet.alphabet_eq_even: A = d.mu_q - 2.{1} for d even
• KostantAlphabet.alphabet_eq_odd: A = d.mu_q - {1} - {-1} for d odd
• KostantAlphabet.alphabet_add_even: additive form, d even
• KostantAlphabet.alphabet_add_odd: additive form, d odd

References

• C. Marín, Integer character values on the ρ-line of Sp(2m), Zenodo (2026), doi:10.5281/zenodo.22683561, prop:alph.

def KostantAlphabet.alphabet {F : Type u_1} [Field F] (ζ : F) (m k : ℕ) : Multiset F

The alphabet {ζ^{±jk} : j = 1..m} as a multiset.

Equations

• KostantAlphabet.alphabet ζ m k = Multiset.map (fun (j : ℕ) => ζ ^ ((j + 1) * k)) (Multiset.range m) + Multiset.map (fun (j : ℕ) => (ζ ^ ((j + 1) * k))⁻¹) (Multiset.range m)

theorem KostantAlphabet.map_range_reflect {α : Type u_2} (g : ℕ → α) (n : ℕ) : Multiset.map (fun (i : ℕ) => g (n - 1 - i)) (Multiset.range n) = Multiset.map g (Multiset.range n)

theorem KostantAlphabet.map_range_mul {α : Type u_2} (f : ℕ → α) (q : ℕ) (hf : ∀ (e : ℕ), f (e + q) = f e) (n : ℕ) : Multiset.map f (Multiset.range (q * n)) = n • Multiset.map f (Multiset.range q)

theorem KostantAlphabet.full_period {F : Type u_1} [Field F] {ζ : F} {t : ℕ} (ht : 0 < t) (hζ : IsPrimitiveRoot ζ t) (k : ℕ) : Multiset.map (fun (e : ℕ) => ζ ^ (k * e)) (Multiset.range t) = k.gcd t • Polynomial.nthRoots (t / k.gcd t) 1

theorem KostantAlphabet.decomposition {F : Type u_1} [Field F] {ζ : F} {t m : ℕ} (k : ℕ) (hm : t = 2 * m + 2) (hζ : IsPrimitiveRoot ζ t) : Multiset.map (fun (e : ℕ) => ζ ^ (k * e)) (Multiset.range t) = {1} + {ζ ^ (k * (m + 1))} + alphabet ζ m k

theorem KostantAlphabet.half_value {F : Type u_1} [Field F] {ζ : F} {t m : ℕ} (k : ℕ) (hm : t = 2 * m + 2) (hζ : IsPrimitiveRoot ζ t) : (Even (k.gcd t) → ζ ^ (k * (m + 1)) = 1) ∧ (Odd (k.gcd t) → ζ ^ (k * (m + 1)) = -1)

theorem KostantAlphabet.alphabet_add_even {F : Type u_1} [Field F] {ζ : F} {t m : ℕ} (k : ℕ) (hm : t = 2 * m + 2) (hζ : IsPrimitiveRoot ζ t) (hd : Even (k.gcd t)) : alphabet ζ m k + 2 • {1} = k.gcd t • Polynomial.nthRoots (t / k.gcd t) 1

The alphabet of a_P^k (additive form, d even): A + 2·{1} = d·μ_q.

theorem KostantAlphabet.alphabet_add_odd {F : Type u_1} [Field F] {ζ : F} {t m : ℕ} (k : ℕ) (hm : t = 2 * m + 2) (hζ : IsPrimitiveRoot ζ t) (hd : Odd (k.gcd t)) : alphabet ζ m k + {1} + {-1} = k.gcd t • Polynomial.nthRoots (t / k.gcd t) 1

The alphabet of a_P^k (additive form, d odd): A + {1} + {-1} = d·μ_q.

theorem KostantAlphabet.alphabet_eq_even {F : Type u_1} [Field F] [DecidableEq F] {ζ : F} {t m : ℕ} (k : ℕ) (hm : t = 2 * m + 2) (hζ : IsPrimitiveRoot ζ t) (hd : Even (k.gcd t)) : alphabet ζ m k = k.gcd t • Polynomial.nthRoots (t / k.gcd t) 1 - 2 • {1}

Proposition (alphabet), d even: A = d·μ_q − 2·{1} as multisets.

theorem KostantAlphabet.alphabet_eq_odd {F : Type u_1} [Field F] [DecidableEq F] {ζ : F} {t m : ℕ} (k : ℕ) (hm : t = 2 * m + 2) (hζ : IsPrimitiveRoot ζ t) (hd : Odd (k.gcd t)) : alphabet ζ m k = k.gcd t • Polynomial.nthRoots (t / k.gcd t) 1 - {1} - {-1}

Proposition (alphabet), d odd: A = d·μ_q − {1} − {-1} as multisets.