Weierstrass Preparation Theorem

Stream: mathlib4

[William Coram]

I am working towards formalising the padic Weierstrass Preparation Theorem. Before I get too deep into it I wanted to check peoples opinions on some of my early definitions.

Firstly, I have defined convergent powerseries as

structure PowerSeries_restricted_c (R : Type*) (c : ℝ) (h  :  0 < c)  [NormedRing R] where
  function : PowerSeries R
  convergence : Tendsto (fun (i : ℕ) => (norm (coeff R i function)) * c^i) atTop (𝓝 0)

Then I have defined the following which is the generalisation of Gauss' norm (when c = 1) - for now I am working over $\mathbb{Q}_p$ but I do want to generalise this to $\mathbb{C}_p$. I do not have a good name for this - and am open to recommendations.

noncomputable
def function : (PowerSeries ℚ_[p])  → ℝ :=
  fun (f : PowerSeries ℚ_[p]) => sSup {padicNormE (coeff _ i f) * c^i | (i : ℕ)}

Note the sSup and not max, this is because I am unsure if there is an implementation of max on infinite sets in Lean.
I give lemmas saying the sSup exists and is attained ( padicNormE (coeff _ i f) * c^i is bounded via convergence property and we can then choose a relevant finset which contained the max and take its finset max), it just depends if people think this should be in the definition or outside of it.

Thus far (modulo some tedious sorrys and showing the convergent powerseries are actually a ring ) I have made progress towards showing this is a norm on PowerSeries and an absolute value on polynomials, and have started working towards the proof of the Theorem (via Gouveas p-adic Numbers book).

As mentioned above, do people think these definitions seem okay, or is there something they think may be better?

[Yakov Pechersky]

We have docs#FormalMultilinearSeries that have API for radii of convergence

[Yakov Pechersky]

For generalization, how about a docs#NontriviallyNormedField that docs#IsUltrametricDist

[William Coram]

And for reference here is the current statement of the Thm. It looks horrible and I probably should break it apart into smaller parts.

theorem Weierstrass_preparation_theorem (hc : 0 < c) (f : PowerSeries_restricted_c ℚ_[p] c) (hN : ∃ N : ℕ,
    (cNorm c p f.1 = padicNormE (coeff ℚ_[p] N f.1) * c^N) ∧ (∀ n : ℕ, N < n →
    (padicNormE (coeff _ N f.1) * c^n ) ≤ cNorm c p f.1 )) :
    ∃ (g : Polynomial ℚ_[p]), Polynomial.degree g = (N : ℕ) ∧ ∃ (h : PowerSeries_restricted_c ℚ_[p] c),
    coeff ℚ_[p] 1 h.1 = 1 ∧ f.1 = g * h.1 ∧ cNorm c p g = padicNormE (Polynomial.coeff g N) * c^N ∧ (cNorm
    c p (h - 1).1) < 1 ∧ (cNorm c p (f - PolyToPowerSeries_restricted c p g).1) < 1  := by
  sorry

[Kevin Buzzard]

Very old (Lean 3) thread: #new members > subtypes @ 💬

I think we want $\mathbb{Z}_p\langle T\rangle$ so probably you shouldn't restrict to fields. You want some commutative ring with some nonarch norm probably.

[Yakov Pechersky]

Then it would be NormedRing and NormOneClass and IsUltrametricDist, normed rings in Mathlib don't require multiplicativity of norms, only submultiplicativity

[Junyan Xu]

#21944 feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring has been opened 5 days ago.

[Junyan Xu]

cc @Nailin Guan

[Nailin Guan]

The version for DVR is in #21859 # feat(RingTheory/Powerseries): Weierstrass preparation

[Nailin Guan]

I reference the proof from GTM 083 chapter7 section1, however I didn't develope the relevant lemma and the version for fields, maybe the DVR version need some change?

[Yakov Pechersky]

Ideally we'd link the IsAdicComplete results with the locally compact iff complete and DVR and finite residue field in #16733

[Nailin Guan]

Yakov Pechersky said:

Ideally we'd link the IsAdicComplete results with the locally compact iff complete and DVR and finite residue field in #16733

