Documentation

Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

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
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
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] :

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

Equations
  • ā‹Æ = ā‹Æ