Constant and linear parts of e_k(2 + x_1, …, 2 + x_m)

Over any commutative ring, e_k(2 + a_j t) ≡ C(m,k) 2^k + C(m−1,k−1) 2^{k−1} (∑ a_j) t (mod t²). For a_j = j² the coefficient of t is T_m C(m−1,k−1) 2^{k−1} with 6 T_m = m(m+1)(2m+1). The same in MvPolynomial form, as homogeneous components of degree 0 and 1.

Main results

• Conductor.LinearCoeff.coeff_zero_esymm_shift, Conductor.LinearCoeff.coeff_one_esymm_shift: the polynomial-in-t form.
• Conductor.LinearCoeff.coeff_one_esymm_sq, Conductor.LinearCoeff.six_mul_T: the case a_j = j².
• Conductor.LinearCoeff.homogeneousComponent_zero_esymm_shift, Conductor.LinearCoeff.homogeneousComponent_one_esymm_shift: the MvPolynomial form.

References

• C. Marín, Conductors of orders generated by character values of Sp(2m), preprint (2026); programs and outputs: Zenodo, doi:10.5281/zenodo.23090540.
• C. Marín, Where the character values of Sp(2m) at a torsion element fail to generate the ring of integers, Zenodo (2026), doi:10.5281/zenodo.22813216 (a longer preprint of the same work).

theorem Conductor.LinearCoeff.sum_powersetCard_sum {R : Type u_1} [CommRing R] (m k : ℕ) (hk : 1 ≤ k) (g : Fin m → R) : ∑ s ∈ Finset.powersetCard k Finset.univ, ∑ i ∈ s, g i = ↑((m - 1).choose (k - 1)) * ∑ i : Fin m, g i

Double counting: Σ_{|s|=k} Σ_{i∈s} g i = C(m−1,k−1) · Σ_i g i (1 ≤ k).

noncomputable def Conductor.LinearCoeff.shift {R : Type u_1} [CommRing R] {m : ℕ} (a : Fin m → R) : Fin m → Polynomial R

The family t ↦ 2 + a_j t in R[t].

Equations

• Conductor.LinearCoeff.shift a j = Polynomial.C 2 + Polynomial.C (a j) * Polynomial.X

theorem Conductor.LinearCoeff.aeval_esymm {R : Type u_1} [CommRing R] (m k : ℕ) (f : Fin m → Polynomial R) : (MvPolynomial.aeval f) (MvPolynomial.esymm (Fin m) R k) = ∑ s ∈ Finset.powersetCard k Finset.univ, ∏ i ∈ s, f i

theorem Conductor.LinearCoeff.coeff_zero_esymm_shift {R : Type u_1} [CommRing R] (m k : ℕ) (a : Fin m → R) : ((MvPolynomial.aeval (shift a)) (MvPolynomial.esymm (Fin m) R k)).coeff 0 = ↑(m.choose k) * 2 ^ k

theorem Conductor.LinearCoeff.coeff_one_prod_shift {R : Type u_1} [CommRing R] {m : ℕ} (a : Fin m → R) (s : Finset (Fin m)) : (∏ i ∈ s, shift a i).coeff 1 = 2 ^ (s.card - 1) * ∑ i ∈ s, a i

theorem Conductor.LinearCoeff.coeff_one_esymm_shift {R : Type u_1} [CommRing R] (m k : ℕ) (hk : 1 ≤ k) (a : Fin m → R) : ((MvPolynomial.aeval (shift a)) (MvPolynomial.esymm (Fin m) R k)).coeff 1 = ↑((m - 1).choose (k - 1)) * 2 ^ (k - 1) * ∑ j : Fin m, a j

Specialisation x_j = j² t

def Conductor.LinearCoeff.T (m : ℕ) : ℕ

T_m = Σ_{j=1}^m j².

Equations

• Conductor.LinearCoeff.T m = ∑ j ∈ Finset.range m, (j + 1) ^ 2

theorem Conductor.LinearCoeff.six_mul_T (m : ℕ) : 6 * T m = m * (m + 1) * (2 * m + 1)

theorem Conductor.LinearCoeff.sum_sq_fin {R : Type u_1} [CommRing R] (m : ℕ) : ∑ j : Fin m, ↑(↑j + 1) ^ 2 = ↑(T m)

theorem Conductor.LinearCoeff.coeff_zero_esymm_sq {R : Type u_1} [CommRing R] (m k : ℕ) : ((MvPolynomial.aeval (shift fun (j : Fin m) => ↑(↑j + 1) ^ 2)) (MvPolynomial.esymm (Fin m) R k)).coeff 0 = ↑(m.choose k) * 2 ^ k

theorem Conductor.LinearCoeff.coeff_one_esymm_sq {R : Type u_1} [CommRing R] (m k : ℕ) (hk : 1 ≤ k) : ((MvPolynomial.aeval (shift fun (j : Fin m) => ↑(↑j + 1) ^ 2)) (MvPolynomial.esymm (Fin m) R k)).coeff 1 = ↑(T m) * ↑((m - 1).choose (k - 1)) * 2 ^ (k - 1)

MvPolynomial form: homogeneous components of esymm(2 + X)

theorem Conductor.LinearCoeff.prodX_mem {R : Type u_1} [CommRing R] {m : ℕ} (t : Finset (Fin m)) : ∏ i ∈ t, MvPolynomial.X i ∈ MvPolynomial.homogeneousSubmodule (Fin m) R t.card

theorem Conductor.LinearCoeff.homogeneousComponent_prod_shift {R : Type u_1} [CommRing R] {m : ℕ} (n : ℕ) (s : Finset (Fin m)) : (MvPolynomial.homogeneousComponent n) (∏ i ∈ s, (MvPolynomial.X i + MvPolynomial.C 2)) = ∑ t ∈ Finset.powersetCard n s, MvPolynomial.C (2 ^ (s.card - n)) * ∏ i ∈ t, MvPolynomial.X i

Degree-n component of ∏_{i∈s} (X_i + 2).

theorem Conductor.LinearCoeff.aeval_esymm_mv {R : Type u_1} [CommRing R] (m k : ℕ) : (MvPolynomial.aeval fun (j : Fin m) => MvPolynomial.X j + MvPolynomial.C 2) (MvPolynomial.esymm (Fin m) R k) = ∑ s ∈ Finset.powersetCard k Finset.univ, ∏ i ∈ s, (MvPolynomial.X i + MvPolynomial.C 2)

theorem Conductor.LinearCoeff.homogeneousComponent_zero_esymm_shift {R : Type u_1} [CommRing R] (m k : ℕ) : (MvPolynomial.homogeneousComponent 0) ((MvPolynomial.aeval fun (j : Fin m) => MvPolynomial.X j + MvPolynomial.C 2) (MvPolynomial.esymm (Fin m) R k)) = MvPolynomial.C (↑(m.choose k) * 2 ^ k)

Degree-0 part of e_k(2 + X): C(m,k)·2^k.

theorem Conductor.LinearCoeff.homogeneousComponent_one_esymm_shift {R : Type u_1} [CommRing R] (m k : ℕ) (hk : 1 ≤ k) : (MvPolynomial.homogeneousComponent 1) ((MvPolynomial.aeval fun (j : Fin m) => MvPolynomial.X j + MvPolynomial.C 2) (MvPolynomial.esymm (Fin m) R k)) = MvPolynomial.C (↑((m - 1).choose (k - 1)) * 2 ^ (k - 1)) * ∑ j : Fin m, MvPolynomial.X j

Degree-1 part of e_k(2 + X): C(m−1,k−1)·2^{k−1}·Σ X_j (1 ≤ k).