The ideals of the ring of restricted power series in one variable

Over a complete nonarchimedean field K and at a positive radius c, the power series restricted at c form the subring PowerSeries.IsRestricted.subring c of K⟦X⟧: the Tate algebra of the closed disc of radius c, which is the usual K⟨X⟩ when c = 1. This file determines its ideals. Every ideal is principal, so the ring is noetherian, and a nonzero ideal is generated by a monic polynomial.

Weierstrass division is the Euclidean algorithm behind this. A nonzero restricted series is distinguished of exactly one degree at c, and dividing by an element of an ideal whose distinguished degree is least leaves a remainder that is a polynomial of degree smaller still; such a remainder lies in the ideal only if it vanishes. Weierstrass preparation then replaces the generator by a monic polynomial of the same degree.

Noetherianity of the Tate algebra in several variables is proved by induction on their number, the inductive step dividing with coefficients in the Tate algebra of one variable fewer. The one-variable case proved here is the base of that induction.

Main results

• TauCeti.PowerSeries.IsDistinguished.span_singleton_eq_of_forall_le and TauCeti.PowerSeries.IsDistinguished.le_of_mem_span_singleton: an element of an ideal whose distinguished degree is least generates that ideal, and conversely a generator has least distinguished degree.
• TauCeti.PowerSeries.isPrincipalIdealRing_isRestricted_subring: every ideal of the ring of restricted power series is principal. Being a subring of K⟦X⟧ over a field, the ring is also an integral domain, so it is a principal ideal domain.
• TauCeti.PowerSeries.isNoetherianRing_isRestricted_subring: the ring is noetherian.
• TauCeti.PowerSeries.exists_isMonicOfDegree_span_singleton_eq: a nonzero ideal is generated by a monic polynomial, distinguished of its own degree.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.6, the noetherianity of the Tate algebra in any number of variables, of which the one-variable case is proved here, and §5.2.2, Theorem 1, the Weierstrass preparation theorem behind the monic generator.

theorem TauCeti.PowerSeries.IsDistinguished.le_of_mem_span_singleton {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s t : ℕ} (hc : 0 < c) {f g : ↥(PowerSeries.IsRestricted.subring c)} (hf : IsDistinguished c s ↑f) (hg : IsDistinguished c t ↑g) (hmem : g ∈ Ideal.span {f}) : s ≤ t

A generator has least distinguished degree. A nonzero multiple of f inside the ring of series restricted at a positive radius is distinguished of a degree at least that of f, because distinguished degrees add along a product. This is the converse of TauCeti.PowerSeries.IsDistinguished.span_singleton_eq_of_forall_le: together the two say that the distinguished degree of a generator of an ideal is the least one occurring in that ideal.

theorem TauCeti.PowerSeries.IsDistinguished.span_singleton_eq_of_forall_le {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {c : ℝ} {s : ℕ} (hc : 0 < c) {I : Ideal ↥(PowerSeries.IsRestricted.subring c)} {f : ↥(PowerSeries.IsRestricted.subring c)} (hfI : f ∈ I) (hf : IsDistinguished c s ↑f) (hmin : ∀ g ∈ I, ∀ (t : ℕ), IsDistinguished c t ↑g → s ≤ t) : Ideal.span {f} = I

An element of least distinguished degree generates. If f lies in an ideal I of the ring of series restricted at a positive radius c, is distinguished of degree s, and no member of I is distinguished of a smaller degree, then f generates I. Dividing a member of I by f leaves a remainder in I of strictly smaller distinguished degree, so the remainder vanishes.

theorem TauCeti.PowerSeries.isPrincipalIdealRing_isRestricted_subring {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {c : ℝ} (hc : 0 < c) : IsPrincipalIdealRing ↥(PowerSeries.IsRestricted.subring c)

The ring of restricted power series in one variable is a principal ideal ring. Over a complete nonarchimedean field and at a positive radius, every ideal of the ring of restricted series is generated by one element: a member of least distinguished degree. Being a subring of K⟦X⟧ over a field, the ring is also an integral domain, so it is a principal ideal domain.

theorem TauCeti.PowerSeries.isNoetherianRing_isRestricted_subring {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {c : ℝ} (hc : 0 < c) : IsNoetherianRing ↥(PowerSeries.IsRestricted.subring c)

The ring of restricted power series in one variable is noetherian, over a complete nonarchimedean field and at a positive radius.

theorem TauCeti.PowerSeries.exists_isMonicOfDegree_span_singleton_eq {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {c : ℝ} (hc : 0 < c) {I : Ideal ↥(PowerSeries.IsRestricted.subring c)} (hI : I ≠ ⊥) : ∃ (g : ↥(PowerSeries.IsRestricted.subring c)) (ω : Polynomial K) (n : ℕ), ω.IsMonicOfDegree n ∧ IsDistinguished c n ↑ω ∧ ↑g = ↑ω ∧ Ideal.span {g} = I

A nonzero ideal of the ring of restricted power series is generated by a monic polynomial. Over a complete nonarchimedean field and at a positive radius c, a nonzero ideal has a generator g whose underlying series is a monic polynomial ω, distinguished of its own degree n; by TauCeti.PowerSeries.IsDistinguished.le_of_mem_span_singleton, n is then the least distinguished degree occurring in the ideal.