Newton polygons

Stream: mathlib4

[Michael Stoll]

Is the theory of Newton polygons in the works somewhere? (Mathlib.RingTheory.Henselian is a leaf file, so it is likely not in Mathlib.)

What I would need is the statement that the Newton polygon of an irreducible polynomial (over a Henselian local ring) consists of a single segment (or, rather, the equivalent statement on the valuations of the coefficients).

[Johan Commelin]

I'm not aware of any wip in this direction, but it would be cool to have it!

[William Coram]

Hey, I have a very early wip file on Newton polygons (see https://github.com/WilliamCoram/Project/blob/main/Project/Gouvea.lean , I plan on following Gouvea's p-adic Numbers book for most of the content. A theorem saying irreducible polynomials are pure (prop 6.4.2) will eventually be included. This may take a while though, as I will have to work my way through Weierstrass' preparation theorem first (or at least a polynomial version initially). I plan on posting about this soon asking for feedback and support on defining things idiomatically.

[William Coram]

Re: asking for feedback. Right now I have a few ways I think that defining things could work, but I am unsure if they are the best or if they may cause issues later on down the line.

Firstly, for Newton Polygons I have the following definitions:

variable (F M L : Type*) [OrderedSemiring F] [AddCommMonoid M] [OrderedSemiring L] [Module F M]
    [Module F L]

variable (U : Set (Prod M L))

/-- NewtonPolygon via inequalities-/
def NewtonPolygon : Set (Prod M L) :=
    {u : Prod M L | (∃ u' : convexHull F U, u'.1 = u) ∧ (∀ (q : convexHull F U) (h : q.1.1 = u.1),
    u.2 ≤ q.1.2)}

/-- NewtonPolygon via sInf-/
def NewtonPolygon2 [InfSet L] : Set (Prod M L) :=
  {u : Prod M L | (∃ u' : convexHull F U, u'.1.1 = u.1) ∧
  (u.2 = sInf {v : L | ∃ v' : convexHull F U,  v'.1.1 = u.1 ∧ v = v'.1.2})}

The second one is my preferred definition, but I have questions on whether the api of sInf is something I want to delve into.

Naturally, I then define

def NewtonPolygon_breaks : Set (Prod M L) :=
    (NewtonPolygon F M L U) ∩ U

to give prospective points of slopes.

I then reduce to the case of k^2, for k a field (think this may be the most general case for when a 'slope' may make sense - further generalisations are welcome). To define a slope at a point I first need to define its next point. Which I do by the following:

/
variable (k : Type*) [OrderedRing k] [Field k] [InfSet k]
variable (t : Set (Prod k k))

-- NextPoint via defintion of a set-/
def NextPoint (l : NewtonPolygon_breaks k k k t) : Set (NewtonPolygon_breaks k k k t) :=
  {u | u.1.1 > l.1.1 ∧ (∀ (y : NewtonPolygon_breaks k k k t) (h : y.1.1 > l.1.1), y.1.1 ≥ u.1.1)}

as in the Newton Polygon definition this could also be defined using sInf. Of course, this is a set and not actually a point - but in cases of there not being a next point this would reduce to showing the set is empty. I haven't got that far, but I'm thinking it being a set may be an advantage?
However, I could also define it explicitly as

def NextPoint3 (l : NewtonPolygon_breaks k k k t) : Prod k k :=
  (sInf {u : k | ∃ u' : NewtonPolygon_breaks k k k t, u'.1.1 = u ∧ u > l.1.1} ,
  sInf {u : k | ∃ u' : NewtonPolygon_breaks k k k t,
  u'.1.1 = sInf {v : k | ∃ v' : NewtonPolygon_breaks k k k t, v'.1.1 = v ∧ v > l.1.1} ∧ u = u'.1.2})

the first sInf in the second coordinate can be removed - but I cannot think of a way to do this nicely right now.
I could also define this point using a structure. I have not used these environments yet, but perhaps this would be the best way.

Finally, to define slopes I then give

def NewtonPolygon_slope_length (l : NewtonPolygon_breaks k k k t) (m : NextPoint k t l) : k :=
  (m.1.1.1 - l.1.1)

def NewtonPolygon_slope_length3 (l : NewtonPolygon_breaks k k k t) : k :=
  (NextPoint3 k t l).1 - l.1.1

To me an advantage of defining next points using the second definition (famously called NextPoint3) is that you need to give one less hypothesis (namely not an element in the set of NextPoint) in slope_length3. Perhaps, this is a wrong way to think though?

The definitions of slopes are then just a natural continuation of these

noncomputable
def NewtonPolygon_slope (l : NewtonPolygon_breaks k k k t) (m : NextPoint k t l) : k :=
  (m.1.1.2 - l.1.2) / (NewtonPolygon_slope_length k t l m)


def NewtonPolygon_slope3 (l : NewtonPolygon_breaks k k k t) : k :=
  ((NextPoint3 k t l).2 - l.1.2) / ((NextPoint3 k t l).1 - l.1.1)

Any advice on my method to define slopes would be appreciated, especially if you think theres a much more natural way this can be done which I may have missed.

[Kevin Buzzard]

Can you describe what all your variables will be for an example like the polynomial $X^2+p$ over the $p$-adic numbers? Right now I think I'm just lost in the generalities.

[Kevin Buzzard]

William Coram said:

To define a slope at a point I first need to define its next point. Which I do by the following:

variable (k : Type*) [OrderedRing k] [Field k] [InfSet k]
...

This is almost surely wrong. This says "let $k$ be a set, then put an addition and multiplication and ordering on it making it an ordered ring, and then put a completely different addition and multiplication on it making it a field, and then also put a function on it with no axioms but called sInf".

[Mitchell Lee]

I think you have defined the lower boundary of the upper convex hull of a set of points. This construction is involved in the definition of the Newton polygon, but it should not be referred to as a "Newton polygon". A Newton polygon is associated with a polynomial in one variable over a (semi)ring with a valuation.

[Mitchell Lee]

Moreover, I suspect it is easier to work with the entire upper convex hull of the set $U \subseteq M \times L$, rather than merely the lower boundary of the upper convex hull of $U$. This can be expressed simply as the Minkowski sum $\operatorname{conv}(U) + \{0\} \times L_{\geq 0}$, which is a convex body (docs#ConvexBody).

[Mitchell Lee]

It is worth noting that the convex geometry in mathlib is still in its early stages of development. Perhaps it is prudent to add a good definition of a "(convex) polygon" (or better, "polyhedron" and "polytope") before trying to add the definition of a "Newton polygon".

[Michael Stoll]

My instinct would be to define a Newton Polygon as a (strictly) lower convex sequence of segments (given by the vertices as two functions fromFin n or some more general linearly ordered finite type with values in an ordered field k).
Then have functions giving the Newton Polygon associated to a finite set of points in k² and giving the relevant set of points associated to a polynomial over a discretely values ring or field.

[William Coram]

I think you have defined the lower boundary of the upper convex hull of a set of points. This construction is involved in the definition of the Newton polygon, but it should not be referred to as a "Newton polygon". A Newton polygon is associated with a polynomial in one variable over a (semi)ring with a valuation.

Yes, you are right - I was defining the lower boundary of the upper convex hull, and wrongly calling it a Newton polygon. I really only want this for when the set is defined via a polynomial, but in more generality the name does need to be changed. Thanks for pointing this out.

[William Coram]

Kevin Buzzard said:

This is almost surely wrong. This says "let $k$ be a set, then put an addition and multiplication and ordering on it making it an ordered ring, and then put a completely different addition and multiplication on it making it a field, and then also put a function on it with no axioms but called sInf".

I naively, presumed lean would match the operations for OrderedRing and Field - I realise I could just use LinearOrderedField now, which I will do. [InfSet k] is there to allow me to use sInf (which sounds like it may not be the best way) - is there a way I could have combined this with the previous statements?

[Yaël Dillies]

The only conditionally complete linear ordered field is ℝ. Why not specialise your definition to ℝ?

[Michael Stoll]

It may be useful to also be able to use the rationals, for example. I don't think we need completeness to work with Newton Polygons, which are basically combinatorial objects.

[Kevin Buzzard]

William Coram said:

I naively, presumed lean would match the operations for OrderedRing and Field

You can work out what Lean does by looking at e.g. the definitions in the docs. Clicking on docs#OrderedRing you can see that [OrderedRing R] means "assume there is an addition, a multiplication a 1,..., satisfiying this axiom and that axiom and that axiom..." and then from docs#Field you can see that [Field R] means "assume there is another addition, another multiplication...". And if you check out docs#InfSet you'll see it means literally nothing more than "assume there is some completely arbitrary function called sInf from Set R to R satisfying no axioms at all". When I was a beginner I just thought Lean did a lot of magic, but in fact Lean does not do any magic, everything it does is completely logical, so if you tell it [OrderedRing R] [Field R] [InfSet R] then it will do literally what the documentation of those classes says it will do, no more and no less.

• I realise I could just use LinearOrderedField now, which I will do. [InfSet k] is there to allow me to use sInf (which sounds like it may not be the best way) - is there a way I could have combined this with the previous statements?

Well really there are two or three questions here. Are you asking that sInf really is the inf for any subset of your field? You can't be, because you want the reals to work, what is the inf of the empty set, or the field itself? So you can't hope to have a sInf which satisfies that sInf X is always the inf of X for any subset X of your field. So really the answer to the question you're asking involving about what will "allow me to use sInf" is "what exactly do you mean by that?".

Now if I stop being autistic for a bit and conjecture that you mean "any nonempty bounded-below set has an inf" then Yael's comment becomes pertinent -- what examples do you have in mind other than the real numbers? If none, then why not just use the real numbers?

But there is a third question, which is why you want sInf at all. As Michael points out, the theory of newton polygons works fine with the rational numbers, and you are not "allowed to use sInf" on these if I interpret your comment as meaning "I want every nonempty bounded-below set to have to an inf". So now the question becomes "are you sure you should be using Infs of infinite sets at all because now you are ruling out examples where the theory should surely be fine". And of course finite Infs, which are surely all you need for the theory, already exist for all linearly ordered fields. So maybe you need to rethink your design decisions to avoid sInfs, rather than asking how to be allowed to use them.

[William Coram]

Kevin Buzzard said:

Now if I stop being autistic for a bit and conjecture that you mean "any nonempty bounded-below set has an inf" then Yael's comment becomes pertinent -- what examples do you have in mind other than the real numbers? If none, then why not just use the real numbers?

So maybe you need to rethink your design decisions to avoid sInfs, rather than asking how to be allowed to use them.

Yes, your conjecture was correct . I did not have any other examples than $\R$ in mind- but it would be pertinent to not neglect $\mathbb{Q}$, if it is something which can be used.

I was not set on using sInf regardless, hence why I had multiple definitions, and I appreciate the deconstructions of why it may be best to not use it.

As a more math question, is there a reason to consider Newton polygons over $\mathbb{Q}$ instead of $\R$?

[William Coram]

And thanks for the explanation of what lean does (or doesnt do in the case of magic). I will pay more attention to this in the future!

[Michael Stoll]

William Coram said:

As a more math question, is there a reason to consider Newton polygons over Q instead of R?

You can compute with rational numbers :smile:

[Mitchell Lee]

Think of the Newton polygon as a (convex) polyhedron (i.e. a finite intersection of half planes) rather than merely as a set. Here are some important facts about polyhedra; they are all true in any finite dimensional affine space over an ordered field.

• The convex hull of a finite set of points is a polyhedron.
• The Minkowski sum of two polyhedra is a polyhedron.

These constructions should be sufficient to define the Newton polygon; the difficulties with sInf will go away if it is defined this way.

Unfortunately, these constructions are not currently in mathlib. In fact, there is not really a definition of a "polyhedron" at all. But I think this all should be done before trying to define the Newton polygon; it would make it a lot easier.

[Mitchell Lee]

(deleted)

[Yaël Dillies]

Note that outside of mathlib these constructions do exist, so it's just a matter of upstreaming them

[Scott Carnahan]

I don't understand why we need the vertical axis coordinate to have a field structure. As far as I can tell, you only want to divide by integers.

[Michael Stoll]

Yes, an ordered ℚ-algebra should be enough.

[Yaël Dillies]

My goto assumption for this setup is [Module ℚ α]

[Michael Stoll]

You need a linear ordering to state the convexity condition.

[Joseph Myers]

It's unclear (at least to me) what the right definition of half-spaces, and thus of convex polyhedral sets, is in (an affine space over) a ℚ-module. Is a half-space defined by an affine map to ℚ having nonnegative values? Or can you take the points with rational coordinates in any convex polyhedron in a corresponding ℝ-module (i.e. use ℝ, or more generally an ordered ℚ-module, as the codomain of the affine map for defining a half-space)? Which of these more general versions of convexity (versus just doing it in real affine spaces) are actually of use?

[Mitchell Lee]

The former. This recovers the definition of a "rational polyhedron" which is useful in (e.g.) the theory of toric varieties

[William Coram]

Some progress has been made but I have a few questions that have been raised from the work.
Firstly, from Michael's suggestion I have tried a new definition of lower convex hulls as the following

structure lowerconvexhull_R2 where
  set : Set (Prod ℝ ℝ) -- Defining set of the lch
  points : ℕ → Prod ℝ ℝ -- function indexing vertices of the lch
  slopes : ℕ → EReal -- slope between i and i + 1 vertex
  relation : ∀ i : ℕ, slopes i ≠ ⊤ ∧ slopes i ≠ ⊥ →
    (points (i + 1)).2 - (points i).2 = slopes i * ((points (i + 1)).1 - (points i).1)
    -- we actually have segments touching
  slopes_increase : ∀ i : ℕ, slopes i ≤ slopes (i + 1) -- convexity condition

Apologies for still working in $\R$, I still need to change to the ordered $\mathbb{Q}$-algebras as mentioned.

Note EReal in the slopes.
When considering polynomials and not powerseries, these have a finite endpoint of the NP, but we can think of it as ending with a vertical line going up at the end point., hence it having slope '$\top$' . Likwise '$\bot$' comes from Powerseries like $1 + \sum_{i=1}^{\infty} p^{-i} x^i$. This has NewtonPolygon of the vertical line down from the origin.

This gives my first question. Do we want Newton Polygons of just restricted powerseries or all of them?

Secondly, do we care about $\top$ and $\bot$? My supervisor has suggested we could try using junk variables, but this means we could no longer use the slopes_increase part of the definition.

Thirdly, the method of finding a function that indexs the points for a restricted powerseries I have been using sInf to find the minimum of slopes from a point.
However an example like $1+∑_{n=1}^∞​ p^{l(n)} x^n$ where $l(n)$ is the floor of $\log n$, which is a restricted powerseries, also has Newton Polygon of the positive x-axis. But we cannot find a next point from $i = 2$ as $(i , \nu_p (a_i))$ is not on the line for any $i > 2$. After $(2,0)$ is the points indexing function just the constant function giving $(2,0)$ ? We could instead say $3 \mapsto (3,0)$. But now this is not in the original set of $(i , \nu_p (a_i))$, which seems a problem. (Because the vertices gives us information we will use in later theorems).

An idea me and my supervisor have had is to instead define this all for just polynomials (in other words lower convex hulls of a finite set of points). We can then say that the Newton polygon of a powerseries is then given by the family of Newton polygons of its truncated polynomials; and take the 'limit' of these - which we are unsure of how to begin formalising.

Any thoughts would be appreciated.

I also realise I have lost a lof of generality, specifically only working in dimension two right now. Could this method feasibly be extended to higher dimensions?

[Michael Stoll]

I was thinking of something along the following lines.

import Mathlib

structure NewtonPolygon (k : Type*) [LinearOrderedField k] where
  /-- The number of points -/
  n : ℕ
  /-- `x j` is the x-coordinate of the `j`th point when `0 ≤ j < n`. -/
  x : ℕ → k
  /-- `y j` is the y-coordinate of the `j`th point when `0 ≤ j < n`. -/
  y : ℕ → k
  /-- The x-coordinates are strictly increasing -/
  increasing : StrictMonoOn x (Set.Ico 0 n)
  /-- The Newton polygon is lower convex.
  This considers three successive points with indices `j`, `j+1` and `j+2`.
  (Replace `<` by `≤` if successive slopes are allowed to be equal). -/
  convex : ∀ j : ℕ, j + 2 < n →
      x j * y (j + 2) + x (j + 1) * y j  + x (j + 2) * y (j + 1) <
        x j * y (j + 1) + x (j + 1) * y (j + 2) + x (j + 2) * y j

namespace NewtonPolygon

variable {k : Type*} [LinearOrderedField k]

/-- The slopes of a Newton polygon. -/
def slope (NP : NewtonPolygon k) (j : ℕ) : k :=
  (NP.y (j + 1) - NP.y j) / (NP.x (j + 1) - NP.x j)

/-- The segments have positive (projected) length. -/
lemma length_pos (NP : NewtonPolygon k) {j : ℕ} (hj : j ∈ Set.Ico 0 (NP.n - 1)) :
    0 < NP.x (j + 1) - NP.x j := by
  rw [sub_pos]
  simp only [Set.mem_Ico, zero_le, true_and] at hj
  refine NP.increasing ?_ ?_ (lt_add_one j) <;> simp <;> omega

/-- The slopes are strictly increasing. -/
lemma slope_strictMonoOn (NP : NewtonPolygon k) : StrictMonoOn NP.slope (Set.Ico 0 (NP.n - 1)) := by
  refine strictMonoOn_of_lt_succ Set.ordConnected_Ico ?_
  intro j hj₁ hj₂ hj₃
  simp only [slope]
  have h₁ : 0 < NP.x (j + 1) - NP.x j := NP.length_pos hj₂
  have h₂ : 0 < NP.x (j + 2) - NP.x (j + 1) := NP.length_pos hj₃
  simp +arith only [Nat.succ_eq_succ, Nat.succ_eq_add_one]
  rw [div_lt_div_iff₀ h₁ h₂, ← sub_pos]
  have := NP.convex j (by simp at hj₃; omega)
  rw [← sub_pos] at this
  convert this using 1
  ring_nf -- strangely, `ring` complains that it doesn't solve the goal even though it does?

Note that the functions x and y are defined on all of ℕ, but only the values below n are relevant. This avoids hassle with subtypes (like Fin n).

[Michael Stoll]

I think it is reasonable to first consider polynomials and worry about power series later.

Also, higher dimensions are probably quite a bit more diffcult, so I would stick to polynomials in one variable.

[Kevin Buzzard]

Some kind of theory does exist in higher dimensions but I could never fathom out what it was useful for, I agree that sticking to one variable is a good idea!

[Michael Stoll]

One can consider the polytope that is the convex hull of all the exponent tuples that occur in a multivariate polynomial. For Laurent polys in two variables, the number of interior lattice points is the arithmetic genus of the curve defined by the polynomial IIRC, and there will be some statements in higher dimensions, I imagine.

But, at least as far as I am concerned, the vast majority of applications is for polynomials (or perhaps power series -- Strassmann's Theorem comes to mind) over discretely values fields, so that should be the first goal.

[Judith Ludwig]

I'm late to join the discussion but let me just add: I'm happy to see Newton polygons being developed in mathlib and I agree there are many important results for polynomials over discretely valued fields.

For what it's worth, let me mention a situation, where a more general formalism of Newton polygons is quite important, which is in the context of Fontaine's ring $\mathbb{A}_{\mathrm{inf}}$ and related rings. These rings are crucial for $p$-adic Hodge theory and for making a curve that is known as the Fargues-Fontaine curve. In the work of Fargues and Fontaine, Newton polygons enter quite crucially as they help to understand elements of these rings (and their zeroes). How does this connect back to power-series? To simplify the story: There are two versions of $\mathbb{A}_{\mathrm{inf}}$, a mixed-characteristic and an equal characteristic version. And in equal characteristic $\mathbb{A}_{\mathrm{inf}}$ is equal to a power series ring $R[[X]]$ in one variable over a valuation ring $R$, and this valuation ring is not discrete. So I can quite believe that some flexibility in the setup of Newton polygons will be useful in the future.