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.
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 inverse
is continuous at each unit of R
.
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.
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.