feat(geometry/manifold/instances/units_of_normed_algebra): the units …

…of a normed algebra are a topological group and a smooth manifold (#6981)

I decided to make a small PR now with only a partial result because Heather suggested proving GL^n is a Lie group on Zulip, and I wanted to share the work I did so that whoever wants to take over the task does not have to start from scratch.

Most of the ideas in this PR are by @hrmacbeth, as I was planning on doing a different proof, but I agreed Heather's one was better.

What remains to do in a future PR to prove GLn is a Lie group is to add and prove the following instance to the file `geometry/manifold/instances/units_of_normed_algebra.lean`:

```
instance units_of_normed_algebra.lie_group
  {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
  {R : Type*} [normed_ring R] [normed_algebra 𝕜 R] [complete_space R] :
  lie_group (model_with_corners_self 𝕜 R) (units R) :=
{
  smooth_mul := begin
    sorry,
  end,
  smooth_inv := begin
    sorry,
  end,
  ..units_of_normed_algebra.smooth_manifold_with_corners, /- Why does it not find the instance alone? -/
}
```


Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

src/algebra/group/prod.lean

@@ -6,6 +6,7 @@ Authors: Simon Hudon, Patrick Massot, Yury Kudryashov
 import algebra.group.hom
 import data.equiv.mul_add
 import data.prod
+import algebra.opposites
 
 /-!
 # Monoid, group etc structures on `M × N`
@@ -317,3 +318,17 @@ def prod_units : units (M × N) ≃* units M × units N :=
 end
 
 end mul_equiv
+
+section units
+
+open opposite
+
+/-- Canonical homomorphism of monoids from `units α` into `α × αᵒᵖ`.
+Used mainly to define the natural topology of `units α`. -/
+def embed_product (α : Type*) [monoid α] : units α →* α × αᵒᵖ :=
+{ to_fun := λ x, ⟨x, op ↑x⁻¹⟩,
+  map_one' := by simp only [one_inv, eq_self_iff_true, units.coe_one, op_one, prod.mk_eq_one,
+    and_self],
+  map_mul' := λ x y, by simp only [mul_inv_rev, op_mul, units.coe_mul, prod.mk_mul_mk] }
+
+end units

src/analysis/normed_space/units.lean

@@ -267,3 +267,34 @@ begin
 end
 
 end normed_ring
+
+namespace units
+open opposite filter normed_ring
+
+/-- In a normed ring, the coercion from `units R` (equipped with the induced topology from the
+embedding in `R × R`) to `R` is an open map. -/
+lemma is_open_map_coe : is_open_map (coe : units R → R) :=
+begin
+  rw is_open_map_iff_nhds_le,
+  intros x s,
+  rw [mem_map, mem_nhds_induced],
+  rintros ⟨t, ht, hts⟩,
+  obtain ⟨u, hu, v, hv, huvt⟩ :
+    ∃ (u : set R), u ∈ 𝓝 ↑x ∧ ∃ (v : set Rᵒᵖ), v ∈ 𝓝 (opposite.op ↑x⁻¹) ∧ u.prod v ⊆ t,
+  { simpa [embed_product, mem_nhds_prod_iff] using ht },
+  have : u ∩ (op ∘ ring.inverse) ⁻¹' v ∩ (set.range (coe : units R → R)) ∈ 𝓝 ↑x,
+  { refine inter_mem_sets (inter_mem_sets hu _) (units.nhds x),
+    refine (continuous_op.continuous_at.comp (inverse_continuous_at x)).preimage_mem_nhds _,
+    simpa using hv },
+  refine mem_sets_of_superset this _,
+  rintros _ ⟨⟨huy, hvy⟩, ⟨y, rfl⟩⟩,
+  have : embed_product R y ∈ u.prod v := ⟨huy, by simpa using hvy⟩,
+  simpa using hts (huvt this)
+end
+
+/-- In a normed ring, the coercion from `units R` (equipped with the induced topology from the
+embedding in `R × R`) to `R` is an open embedding. -/
+lemma open_embedding_coe : open_embedding (coe : units R → R) :=
+open_embedding_of_continuous_injective_open continuous_coe ext is_open_map_coe
+
+end units

src/geometry/manifold/charted_space.lean

@@ -489,7 +489,7 @@ atlas members are just the identity -/
 by simp [atlas, charted_space.atlas]
 
 /-- In the model space, chart_at is always the identity -/
-@[simp, mfld_simps] lemma chart_at_self_eq {H : Type*} [topological_space H] {x : H} :
+lemma chart_at_self_eq {H : Type*} [topological_space H] {x : H} :
   chart_at H x = local_homeomorph.refl H :=
 by simpa using chart_mem_atlas H x
 
@@ -815,35 +815,66 @@ end maximal_atlas
 
 section singleton
 variables {α : Type*} [topological_space α]
-variables (e : local_homeomorph α H)
+
+namespace local_homeomorph
+
+variable (e : local_homeomorph α H)
 
 /-- If a single local homeomorphism `e` from a space `α` into `H` has source covering the whole
 space `α`, then that local homeomorphism induces an `H`-charted space structure on `α`.
 (This condition is equivalent to `e` being an open embedding of `α` into `H`; see
-`local_homeomorph.to_open_embedding` and `open_embedding.to_local_homeomorph`.) -/
+`open_embedding.singleton_charted_space`.) -/
 def singleton_charted_space (h : e.source = set.univ) : charted_space H α :=
 { atlas := {e},
   chart_at := λ _, e,
   mem_chart_source := λ _, by simp only [h] with mfld_simps,
   chart_mem_atlas := λ _, by tauto }
 
