Series of bounded degree in the distinguished variable, and polynomials over the tail ring

Freitag writes 𝒪_{n−1}[z_n : m] for the polynomials in z_n over 𝒪_{n−1} of degree < m, a free 𝒪_{n−1}-module with basis 1, z_n, …, z_n^{m−1} [Fre17, Ch. I, §10]. With the distinguished variable x_0 of the Weierstrass theory (splitFirst, liftTail, weierstrassPoly), a series f in m + 1 variables has x_0-degree < N (DegLt N f) if coeff ν f = 0 whenever N ≤ ν 0, the remainder condition of the Weierstrass division theorems. This module collects:

• the algebra of DegLt (sums, products with the additive bound, tail series, X 0-powers, Weierstrass polynomials);
• the correspondence ofPoly P := splitFirst⁻¹ (P : PowerSeries A), A = MvPowerSeries (Fin m) K the tail ring: polynomials in x_0 over the tail ring as series, weierstrassPoly e c = ofPoly (weierstrassPolynomial e c), and a series of x_0-degree < N is ofPoly of its truncation;
• a monic polynomial in x_0 of degree e (a weierstrassPoly e c without the vanishing condition on c) is x_0-regular of some order d' ≤ e (exists_isRegularIn_weierstrassPoly): the "normalized polynomials" of Oka's lemma are regular, so the Weierstrass theorems apply to them.

Every statement is bookkeeping for Oka's lemma (Lemma.lean) and for the polynomial sections of the coherence theorem (Hironaka/AnalyticSpace/Oka).

def Analytic.DegLt {K : Type u_1} [RCLike K] {m : ℕ} (N : ℕ) (f : MvPowerSeries (Fin (m + 1)) K) : Prop

f has x_0-degree < N: every monomial with x_0-exponent ≥ N has coefficient 0.

Equations

• Analytic.DegLt N f = ∀ (ν : Fin (m + 1) →₀ ℕ), N ≤ ν 0 → (MvPowerSeries.coeff ν) f = 0

theorem Analytic.DegLt.mono {K : Type u_1} [RCLike K] {m N N' : ℕ} (h : N ≤ N') {f : MvPowerSeries (Fin (m + 1)) K} (hf : DegLt N f) : DegLt N' f

theorem Analytic.DegLt.zero {K : Type u_1} [RCLike K] {m : ℕ} (N : ℕ) : DegLt N 0

theorem Analytic.DegLt.add {K : Type u_1} [RCLike K] {m N : ℕ} {f g : MvPowerSeries (Fin (m + 1)) K} (hf : DegLt N f) (hg : DegLt N g) : DegLt N (f + g)

theorem Analytic.DegLt.neg {K : Type u_1} [RCLike K] {m N : ℕ} {f : MvPowerSeries (Fin (m + 1)) K} (hf : DegLt N f) : DegLt N (-f)

theorem Analytic.DegLt.sub {K : Type u_1} [RCLike K] {m N : ℕ} {f g : MvPowerSeries (Fin (m + 1)) K} (hf : DegLt N f) (hg : DegLt N g) : DegLt N (f - g)

theorem Analytic.DegLt.sum {K : Type u_1} [RCLike K] {m N : ℕ} {ι : Type u_2} (s : Finset ι) {f : ι → MvPowerSeries (Fin (m + 1)) K} (hf : ∀ i ∈ s, DegLt N (f i)) : DegLt N (∑ i ∈ s, f i)

theorem Analytic.DegLt.mul {K : Type u_1} [RCLike K] {m a b : ℕ} {f g : MvPowerSeries (Fin (m + 1)) K} (hf : DegLt a f) (hg : DegLt b g) : DegLt (a + b) (f * g)

The x_0-degrees add under multiplication (< a and < b give < a + b; the sharp form < a + b − 1 is mul_succ).

theorem Analytic.DegLt.mul_succ {K : Type u_1} [RCLike K] {m a b : ℕ} {f g : MvPowerSeries (Fin (m + 1)) K} (hf : DegLt (a + 1) f) (hg : DegLt (b + 1) g) : DegLt (a + b + 1) (f * g)

