mathlib3 documentation

analysis.normed_space.units

The group of units of a complete normed ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 one_sub, add and unit_of_nearby 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 is_open: the group of units of a complete normed ring is an open subset of the ring.

The function inverse (defined in algebra.ring), 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 inverse_add, inverse_add_norm and inverse_add_norm_diff_nth_order) cover the asymptotic properties of inverse (x + t) as t → 0.

@[simp]

theorem units.coe_one_sub {R : Type u_1} [normed_ring R] [complete_space R] (t : R) (h : ‖t‖ < 1) :

↑(units.one_sub t h) = 1 - t

noncomputable def units.one_sub {R : Type u_1} [normed_ring R] [complete_space R] (t : R) (h : ‖t‖ < 1) :

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.one_sub t h = {val := 1 - t, inv := ∑' (n : ℕ), t ^ n, val_inv := _, inv_val := _}

noncomputable def units.add {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) (t : R) (h : ‖t‖ < ‖↑x⁻¹ ‖⁻¹) :

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

x.add t h = (x * units.one_sub (-(↑x⁻¹ * t)) _).copy (↑x + t) _ ↑(x * units.one_sub (-(↑x⁻¹ * t)) _)⁻¹ _

@[simp]

theorem units.coe_add {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) (t : R) (h : ‖t‖ < ‖↑x⁻¹ ‖⁻¹) :

↑(x.add t h) = ↑x + t

noncomputable def units.unit_of_nearby {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) (y : R) (h : ‖y - ↑x‖ < ‖↑x⁻¹ ‖⁻¹) :

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

x.unit_of_nearby y h = (x.add (y - ↑x) h).copy y _ ↑(x.add (y - ↑x) h)⁻¹ _

@[simp]

theorem units.coe_unit_of_nearby {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) (y : R) (h : ‖y - ↑x‖ < ‖↑x⁻¹ ‖⁻¹) :

↑(x.unit_of_nearby y h) = y

@[protected]

theorem units.is_open {R : Type u_1} [normed_ring R] [complete_space R] :

is_open {x : R | is_unit x}

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

@[protected]

theorem units.nhds {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) :

{x : R | is_unit x} ∈ nhds ↑x

theorem nonunits.subset_compl_ball {R : Type u_1} [normed_ring R] [complete_space 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.

@[protected]

theorem nonunits.is_closed {R : Type u_1} [normed_ring R] [complete_space R] :

is_closed (nonunits R)

theorem normed_ring.inverse_one_sub {R : Type u_1} [normed_ring R] [complete_space R] (t : R) (h : ‖t‖ < 1) :

ring.inverse (1 - t) = ↑(units.one_sub t h)⁻¹

theorem normed_ring.inverse_add {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) :

∀ᶠ (t : R) in nhds 0, ring.inverse (↑x + t) = ring.inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

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

theorem normed_ring.inverse_one_sub_nth_order {R : Type u_1} [normed_ring R] [complete_space R] (n : ℕ) :

∀ᶠ (t : R) in nhds 0, ring.inverse (1 - t) = (finset.range n).sum (λ (i : ℕ), t ^ i) + t ^ n * ring.inverse (1 - t)

theorem normed_ring.inverse_add_nth_order {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) (n : ℕ) :

∀ᶠ (t : R) in nhds 0, ring.inverse (↑x + t) = (finset.range n).sum (λ (i : ℕ), (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * ring.inverse (↑x + t)

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

theorem normed_ring.inverse_one_sub_norm {R : Type u_1} [normed_ring R] [complete_space R] :

(λ (t : R), ring.inverse (1 - t)) =O[nhds 0] λ (t : R), 1

theorem normed_ring.inverse_add_norm {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) :

(λ (t : R), ring.inverse (↑x + t)) =O[nhds 0] λ (t : R), 1

The function λ t, inverse (x + t) is O(1) as t → 0.

theorem normed_ring.inverse_add_norm_diff_nth_order {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) (n : ℕ) :

(λ (t : R), ring.inverse (↑x + t) - (finset.range n).sum (λ (i : ℕ), (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[nhds 0] λ (t : R), ‖t‖ ^ n

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

theorem normed_ring.inverse_add_norm_diff_first_order {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) :

(λ (t : R), ring.inverse (↑x + t) - ↑x⁻¹) =O[nhds 0] λ (t : R), ‖t‖

The function λ t, inverse (x + t) - x⁻¹ is O(t) as t → 0.

theorem normed_ring.inverse_add_norm_diff_second_order {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) :

(λ (t : R), ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[nhds 0] λ (t : R), ‖t‖ ^ 2

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

theorem normed_ring.inverse_continuous_at {R : Type u_1} [normed_ring R] [complete_space R] (x : Rˣ) :

continuous_at ring.inverse ↑x

The function inverse is continuous at each unit of R.

theorem units.is_open_map_coe {R : Type u_1} [normed_ring R] [complete_space R] :

is_open_map coe

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 units.open_embedding_coe {R : Type u_1} [normed_ring R] [complete_space R] :

open_embedding coe

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 ideal.eq_top_of_norm_lt_one {R : Type u_1} [normed_ring R] [complete_space R] (I : ideal R) {x : R} (hxI : x ∈ I) (hx : ‖1 - x‖ < 1) :

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

theorem ideal.closure_ne_top {R : Type u_1} [normed_ring R] [complete_space R] (I : ideal R) (hI : I ≠ ⊤) :

I.closure ≠ ⊤

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

theorem ideal.is_maximal.closure_eq {R : Type u_1} [normed_ring R] [complete_space R] {I : ideal R} (hI : I.is_maximal) :

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

@[protected, instance]

def ideal.is_maximal.is_closed {R : Type u_1} [normed_ring R] [complete_space R] {I : ideal R} [hI : I.is_maximal] :

Maximal ideals in complete normed rings are closed.