Units and the Jacobson radical of normed rings

In a normed ring with summable geometric series, Ring.inverse is continuous at every unit (NormedRing.inverse_continuousAt), but it jumps to 0 at the boundary of the open set of units. When the nonunits also form an open set, as in a complete discretely valued ring such as ℤ_p, there is no such boundary and Ring.inverse is continuous everywhere.

The Neumann series also gives explicit bounds: ‖(1 - x)⁻¹‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹ when ‖x‖ < 1, and, when ‖1‖ = 1, ‖(u + t)⁻¹‖ ≤ ‖u⁻¹‖ / (1 - ‖u⁻¹‖ * ‖t‖) for a unit u with ‖u⁻¹‖ * ‖t‖ < 1; in particular (1 - w) * u + d is a unit with ‖((1 - w) * u + d)⁻¹‖ ≤ M / (1 - ‖w‖ - M * ‖d‖) when ‖u⁻¹‖ ≤ M, ‖w‖ < 1 and M * ‖d‖ < 1 - ‖w‖. Mathlib records these inverses only through asymptotic O-bounds such as NormedRing.inverse_add_norm; the explicit constants are needed for inductive constructions that perturb a unit infinitely often, such as Cohen–Hewitt factorization.

The Jacobson radical is closed, as an intersection of maximal left ideals, using Mathlib's Ring.jacobson_eq_sInf_isMaximal and Ideal.IsMaximal.isClosed. See Dales, Banach Algebras and Automatic Continuity, §§1.3–1.5.

theorem NormedRing.continuous_inverse_of_isOpen_nonunits {R : Type u_1} [NormedRing R] [HasSummableGeomSeries R] (h : IsOpen (nonunits R)) : Continuous Ring.inverse

If the nonunits of a normed ring with summable geometric series form an open set, then Ring.inverse is continuous: it is continuous at every unit, and locally zero at every nonunit.

theorem NormedRing.norm_inverse_one_sub_le {R : Type u_1} [NormedRing R] [HasSummableGeomSeries R] {x : R} (hx : ‖x‖ < 1) : ‖Ring.inverse (1 - x)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

The Neumann-series bound for the inverse of 1 - x when ‖x‖ < 1. The identity need not have norm one; when it does, the bound reads ‖(1 - x)⁻¹‖ ≤ (1 - ‖x‖)⁻¹.

theorem NormedRing.norm_inverse_add_le {R : Type u_1} [NormedRing R] [HasSummableGeomSeries R] [NormOneClass R] (u : Rˣ) {t : R} (ht : ‖↑u⁻¹‖ * ‖t‖ < 1) : ‖Ring.inverse (↑u + t)‖ ≤ ‖↑u⁻¹‖ / (1 - ‖↑u⁻¹‖ * ‖t‖)

In a normed ring with ‖1‖ = 1 and summable geometric series, perturbing a unit u by t with ‖u⁻¹‖ * ‖t‖ < 1 gives an element whose inverse has norm at most ‖u⁻¹‖ / (1 - ‖u⁻¹‖ * ‖t‖). The perturbed element is a unit by Units.add.

theorem NormedRing.isUnit_one_sub_mul_add_and_norm_inverse_le {R : Type u_1} [NormedRing R] [HasSummableGeomSeries R] [NormOneClass R] {a w d : R} {M : ℝ} (ha : IsUnit a) (hM : ‖Ring.inverse a‖ ≤ M) (hw : ‖w‖ < 1) (hd : M * ‖d‖ < 1 - ‖w‖) : IsUnit ((1 - w) * a + d) ∧ ‖Ring.inverse ((1 - w) * a + d)‖ ≤ M / (1 - ‖w‖ - M * ‖d‖)

Perturbing a unit a with ‖a⁻¹‖ ≤ M to (1 - w) * a + d, where ‖w‖ < 1 and M * ‖d‖ < 1 - ‖w‖, gives a unit whose inverse has norm at most M / (1 - ‖w‖ - M * ‖d‖).

theorem TauCeti.Ring.isClosed_jacobson (A : Type u_1) [NormedRing A] [HasSummableGeomSeries A] : IsClosed ↑(Ring.jacobson A)

The Jacobson radical of a normed ring with summable geometric series is closed.