My PR is not yet the ideal statement, as some uniqueness are a bit weak(but actually equivalent), so I don't mind to have some change :smile:

[Nailin Guan]

William Coram said:

And for reference here is the current statement of the Thm. It looks horrible and I probably should break it apart into smaller parts.

theorem Weierstrass_preparation_theorem (hc : 0 < c) (f : PowerSeries_restricted_c ℚ_[p] c) (hN : ∃ N : ℕ,
    (cNorm c p f.1 = padicNormE (coeff ℚ_[p] N f.1) * c^N) ∧ (∀ n : ℕ, N < n →
    (padicNormE (coeff _ N f.1) * c^n ) ≤ cNorm c p f.1 )) :
    ∃ (g : Polynomial ℚ_[p]), Polynomial.degree g = (N : ℕ) ∧ ∃ (h : PowerSeries_restricted_c ℚ_[p] c),
    coeff ℚ_[p] 1 h.1 = 1 ∧ f.1 = g * h.1 ∧ cNorm c p g = padicNormE (Polynomial.coeff g N) * c^N ∧ (cNorm
    c p (h - 1).1) < 1 ∧ (cNorm c p (f - PolyToPowerSeries_restricted c p g).1) < 1  := by
  sorry

Sorry that I can't get the informal statement clearly from this, could you give some reference about it? Thank you. It is a bit different from what I know currently.

[William Coram]

Nailin Guan said:

Sorry that I can't get the informal statement clearly from this, could you give some reference about it? Thank you. It is a bit different from what I know currently.

Its Theorem 7.2.10 In Gouvea - padic Numbers

[Kevin Buzzard]

For Weierstrass prep I think we should formalize the version in Bosch--Guentzer--Remmert. Let $k$ be a field complete with respect to a nontrivial nonarch norm, let $T_n$ be $k\langle X_1,X_2,\ldots,X_n\rangle$ be the Tate algebra in a finite number of variables. If $g=\sum_{i=0}^{\infty}g_i(X_1,X_2,\ldots,X_{n-1})X_n^i\in T_n$ with the $g_i\in T_{n-1}$ then we say $g$ is "$X_n$-distinguished of degree $s$" if $g_s$ is a unit, $|g_s|=|g|$ and $|g_s|>|g_r|$ for all $r>s$. The theorem is that if $g$ is $X_n$-distinguished of degree $s$ then we can write $g=u\omega$ with $u\in T_n^\times$ and $\omega\in T_{n-1}[X_n]$ a polynomial of degree $s$ with $|\omega|=1$.

[Riccardo Brasca]

Late to the party, but what is the link with #21944?

[Nailin Guan]

I think I should state my statement in #21944 here for convenience:
For a complete local ring R, every f a formal powerseries over R, if not all coefficient is in the maxiaml ideal then it can be factored into the product of a distinguish polynomial (monic and other coeficient in the maximal ideal) and an unit

[Nailin Guan]

These are pretty different as I only consider formal powerseries, are they somehow related?

[Kevin Buzzard]

Yes they are two different theorems! One is about open discs, one is about closed discs. But historically they are both called Weierstrass Prep.

[William Coram]

Kevin Buzzard said:

For Weierstrass prep I think we should formalize the version in Bosch--Guentzer--Remmert.

This if specifically for the Gauss norm (i.e. c = 1 in my function) right? Is this something we would wish to generalise to these other norms?
From Gouvea's book where he initially proves W.P.T for c = 1, the proof for positive c is not immediate but requires adaptation of a few lemmas. Has a similar thing been done for BGR's version or will the generalised version have to be done from scratch (maybe its in the book, but I have not had time to look closely yet)?

[Kevin Buzzard]

I don't have access to the book right now but my money would be on the proof starting "reduce to the case $|g|=1$ by rescaling and then reduce mod max ideal of integers of k"

[Michael Stoll]

You may need to extend your field to be able to rescale (the absolute value is usually not surjective).

[Kevin Buzzard]

I agree in general but for the statement I gave above with Tate algebras I think we don't need to do this