Deep power-sum congruences

DefinitionDivided-power ideal#✓fully proved

An ideal \(I\) of a commutative ring \(A\) is a divided-power ideal when for every \(a \in I\) and every integer \(k \ge 1\) there is \(c \in I\) with \(a^k = k! \, c\), that is, \(a^k \in k! \, I\). For a prime \(p\), in a torsion-free \(\mathbb{Z}_{(p)}\)-algebra this says \(a^k / k! \in I\).

def IsDividedPowerIdeal {A : Type*} [CommRing A] (I : Ideal A) : Prop :=
  ∀ a ∈ I, ∀ k : ℕ, 1 ≤ k → ∃ c ∈ I, a ^ k = (k.factorial : A) * c

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 2.2.

Used by 12

Used byIdeals with divided powers are divided-power ideals · The zero ideal is a divided-power ideal · The \(p\)-th power criterion for divided-power ideals · When the maximal ideal of a DVR is a divided-power ideal · Powers of the maximal ideal of a DVR that are divided-power ideals · Divided-power ideals generated by a set · \((p)\) is a divided-power ideal of \(\mathbb{Z}_p\) · Product of a divided-power ideal with an ideal · Congruence of products over a partition with multiplicities divisible by \(p^v\) · Power-sum congruences imply elementary symmetric congruences · Congruent elementary symmetric functions give deep power-sum congruences · Powers of elements congruent modulo a divided-power ideal

TheoremThe zero ideal is a divided-power ideal#✓fully proved

In every commutative ring, the zero ideal is a divided-power ideal.

theorem isDividedPowerIdeal_bot {A : Type*} [CommRing A] : IsDividedPowerIdeal (⊥ : Ideal A)

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 2.2 (the definition).

Uses 1

Statement usesDivided-power ideal

TheoremIdeals with divided powers are divided-power ideals#✓fully proved

Let \(I\) be an ideal of a commutative ring \(A\). If \(I\) carries a divided-power structure \((\gamma_k)_{k \ge 0}\) in the usual sense, then \(I\) is a divided-power ideal: for every \(a \in I\) and every \(k \ge 1\) there is \(c \in I\) with \(a^k = k!\, c\).

theorem DividedPowers.isDividedPowerIdeal {A : Type*} [CommRing A] {I : Ideal A}
    (hI : DividedPowers I) : IsDividedPowerIdeal I

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 2.2 (the maps γ_k(a) = a ^ k / k!).

Uses 1

Statement usesDivided-power ideal

DefinitionElementary symmetric functions of a polynomial#✓fully proved

Let \(P\) be a polynomial of degree \(d\) over a commutative ring, with \(d = 0\) for \(P = 0\). For a natural number \(n\), \(e_n(P)\) is \((-1)^n\) times the coefficient of \(X^{d - n}\) in \(P\) if \(n \le d\), and \(0\) if \(n > d\). In particular \(e_0(P) = 1\) when \(P\) is monic.

noncomputable def polyElemSymm {A : Type*} [CommRing A] (P : A[X]) (n : ℕ) : A :=
  if n ≤ P.natDegree then (-1) ^ n * P.coeff (P.natDegree - n) else 0

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 3.2, Notation.

Used by 7

Used byElementary symmetric functions vanish above the degree · Power-sum congruences imply elementary symmetric congruences · The zeroth elementary symmetric function of a monic polynomial · Power sums of a polynomial · The first power sum is the first elementary symmetric function · Congruent elementary symmetric functions give deep power-sum congruences · Newton's recurrence for the power sums of a polynomial

TheoremThe zeroth elementary symmetric function of a monic polynomial#✓fully proved

For every monic polynomial \(P\) over a commutative ring, \(e_0(P) = 1\).

theorem polyElemSymm_zero {A : Type*} [CommRing A] {P : A[X]} (hP : P.Monic) :
    polyElemSymm P 0 = 1

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 3.2, Notation.

Uses 1

Statement usesElementary symmetric functions of a polynomial

TheoremElementary symmetric functions vanish above the degree#✓fully proved

Let \(P\) be a polynomial of degree \(d\) over a commutative ring, with \(d = 0\) for \(P = 0\). Then \(e_n(P) = 0\) for every \(n > d\).

theorem polyElemSymm_of_natDegree_lt {A : Type*} [CommRing A] {P : A[X]} {n : ℕ}
    (h : P.natDegree < n) : polyElemSymm P n = 0

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 3.2, Notation.

Uses 1

Statement usesElementary symmetric functions of a polynomial

DefinitionPower sums of a polynomial#✓fully proved

For a polynomial \(P\) over a commutative ring \(A\), with elementary symmetric functions \(e_i = e_i(P)\), the power sums \(p_n = p_n(P) \in A\) are defined recursively: \(p_0\) is the degree of \(P\) as a natural number (\(0\) for \(P = 0\)), and for \(n \ge 1\) Newton's identity holds:

\[p_n = \sum_{i=1}^{n-1} (-1)^{i-1} e_i\, p_{n-i} + (-1)^{n-1} n\, e_n.\]

If \(P\) is monic and \(P = (X - \alpha_1) \cdots (X - \alpha_d)\), then \(p_n = \alpha_1^n + \cdots + \alpha_d^n\) for every \(n\).