The sharp form: degrees ≤ a and ≤ b give degree ≤ a + b.

theorem Analytic.DegLt.one_mul {K : Type u_1} [RCLike K] {m N : ℕ} {f g : MvPowerSeries (Fin (m + 1)) K} (hf : DegLt 1 f) (hg : DegLt N g) : DegLt N (f * g)

A series of x_0-degree < 1 (a tail series) times a series of x_0-degree < N.

theorem Analytic.DegLt.smul {K : Type u_1} [RCLike K] {m N : ℕ} (c : K) {f : MvPowerSeries (Fin (m + 1)) K} (hf : DegLt N f) : DegLt N (c • f)

theorem Analytic.degLt_liftTail {K : Type u_1} [RCLike K] {m : ℕ} (c : MvPowerSeries (Fin m) K) : DegLt 1 (liftTail c)

theorem Analytic.degLt_X_zero_pow {K : Type u_1} [RCLike K] {m : ℕ} (k : ℕ) : DegLt (k + 1) (MvPowerSeries.X 0 ^ k)

theorem Analytic.degLt_weierstrassPoly {K : Type u_1} [RCLike K] {m : ℕ} (e : ℕ) (c : Fin e → MvPowerSeries (Fin m) K) : DegLt (e + 1) (weierstrassPoly e c)

A monic polynomial in x_0 of degree e with tail coefficients has x_0-degree < e + 1.

theorem Analytic.degLt_iff_splitFirst {K : Type u_1} [RCLike K] {m N : ℕ} {f : MvPowerSeries (Fin (m + 1)) K} : DegLt N f ↔ ∀ (k : ℕ), N ≤ k → (PowerSeries.coeff k) ((splitFirst K m) f) = 0

DegLt through the split of the first variable: the coefficients of x_0^k, k ≥ N, vanish.

noncomputable def Analytic.ofPolyHom {K : Type u_1} [RCLike K] {m : ℕ} : Polynomial (MvPowerSeries (Fin m) K) →+* MvPowerSeries (Fin (m + 1)) K

Polynomials in x_0 over the tail ring A = 𝒪_{n−1}, as series in all variables: the ring homomorphism A[X] → 𝒪_n, X ↦ x_0, C a ↦ liftTail a.

Equations

• Analytic.ofPolyHom = (Analytic.splitFirst K m).symm.toRingEquiv.toRingHom.comp Polynomial.coeToPowerSeries.ringHom

noncomputable def Analytic.ofPoly {K : Type u_1} [RCLike K] {m : ℕ} (P : Polynomial (MvPowerSeries (Fin m) K)) : MvPowerSeries (Fin (m + 1)) K

The tail ring A = 𝒪_{n−1}-side polynomial P in x_0, as a series in all variables.

Equations

• Analytic.ofPoly P = Analytic.ofPolyHom P

theorem Analytic.ofPoly_def {K : Type u_1} [RCLike K] {m : ℕ} (P : Polynomial (MvPowerSeries (Fin m) K)) : ofPoly P = (splitFirst K m).symm ↑P

theorem Analytic.splitFirst_ofPoly {K : Type u_1} [RCLike K] {m : ℕ} (P : Polynomial (MvPowerSeries (Fin m) K)) : (splitFirst K m) (ofPoly P) = ↑P

theorem Analytic.ofPoly_add {K : Type u_1} [RCLike K] {m : ℕ} (P Q : Polynomial (MvPowerSeries (Fin m) K)) : ofPoly (P + Q) = ofPoly P + ofPoly Q

theorem Analytic.ofPoly_mul {K : Type u_1} [RCLike K] {m : ℕ} (P Q : Polynomial (MvPowerSeries (Fin m) K)) : ofPoly (P * Q) = ofPoly P * ofPoly Q

theorem Analytic.ofPoly_neg {K : Type u_1} [RCLike K] {m : ℕ} (P : Polynomial (MvPowerSeries (Fin m) K)) : ofPoly (-P) = -ofPoly P

