# mathlibdocumentation

geometry.manifold.instances.units_of_normed_algebra

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

## TODO #

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

• smoothness of multiplication and inversion in the charts, i.e. as functions on the normed 𝕜-space R: see times_cont_diff_at_ring_inverse for the inversion result, and times_cont_diff_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 structure f.singleton_smooth_manifold_with_corners, characterization of smoothness of functions to/from this manifold in terms of smoothness in the target space. See the pair of lemmas times_cont_mdiff_coe_sphere and times_cont_mdiff.cod_restrict_sphere for a model. None of this should be particularly difficult.
@[instance]
def units.charted_space {R : Type u_1} [normed_ring R]  :
(units R)
Equations
theorem units.chart_at_apply {R : Type u_1} [normed_ring R] {a b : units R} :
(chart_at R a) b = b
theorem units.chart_at_source {R : Type u_1} [normed_ring R] {a : units R} :
@[instance]
def units.smooth_manifold_with_corners {R : Type u_1} [normed_ring R] {𝕜 : Type u_2} [ R] :