noncomputable def polyPowerSum {A : Type*} [CommRing A] (P : A[X]) : ℕ → A
  | 0 => P.natDegree
  | n + 1 => (-1) ^ n * ((n + 1 : ℕ) : A) * polyElemSymm P (n + 1) +
      ∑ i : Fin n, (-1) ^ (i : ℕ) * polyElemSymm P (i + 1) * polyPowerSum P (n - i)
  decreasing_by omega

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Sections 2.1 and 3.2 (Newton's identities, Macdonald I.2.11').

Uses 1 · Used by 5

Statement usesElementary symmetric functions of a polynomial

Used byPower-sum congruences imply elementary symmetric congruences · The first power sum is the first elementary symmetric function · Congruent elementary symmetric functions give deep power-sum congruences · Newton's recurrence for the power sums of a polynomial · The zeroth power sum of a polynomial is its degree

TheoremThe zeroth power sum of a polynomial is its degree#✓fully proved

For every polynomial \(P\) over a commutative ring \(A\), the power sum \(p_0(P)\) equals the degree of \(P\) as a natural number (taken to be \(0\) for \(P = 0\)), viewed as an element of \(A\).

theorem polyPowerSum_zero {A : Type*} [CommRing A] (P : A[X]) :
    polyPowerSum P 0 = P.natDegree

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 3.2, Notation.

Uses 1

Statement usesPower sums of a polynomial

TheoremThe first power sum is the first elementary symmetric function#✓fully proved

For every polynomial \(P\) over a commutative ring, \(p_1(P) = e_1(P)\).

theorem polyPowerSum_one {A : Type*} [CommRing A] (P : A[X]) :
    polyPowerSum P 1 = polyElemSymm P 1

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 3.2 (Newton's identities).

Uses 2

Statement usesElementary symmetric functions of a polynomial · Power sums of a polynomial

TheoremNewton's recurrence for the power sums of a polynomial#✓fully proved

For every polynomial \(P\) over a commutative ring and every \(n \ge 0\), writing \(e_i = e_i(P)\) and \(p_i = p_i(P)\) for the elementary symmetric functions and power sums of \(P\),

\[p_{n+1} = (-1)^n (n+1)\, e_{n+1} + \sum_{i=0}^{n-1} (-1)^i e_{i+1}\, p_{n-i}.\]

theorem polyPowerSum_succ {A : Type*} [CommRing A] (P : A[X]) (n : ℕ) :
    polyPowerSum P (n + 1) = (-1) ^ n * ((n + 1 : ℕ) : A) * polyElemSymm P (n + 1) +
      ∑ i : Fin n, (-1) ^ (i : ℕ) * polyElemSymm P (i + 1) * polyPowerSum P (n - i)

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 3.2 (Newton's identities).

Uses 2

Statement usesElementary symmetric functions of a polynomial · Power sums of a polynomial

TheoremA prime-exponent criterion for powers in an ideal#●ready to prove

Let \(p\) be a prime, \(v_p\) the \(p\)-adic valuation, and \(\mathfrak{b}\) an ideal of a commutative ring \(B\). The following are equivalent: for every \(n \ge 1\) and every \(a \in \mathfrak{b}\) there is \(c \in \mathfrak{b}\) with \(a^n = p^{v_p(n!)} c\); and for every \(a \in \mathfrak{b}\) there is \(c \in \mathfrak{b}\) with \(a^p = p c\).

public theorem_wanted pow_mem_prime_pow_padicValNat_factorial_iff {p : ℕ} [Fact p.Prime]
    {B : Type*} [CommRing B] (I : Ideal B) :
    (∀ n : ℕ, 1 ≤ n → ∀ a ∈ I, ∃ c ∈ I, a ^ n = (p : B) ^ padicValNat p n.factorial * c) ↔
      ∀ a ∈ I, ∃ c ∈ I, a ^ p = (p : B) * c

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Proposition 3.

TheoremThe \(p\)-th power criterion for divided-power ideals#●ready to prove

Let \(p\) be a prime and let \(A\) be a commutative ring in which every natural number not divisible by \(p\) is a unit (a \(\mathbb{Z}_{(p)}\)-algebra). An ideal \(\mathfrak{a}\) of \(A\) is a divided-power ideal if and only if for every \(a \in \mathfrak{a}\) there is \(c \in \mathfrak{a}\) with \(a^p = p\,c\), that is, \(a^p \in p\mathfrak{a}\).

The paper also assumes \(A\) torsion-free; the statement does not need it.

public theorem_wanted isDividedPowerIdeal_iff_pow_prime_mem {p : ℕ} [Fact p.Prime]
    {A : Type*} [CommRing A] (hA : ∀ n : ℕ, ¬ p ∣ n → IsUnit (n : A)) (I : Ideal A) :
    IsDividedPowerIdeal I ↔ ∀ a ∈ I, ∃ c ∈ I, a ^ p = (p : A) * c

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Corollary 4.

Uses 1

Statement usesDivided-power ideal

TheoremDivided-power ideals generated by a set#●ready to prove

Let \(p\) be a prime and \(A\) a commutative ring in which every natural number not divisible by \(p\) is a unit (a \(\mathbb{Z}_{(p)}\)-algebra). For a subset \(S \subseteq A\), the ideal \(\mathfrak{a}\) generated by \(S\) is a divided-power ideal if and only if for every \(a \in S\) there is \(c \in \mathfrak{a}\) with \(a^p = pc\), that is, \(a^p \in p\mathfrak{a}\).

Torsion-freeness of \(A\) is not needed.

public theorem_wanted isDividedPowerIdeal_span_iff {p : ℕ} [Fact p.Prime]
    {A : Type*} [CommRing A] (hA : ∀ n : ℕ, ¬ p ∣ n → IsUnit (n : A)) (S : Set A) :
    IsDividedPowerIdeal (Ideal.span S) ↔ ∀ a ∈ S, ∃ c ∈ Ideal.span S, a ^ p = (p : A) * c

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Proposition 5.

Uses 1

Statement usesDivided-power ideal

TheoremProduct of a divided-power ideal with an ideal#●ready to prove

Let \(A\) be a commutative ring. If \(\mathfrak{a}\) is a divided-power ideal of \(A\), then for every ideal \(\mathfrak{b}\) of \(A\) the product \(\mathfrak{a}\mathfrak{b}\) is a divided-power ideal.

public theorem_wanted IsDividedPowerIdeal.mul {A : Type*} [CommRing A] {I : Ideal A}
    (hI : IsDividedPowerIdeal I) (J : Ideal A) : IsDividedPowerIdeal (I * J)

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Corollary 6.

Uses 1

Statement usesDivided-power ideal

TheoremPowers of the maximal ideal of a DVR that are divided-power ideals#●ready to prove

Let \(p\) be a prime and let \(O\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) such that \(pO = \mathfrak{m}^e\) for some integer \(e \ge 1\). Then for every \(k \ge 0\), the ideal \(\mathfrak{m}^k\) is a divided-power ideal if and only if \(e \le (p - 1)k\).

Equivalently, with \(v_p(\mathfrak{m}) = 1/e\), the condition is \(v_p(\mathfrak{m}^k) \ge 1/(p - 1)\). The paper states this for \(p\)-adic discrete valuation rings and remarks that it also holds for localizations of rings of integers; here \(O\) is any such ring, and the zero ideal is omitted.

public theorem_wanted isDividedPowerIdeal_maximalIdeal_pow_iff {p : ℕ} [Fact p.Prime]
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] {e : ℕ} (he0 : e ≠ 0)
    (he : Ideal.span {(p : O)} = IsLocalRing.maximalIdeal O ^ e) (k : ℕ) :
    IsDividedPowerIdeal (IsLocalRing.maximalIdeal O ^ k) ↔ e ≤ (p - 1) * k

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Lemma 7.

Uses 1

Statement usesDivided-power ideal

TheoremWhen the maximal ideal of a DVR is a divided-power ideal#●ready to prove

Let \(p\) be a prime and let \(O\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) such that \(pO = \mathfrak{m}^e\) for some integer \(e \ge 1\). Then \(\mathfrak{m}\) is a divided-power ideal if and only if \(e \le p - 1\).

public theorem_wanted isDividedPowerIdeal_maximalIdeal_iff {p : ℕ} [Fact p.Prime]
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] {e : ℕ} (he0 : e ≠ 0)
    (he : Ideal.span {(p : O)} = IsLocalRing.maximalIdeal O ^ e) :
    IsDividedPowerIdeal (IsLocalRing.maximalIdeal O) ↔ e ≤ p - 1

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Corollary 8.

