Units of restricted power series

Let R be a complete ultrametric normed ring with ‖1‖ = 1, and let c be positive polyradii. A restricted series f ∈ R{X/c} close to a constant a that is a multiplicative unit of R (TauCeti.IsNormMulUnit), in the sense that ‖f - a‖ < ‖a‖ for the Gauss norm, factors as

f = a * (1 - x),    x = a⁻¹ * (a - f),    ‖x‖ = ‖f - a‖ / ‖a‖ < 1,

so it is invertible with inverse given by the Neumann series ∑ₙ xⁿ a⁻¹, and it is again a multiplicative unit, of norm ‖a‖. This is the Neumann series criterion TauCeti.IsNormMulUnit.of_norm_sub_lt applied to the constant series a. No commutativity of R and no multiplicativity of its norm is needed; in particular R may have nilpotents. Over the dual numbers K[ε] the series 1 + εX is a unit although its coefficient ε may have norm one, so the converse below does not extend to such rings.

When the norm of R is multiplicative and R is nontrivial, the converse holds: a restricted series is a unit exactly when its constant coefficient is a unit and strictly dominates the weighted norm ‖aₜ‖ cᵗ of every other coefficient. Restrictedness turns these pointwise strict inequalities into a uniform one, which is what the Neumann series needs. Over a field, or any division ring, the constant coefficient need only be nonzero. These criteria hold at arbitrary positive polyradii.

Main results

• MvPowerSeries.isNormMulUnit_C: constants preserve multiplicative units.
• MvPowerSeries.isNormMulUnit_of_norm_sub_C_lt: a series within less than ‖a‖ of a constant multiplicative unit a is a multiplicative unit; MvPowerSeries.hasSum_inverse_of_norm_sub_C_lt gives its inverse as a Neumann series and MvPowerSeries.norm_inverse_of_norm_sub_C_lt computes its norm as ‖a‖⁻¹.
• MvPowerSeries.isNormMulUnit_of_norm_coeff_mul_prod_lt: a series whose constant coefficient is a multiplicative unit strictly dominating every other weighted coefficient is a multiplicative unit.
• MvPowerSeries.norm_coeff_mul_prod_lt_of_isUnit: for a multiplicative coefficient norm, the constant coefficient of a unit strictly dominates every other weighted coefficient.
• MvPowerSeries.isUnit_iff_isUnit_constantCoeff_and_norm_coeff_mul_prod_lt and, over a division ring, MvPowerSeries.isUnit_iff_constantCoeff_ne_zero_and_norm_coeff_mul_prod_lt: the units of R{X/c}.
• MvPowerSeries.forall_norm_coeff_sub_C_lt_iff: the constant coefficient strictly dominates every coefficient of f - C (constantCoeff f) iff it is nonzero and strictly dominates every other coefficient of f.

References

• F. Martin, Overconvergent subanalytic subsets in the framework of Berkovich spaces, J. Eur. Math. Soc. 18 (2016), Lemma 1.21 and Remark 1.22.
• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.1.3, Proposition 1.

theorem MvPowerSeries.isNormMulUnit_C {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] {u : R} (hu : TauCeti.IsNormMulUnit u) : TauCeti.IsNormMulUnit ⟨C u, ⋯⟩

Constant series preserve multiplicative units, since taking constant series is a norm-preserving ring homomorphism.

theorem MvPowerSeries.isNormMulUnit_of_norm_sub_C_lt {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] [CompleteSpace R] {a : R} (ha : TauCeti.IsNormMulUnit a) {f : ↥(IsRestricted.subring c)} (hf : ‖f - ⟨C a, ⋯⟩‖ < ‖a‖) : TauCeti.IsNormMulUnit f

Neumann series criterion. Over a complete ultrametric ring, a restricted series whose distance from a constant multiplicative unit a is less than ‖a‖ is a multiplicative unit.

theorem MvPowerSeries.hasSum_inverse_of_norm_sub_C_lt {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] [CompleteSpace R] {a : Rˣ} (ha : TauCeti.IsNormMulUnit ↑a) {f : ↥(IsRestricted.subring c)} (hf : ‖f - ⟨C ↑a, ⋯⟩‖ < ‖↑a‖) : HasSum (fun (n : ℕ) => (⟨C ↑a⁻¹, ⋯⟩ * (⟨C ↑a, ⋯⟩ - f)) ^ n * ⟨C ↑a⁻¹, ⋯⟩) (Ring.inverse f)

