Bhargava p-orderings

DefinitionPrefix-product valuation#✓fully proved

Let \(R\) be a commutative ring, \(\mathfrak p\) a nonzero prime ideal of \(R\) and \((a_k)_{k \ge 0}\) a sequence in \(R\). For \(n \in \mathbb N\) and \(x \in R\), the stage-\(n\) prefix-product valuation of \(x\) is the multiplicity of \(\mathfrak p\) in the principal ideal generated by \(\prod_{k < n} (x - a_k)\): the largest \(m \in \mathbb N\) such that \(\mathfrak p^m\) divides this ideal, or \(\infty\) if every power of \(\mathfrak p\) divides it.

noncomputable def pOrderingValuation
    {R : Type*} [CommRing R]
    (p : IsDedekindDomain.HeightOneSpectrum R) (a : ℕ → R) (n : ℕ)
    (x : R) : ℕ∞ :=
  emultiplicity p.asIdeal
    (Ideal.span {(Finset.range n).prod fun k => x - a k})

Sources

• Takeda, Introduction, lines 52-60.

Used by 9

Used byA set with a p-ordering is infinite · Building a p-ordering · Each term of a p-ordering attains the least valuation · Bhargava p-ordering · The stage-zero condition of a p-ordering is automatic · Unfolding the definition of a p-ordering · Terms of a p-ordering lie in the set · Minimality of a p-ordering · The stage-zero valuation vanishes

DefinitionBhargava p-ordering#✓fully proved

Let \(R\) be a Dedekind domain, \(\mathfrak p\) a nonzero prime ideal of \(R\), \(S \subseteq R\) and \((a_n)_{n \ge 0}\) a sequence in \(R\). Write \(v_n(x)\) for the stage-\(n\) prefix-product valuation of \(x \in R\) with respect to \(\mathfrak p\) and \((a_n)\), the multiplicity of \(\mathfrak p\) in the ideal generated by \(\prod_{k < n} (x - a_k)\). Then \((a_n)\) is a \(\mathfrak p\)-ordering of \(S\) when \(S\) is infinite, \(a_n \in S\) for every \(n\), and \(v_n(a_n) \le v_n(x)\) for every \(n\) and every \(x \in S\).

def IsPOrdering
    {R : Type*} [CommRing R] [IsDedekindDomain R]
    (p : IsDedekindDomain.HeightOneSpectrum R) (S : Set R)
    (a : ℕ → R) : Prop :=
  S.Infinite ∧ (∀ n, a n ∈ S) ∧
    ∀ n, ∀ x ∈ S,
      pOrderingValuation p a n (a n) ≤ pOrderingValuation p a n x

Sources

• Takeda, Introduction, lines 52-60.

Uses 1 · Used by 7

Statement usesPrefix-product valuation

Used byA set with a p-ordering is infinite · Building a p-ordering · Each term of a p-ordering attains the least valuation · The stage-zero condition of a p-ordering is automatic · Unfolding the definition of a p-ordering · Terms of a p-ordering lie in the set · Minimality of a p-ordering

TheoremUnfolding the definition of a p-ordering#✓fully proved

Let \(R\) be a Dedekind domain, \(\mathfrak p\) a nonzero prime ideal of \(R\), \(S \subseteq R\) and \((a_n)_{n \ge 0}\) a sequence in \(R\), and write \(v_n\) for the stage-\(n\) prefix-product valuation with respect to \(\mathfrak p\) and \((a_n)\). Then \((a_n)\) is a \(\mathfrak p\)-ordering of \(S\) if and only if \(S\) is infinite, \(a_n \in S\) for every \(n\), and \(v_n(a_n) \le v_n(x)\) for every \(n\) and every \(x \in S\).