Uses 1

Statement usesDivided-power ideal

Theorem\((p)\) is a divided-power ideal of \(\mathbb{Z}_p\)#●ready to prove

For every prime \(p\), the ideal generated by \(p\) in the ring \(\mathbb{Z}_p\) of \(p\)-adic integers is a divided-power ideal.

public theorem_wanted isDividedPowerIdeal_span_prime_padicInt (p : ℕ) [Fact p.Prime] :
    IsDividedPowerIdeal (Ideal.span {(p : ℤ_[p])})

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Corollary 8, last sentence.

Uses 1

Statement usesDivided-power ideal

TheoremCongruent elementary symmetric functions give deep power-sum congruences#●ready to prove

Let \(p\) be a prime and let \(A\) be a commutative ring without additive torsion in which every natural number not divisible by \(p\) is a unit (a torsion-free \(\mathbb{Z}_{(p)}\)-algebra). Let \(\mathfrak{a}\) be a divided-power ideal of \(A\), let \(P, Q \in A[X]\) be monic and let \(N \ge 1\); write \(e_n\) and \(p_n\) for the elementary symmetric functions and power sums of a polynomial. If \(e_n(P) - e_n(Q) \in \mathfrak{a}\) for every \(n\) with \(1 \le n \le N\), then there is \(c \in \mathfrak{a}\) with \(p_N(P) - p_N(Q) = N c\), that is, \(p_N(P) \equiv p_N(Q) \pmod{N \mathfrak{a}}\).

public theorem_wanted polyPowerSum_sub_mem_of_polyElemSymm_sub_mem {p : ℕ} [Fact p.Prime]
    {A : Type*} [CommRing A] [IsAddTorsionFree A] (hA : ∀ n : ℕ, ¬ p ∣ n → IsUnit (n : A))
    {I : Ideal A} (hI : IsDividedPowerIdeal I) {P Q : A[X]} (hP : P.Monic) (hQ : Q.Monic)
    {N : ℕ} (hN : 1 ≤ N)
    (h : ∀ n, 1 ≤ n → n ≤ N → polyElemSymm P n - polyElemSymm Q n ∈ I) :
    ∃ c ∈ I, polyPowerSum P N - polyPowerSum Q N = (N : A) * c

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Proposition 12.

