Quotients by distinguished restricted power series

Weierstrass division identifies the quotient of restricted series by a distinguished monic polynomial with its polynomial quotient. Preparation extends this description to any distinguished restricted series with a unit dominant coefficient. In particular, these quotients are finite free over the coefficient ring. This is the finite-module step in the induction proving noetherianity of Tate algebras: after making a series distinguished in the last variable, its quotient is finite over the Tate algebra in the remaining variables.

The radius may be any positive real number, and the coefficients may lie in a complete ultrametric normed commutative ring with multiplicative norm. No noetherian or field hypothesis is required.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §§5.2.1–5.2.2 and §5.2.6.

The polynomial-to-series quotient comparison follows the construction of Mathlib's Polynomial.IsDistinguishedAt.algEquivQuotient, for adically complete rings and unrestricted series. Here Gauss-norm Weierstrass division supplies the existence and uniqueness instead.

theorem TauCeti.PowerSeries.IsDistinguished.polynomialToRestricted_dvd_iff {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s : ℕ} {p : Polynomial R} (hp : IsDistinguished c s ↑p) (hc : 0 < c) (hm : p.IsMonicOfDegree s) (g : Polynomial R) : (polynomialToRestricted c) p ∣ (polynomialToRestricted c) g ↔ p ∣ g

Divisibility of polynomials by a distinguished monic polynomial is unchanged on passing to restricted series. The assertion needs uniqueness of division, but not completeness.

noncomputable def TauCeti.PowerSeries.IsDistinguished.polynomialQuotientEquiv {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s : ℕ} {p : Polynomial R} [CompleteSpace R] (hp : IsDistinguished c s ↑p) (hc : 0 < c) (hm : p.IsMonicOfDegree s) : (Polynomial R ⧸ Ideal.span {p}) ≃ₐ[R] ↥(PowerSeries.IsRestricted.subring c) ⧸ Ideal.span {(polynomialToRestricted c) p}

The inclusion of polynomials induces the quotient comparison for a distinguished monic polynomial. Its inverse sends a series class to the class of its Weierstrass remainder.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PowerSeries.IsDistinguished.polynomialQuotientEquiv_mk {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s : ℕ} {p : Polynomial R} [CompleteSpace R] (hp : IsDistinguished c s ↑p) (hc : 0 < c) (hm : p.IsMonicOfDegree s) (g : Polynomial R) : (hp.polynomialQuotientEquiv hc hm) ((Ideal.Quotient.mk (Ideal.span {p})) g) = (Ideal.Quotient.mk (Ideal.span {(polynomialToRestricted c) p})) ((polynomialToRestricted c) g)

On a polynomial representative, the comparison is the usual polynomial inclusion.

@[simp]

theorem TauCeti.PowerSeries.IsDistinguished.polynomialQuotientEquiv_symm_mk {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s : ℕ} {p : Polynomial R} [CompleteSpace R] (hp : IsDistinguished c s ↑p) (hc : 0 < c) (hm : p.IsMonicOfDegree s) (g : Polynomial R) : (hp.polynomialQuotientEquiv hc hm).symm ((Ideal.Quotient.mk (Ideal.span {(polynomialToRestricted c) p})) ((polynomialToRestricted c) g)) = (Ideal.Quotient.mk (Ideal.span {p})) g

The inverse comparison sends the class of a polynomial to its polynomial quotient class.

theorem TauCeti.PowerSeries.IsDistinguished.polynomialQuotientEquiv_symm_mk_of_mul_add_eq {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s : ℕ} {p : Polynomial R} [CompleteSpace R] (hp : IsDistinguished c s ↑p) (hc : 0 < c) (hm : p.IsMonicOfDegree s) (g q r : ↥(PowerSeries.IsRestricted.subring c)) (hr : ∀ (n : ℕ), s ≤ n → (PowerSeries.coeff n) ↑r = 0) (hqr : q * (polynomialToRestricted c) p + r = g) : (hp.polynomialQuotientEquiv hc hm).symm ((Ideal.Quotient.mk (Ideal.span {(polynomialToRestricted c) p})) g) = (Ideal.Quotient.mk (Ideal.span {p})) ((PowerSeries.trunc s) ↑r)

Given a Weierstrass decomposition of any restricted series, the inverse comparison sends its class to the polynomial quotient class of the truncated remainder.

theorem TauCeti.PowerSeries.IsDistinguished.exists_polynomialQuotientEquiv {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s : ℕ} [CompleteSpace R] {f : ↥(PowerSeries.IsRestricted.subring c)} (hf : IsDistinguished c s ↑f) (hc : 0 < c) (hu : IsUnit ((PowerSeries.coeff s) ↑f)) : ∃ (p : Polynomial R), p.IsMonicOfDegree s ∧ Nonempty ((Polynomial R ⧸ Ideal.span {p}) ≃ₐ[R] ↥(PowerSeries.IsRestricted.subring c) ⧸ Ideal.span {f})

A distinguished restricted series with a unit dominant coefficient has the same quotient algebra as a monic polynomial of its distinguished degree.

theorem TauCeti.PowerSeries.IsDistinguished.finite_quotient {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s : ℕ} [CompleteSpace R] {f : ↥(PowerSeries.IsRestricted.subring c)} (hf : IsDistinguished c s ↑f) (hc : 0 < c) (hu : IsUnit ((PowerSeries.coeff s) ↑f)) : Module.Finite R (↥(PowerSeries.IsRestricted.subring c) ⧸ Ideal.span {f})

The quotient by a distinguished restricted series with a unit dominant coefficient is a finite module over the coefficient ring.

theorem TauCeti.PowerSeries.IsDistinguished.free_quotient {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s : ℕ} [CompleteSpace R] {f : ↥(PowerSeries.IsRestricted.subring c)} (hf : IsDistinguished c s ↑f) (hc : 0 < c) (hu : IsUnit ((PowerSeries.coeff s) ↑f)) : Module.Free R (↥(PowerSeries.IsRestricted.subring c) ⧸ Ideal.span {f})

The quotient by a distinguished restricted series with a unit dominant coefficient is free over the coefficient ring.