theorem isPOrdering_unfold
    {R : Type*} [CommRing R] [IsDedekindDomain R]
    {p : IsDedekindDomain.HeightOneSpectrum R} {S : Set R}
    {a : ℕ → R} :
    IsPOrdering p S a ↔
      S.Infinite ∧ (∀ n, a n ∈ S) ∧
        ∀ n, ∀ x ∈ S,
          pOrderingValuation p a n (a n) ≤
            pOrderingValuation p a n x

Uses 2

Statement usesBhargava p-ordering · Prefix-product valuation

TheoremA set with a p-ordering is infinite#✓fully proved

Let \(R\) be a Dedekind domain, \(\mathfrak p\) a nonzero prime ideal of \(R\) and \(S \subseteq R\). If some sequence in \(R\) is a \(\mathfrak p\)-ordering of \(S\), then \(S\) is infinite.

theorem IsPOrdering.infinite
    {R : Type*} [CommRing R] [IsDedekindDomain R]
    {p : IsDedekindDomain.HeightOneSpectrum R} {S : Set R}
    {a : ℕ → R} (h : IsPOrdering p S a) : S.Infinite

Uses 2 · Used by 1

Statement usesBhargava p-ordering

Proof usesPrefix-product valuation

Used byThe stage-zero condition of a p-ordering is automatic

TheoremTerms of a p-ordering lie in the set#✓fully proved

Let \(R\) be a Dedekind domain, \(\mathfrak p\) a nonzero prime ideal of \(R\), \(S \subseteq R\) and \((a_n)_{n \ge 0}\) a \(\mathfrak p\)-ordering of \(S\). Then \(a_n \in S\) for every \(n\).

theorem IsPOrdering.mem
    {R : Type*} [CommRing R] [IsDedekindDomain R]
    {p : IsDedekindDomain.HeightOneSpectrum R} {S : Set R}
    {a : ℕ → R} (h : IsPOrdering p S a) (n : ℕ) : a n ∈ S

Uses 2 · Used by 2

Statement usesBhargava p-ordering

Proof usesPrefix-product valuation

Used byEach term of a p-ordering attains the least valuation · The stage-zero condition of a p-ordering is automatic

TheoremMinimality of a p-ordering#✓fully proved

Let \(R\) be a Dedekind domain, \(\mathfrak p\) a nonzero prime ideal of \(R\), \(S \subseteq R\) and \((a_n)_{n \ge 0}\) a \(\mathfrak p\)-ordering of \(S\), and write \(v_n\) for the stage-\(n\) prefix-product valuation with respect to \(\mathfrak p\) and \((a_n)\). Then \(v_n(a_n) \le v_n(x)\) for every \(n\) and every \(x \in S\).

theorem IsPOrdering.min_le
    {R : Type*} [CommRing R] [IsDedekindDomain R]
    {p : IsDedekindDomain.HeightOneSpectrum R} {S : Set R}
    {a : ℕ → R} (h : IsPOrdering p S a) (n : ℕ) (x : R)
    (hx : x ∈ S) :
    pOrderingValuation p a n (a n) ≤ pOrderingValuation p a n x

Uses 2 · Used by 2

Statement usesBhargava p-ordering · Prefix-product valuation

Used byEach term of a p-ordering attains the least valuation · The stage-zero condition of a p-ordering is automatic

TheoremEach term of a p-ordering attains the least valuation#✓fully proved

Let \(R\) be a Dedekind domain, \(\mathfrak p\) a nonzero prime ideal of \(R\), \(S \subseteq R\) and \((a_n)_{n \ge 0}\) a \(\mathfrak p\)-ordering of \(S\), and write \(v_n\) for the stage-\(n\) prefix-product valuation with respect to \(\mathfrak p\) and \((a_n)\). Then for every \(n\), \(v_n(a_n)\) is the least element of \(\{v_n(x) : x \in S\}\).

theorem IsPOrdering.isLeast
    {R : Type*} [CommRing R] [IsDedekindDomain R]
    {p : IsDedekindDomain.HeightOneSpectrum R} {S : Set R}
    {a : ℕ → R} {n : ℕ} (h : IsPOrdering p S a) :
    IsLeast (pOrderingValuation p a n '' S)
      (pOrderingValuation p a n (a n))