Uses 3

Statement usesDivided-power ideal · Elementary symmetric functions of a polynomial · Power sums of a polynomial

TheoremPower-sum congruences imply elementary symmetric congruences#●ready to prove

Let \(p\) be a prime and \(A\) a torsion-free commutative ring in which every natural number not divisible by \(p\) is a unit (a torsion-free \(\mathbb{Z}_{(p)}\)-algebra). Let \(\mathfrak{a}\) be a divided-power ideal of \(A\), let \(P, Q \in A[X]\) be monic and let \(N\) be a natural number. Suppose that for every \(n\) with \(1 \le n \le N\) there is \(c \in \mathfrak{a}\) with \(p_n(P) - p_n(Q) = n c\), that is, \(p_n(P) \equiv p_n(Q) \pmod{n \mathfrak{a}}\). Then \(e_n(P) - e_n(Q) \in \mathfrak{a}\) for every \(n\) with \(1 \le n \le N\).

public theorem_wanted polyElemSymm_sub_mem_of_polyPowerSum_sub_mem {p : ℕ} [Fact p.Prime]
    {A : Type*} [CommRing A] [IsAddTorsionFree A] (hA : ∀ n : ℕ, ¬ p ∣ n → IsUnit (n : A))
    {I : Ideal A} (hI : IsDividedPowerIdeal I) {P Q : A[X]} (hP : P.Monic) (hQ : Q.Monic)
    {N : ℕ}
    (h : ∀ n, 1 ≤ n → n ≤ N → ∃ c ∈ I, polyPowerSum P n - polyPowerSum Q n = (n : A) * c) :
    ∀ n, 1 ≤ n → n ≤ N → polyElemSymm P n - polyElemSymm Q n ∈ I

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Proposition 13.

Uses 3

Statement usesDivided-power ideal · Elementary symmetric functions of a polynomial · Power sums of a polynomial

TheoremExponential of a power-sum series restricted to a set of degrees#●ready to prove

Let \(\sigma\) be a finite set of variables, and in \(\mathbb{Q}[x_i : i \in \sigma]\) let \(p_s = \sum_{i \in \sigma} x_i^s\) be the \(s\)-th power sum. Let \(S\) be a set of natural numbers and let \(P_S(t) = \sum_{s \in S,\ s \ge 1} \frac{(-1)^{s-1}}{s} p_s t^s\). For a partition \(\lambda\) of \(n\) with parts \(\lambda_1, \dots, \lambda_\ell\), write \(p_\lambda = p_{\lambda_1} \cdots p_{\lambda_\ell}\), \(\varepsilon_\lambda = (-1)^{n - \ell}\) and \(z_\lambda = \prod_a a^{r_a} \, r_a!\), where \(r_a\) is the number of parts equal to \(a\) and the product runs over the distinct parts \(a\). Then, as formal power series in \(t\) with coefficients in \(\mathbb{Q}[x_i : i \in \sigma]\), \(\exp P_S(t) = \sum_{n \ge 0} c_n t^n\), where \(c_n\) is the sum of \(\varepsilon_\lambda p_\lambda / z_\lambda\) over the partitions \(\lambda\) of \(n\) all of whose parts lie in \(S\).

public theorem_wanted exp_signedPowerSumSeries_eq_sum_partitions (σ : Type*) [Fintype σ]
    (S : Set ℕ) [DecidablePred (· ∈ S)] :
    (PowerSeries.subst (PowerSeries.mk fun s => if s ∈ S ∧ s ≠ 0 then
        ((-1 : ℚ) ^ (s - 1) / s) • MvPolynomial.psum σ ℚ s else 0) (PowerSeries.exp ℚ) :
        PowerSeries (MvPolynomial σ ℚ)) =
      PowerSeries.mk fun n => ∑ l : n.Partition with ∀ a ∈ l.parts, a ∈ S,
        ((-1 : ℚ) ^ (n - Multiset.card l.parts) /
          ((l.parts.toFinset.prod fun a => a ^ l.parts.count a * (l.parts.count a).factorial :
            ℕ) : ℚ)) • (l.parts.map (MvPolynomial.psum σ ℚ)).prod

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Proposition 19.

TheoremThe generating function of the elementary symmetric polynomials#●ready to prove

Let \(\sigma\) be a finite set of variables, and in \(\mathbb{Q}[x_i : i \in \sigma]\) let \(e_k\) be the \(k\)-th elementary symmetric polynomial and \(p_n = \sum_{i \in \sigma} x_i^n\) the \(n\)-th power sum. Then, as formal power series in \(t\) with coefficients in \(\mathbb{Q}[x_i : i \in \sigma]\),

\[\sum_{k \ge 0} e_k t^k = \exp\Big(\sum_{n \ge 1} \frac{(-1)^{n-1}}{n} p_n t^n\Big).\]

public theorem_wanted exp_signedPowerSumSeries_eq_esymmSeries (σ : Type*) [Fintype σ] :
    (PowerSeries.subst (PowerSeries.mk fun n => if n = 0 then 0 else
        ((-1 : ℚ) ^ (n - 1) / n) • MvPolynomial.psum σ ℚ n) (PowerSeries.exp ℚ) :
        PowerSeries (MvPolynomial σ ℚ)) =
      PowerSeries.mk fun k => MvPolynomial.esymm σ ℚ k

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Proposition 20.