theorem Analytic.ofPoly_zero {K : Type u_1} [RCLike K] {m : ℕ} : ofPoly 0 = 0

theorem Analytic.ofPoly_one {K : Type u_1} [RCLike K] {m : ℕ} : ofPoly 1 = 1

theorem Analytic.ofPoly_pow {K : Type u_1} [RCLike K] {m : ℕ} (P : Polynomial (MvPowerSeries (Fin m) K)) (k : ℕ) : ofPoly (P ^ k) = ofPoly P ^ k

theorem Analytic.ofPoly_sum {K : Type u_1} [RCLike K] {m : ℕ} {ι : Type u_2} (s : Finset ι) (P : ι → Polynomial (MvPowerSeries (Fin m) K)) : ofPoly (∑ i ∈ s, P i) = ∑ i ∈ s, ofPoly (P i)

theorem Analytic.ofPoly_X {K : Type u_1} [RCLike K] {m : ℕ} : ofPoly Polynomial.X = MvPowerSeries.X 0

theorem Analytic.ofPoly_C {K : Type u_1} [RCLike K] {m : ℕ} (a : MvPowerSeries (Fin m) K) : ofPoly (Polynomial.C a) = liftTail a

theorem Analytic.ofPoly_weierstrassPolynomial {K : Type u_1} [RCLike K] {m : ℕ} (e : ℕ) (c : Fin e → MvPowerSeries (Fin m) K) : ofPoly (weierstrassPolynomial e c) = weierstrassPoly e c

theorem Analytic.degLt_ofPoly {K : Type u_1} [RCLike K] {m : ℕ} (P : Polynomial (MvPowerSeries (Fin m) K)) : DegLt (P.natDegree + 1) (ofPoly P)

ofPoly P has x_0-degree < natDegree P + 1.

theorem Analytic.degLt_ofPoly_of_natDegree_lt {K : Type u_1} [RCLike K] {m N : ℕ} {P : Polynomial (MvPowerSeries (Fin m) K)} (hP : P.natDegree < N) : DegLt N (ofPoly P)

ofPoly of a polynomial of degree < N (as a natural-number bound) has x_0-degree < N.

noncomputable def Analytic.toPoly {K : Type u_1} [RCLike K] {m : ℕ} (N : ℕ) (f : MvPowerSeries (Fin (m + 1)) K) : Polynomial (MvPowerSeries (Fin m) K)

The truncation of a series of x_0-degree < N, as a polynomial over the tail ring.

Equations

• Analytic.toPoly N f = (PowerSeries.trunc N) ((Analytic.splitFirst K m) f)

theorem Analytic.ofPoly_toPoly {K : Type u_1} [RCLike K] {m N : ℕ} {f : MvPowerSeries (Fin (m + 1)) K} (hf : DegLt N f) : ofPoly (toPoly N f) = f

theorem Analytic.natDegree_toPoly_lt {K : Type u_1} [RCLike K] {m : ℕ} (N : ℕ) (f : MvPowerSeries (Fin (m + 1)) K) (hN : 0 < N) : (toPoly N f).natDegree < N

theorem Analytic.exists_isRegularIn_ofPoly {K : Type u_1} [RCLike K] {m : ℕ} {Q : Polynomial (MvPowerSeries (Fin m) K)} (hQ : Q.Monic) : ∃ d' ≤ Q.natDegree, IsRegularIn (ofPoly Q) d'

A "normalized polynomial" in the sense of [Fre17, Ch. I, §10], ofPoly Q for a monic Q in x_0 over the tail ring, is x_0-regular of some order d' ≤ natDegree Q (the order of Q with its coefficients reduced modulo the maximal ideal), so the Weierstrass division and preparation theorems apply to it.

theorem Analytic.exists_isRegularIn_weierstrassPoly {K : Type u_1} [RCLike K] {m : ℕ} (e : ℕ) (c : Fin e → MvPowerSeries (Fin m) K) : ∃ d' ≤ e, IsRegularIn (weierstrassPoly e c) d'