Uses 4

Statement usesBhargava p-ordering · Prefix-product valuation

Proof usesTerms of a p-ordering lie in the set · Minimality of a p-ordering

TheoremBuilding a p-ordering#✓fully proved

Let \(R\) be a Dedekind domain, \(\mathfrak p\) a nonzero prime ideal of \(R\), \(S \subseteq R\) and \((a_n)_{n \ge 0}\) a sequence in \(R\), and write \(v_n\) for the stage-\(n\) prefix-product valuation with respect to \(\mathfrak p\) and \((a_n)\). If \(S\) is infinite, \(a_n \in S\) for every \(n\), and \(v_n(a_n) \le v_n(x)\) for every \(n\) and every \(x \in S\), then \((a_n)\) is a \(\mathfrak p\)-ordering of \(S\).

theorem IsPOrdering.intro
    {R : Type*} [CommRing R] [IsDedekindDomain R]
    {p : IsDedekindDomain.HeightOneSpectrum R} {S : Set R}
    {a : ℕ → R} (hinf : S.Infinite) (hmem : ∀ n, a n ∈ S)
    (hmin : ∀ n, ∀ x ∈ S,
      pOrderingValuation p a n (a n) ≤ pOrderingValuation p a n x) :
    IsPOrdering p S a

Uses 2

Statement usesBhargava p-ordering · Prefix-product valuation

TheoremThe stage-zero valuation vanishes#✓fully proved

Let \(R\) be a commutative ring, \(\mathfrak p\) a nonzero prime ideal of \(R\) and \((a_n)_{n \ge 0}\) a sequence in \(R\). For every \(x \in R\), the stage-\(0\) prefix-product valuation of \(x\) with respect to \(\mathfrak p\) and \((a_n)\) is \(0\): the product is empty, so the ideal is all of \(R\).

theorem pOrderingValuation_zero
    {R : Type*} [CommRing R]
    (p : IsDedekindDomain.HeightOneSpectrum R) (a : ℕ → R)
    (x : R) : pOrderingValuation p a 0 x = 0

Uses 1 · Used by 1

Statement usesPrefix-product valuation

Used byThe stage-zero condition of a p-ordering is automatic

TheoremThe stage-zero condition of a p-ordering is automatic#✓fully proved

Let \(R\) be a Dedekind domain, \(\mathfrak p\) a nonzero prime ideal of \(R\), \(S \subseteq R\) and \((a_n)_{n \ge 0}\) a sequence in \(R\), and write \(v_n\) for the stage-\(n\) prefix-product valuation with respect to \(\mathfrak p\) and \((a_n)\). Then \((a_n)\) is a \(\mathfrak p\)-ordering of \(S\) if and only if \(S\) is infinite, \(a_n \in S\) for every \(n\), and \(v_n(a_n) \le v_n(x)\) for every \(n \ge 1\) and every \(x \in S\).

Since every stage-zero valuation is \(0\), the term \(a_0\) may be any element of \(S\).

theorem isPOrdering_iff_pos
    {R : Type*} [CommRing R] [IsDedekindDomain R]
    {p : IsDedekindDomain.HeightOneSpectrum R} {S : Set R}
    {a : ℕ → R} :
    IsPOrdering p S a ↔
      S.Infinite ∧ (∀ n, a n ∈ S) ∧
        ∀ n, 1 ≤ n → ∀ x ∈ S,
          pOrderingValuation p a n (a n) ≤
            pOrderingValuation p a n x

Uses 6

Statement usesBhargava p-ordering · Prefix-product valuation

Proof usesA set with a p-ordering is infinite · Terms of a p-ordering lie in the set · Minimality of a p-ordering · The stage-zero valuation vanishes

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.