TheoremElementary symmetric polynomials in terms of power sums#●ready to prove

Let \(\sigma\) be a finite set of variables, and in \(\mathbb{Q}[x_i : i \in \sigma]\) let \(e_n\) be the \(n\)-th elementary symmetric polynomial and \(p_k = \sum_{i \in \sigma} x_i^k\) the \(k\)-th power sum. For a partition \(\lambda\) of \(n\) with parts \(\lambda_1, \dots, \lambda_\ell\), write \(p_\lambda = p_{\lambda_1} \cdots p_{\lambda_\ell}\), \(\varepsilon_\lambda = (-1)^{n - \ell}\) and \(z_\lambda = \prod_a a^{r_a} \, r_a!\), where \(r_a\) is the number of parts equal to \(a\) and the product runs over the distinct parts \(a\). Then for every \(n \ge 0\),

\[e_n = \sum_{\lambda \vdash n} \frac{\varepsilon_\lambda}{z_\lambda} \, p_\lambda.\]

public theorem_wanted esymm_eq_sum_partitions (σ : Type*) [Fintype σ] (n : ℕ) :
    MvPolynomial.esymm σ ℚ n = ∑ l : n.Partition,
      ((-1 : ℚ) ^ (n - Multiset.card l.parts) /
        ((l.parts.toFinset.prod fun a => a ^ l.parts.count a * (l.parts.count a).factorial :
          ℕ) : ℚ)) • (l.parts.map (MvPolynomial.psum σ ℚ)).prod

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Corollary 21.

TheoremKummer's theorem for multinomial coefficients#●ready to prove

Let \(p\) be a prime and let \(r_1, \dots, r_k\) be natural numbers with sum \(m\). For \(i \ge 1\) let \(c_i = \lfloor ((r_1 \bmod p^i) + \dots + (r_k \bmod p^i)) / p^i \rfloor\). Then

\[v_p\binom{m}{r_1, \dots, r_k} = \sum_{i=1}^{m} c_i.\]

Here \(c_i\) is the carry into digit position \(i\) when \(r_1 + \dots + r_k\) is added in base \(p\), and \(c_i = 0\) for \(i > m\), so the right side is the sum of all the carries.

public theorem_wanted padicValNat_multinomial_eq_sum_carries {p : ℕ} [Fact p.Prime] {ι : Type*}
    (s : Finset ι) (r : ι → ℕ) :
    padicValNat p (Nat.multinomial s r) =
      ∑ i ∈ Finset.Icc 1 (∑ j ∈ s, r j), (∑ j ∈ s, r j % p ^ i) / p ^ i

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Theorem 23.

TheoremA valuation bound from Kummer's theorem#●ready to prove

Let \(p\) be a prime, let \(r_1, \dots, r_k\) be natural numbers with sum \(m\), and let \(j\) be an index with \(r_j \ne 0\). Then

\[v_p(m) \le v_p(r_j) + v_p\binom{m}{r_1, \dots, r_k},\]

that is, \(v_p(r_j) \ge v_p(m) - v_p\binom{m}{r_1, \dots, r_k}\).

The hypothesis \(r_j \ne 0\) is needed because \(v_p(0)\) is taken to be \(0\): for \((r_1, r_2) = (0, p)\) the inequality fails at \(j = 1\). With the paper's convention \(v_p(0) = \infty\) that case is trivial.

public theorem_wanted padicValNat_sum_le_add_padicValNat_multinomial {p : ℕ} [Fact p.Prime]
    {ι : Type*} (s : Finset ι) (r : ι → ℕ) {j : ι} (hj : j ∈ s) (hr : r j ≠ 0) :
    padicValNat p (∑ i ∈ s, r i) ≤ padicValNat p (r j) + padicValNat p (Nat.multinomial s r)

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Corollary 24.

TheoremPowers of elements congruent modulo a divided-power ideal#●ready to prove

Let \(p\) be a prime, let \(A\) be a commutative ring in which every natural number not divisible by \(p\) is a unit (a \(\mathbb{Z}_{(p)}\)-algebra), and let \(\mathfrak{a}\) be a divided-power ideal of \(A\). If \(x, y \in A\) satisfy \(x - y \in \mathfrak{a}\), then for every \(m \ge 0\) there is \(c \in \mathfrak{a}\) with \(x^{p^m} - y^{p^m} = p^m c\), and for every \(n \ge 0\) there is \(c \in \mathfrak{a}\) with \(x^n - y^n = n c\).

The ring \(A\) is not assumed to be torsion-free.

public theorem_wanted pow_sub_pow_mem_of_sub_mem {p : ℕ} [Fact p.Prime] {A : Type*} [CommRing A]
    (hA : ∀ n : ℕ, ¬ p ∣ n → IsUnit (n : A)) {I : Ideal A} (hI : IsDividedPowerIdeal I)
    {x y : A} (hxy : x - y ∈ I) :
    (∀ m : ℕ, ∃ c ∈ I, x ^ p ^ m - y ^ p ^ m = (p : A) ^ m * c) ∧
      ∀ n : ℕ, ∃ c ∈ I, x ^ n - y ^ n = (n : A) * c

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Lemma 25.