The Neumann series of the inverse. If ‖f - a‖ < ‖a‖ for a constant multiplicative unit a, then x = a⁻¹ * (a - f) has norm less than one and f⁻¹ = ∑ₙ xⁿ * a⁻¹.

theorem MvPowerSeries.norm_inverse_of_norm_sub_C_lt {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] [CompleteSpace R] {a : R} (ha : TauCeti.IsNormMulUnit a) {f : ↥(IsRestricted.subring c)} (hf : ‖f - ⟨C a, ⋯⟩‖ < ‖a‖) : ‖Ring.inverse f‖ = ‖a‖⁻¹

If ‖f - a‖ < ‖a‖ for a constant multiplicative unit a, then the inverse of f has norm ‖a‖⁻¹.

theorem MvPowerSeries.isNormMulUnit_of_norm_coeff_mul_prod_lt {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] [NormOneClass R] [CompleteSpace R] {f : ↥(IsRestricted.subring c)} (h0 : TauCeti.IsNormMulUnit (constantCoeff ↑f)) (h : ∀ (t : σ →₀ ℕ), t ≠ 0 → (‖(coeff t) ↑f‖ * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) < ‖constantCoeff ↑f‖) : TauCeti.IsNormMulUnit f

Dominant constant coefficient. Over a complete ultrametric norm-one ring, a restricted series whose constant coefficient is a multiplicative unit strictly dominating the weighted norm of every other coefficient is a multiplicative unit.

theorem MvPowerSeries.norm_coeff_mul_prod_lt_of_isUnit {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] [NormMulClass R] [Nontrivial R] {f : ↥(IsRestricted.subring c)} (hf : IsUnit f) {t : σ →₀ ℕ} (ht : t ≠ 0) : (‖(coeff t) ↑f‖ * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) < ‖constantCoeff ↑f‖

The constant coefficient of a unit dominates. For a multiplicative coefficient norm, the constant coefficient of a unit of the ring of restricted series strictly dominates the weighted norm of every other coefficient.

theorem MvPowerSeries.isUnit_iff_isUnit_constantCoeff_and_norm_coeff_mul_prod_lt {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] [NormMulClass R] [Nontrivial R] [CompleteSpace R] (f : ↥(IsRestricted.subring c)) : IsUnit f ↔ IsUnit (constantCoeff ↑f) ∧ ∀ (t : σ →₀ ℕ), t ≠ 0 → (‖(coeff t) ↑f‖ * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) < ‖constantCoeff ↑f‖

The units of the ring of restricted series. Over a complete ultrametric normed ring with multiplicative norm, a restricted series is a unit exactly when its constant coefficient is a unit and strictly dominates the weighted norm of every other coefficient.

theorem MvPowerSeries.isUnit_iff_constantCoeff_ne_zero_and_norm_coeff_mul_prod_lt {σ : Type u_1} {K : Type u_2} [NormedDivisionRing K] [IsUltrametricDist K] [CompleteSpace K] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (f : ↥(IsRestricted.subring c)) : IsUnit f ↔ constantCoeff ↑f ≠ 0 ∧ ∀ (t : σ →₀ ℕ), t ≠ 0 → (‖(coeff t) ↑f‖ * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) < ‖constantCoeff ↑f‖

The units of a Tate algebra over a division ring. Over a complete ultrametric normed division ring, for instance a field, a restricted series is a unit exactly when its constant coefficient is nonzero and strictly dominates the weighted norm of every other coefficient, that is, when the constant coefficient is the only one attaining the Gauss norm.

theorem MvPowerSeries.forall_norm_coeff_sub_C_lt_iff {σ : Type u_1} {R : Type u_2} [NormedRing R] (f : MvPowerSeries σ R) : (∀ (t : σ →₀ ℕ), ‖(coeff t) (f - C (constantCoeff f))‖ < ‖constantCoeff f‖) ↔ constantCoeff f ≠ 0 ∧ ∀ (t : σ →₀ ℕ), t ≠ 0 → ‖(coeff t) f‖ < ‖constantCoeff f‖

The constant coefficient a of a series dominates the coefficients of f - a strictly iff it is nonzero and dominates all other coefficients of f strictly.