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).


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

theorem Units.chartAt_apply {R : Type u_1} [NormedRing R] [CompleteSpace R] {a : RĖ£} {b : RĖ£} :
ā†‘(chartAt R a) b = ā†‘b
theorem Units.chartAt_source {R : Type u_1} [NormedRing R] [CompleteSpace R] {a : RĖ£} :
(chartAt R a).toLocalEquiv.source = Set.univ