Uses 1

Statement usesDivided-power ideal

TheoremCongruence of products over a partition with multiplicities divisible by \(p^v\)#●ready to prove

Let \(p\) be a prime, \(A\) a commutative ring and \(\mathfrak{a}\) a divided-power ideal of \(A\). Let \(f, g : \mathbb{N} \to A\) satisfy \(f_n - g_n \in \mathfrak{a}\) for every \(n \ge 1\). For a partition \(\lambda = (\lambda_1, \dots, \lambda_k)\) of a natural number \(m\), write \(f_\lambda = f_{\lambda_1} \cdots f_{\lambda_k}\) and \(g_\lambda = g_{\lambda_1} \cdots g_{\lambda_k}\). If \(v\) is a natural number such that every part of \(\lambda\) occurs a multiple of \(p^v\) times, then \(f_\lambda - g_\lambda = p^v c\) for some \(c \in \mathfrak{a}\), that is, \(f_\lambda \equiv g_\lambda \bmod p^v \mathfrak{a}\).

The paper takes \(v = v_p(\lambda) = \min_i v_p(\lambda_i)\), which is false: for \(p = 2\), \(\lambda = (2)\), \(A = \mathbb{Z}_{(2)}\), \(\mathfrak{a} = (2)\), \(f_n = e_n(X^2 + 2)\) and \(g_n = e_n(X^2)\), where \(e_n(P)\) is the \(n\)-th elementary symmetric function of the roots of \(P\), \(f_n \equiv g_n \bmod 2\) for all \(n\) but \(f_2 - g_2 = 2 \notin 4\mathbb{Z}_{(2)}\). The paper's proof writes \(\lambda = \mu^{p^v}\) in the partition monoid, which uses the multiplicity condition stated here. The paper's symmetric functions are abstracted to arbitrary sequences \(f, g\), as the statement only uses their values.

public theorem_wanted multiset_prod_sub_prod_mem_of_count_dvd {p : ℕ} [Fact p.Prime]
    {A : Type*} [CommRing A] {I : Ideal A} (hI : IsDividedPowerIdeal I) (f g : ℕ → A)
    (hfg : ∀ n, 1 ≤ n → f n - g n ∈ I) {n : ℕ} (l : n.Partition) {v : ℕ}
    (hv : ∀ a ∈ l.parts, p ^ v ∣ l.parts.count a) :
    ∃ c ∈ I, (l.parts.map f).prod - (l.parts.map g).prod = (p : A) ^ v * c

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Corollary 26.

Uses 1

Statement usesDivided-power ideal

TheoremMöbius sum over the divisors prime to a given prime#●ready to prove

Let \(p\) be a prime, \(\mu\) the Möbius function and \(n \ge 1\). The sum of \(\mu(d)\) over the divisors \(d\) of \(n\) with \(p \nmid d\) is \(1\) if \(n\) is a power of \(p\) (including \(n = 1 = p^0\)) and \(0\) otherwise.

public theorem_wanted sum_moebius_divisors_not_dvd_prime {p : ℕ} (hp : p.Prime) {n : ℕ}
    (hn : n ≠ 0) :
    ∑ d ∈ n.divisors with ¬ p ∣ d, ArithmeticFunction.moebius d =
      if p ^ Nat.log p n = n then 1 else 0

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Lemma 28.

TheoremThe Artin–Hasse exponential has \(p\)-integral coefficients#●ready to prove

Let \(p\) be a prime and let \(F(z) = \exp\big(\sum_{j \ge 0} z^{p^j} / p^j\big) \in \mathbb{Q}[[z]]\) be the Artin–Hasse exponential. For every \(n \ge 0\), the coefficient of \(z^n\) in \(F\), written in lowest terms, has a denominator not divisible by \(p\).

public theorem_wanted artinHasse_coeff_den_not_dvd (p : ℕ) [Fact p.Prime] (n : ℕ) :
    ¬ p ∣ (PowerSeries.coeff n (PowerSeries.subst
      (PowerSeries.mk fun m : ℕ => if p ^ Nat.log p m = m then (m : ℚ)⁻¹ else 0)
      (PowerSeries.exp ℚ) : PowerSeries ℚ)).den

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Corollary 29.

TheoremThe Artin–Hasse exponential as a product#●ready to prove

Let \(p\) be a prime, let \(\mu\) be the Möbius function and let \(F(z) = \exp\big(\sum_{j \ge 0} z^{p^j} / p^j\big) \in \mathbb{Q}[[z]]\) be the Artin–Hasse exponential. For \(d \ge 1\) and \(a \in \mathbb{Q}\) write \((1 - z^d)^a = \exp\big(a \log(1 - z^d)\big)\), where \(\log(1 - z^d) = -\sum_{k \ge 1} z^{dk}/k\). Then for every \(N \ge 0\), \(F\) has the same coefficients of \(z^0, \dots, z^N\) as the finite product of the series \((1 - z^d)^{-\mu(d)/d}\) over the integers \(1 \le d \le N\) not divisible by \(p\). Since the factors with \(d > N\) are \(1 + O(z^{N+1})\), this is the identity \(F(z) = \prod_{p \nmid d} (1 - z^d)^{-\mu(d)/d}\) read coefficientwise.

