The group of units of a complete normed ring

This file contains the basic theory for the group of units (invertible elements) of a complete normed ring (Banach algebras being a notable special case).

Main results

The constructions Units.oneSub, Units.add, and Units.ofNearby state, in varying forms, that perturbations of a unit are units. The latter two are not stated in their optimal form; more precise versions would use the spectral radius.

The first main result is Units.isOpen: the group of units of a complete normed ring is an open subset of the ring.

The function Ring.inverse (defined elsewhere), for a ring R, sends a : R to a⁻¹ if a is a unit and 0 if not. The other major results of this file (notably NormedRing.inverse_add, NormedRing.inverse_add_norm and NormedRing.inverse_add_norm_diff_nth_order) cover the asymptotic properties of Ring.inverse (x + t) as t → 0.

@[simp]

theorem Units.val_oneSub {R : Type u_1} [NormedRing R] [CompleteSpace R] (t : R) (h : ‖t‖ < 1) : ↑(Units.oneSub t h) = 1 - t

def Units.oneSub {R : Type u_1} [NormedRing R] [CompleteSpace R] (t : R) (h : ‖t‖ < 1) : Rˣ

In a complete normed ring, a perturbation of 1 by an element t of distance less than 1 from 1 is a unit. Here we construct its Units structure.

Equations