-lemma singleton_charted_space_one_chart (h : e.source = set.univ) (e' : local_homeomorph α H)
-  (h' : e' ∈ (singleton_charted_space e h).atlas) : e' = e := h'
+@[simp, mfld_simps] lemma singleton_charted_space_chart_at_eq (h : e.source = set.univ) {x : α} :
+  @chart_at H _ α _ (e.singleton_charted_space h) x = e := rfl
+
+lemma singleton_charted_space_chart_at_source
+  (h : e.source = set.univ) {x : α} :
+  (@chart_at H _ α _ (e.singleton_charted_space h) x).source = set.univ := h
+
+lemma singleton_charted_space_mem_atlas_eq (h : e.source = set.univ)
+  (e' : local_homeomorph α H) (h' : e' ∈ (e.singleton_charted_space h).atlas) : e' = e := h'
 
 /-- Given a local homeomorphism `e` from a space `α` into `H`, if its source covers the whole
 space `α`, then the induced charted space structure on `α` is `has_groupoid G` for any structure
 groupoid `G` which is closed under restrictions. -/
 lemma singleton_has_groupoid (h : e.source = set.univ) (G : structure_groupoid H)
-  [closed_under_restriction G] : @has_groupoid _ _ _ _ (singleton_charted_space e h) G :=
+  [closed_under_restriction G] : @has_groupoid _ _ _ _ (e.singleton_charted_space h) G :=
 { compatible := begin
     intros e' e'' he' he'',
-    rw singleton_charted_space_one_chart e h e' he',
-    rw singleton_charted_space_one_chart e h e'' he'',
+    rw e.singleton_charted_space_mem_atlas_eq h e' he',
+    rw e.singleton_charted_space_mem_atlas_eq h e'' he'',
     refine G.eq_on_source _ e.trans_symm_self,
     have hle : id_restr_groupoid ≤ G := (closed_under_restriction_iff_id_le G).mp (by assumption),
     exact structure_groupoid.le_iff.mp hle _ (id_restr_groupoid_mem _),
   end }
 
+end local_homeomorph
+
+namespace open_embedding
+
+variable [nonempty α]
+
+/-- An open embedding of `α` into `H` induces an `H`-charted space structure on `α`.
+See `ocal_homeomorph.singleton_charted_space` -/
+def singleton_charted_space {f : α → H} (h : open_embedding f) :
+  charted_space H α := (h.to_local_homeomorph f).singleton_charted_space (h.source f)
+
+lemma singleton_charted_space_chart_at_eq {f : α → H} (h : open_embedding f) {x : α} :
+  ⇑(@chart_at H _ α _ (h.singleton_charted_space) x) = f := rfl
+
+lemma singleton_has_groupoid {f : α → H} (h : open_embedding f)
+  (G : structure_groupoid H) [closed_under_restriction G] :
+  @has_groupoid _ _ _ _ h.singleton_charted_space G :=
+(h.to_local_homeomorph f).singleton_has_groupoid (h.source f) G
+
+end open_embedding
+
 end singleton
 
 namespace topological_space.opens

src/geometry/manifold/instances/units_of_normed_algebra.lean

@@ -0,0 +1,65 @@
+/-
+Copyright © 2021 Nicolò Cavalleri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nicolò Cavalleri, Heather Macbeth
+-/
+
+import geometry.manifold.smooth_manifold_with_corners
+import analysis.normed_space.units
+
+/-!
+# 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.
+
+-/
+
+noncomputable theory
+
+open_locale manifold
+
+namespace units
+
+variables {R : Type*} [normed_ring R] [complete_space R]
+
+instance : charted_space R (units R) := open_embedding_coe.singleton_charted_space
+
+lemma chart_at_apply {a : units R} {b : units R} : chart_at R a b = b := rfl
+lemma chart_at_source {a : units R} : (chart_at R a).source = set.univ := rfl
+
+variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] [normed_algebra 𝕜 R]
+
+instance : smooth_manifold_with_corners 𝓘(𝕜, R) (units R) :=
+open_embedding_coe.singleton_smooth_manifold_with_corners 𝓘(𝕜, R)
+
+end units

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -551,6 +551,13 @@ class smooth_manifold_with_corners {𝕜 : Type*} [nondiscrete_normed_field 𝕜
   (M : Type*) [topological_space M] [charted_space H M] extends
   has_groupoid M (times_cont_diff_groupoid ∞ I) : Prop
 
+lemma smooth_manifold_with_corners.mk' {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+  {E : Type*} [normed_group E] [normed_space 𝕜 E]
+  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
+  (M : Type*) [topological_space M] [charted_space H M]
+  [gr : has_groupoid M (times_cont_diff_groupoid ∞ I)] :
+  smooth_manifold_with_corners I M := { ..gr }
+
 lemma smooth_manifold_with_corners_of_times_cont_diff_on
   {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
   {E : Type*} [normed_group E] [normed_space 𝕜 E]
@@ -625,6 +632,39 @@ instance prod {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 
 end smooth_manifold_with_corners
 
+lemma local_homeomorph.singleton_smooth_manifold_with_corners
+  {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+  {E : Type*} [normed_group E] [normed_space 𝕜 E]
+  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
+  {M : Type*} [topological_space M]
+  (e : local_homeomorph M H) (h : e.source = set.univ) :
+  @smooth_manifold_with_corners 𝕜 _ E _ _ H _ I M _ (e.singleton_charted_space h) :=
+@smooth_manifold_with_corners.mk' _ _ _ _ _ _ _ _ _ _ (id _) $
+e.singleton_has_groupoid h (times_cont_diff_groupoid ∞ I)
+
+lemma open_embedding.singleton_smooth_manifold_with_corners
+  {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+  {E : Type*} [normed_group E] [normed_space 𝕜 E]
+  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
+  {M : Type*} [topological_space M]
+  [nonempty M] {f : M → H} (h : open_embedding f) :
+  @smooth_manifold_with_corners 𝕜 _ E _ _ H _ I M _ h.singleton_charted_space :=
+(h.to_local_homeomorph f).singleton_smooth_manifold_with_corners I (h.source f)
+
+namespace topological_space.opens
+
+open topological_space
+
+variables  {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+  {E : Type*} [normed_group E] [normed_space 𝕜 E]
+  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
+  {M : Type*} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
+  (s : opens M)
+
+instance : smooth_manifold_with_corners I s := { ..s.has_groupoid (times_cont_diff_groupoid ∞ I) }
+
+end topological_space.opens
+
 section extended_charts
 open_locale topological_space
 

src/topology/algebra/group.lean

@@ -678,3 +678,13 @@ instance additive.topological_add_group {G} [h : topological_space G]
 instance multiplicative.topological_group {G} [h : topological_space G]
   [add_group G] [topological_add_group G] : @topological_group (multiplicative G) h _ :=
 { continuous_inv := @continuous_neg G _ _ _ }
+
+namespace units
+
+variables [monoid α] [topological_space α] [has_continuous_mul α]
+
+instance : topological_group (units α) :=
+{ continuous_inv := continuous_induced_rng ((continuous_unop.comp (continuous_snd.comp
+    (@continuous_embed_product α _ _))).prod_mk (continuous_op.comp continuous_coe)) }
+
+end units

src/topology/algebra/monoid.lean

@@ -274,6 +274,58 @@ continuous.comp (continuous_pow n) h
 
 end has_continuous_mul
 
+section op
+
+open opposite
+
+/-- Put the same topological space structure on the opposite monoid as on the original space. -/
+instance [_i : topological_space α] : topological_space αᵒᵖ :=
+topological_space.induced (unop : αᵒᵖ → α) _i
+
+variables [topological_space α]
+
+lemma continuous_unop : continuous (unop : αᵒᵖ → α) := continuous_induced_dom
+lemma continuous_op : continuous (op : α → αᵒᵖ) := continuous_induced_rng continuous_id
+
+variables [monoid α] [has_continuous_mul α]
+
+/-- If multiplication is continuous in the monoid `α`, then it also is in the monoid `αᵒᵖ`. -/
+instance : has_continuous_mul αᵒᵖ :=
+⟨ let h₁ := @continuous_mul α _ _ _ in
+  let h₂ : continuous (λ p : α × α, _) := continuous_snd.prod_mk continuous_fst in
+  continuous_induced_rng $ (h₁.comp h₂).comp (continuous_unop.prod_map continuous_unop) ⟩
+
+end op
+
+namespace units
+
+open opposite
+
+variables [topological_space α] [monoid α]
+
+/-- The units of a monoid are equipped with a topology, via the embedding into `α × α`. -/
+instance : topological_space (units α) :=
+topological_space.induced (embed_product α) (by apply_instance)
+
+lemma continuous_embed_product : continuous (embed_product α) :=
+continuous_induced_dom
+
+lemma continuous_coe : continuous (coe : units α → α) :=
+by convert continuous_fst.comp continuous_induced_dom
+
+variables [has_continuous_mul α]
+
+/-- If multiplication on a monoid is continuous, then multiplication on the units of the monoid,
+with respect to the induced topology, is continuous.
+
+Inversion is also continuous, but we register this in a later file, `topology.algebra.group`,
+because the predicate `has_continuous_inv` has not yet been defined. -/
+instance : has_continuous_mul (units α) :=
+⟨ let h := @continuous_mul (α × αᵒᵖ) _ _ _ in
+  continuous_induced_rng $ h.comp $ continuous_embed_product.prod_map continuous_embed_product ⟩
+
+end units
+
 section
 
 variables [topological_space M] [comm_monoid M]