public theorem_wanted artinHasse_eq_prod_one_sub_pow (p : ℕ) [Fact p.Prime] (N : ℕ) :
    PowerSeries.trunc (N + 1) (PowerSeries.subst
      (PowerSeries.mk fun m : ℕ => if p ^ Nat.log p m = m then (m : ℚ)⁻¹ else 0)
      (PowerSeries.exp ℚ) : PowerSeries ℚ) =
    PowerSeries.trunc (N + 1) (∏ d ∈ Finset.Icc 1 N with ¬ p ∣ d,
      (PowerSeries.subst (PowerSeries.mk fun m : ℕ => if m ≠ 0 ∧ d ∣ m then
          (-(ArithmeticFunction.moebius d : ℚ) / d) * (-(d : ℚ) / m) else 0)
        (PowerSeries.exp ℚ) : PowerSeries ℚ))

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Proposition 27.

Definition\(p\)-splitting of multisets of parts#✓fully proved

Let \(p\) be a natural number and \(s\), \(t\) multisets of natural numbers (multisets of parts). Then \(s\) is a \(p\)-splitting of \(t\) when there is \(u \ge 1\) such that \(t\) contains the part \(pu\) and \(s\) is obtained from \(t\) by removing one instance of \(pu\) and adding \(p\) copies of \(u\).

public def IsPSplitting (p : ℕ) (s t : Multiset ℕ) : Prop :=
  ∃ u, 1 ≤ u ∧ p * u ∈ t ∧ s = t.erase (p * u) + Multiset.replicate p u

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Definition 30.

Used by 3

Used by\(p\) copies of \(u\) form a \(p\)-splitting of \(\{pu\}\) · The \(p\)-equivalence class of a multiset of parts · The class sum of the empty partition

Theorem\(p\) copies of \(u\) form a \(p\)-splitting of \(\{pu\}\)#✓fully proved

For every natural number \(p\) and every integer \(u \ge 1\), the multiset consisting of \(p\) copies of \(u\) is a \(p\)-splitting of the one-element multiset \(\{pu\}\).

public theorem isPSplitting_replicate_singleton (p : ℕ) {u : ℕ} (hu : 1 ≤ u) :
    IsPSplitting p (Multiset.replicate p u) {p * u}

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Definition 30.

Uses 1

Statement uses\(p\)-splitting of multisets of parts

DefinitionThe \(p\)-equivalence class of a multiset of parts#✓fully proved

Let \(p\) be a natural number and \(\lambda\) a multiset of natural numbers whose elements sum to \(n\). The \(p\)-equivalence class \(C_\lambda\) is the set of partitions \(\mu\) of \(n\) with \(\mu \sim_p \lambda\), where \(\sim_p\) (\(p\)-equivalence) is the equivalence relation on multisets of natural numbers generated by \(p\)-splitting.

public noncomputable def pEquivClass (p : ℕ) (s : Multiset ℕ) : Finset s.sum.Partition := by
  classical
  exact Finset.univ.filter fun μ => Relation.EqvGen (IsPSplitting p) μ.parts s

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Definition 31.

Uses 1 · Used by 3

Statement uses\(p\)-splitting of multisets of parts

Used byThe \(p\)-equivalence class sum · For odd \(p\) the signs in \(g_\lambda\) are constant · The class sum of the empty partition

DefinitionThe \(p\)-equivalence class sum#✓fully proved

Let \(\sigma\) be a finite set of variables, let \(p\) be a natural number and let \(\lambda\) be a multiset of natural numbers whose elements sum to \(n\). In \(\mathbb{Q}[x_i : i \in \sigma]\) let \(p_k = \sum_{i \in \sigma} x_i^k\) be the \(k\)-th power sum. For a partition \(\mu\) of \(n\) with parts \(\mu_1, \dots, \mu_\ell\), write \(p_\mu = p_{\mu_1} \cdots p_{\mu_\ell}\), \(\varepsilon_\mu = (-1)^{n - \ell}\) and \(z_\mu = \prod_a a^{r_a} \, r_a!\), where \(r_a\) is the number of parts of \(\mu\) equal to \(a\) and the product runs over the distinct parts \(a\) of \(\mu\). The \(p\)-equivalence class sum of \(\lambda\) is

\[g_\lambda = \sum_{\mu \in C_\lambda} \frac{\varepsilon_\mu}{z_\mu} \, p_\mu,\]

where \(C_\lambda\) is the \(p\)-equivalence class of \(\lambda\): the set of partitions of \(n\) that are \(p\)-equivalent to \(\lambda\).

public noncomputable def pEquivClassSum (σ : Type*) [Fintype σ] (p : ℕ) (s : Multiset ℕ) :
    MvPolynomial σ ℚ :=
  ∑ μ ∈ pEquivClass p s, ((-1 : ℚ) ^ (s.sum - Multiset.card μ.parts) /
    ((μ.parts.toFinset.prod fun a => a ^ μ.parts.count a * (μ.parts.count a).factorial : ℕ) : ℚ)) • (μ.parts.map (MvPolynomial.psum σ ℚ)).prod

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 5.2, display (8).

Uses 1 · Used by 4

Statement usesThe \(p\)-equivalence class of a multiset of parts

Used byMultiplicativity of \(g_\lambda\) over disjoint parts · \(g_\lambda\) is \(p\)-integral · For odd \(p\) the signs in \(g_\lambda\) are constant · The class sum of the empty partition

