Three operations on segment polynomials

Let t be a primitive 2q-th root of unity in a field K. A segment polynomial is seg t a n = ∏_{j<n} (X − t^(a − 2j)), a string of n roots with step t⁻²; F t n is the segment of SU(n) (exponents n − 1, n − 3, …, 1 − n) and Gsp t m that of Sp(2m). The subrings A generated by their coefficients satisfy three identities.

Main results

• NotaPuente.A_F_odd_eq_A_Gsp: A_SU(2m+1) = A_Sp(2m).
• NotaPuente.A_F_eq_A_F_sub: A_SU(n) = A_SU(q−n) for n ≤ q.
• NotaPuente.A_F_add_q: A_SU(n+q) = A_SU(n).
• NotaPuente.A_neg, NotaPuente.A_comp_neg_X: A is invariant under p ↦ −p and p ↦ p(−X).

References

• C. Marín, Non-real orders of character values of GL(n), preprint (2026).
• C. Marín, The ring of character values depends only on the segment: SU(n), Sp(2m) and GL(n) at a torsion element, Zenodo (2026), doi:10.5281/zenodo.22847476.

New general facts about A: invariance under p ↦ -p and p ↦ p(-X).

theorem NotaPuente.A_neg {R : Type u_1} [CommRing R] (p : Polynomial R) : A (-p) = A p

theorem NotaPuente.A_neg_one_pow_mul {R : Type u_1} [CommRing R] (k : ℕ) (p : Polynomial R) : A ((-1) ^ k * p) = A p

theorem NotaPuente.A_comp_neg_X_le {R : Type u_1} [CommRing R] (p : Polynomial R) : A (p.comp (-Polynomial.X)) ≤ A p

theorem NotaPuente.A_comp_neg_X {R : Type u_1} [CommRing R] (p : Polynomial R) : A (p.comp (-Polynomial.X)) = A p

theorem NotaPuente.A_neg_one_pow_mul_comp {R : Type u_1} [CommRing R] (k : ℕ) (p : Polynomial R) : A ((-1) ^ k * p.comp (-Polynomial.X)) = A p

noncomputable def NotaPuente.seg {K : Type u_1} [Field K] (t : K) (a : ℤ) (n : ℕ) : Polynomial K

String of n roots t^a, t^(a-2), …, t^(a-2(n-1)).

Equations

• NotaPuente.seg t a n = ∏ j ∈ Finset.range n, (Polynomial.X - Polynomial.C (t ^ (a - 2 * ↑j)))

noncomputable def NotaPuente.F {K : Type u_1} [Field K] (t : K) (n : ℕ) : Polynomial K

Segment polynomial of SU(n).

Equations

• NotaPuente.F t n = NotaPuente.seg t (↑n - 1) n

noncomputable def NotaPuente.Gsp {K : Type u_1} [Field K] (t : K) (m : ℕ) : Polynomial K

Segment polynomial of Sp(2m).

Equations

• NotaPuente.Gsp t m = ∏ j ∈ Finset.range m, (Polynomial.X - Polynomial.C (t ^ (2 * (↑j + 1)))) * (Polynomial.X - Polynomial.C (t ^ (-(2 * (↑j + 1)))))

theorem NotaPuente.seg_monic {K : Type u_1} [Field K] (t : K) (a : ℤ) (n : ℕ) : (seg t a n).Monic

theorem NotaPuente.seg_add {K : Type u_1} [Field K] (t : K) (a : ℤ) (n k : ℕ) : seg t a (n + k) = seg t a n * seg t (a - 2 * ↑n) k

theorem NotaPuente.seg_zero {K : Type u_1} [Field K] (t : K) (a : ℤ) : seg t a 0 = 1

theorem NotaPuente.seg_one {K : Type u_1} [Field K] (t : K) (a : ℤ) : seg t a 1 = Polynomial.X - Polynomial.C (t ^ a)

theorem NotaPuente.pow_q_eq_neg_one {K : Type u_1} [Field K] {t : K} {q : ℕ} (hq : 0 < q) (ht : IsPrimitiveRoot t (2 * q)) : t ^ q = -1

theorem NotaPuente.t_ne_zero {K : Type u_1} [Field K] {t : K} {q : ℕ} (hq : 0 < q) (ht : IsPrimitiveRoot t (2 * q)) : t ≠ 0

theorem NotaPuente.seg_sub_q {K : Type u_1} [Field K] {t : K} {q : ℕ} (hq : 0 < q) (ht : IsPrimitiveRoot t (2 * q)) (a : ℤ) (n : ℕ) : seg t (a - ↑q) n = (-1) ^ n * (seg t a n).comp (-Polynomial.X)

Translation by q: shifting every exponent by -q multiplies each root by t^(-q) = -1.

theorem NotaPuente.seg_q_int {K : Type u_1} [Field K] {t : K} {q : ℕ} (hq : 0 < q) (ht : IsPrimitiveRoot t (2 * q)) (a : ℤ) : ∃ (H : Polynomial ℤ), H.Monic ∧ seg t a q = Polynomial.map (Int.castRingHom K) H

A full parity class: q consecutive roots of the string give X^q - c, c = (t^a)^q = ±1; hence it is the image of a monic integer polynomial.

Proposition 2.2

theorem NotaPuente.F_odd_eq {K : Type u_1} [Field K] (t : K) (m : ℕ) : F t (2 * m + 1) = Gsp t m * (Polynomial.X - Polynomial.C 1)

Factorisation behind (a): F (2m+1) = Gsp m * (X - 1).

theorem NotaPuente.A_F_odd_eq_A_Gsp {K : Type u_1} [Field K] (t : K) (m : ℕ) : A (F t (2 * m + 1)) = A (Gsp t m)

Prop. 2.2(a): A_SU(2m+1) = A_Sp(2m) (no hypothesis on t needed).

theorem NotaPuente.A_F_eq_A_F_sub {K : Type u_1} [Field K] {t : K} {q : ℕ} (hq : 0 < q) (ht : IsPrimitiveRoot t (2 * q)) {n : ℕ} (hn : n ≤ q) : A (F t n) = A (F t (q - n))

Prop. 2.2(b): A_SU(n) = A_SU(q-n) for n ≤ q (the paper states 1 ≤ n < q).

theorem NotaPuente.A_F_add_q {K : Type u_1} [Field K] {t : K} {q : ℕ} (hq : 0 < q) (ht : IsPrimitiveRoot t (2 * q)) (n : ℕ) : A (F t (n + q)) = A (F t n)

Prop. 2.2(c): A_SU(n+q) = A_SU(n).