mathlib documentation


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 continuous_linear_map.to_normed_algebra), 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 : lie_group π“˜(π•œ, R) (units R) :=
{ smooth_mul := sorry,
  smooth_inv := sorry,
  ..units.smooth_manifold_with_corners }

The ingredients needed for the construction are

theorem units.chart_at_apply {R : Type u_1} [normed_ring R] [complete_space R] {a b : units R} :
def units.smooth_manifold_with_corners {R : Type u_1} [normed_ring R] [complete_space R] {π•œ : Type u_2} [nondiscrete_normed_field π•œ] [normed_algebra π•œ R] :