TheoremThe class sum of the empty partition#✓fully proved

For every finite set of variables \(\sigma\) and every natural number \(p\), the \(p\)-equivalence class sum of the empty multiset is \(g_\emptyset = 1\).

public theorem pEquivClassSum_zero (σ : Type*) [Fintype σ] (p : ℕ) :
    pEquivClassSum σ p 0 = 1

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Section 5.2.

Uses 3

Statement usesThe \(p\)-equivalence class sum

Proof uses\(p\)-splitting of multisets of parts · The \(p\)-equivalence class of a multiset of parts

TheoremMultiplicativity of \(g_\lambda\) over disjoint parts#●ready to prove

Let \(p\) be a prime, \(\sigma\) a finite set of variables, and for a multiset \(\lambda\) of parts let \(g_\lambda\) be its \(p\)-equivalence class sum in \(\mathbb{Q}[x_i : i \in \sigma]\). Let \(\lambda\) and \(\mu\) be multisets of natural numbers, none of whose elements is divisible by \(p\) (so no part is \(0\)), with no part in common. Then \(g_{\lambda + \mu} = g_\lambda \, g_\mu\), where \(\lambda + \mu\) is the union of \(\lambda\) and \(\mu\) counted with multiplicity. Moreover \(g_\lambda = \prod_u g_{(u)^{r_u(\lambda)}}\), the product over the distinct parts \(u\) of \(\lambda\), where \(r_u(\lambda)\) is the number of times \(u\) occurs in \(\lambda\) and \((u)^r\) is the multiset of \(r\) copies of \(u\).

public theorem_wanted pEquivClassSum_add_of_disjoint (σ : Type*) [Fintype σ] {p : ℕ}
    [Fact p.Prime] {s t : Multiset ℕ} (hs : ∀ a ∈ s, ¬ p ∣ a) (ht : ∀ a ∈ t, ¬ p ∣ a)
    (hst : ∀ a ∈ s, a ∉ t) :
    pEquivClassSum σ p (s + t) = pEquivClassSum σ p s * pEquivClassSum σ p t ∧
      pEquivClassSum σ p s =
        ∏ u ∈ s.toFinset, pEquivClassSum σ p (Multiset.replicate (s.count u) u)

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Lemma 34.

Uses 1

Statement usesThe \(p\)-equivalence class sum

TheoremFor odd \(p\) the signs in \(g_\lambda\) are constant#●ready to prove

Let \(p\) be an odd prime, \(\sigma\) a finite set of variables and \(\lambda\) a partition of \(n\) with \(\ell(\lambda)\) parts. Then the \(p\)-equivalence class sum \(g_\lambda\) in \(\mathbb{Q}[x_i : i \in \sigma]\) satisfies

\[g_\lambda = (-1)^{n - \ell(\lambda)} \sum_{\mu \in C_\lambda} \frac{p_\mu}{z_\mu},\]

where \(C_\lambda\) is the \(p\)-equivalence class of \(\lambda\) (the partitions \(\mu\) of \(n\) with \(\mu \sim_p \lambda\)), \(p_\mu = \prod_i p_{\mu_i}\) is the product of the power sums \(p_k = \sum_{i \in \sigma} x_i^k\), and \(z_\mu = \prod_a a^{r_a} \, r_a!\), the product over the distinct parts \(a\) of \(\mu\), with \(r_a\) the number of parts of \(\mu\) equal to \(a\).

public theorem_wanted pEquivClassSum_eq_neg_one_pow_smul (σ : Type*) [Fintype σ] {p : ℕ}
    [Fact p.Prime] (hp : Odd p) {n : ℕ} (l : n.Partition) :
    pEquivClassSum σ p l.parts = ((-1 : ℚ) ^ (n - Multiset.card l.parts)) •
      ∑ μ ∈ pEquivClass p l.parts, (1 / ((μ.parts.toFinset.prod fun a => a ^ μ.parts.count a * (μ.parts.count a).factorial : ℕ) : ℚ)) • (μ.parts.map (MvPolynomial.psum σ ℚ)).prod

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Lemma 35.

Uses 2

Statement usesThe \(p\)-equivalence class of a multiset of parts · The \(p\)-equivalence class sum

Theorem\(g_\lambda\) is \(p\)-integral#●ready to prove

Let \(p\) be a prime, \(\sigma\) a finite set of variables and \(\lambda\) a partition of \(n\). Every coefficient of the \(p\)-equivalence class sum \(g_\lambda\) in \(\mathbb{Q}[x_i : i \in \sigma]\) is a rational number whose denominator in lowest terms is not divisible by \(p\).

This is the paper's \(g_\lambda \in \Lambda_{\mathbb{Z}_{(p)}}\), in finitely many variables.

public theorem_wanted pEquivClassSum_coeff_den_not_dvd (σ : Type*) [Fintype σ] {p : ℕ}
    [Fact p.Prime] {n : ℕ} (l : n.Partition) (m : σ →₀ ℕ) :
    ¬ p ∣ ((pEquivClassSum σ p l.parts).coeff m).den

Sources

• S. Anni, A. Ghitza and A. Medvedovsky, Elementary Symmetric Functions and Deep Power-Sum Congruences, INTEGERS 24 (2024), Article A46, Proposition 36.

Uses 1

Statement usesThe \(p\)-equivalence class sum

15 fully proved22 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.