Units of a normed algebra #
This file is a stub, containing a construction of the charted space structure on the group of units
of a complete normed ring R
, and of the smooth manifold structure on the group of units of a
complete normed š
-algebra R
.
This manifold is actually a Lie group, which eventually should be the main result of this file.
An important special case of this construction is the general linear group. For a normed space V
over a field š
, the š
-linear endomorphisms of V
are a normed š
-algebra (see
ContinuousLinearMap.toNormedAlgebra
), so this construction provides a Lie group structure on
its group of units, the general linear group GL(š
, V
).
TODO #
The Lie group instance requires the following fields:
instance : LieGroup š(š, R) RĖ£ :=
{ Units.smoothManifoldWithCorners with
smooth_mul := sorry,
smooth_inv := sorry }
The ingredients needed for the construction are
- smoothness of multiplication and inversion in the charts, i.e. as functions on the normed
š
-spaceR
: seecontDiffAt_ring_inverse
for the inversion result, andcontDiff_mul
(needs to be generalized from field to algebra) for the multiplication result - for an open embedding
f
, whose domain is equipped with the induced manifold structuref.singleton_smoothManifoldWithCorners
, characterization of smoothness of functions to/from this manifold in terms of smoothness in the target space. See the pair of lemmasContMDiff_coe_sphere
andContMDiff.codRestrict_sphere
for a model. None of this should be particularly difficult.