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

TODO

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

• smoothness of multiplication and inversion in the charts, i.e. as functions on the normed 𝕜-space R: see contDiffAt_ring_inverse for the inversion result, and contDiff_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_smoothManifoldWithCorners, characterization of smoothness of functions to/from this manifold in terms of smoothness in the target space. See the pair of lemmas ContMDiff_coe_sphere and ContMDiff.codRestrict_sphere for a model. None of this should be particularly difficult.

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

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

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