Restricted power series as a normed ring

Let R be a nonarchimedean normed ring and c a positive real number. The ring PowerSeries.IsRestricted.subring c of power series ∑ aₙ Xⁿ over R with ‖aₙ‖ cⁿ → 0 carries the Gauss norm ‖∑ aₙ Xⁿ‖ = sup ‖aₙ‖ cⁿ. This file makes it a normed ring for that norm, and shows that the norm inherits the properties of the norm on R that the theory of Tate algebras uses:

• it is ultrametric;
• it is multiplicative when the norm on R is;
• it is complete when R is complete.

At the unit radius over a complete nonarchimedean field K, the result is the Tate algebra K⟨X⟩ with its Gauss norm. Iterating the construction, the ring of series in one more variable restricted over K⟨X₁, …, Xₙ₋₁⟩ is again complete, ultrametric and multiplicatively normed. This is the setting in which Bosch–Güntzer–Remmert apply Weierstrass division in n variables, and it is exactly the hypothesis set of TauCeti.PowerSeries.IsDistinguished.existsUnique_mul_add_eq_subring.

The radius is supplied as an instance argument [Fact (0 < c)]; at the unit radius it is found automatically.

Main results

• TauCeti.PowerSeries.norm_eq_gaussNorm: the norm of a restricted series is its Gauss norm.
• TauCeti.PowerSeries.norm_le_iff: the norm is bounded by r ≥ 0 exactly when every weighted coefficient norm ‖aₙ‖ cⁿ is.
• TauCeti.PowerSeries.norm_C, TauCeti.PowerSeries.norm_X: constants keep their norm, and the variable has norm c.
• TauCeti.PowerSeries.nnnorm_eq_gaussValuation: the norm is the Gauss valuation TauCeti.PowerSeries.gaussValuation.
• Instances: NormedRing, NormedCommRing, IsUltrametricDist, NormOneClass, NormMulClass and CompleteSpace on PowerSeries.IsRestricted.subring c.

Apply the norm lemmas by qualified name, for example TauCeti.PowerSeries.norm_eq_gaussNorm f. The normed and completeness instances are supplied by the multivariate construction in TauCeti.RingTheory.MvPowerSeries.TateAlgebra.Basic. Elements of the restricted subring have type Subtype, rather than a new Tate algebra type.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.1.1 and §5.2.1.

@[instance_reducible]

noncomputable instance TauCeti.PowerSeries.instNormedRingIsRestrictedSubring {R : Type u_1} [NormedRing R] [IsUltrametricDist R] (c : ℝ) [hc : Fact (0 < c)] : NormedRing ↥(PowerSeries.IsRestricted.subring c)

The multivariate Gauss norm, specialized to the constant polyradius on Unit. Mathlib's univariate subring is a semireducible wrapper for instance matching, so this specialization supplies the same normed-ring data explicitly.

Equations

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

theorem TauCeti.PowerSeries.norm_eq_gaussNorm {R : Type u_1} [NormedRing R] [IsUltrametricDist R] {c : ℝ} [hc : Fact (0 < c)] (f : ↥(PowerSeries.IsRestricted.subring c)) : ‖f‖ = PowerSeries.gaussNorm norm c ↑f

The norm of a restricted power series is its Gauss norm.

theorem TauCeti.PowerSeries.norm_coeff_mul_pow_le {R : Type u_1} [NormedRing R] [IsUltrametricDist R] {c : ℝ} [hc : Fact (0 < c)] (f : ↥(PowerSeries.IsRestricted.subring c)) (n : ℕ) : ‖(PowerSeries.coeff n) ↑f‖ * c ^ n ≤ ‖f‖

Each weighted coefficient norm ‖aₙ‖ cⁿ of a restricted series is bounded by its norm.

theorem TauCeti.PowerSeries.norm_le_iff {R : Type u_1} [NormedRing R] [IsUltrametricDist R] {c : ℝ} [hc : Fact (0 < c)] {f : ↥(PowerSeries.IsRestricted.subring c)} {r : ℝ} (hr : 0 ≤ r) : ‖f‖ ≤ r ↔ ∀ (n : ℕ), ‖(PowerSeries.coeff n) ↑f‖ * c ^ n ≤ r

The norm of a restricted series is bounded by a nonnegative r exactly when every weighted coefficient norm ‖aₙ‖ cⁿ is.

@[simp]

theorem TauCeti.PowerSeries.norm_C {R : Type u_1} [NormedRing R] [IsUltrametricDist R] {c : ℝ} [hc : Fact (0 < c)] (a : R) : ‖⟨PowerSeries.C a, ⋯⟩‖ = ‖a‖

A constant series has the norm of its coefficient.

@[simp]

theorem TauCeti.PowerSeries.norm_X {R : Type u_1} [NormedRing R] [IsUltrametricDist R] {c : ℝ} [hc : Fact (0 < c)] [NormOneClass R] : ‖⟨PowerSeries.X, ⋯⟩‖ = c

The variable has norm c.

theorem TauCeti.PowerSeries.nnnorm_eq_gaussValuation {R : Type u_1} [NormedRing R] [IsUltrametricDist R] {c : ℝ} [hc : Fact (0 < c)] [NormMulClass R] [NormOneClass R] (f : ↥(PowerSeries.IsRestricted.subring c)) : ‖f‖₊ = (gaussValuation ⋯) f

The norm of a restricted series is its Gauss valuation.

instance TauCeti.PowerSeries.instIsUltrametricDistSubtypePowerSeriesMemSubringSubring_tauCeti {R : Type u_1} [NormedRing R] [IsUltrametricDist R] (c : ℝ) [hc : Fact (0 < c)] : IsUltrametricDist ↥(PowerSeries.IsRestricted.subring c)

instance TauCeti.PowerSeries.instNormOneClassSubtypePowerSeriesMemSubringSubring_tauCeti {R : Type u_1} [NormedRing R] [IsUltrametricDist R] (c : ℝ) [hc : Fact (0 < c)] [NormOneClass R] : NormOneClass ↥(PowerSeries.IsRestricted.subring c)

instance TauCeti.PowerSeries.instNormMulClassSubtypePowerSeriesMemSubringSubring_tauCeti {R : Type u_1} [NormedRing R] [IsUltrametricDist R] (c : ℝ) [hc : Fact (0 < c)] [NormMulClass R] : NormMulClass ↥(PowerSeries.IsRestricted.subring c)

The multiplicative multivariate Gauss norm specialized to one variable.

instance TauCeti.PowerSeries.instCompleteSpaceSubtypePowerSeriesMemSubringSubring_tauCeti {R : Type u_1} [NormedRing R] [IsUltrametricDist R] (c : ℝ) [hc : Fact (0 < c)] [CompleteSpace R] : CompleteSpace ↥(PowerSeries.IsRestricted.subring c)

Completeness of the multivariate Gauss norm specialized to one variable.

@[instance_reducible]

noncomputable instance TauCeti.PowerSeries.instNormedCommRingIsRestrictedSubring {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] (c : ℝ) [Fact (0 < c)] : NormedCommRing ↥(PowerSeries.IsRestricted.subring c)

The normed commutative multivariate restricted-series ring specialized to one variable.

Equations

• TauCeti.PowerSeries.instNormedCommRingIsRestrictedSubring c = { toNormedRing := TauCeti.PowerSeries.instNormedRingIsRestrictedSubring c, mul_comm := ⋯ }