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 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.
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.
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.
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
The group of units of a complete normed ring is an open subset of the ring.
The formula inverse (x + t) = inverse (1 + x⁻¹ * t) * x⁻¹ holds for t sufficiently small.
The formula
inverse (x + t) = (∑ i in range n, (- x⁻¹ * t) ^ i) * x⁻¹ + (- x⁻¹ * t) ^ n * inverse (x + t)
holds for t sufficiently small.
The function λ t, inverse (x + t) is O(1) as t → 0.
The function
λ t, inverse (x + t) - (∑ i in range n, (- x⁻¹ * t) ^ i) * x⁻¹
is O(t ^ n) as t → 0.
The function λ t, inverse (x + t) - x⁻¹ is O(t) as t → 0.
The function
λ t, inverse (x + t) - x⁻¹ + x⁻¹ * t * x⁻¹
is O(t ^ 2) as t → 0.
The function inverse is continuous at each unit of R.