Multiplicative units of normed rings

This file develops the ring-specific properties of TauCeti.IsNormMulUnit, whose definition and multiplicative closure properties live in TauCeti.Analysis.Normed.Monoid.MulUnit.

A nontrivial normed ring with a multiplicative unit has ‖1‖ = 1. In a seminormed ring, a unit is multiplicative precisely when its inverse has reciprocal norm. Norm-preserving monoid homomorphisms between seminormed rings preserve multiplicative units, even when they are not onto. In a complete ultrametric norm-one ring, small perturbations of one are multiplicative units. More generally, an element f within less than ‖u‖ of a multiplicative unit u is again a multiplicative unit: it factors as f = u * (1 - x) with x = u⁻¹ * (u - f) of norm less than one, so its inverse is the Neumann series ∑ₙ xⁿ * u⁻¹, of norm ‖u‖⁻¹.

References

• F. Martin, Overconvergent subanalytic subsets in the framework of Berkovich spaces, J. Eur. Math. Soc. 18 (2016), Definition 1.20 and Lemma 1.21.

theorem TauCeti.IsNormMulUnit.norm_one {A : Type u_1} [NormedRing A] [Nontrivial A] {u : A} (hu : IsNormMulUnit u) : ‖1‖ = 1

A nontrivial normed ring with a multiplicative unit has ‖1‖ = 1.

theorem Units.isNormMulUnit_iff_norm_inv {R : Type u_1} [SeminormedRing R] (u : Rˣ) : TauCeti.IsNormMulUnit ↑u ↔ ‖↑u⁻¹‖ = ‖↑u‖⁻¹

In a seminormed ring, a unit is multiplicative precisely when its inverse has reciprocal norm. If ‖u‖ = 0 every norm vanishes and both sides hold.

theorem TauCeti.IsNormMulUnit.map {R : Type u_1} {S : Type u_2} [SeminormedRing R] [SeminormedRing S] {u : R} (hu : IsNormMulUnit u) (φ : R →* S) (hφ : ∀ (x : R), ‖φ x‖ = ‖x‖) : IsNormMulUnit (φ u)

Norm-preserving monoid homomorphisms between seminormed rings preserve multiplicative units, even when they are not onto.

theorem TauCeti.isNormMulUnit_one_add {A : Type u_1} [NormedRing A] [NormOneClass A] [HasSummableGeomSeries A] [IsUltrametricDist A] {a : A} (ha : ‖a‖ < 1) : IsNormMulUnit (1 + a)

In an ultrametric norm-one ring with summable geometric series, a perturbation of one by an element of norm less than one is a multiplicative unit.

theorem TauCeti.IsNormMulUnit.of_norm_sub_lt {A : Type u_1} [NormedRing A] [HasSummableGeomSeries A] [IsUltrametricDist A] {u f : A} (hu : IsNormMulUnit u) (hf : ‖f - u‖ < ‖u‖) : IsNormMulUnit f

Neumann series criterion. In an ultrametric ring with summable geometric series, an element whose distance from a multiplicative unit u is less than ‖u‖ is a multiplicative unit.

theorem TauCeti.IsNormMulUnit.hasSum_inverse_of_norm_sub_lt {A : Type u_1} [NormedRing A] [HasSummableGeomSeries A] {u : Aˣ} (hu : IsNormMulUnit ↑u) {f : A} (hf : ‖f - ↑u‖ < ‖↑u‖) : HasSum (fun (n : ℕ) => (↑u⁻¹ * (↑u - f)) ^ n * ↑u⁻¹) (Ring.inverse f)

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

theorem TauCeti.IsNormMulUnit.norm_inverse_of_norm_sub_lt {A : Type u_1} [NormedRing A] [HasSummableGeomSeries A] [IsUltrametricDist A] {u f : A} (hu : IsNormMulUnit u) (hf : ‖f - u‖ < ‖u‖) : ‖Ring.inverse f‖ = ‖u‖⁻¹

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