Units of a normed algebra

We construct the Lie group structure on the group of units of a complete normed 𝕜-algebra R. The group of units Rˣ has a natural smooth manifold structure modelled on R given by its embedding into R. Together with the smoothness of the multiplication and inverse of its elements, Rˣ forms a Lie group.

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), as demonstrated by:

example {V : Type*} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [CompleteSpace V] :
    LieGroup 𝓘(𝕜, V →L[𝕜] V) (V →L[𝕜] V)ˣ := inferInstance

instance Units.instChartedSpace {R : Type u_1} [NormedRing R] [CompleteSpace R] : ChartedSpace R Rˣ

Equations

• Units.instChartedSpace = ⋯.singletonChartedSpace

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).source = Set.univ

instance Units.instSmoothManifoldWithCornersModelWithCornersSelf {R : Type u_1} [NormedRing R] [CompleteSpace R] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 R] : SmoothManifoldWithCorners (modelWithCornersSelf 𝕜 R) Rˣ

Equations

• ⋯ = ⋯

theorem Units.contMDiff_val {R : Type u_1} [NormedRing R] [CompleteSpace R] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 R] {m : ℕ∞} : ContMDiff (modelWithCornersSelf 𝕜 R) (modelWithCornersSelf 𝕜 R) m Units.val

For a complete normed ring R, the embedding of the units Rˣ into R is a smooth map between manifolds.

instance Units.instLieGroupModelWithCornersSelf {R : Type u_1} [NormedRing R] [CompleteSpace R] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 R] : LieGroup (modelWithCornersSelf 𝕜 R) Rˣ

The units of a complete normed ring form a Lie group.

Equations

• ⋯ = ⋯