feat(geometry/manifold): Some lemmas for smooth functions (#7752)

src/geometry/manifold/algebra/lie_group.lean

@@ -26,6 +26,7 @@ groups here are not necessarily finite dimensional.
                                  is an additive Lie group.
 
 ## Implementation notes
+
 A priori, a Lie group here is a manifold with corners.
 
 The definition of Lie group cannot require `I : model_with_corners 𝕜 E E` with the same space as the
@@ -80,14 +81,6 @@ variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 {H'' : Type*} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''}
 {M' : Type*} [topological_space M'] [charted_space H'' M']
 
-localized "notation `L_add` := left_add" in lie_group
-
-localized "notation `R_add` := right_add" in lie_group
-
-localized "notation `L` := left_mul" in lie_group
-
-localized "notation `R` := right_mul" in lie_group
-
 section
 
 variable (I)

src/geometry/manifold/algebra/monoid.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicolò Cavalleri
 -/
 
-import geometry.manifold.times_cont_mdiff
+import geometry.manifold.times_cont_mdiff_map
 
 /-!
 # Smooth monoid
@@ -16,6 +16,8 @@ additive counterpart `has_smooth_add`. These structures are general enough to al
 semigroups.
 -/
 
+open_locale manifold
+
 section
 
 set_option old_structure_cmd true
@@ -112,6 +114,33 @@ lemma smooth_on.mul {f : M → G} {g : M → G} {s : set M}
   smooth_on I' I (f * g) s :=
 ((smooth_mul I).comp_smooth_on (hf.prod_mk hg) : _)
 
+variables (I) (g h : G)
+
+/-- Left multiplication by `g`. It is meant to mimic the usual notation in Lie groups. -/
+def smooth_left_mul : C^∞⟮I, G; I, G⟯ := ⟨(left_mul g), smooth_mul_left⟩
+
+/-- Right multiplication by `g`. It is meant to mimic the usual notation in Lie groups. -/
+def smooth_right_mul : C^∞⟮I, G; I, G⟯ := ⟨(right_mul g), smooth_mul_right⟩
+
+/- Left multiplication. The abbreviation is `MIL`. -/
+localized "notation `𝑳` := smooth_left_mul" in lie_group
+
+/- Right multiplication. The abbreviation is `MIR`. -/
+localized "notation `𝑹` := smooth_right_mul" in lie_group
+
+open_locale lie_group
+
+@[simp] lemma L_apply : (𝑳 I g) h = g * h := rfl
+@[simp] lemma R_apply : (𝑹 I g) h = h * g := rfl
+
+@[simp] lemma L_mul {G : Type*} [semigroup G] [topological_space G] [charted_space H G]
+  [has_smooth_mul I G] (g h : G) : 𝑳 I (g * h) = (𝑳 I g).comp (𝑳 I h) :=
+by { ext, simp only [times_cont_mdiff_map.comp_apply, L_apply, mul_assoc] }
+
+@[simp] lemma R_mul {G : Type*} [semigroup G] [topological_space G] [charted_space H G]
+  [has_smooth_mul I G] (g h : G) : 𝑹 I (g * h) = (𝑹 I h).comp (𝑹 I g) :=
+by { ext, simp only [times_cont_mdiff_map.comp_apply, R_apply, mul_assoc] }
+
 /- Instance of product -/
 @[to_additive]
 instance has_smooth_mul.prod {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
@@ -128,8 +157,6 @@ instance has_smooth_mul.prod {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
     ((smooth_snd.comp smooth_fst).smooth.mul (smooth_snd.comp smooth_snd)),
   .. smooth_manifold_with_corners.prod G G' }
 
-variable (I)
-
 end has_smooth_mul
 
 section monoid

src/geometry/manifold/algebra/smooth_functions.lean

@@ -5,7 +5,6 @@ Authors: Nicolò Cavalleri
 -/
 
 import geometry.manifold.algebra.structures
-import geometry.manifold.times_cont_mdiff_map
 
 /-!
 # Algebraic structures over smooth functions
@@ -23,6 +22,9 @@ variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 {H : Type*} [topological_space H] {I : model_with_corners 𝕜 E H}
 {H' : Type*} [topological_space H'] {I' : model_with_corners 𝕜 E' H'}
 {N : Type*} [topological_space N] [charted_space H N]
+{E'' : Type*} [normed_group E''] [normed_space 𝕜 E'']
+{H'' : Type*} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''}
+{N' : Type*} [topological_space N'] [charted_space H'' N']
 
 namespace smooth_map
 
@@ -37,6 +39,11 @@ lemma coe_mul {G : Type*} [has_mul G] [topological_space G] [charted_space H' G]
   [has_smooth_mul I' G] (f g : C^∞⟮I, N; I', G⟯) :
   ⇑(f * g) = f * g := rfl
 
+@[simp, to_additive] lemma mul_comp {G : Type*} [has_mul G] [topological_space G]
+  [charted_space H' G] [has_smooth_mul I' G] (f g : C^∞⟮I'', N'; I', G⟯) (h : C^∞⟮I, N; I'', N'⟯) :
+(f * g).comp h = (f.comp h) * (g.comp h) :=
+by ext; simp only [times_cont_mdiff_map.comp_apply, coe_mul, pi.mul_apply]
+
 @[to_additive]
 instance has_one {G : Type*} [monoid G] [topological_space G] [charted_space H' G] :
   has_one C^∞⟮I, N; I', G⟯ :=
@@ -164,6 +171,10 @@ lemma smooth_map.coe_smul
   {V : Type*} [normed_group V] [normed_space 𝕜 V] (r : 𝕜) (f : C^∞⟮I, N; 𝓘(𝕜, V), V⟯) :
   ⇑(r • f) = r • f := rfl
 
+@[simp] lemma smooth_map.smul_comp {V : Type*} [normed_group V] [normed_space 𝕜 V]
+  (r : 𝕜) (g : C^∞⟮I'', N'; 𝓘(𝕜, V), V⟯) (h : C^∞⟮I, N; I'', N'⟯) :
+(r • g).comp h = r • (g.comp h) := rfl
+
 instance smooth_map_module
   {V : Type*} [normed_group V] [normed_space 𝕜 V] :
   module 𝕜 C^∞⟮I, N; 𝓘(𝕜, V), V⟯ :=
@@ -215,9 +226,13 @@ is naturally a vector space over the ring of smooth functions from `N` to `𝕜`
 
 instance smooth_map_has_scalar'
   {V : Type*} [normed_group V] [normed_space 𝕜 V] :
-  has_scalar C^∞⟮I, N; 𝓘(𝕜), 𝕜⟯ C^∞⟮I, N; 𝓘(𝕜, V), V⟯ :=
+  has_scalar C^∞⟮I, N; 𝕜⟯ C^∞⟮I, N; 𝓘(𝕜, V), V⟯ :=
 ⟨λ f g, ⟨λ x, (f x) • (g x), (smooth.smul f.2 g.2)⟩⟩
 
+@[simp] lemma smooth_map.smul_comp' {V : Type*} [normed_group V] [normed_space 𝕜 V]
+  (f : C^∞⟮I'', N'; 𝕜⟯) (g : C^∞⟮I'', N'; 𝓘(𝕜, V), V⟯) (h : C^∞⟮I, N; I'', N'⟯) :
+(f • g).comp h = (f.comp h) • (g.comp h) := rfl
+
 instance smooth_map_module'
   {V : Type*} [normed_group V] [normed_space 𝕜 V] :
   module C^∞⟮I, N; 𝓘(𝕜), 𝕜⟯ C^∞⟮I, N; 𝓘(𝕜, V), V⟯ :=