• Units.oneSub t h = { val := 1 - t, inv := ∑' (n : ℕ), t ^ n, val_inv := (_ : (1 - t) * ∑' (i : ℕ), t ^ i = 1), inv_val := (_ : (∑' (i : ℕ), t ^ i) * (1 - t) = 1) }

@[simp]

theorem Units.val_add {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) (t : R) (h : ‖t‖ < ‖↑x⁻¹‖⁻¹) : ↑(Units.add x t h) = ↑x + t

def Units.add {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) (t : R) (h : ‖t‖ < ‖↑x⁻¹‖⁻¹) : Rˣ

In a complete normed ring, a perturbation of a unit x by an element t of distance less than ‖x⁻¹‖⁻¹ from x is a unit. Here we construct its Units structure.

Equations

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

@[simp]

theorem Units.val_ofNearby {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) (y : R) (h : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹) : ↑(Units.ofNearby x y h) = y

def Units.ofNearby {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) (y : R) (h : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹) : Rˣ

In a complete normed ring, an element y of distance less than ‖x⁻¹‖⁻¹ from x is a unit. Here we construct its Units structure.

Equations

• Units.ofNearby x y h = Units.copy (Units.add x (y - ↑x) h) y (_ : y = ↑x + (y - ↑x)) ↑(Units.add x (y - ↑x) h)⁻¹ (_ : ↑(Units.add x (y - ↑x) h)⁻¹ = ↑(Units.add x (y - ↑x) h)⁻¹)

theorem Units.isOpen {R : Type u_1} [NormedRing R] [CompleteSpace R] : IsOpen {x | IsUnit x}

The group of units of a complete normed ring is an open subset of the ring.

theorem Units.nhds {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) : {x | IsUnit x} ∈ nhds ↑x

theorem nonunits.subset_compl_ball {R : Type u_1} [NormedRing R] [CompleteSpace R] : nonunits R ⊆ (Metric.ball 1 1)ᶜ

The nonunits in a complete normed ring are contained in the complement of the ball of radius 1 centered at 1 : R.

theorem nonunits.isClosed {R : Type u_1} [NormedRing R] [CompleteSpace R] : IsClosed (nonunits R)

theorem NormedRing.inverse_one_sub {R : Type u_1} [NormedRing R] [CompleteSpace R] (t : R) (h : ‖t‖ < 1) : Ring.inverse (1 - t) = ↑(Units.oneSub t h)⁻¹

theorem NormedRing.inverse_add {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) : ∀ᶠ (t : R) in nhds 0, Ring.inverse (↑x + t) = Ring.inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

The formula Ring.inverse (x + t) = Ring.inverse (1 + x⁻¹ * t) * x⁻¹ holds for t sufficiently small.

theorem NormedRing.inverse_one_sub_nth_order' {R : Type u_1} [NormedRing R] [CompleteSpace R] (n : ℕ) {t : R} (ht : ‖t‖ < 1) : Ring.inverse (1 - t) = (Finset.sum (Finset.range n) fun i => t ^ i) + t ^ n * Ring.inverse (1 - t)

theorem NormedRing.inverse_one_sub_nth_order {R : Type u_1} [NormedRing R] [CompleteSpace R] (n : ℕ) : ∀ᶠ (t : R) in nhds 0, Ring.inverse (1 - t) = (Finset.sum (Finset.range n) fun i => t ^ i) + t ^ n * Ring.inverse (1 - t)

theorem NormedRing.inverse_add_nth_order {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) (n : ℕ) : ∀ᶠ (t : R) in nhds 0, Ring.inverse (↑x + t) = (Finset.sum (Finset.range n) fun i => (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * Ring.inverse (↑x + t)

The formula Ring.inverse (x + t) = (∑ i in Finset.range n, (- x⁻¹ * t) ^ i) * x⁻¹ + (- x⁻¹ * t) ^ n * Ring.inverse (x + t) holds for t sufficiently small.

theorem NormedRing.inverse_one_sub_norm {R : Type u_1} [NormedRing R] [CompleteSpace R] : (fun t => Ring.inverse (1 - t)) =O[nhds 0] fun _t => 1

theorem NormedRing.inverse_add_norm {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) : (fun t => Ring.inverse (↑x + t)) =O[nhds 0] fun _t => 1

The function fun t ↦ inverse (x + t) is O(1) as t → 0.

theorem NormedRing.inverse_add_norm_diff_nth_order {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) (n : ℕ) : (fun t => Ring.inverse (↑x + t) - (Finset.sum (Finset.range n) fun i => (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[nhds 0] fun t => ‖t‖ ^ n

The function fun t ↦ Ring.inverse (x + t) - (∑ i in Finset.range n, (- x⁻¹ * t) ^ i) * x⁻¹ is O(t ^ n) as t → 0.

theorem NormedRing.inverse_add_norm_diff_first_order {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) : (fun t => Ring.inverse (↑x + t) - ↑x⁻¹) =O[nhds 0] fun t => ‖t‖

The function fun t ↦ Ring.inverse (x + t) - x⁻¹ is O(t) as t → 0.

theorem NormedRing.inverse_add_norm_diff_second_order {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) : (fun t => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[nhds 0] fun t => ‖t‖ ^ 2

The function fun t ↦ Ring.inverse (x + t) - x⁻¹ + x⁻¹ * t * x⁻¹ is O(t ^ 2) as t → 0.

theorem NormedRing.inverse_continuousAt {R : Type u_1} [NormedRing R] [CompleteSpace R] (x : Rˣ) : ContinuousAt Ring.inverse ↑x

The function Ring.inverse is continuous at each unit of R.

theorem Units.openEmbedding_val {R : Type u_1} [NormedRing R] [CompleteSpace R] : OpenEmbedding Units.val

In a normed ring, the coercion from Rˣ (equipped with the induced topology from the embedding in R × R) to R is an open embedding.

theorem Units.isOpenMap_val {R : Type u_1} [NormedRing R] [CompleteSpace R] : IsOpenMap Units.val

In a normed ring, the coercion from Rˣ (equipped with the induced topology from the embedding in R × R) to R is an open map.

theorem Ideal.eq_top_of_norm_lt_one {R : Type u_1} [NormedRing R] [CompleteSpace R] (I : Ideal R) {x : R} (hxI : x ∈ I) (hx : ‖1 - x‖ < 1) : I = ⊤

An ideal which contains an element within 1 of 1 : R is the unit ideal.

theorem Ideal.closure_ne_top {R : Type u_1} [NormedRing R] [CompleteSpace R] (I : Ideal R) (hI : I ≠ ⊤) : Ideal.closure I ≠ ⊤

The Ideal.closure of a proper ideal in a complete normed ring is proper.

theorem Ideal.IsMaximal.closure_eq {R : Type u_1} [NormedRing R] [CompleteSpace R] {I : Ideal R} (hI : Ideal.IsMaximal I) : Ideal.closure I = I

The Ideal.closure of a maximal ideal in a complete normed ring is the ideal itself.

instance Ideal.IsMaximal.isClosed {R : Type u_1} [NormedRing R] [CompleteSpace R] {I : Ideal R} [hI : Ideal.IsMaximal I] : IsClosed ↑I

Maximal ideals in complete normed rings are closed.

Equations

• @Ideal.IsMaximal.isClosed = @Ideal.IsMaximal.isClosed.proof_1