[Merged by Bors] - feat(geometry): first stab on Lie groups

src/analysis/calculus/times_cont_diff.lean

@@ -1238,6 +1238,10 @@ lemma times_cont_diff.times_cont_diff_at {n : with_top ℕ} (h : times_cont_diff
   times_cont_diff_at 𝕜 n f x :=
 times_cont_diff_iff_times_cont_diff_at.1 h x
 
+lemma times_cont_diff.times_cont_diff_within_at {n : with_top ℕ} (h : times_cont_diff 𝕜 n f) :
+  times_cont_diff_within_at 𝕜 n f s x :=
+h.times_cont_diff_at.times_cont_diff_within_at
+
 lemma times_cont_diff_top :
   times_cont_diff 𝕜 ∞ f ↔ ∀ (n : ℕ), times_cont_diff 𝕜 n f :=
 by simp [times_cont_diff_on_univ.symm, times_cont_diff_on_top]
@@ -1484,6 +1488,20 @@ lemma times_cont_diff_on_fst {s : set (E×F)} {n : with_top ℕ} :
   times_cont_diff_on 𝕜 n (prod.fst : E × F → E) s :=
 times_cont_diff.times_cont_diff_on times_cont_diff_fst
 
+/--
+The first projection at a point in a product is `C^∞`.
+-/
+lemma times_cont_diff_at_fst {p : E × F} {n : with_top ℕ} :
+  times_cont_diff_at 𝕜 n (prod.fst : E × F → E) p :=
+times_cont_diff_fst.times_cont_diff_at
+
+/--
+The first projection within a domain at a point in a product is `C^∞`.
+-/
+lemma times_cont_diff_within_at_fst {s : set (E × F)} {p : E × F} {n : with_top ℕ} :
+  times_cont_diff_within_at 𝕜 n (prod.fst : E × F → E) s p :=
+times_cont_diff_fst.times_cont_diff_within_at
+
 /--
 The second projection in a product is `C^∞`.
 -/
@@ -1497,6 +1515,20 @@ lemma times_cont_diff_on_snd {s : set (E×F)} {n : with_top ℕ} :
   times_cont_diff_on 𝕜 n (prod.snd : E × F → F) s :=
 times_cont_diff.times_cont_diff_on times_cont_diff_snd
 
+/--
+The second projection at a point in a product is `C^∞`.
+-/
+lemma times_cont_diff_at_snd {p : E × F} {n : with_top ℕ} :
+  times_cont_diff_at 𝕜 n (prod.snd : E × F → F) p :=
+times_cont_diff_snd.times_cont_diff_at
+
+/--
+The second projection within a domain at a point in a product is `C^∞`.
+-/
+lemma times_cont_diff_within_at_snd {s : set (E × F)} {p : E × F} {n : with_top ℕ} :
+  times_cont_diff_within_at 𝕜 n (prod.snd : E × F → F) s p :=
+times_cont_diff_snd.times_cont_diff_within_at
+
 /--
 The identity is `C^∞`.
 -/
@@ -1876,7 +1908,7 @@ times_cont_diff_on_univ.1 $ times_cont_diff_on.comp (times_cont_diff_on_univ.2 h
 
 /-- The composition of `C^n` functions at points in domains is `C^n`. -/
 lemma times_cont_diff_within_at.comp
-  {n : with_top ℕ} {s : set E} {t : set F} {g : F → G} {f : E → F} {x : E}
+  {n : with_top ℕ} {s : set E} {t : set F} {g : F → G} {f : E → F} (x : E)
   (hg : times_cont_diff_within_at 𝕜 n g t (f x))
   (hf : times_cont_diff_within_at 𝕜 n f s x) (st : s ⊆ f ⁻¹' t) :
   times_cont_diff_within_at 𝕜 n (g ∘ f) s x :=
@@ -1906,10 +1938,10 @@ end
 
 /-- The composition of `C^n` functions at points in domains is `C^n`. -/
 lemma times_cont_diff_within_at.comp' {n : with_top ℕ} {s : set E} {t : set F} {g : F → G}
-  {f : E → F} {x : E}
+  {f : E → F} (x : E)
   (hg : times_cont_diff_within_at 𝕜 n g t (f x)) (hf : times_cont_diff_within_at 𝕜 n f s x) :
   times_cont_diff_within_at 𝕜 n (g ∘ f) (s ∩ f⁻¹' t) x :=
-hg.comp (hf.mono (inter_subset_left _ _)) (inter_subset_right _ _)
+hg.comp x (hf.mono (inter_subset_left _ _)) (inter_subset_right _ _)
 
 /-- The bundled derivative of a `C^{n+1}` function is `C^n`. -/
 lemma times_cont_diff_on_fderiv_within_apply {m n : with_top  ℕ} {s : set E}
@@ -1996,18 +2028,70 @@ lemma times_cont_diff.sub {n : with_top ℕ} {f g : E → F}
   times_cont_diff 𝕜 n (λx, f x - g x) :=
 hf.add hg.neg
 
-/-- The product map of two `C^n` functions is `C^n`. -/
-lemma times_cont_diff_on.map_prod {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
-  {F' : Type*} [normed_group F'] [normed_space 𝕜 F']
-  {s : set E} {t : set E'} {n : with_top ℕ} {f : E → F} {g : E' → F'}
+section prod_map
+variables {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
+{F' : Type*} [normed_group F'] [normed_space 𝕜 F']
+{n : with_top ℕ}
+
+/-- The product map of two `C^n` functions within a set at a point is `C^n`
+within the product set at the product point. -/
+lemma times_cont_diff_within_at.prod_map'
+  {s : set E} {t : set E'} {f : E → F} {g : E' → F'} {p : E × E'}
+  (hf : times_cont_diff_within_at 𝕜 n f s p.1) (hg : times_cont_diff_within_at 𝕜 n g t p.2) :
+  times_cont_diff_within_at 𝕜 n (prod.map f g) (set.prod s t) p :=
+(hf.comp p times_cont_diff_within_at_fst (prod_subset_preimage_fst _ _)).prod
+  (hg.comp p times_cont_diff_within_at_snd (prod_subset_preimage_snd _ _))
+
+lemma times_cont_diff_within_at.prod_map
+  {s : set E} {t : set E'} {f : E → F} {g : E' → F'} {x : E} {y : E'}
+  (hf : times_cont_diff_within_at 𝕜 n f s x) (hg : times_cont_diff_within_at 𝕜 n g t y) :
+  times_cont_diff_within_at 𝕜 n (prod.map f g) (set.prod s t) (x, y) :=
+begin
+  apply times_cont_diff_within_at.prod_map',
+  exacts [hf, hg]
+end
+
+/-- The product map of two `C^n` functions on a set is `C^n` on the product set. -/
+lemma times_cont_diff_on.prod_map {s : set E} {t : set E'} {f : E → F} {g : E' → F'}
   (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g t) :
   times_cont_diff_on 𝕜 n (prod.map f g) (set.prod s t) :=
+(hf.comp times_cont_diff_on_fst (prod_subset_preimage_fst _ _)).prod
+  (hg.comp (times_cont_diff_on_snd) (prod_subset_preimage_snd _ _))
+
+/-- The product map of two `C^n` functions within a set at a point is `C^n`
+within the product set at the product point. -/
+lemma times_cont_diff_at.prod_map {f : E → F} {g : E' → F'} {x : E} {y : E'}
+  (hf : times_cont_diff_at 𝕜 n f x) (hg : times_cont_diff_at 𝕜 n g y) :
+  times_cont_diff_at 𝕜 n (prod.map f g) (x, y) :=
 begin
-  have hs : s.prod t ⊆ (prod.fst) ⁻¹' s := by { rintros x ⟨h_x_1, h_x_2⟩, exact h_x_1, },
-  have ht : s.prod t ⊆ (prod.snd) ⁻¹' t := by { rintros x ⟨h_x_1, h_x_2⟩, exact h_x_2, },
-  exact (hf.comp (times_cont_diff_on_fst) hs).prod (hg.comp (times_cont_diff_on_snd) ht),
+  rw times_cont_diff_at at *,
+  convert hf.prod_map hg,
+  simp only [univ_prod_univ]
 end
 
+/-- The product map of two `C^n` functions within a set at a point is `C^n`
+within the product set at the product point. -/
+lemma times_cont_diff_at.prod_map' {f : E → F} {g : E' → F'} {p : E × E'}
+  (hf : times_cont_diff_at 𝕜 n f p.1) (hg : times_cont_diff_at 𝕜 n g p.2) :
+  times_cont_diff_at 𝕜 n (prod.map f g) p :=
+begin
+  rcases p,
+  apply times_cont_diff_at.prod_map,
+  exacts [hf, hg]
+end
+
+/-- The product map of two `C^n` functions is `C^n`. -/
+lemma times_cont_diff.prod_map
+  {s : set E} {t : set E'} {f : E → F} {g : E' → F'}
+  (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) :
+  times_cont_diff 𝕜 n (prod.map f g) :=
+begin
+  rw times_cont_diff_iff_times_cont_diff_at at *,
+  exact λ ⟨x, y⟩, (hf x).prod_map (hg y)
+end
+
+end prod_map
+
 section real
 /-!
 ### Results over `ℝ`

src/data/equiv/local_equiv.lean

@@ -77,7 +77,7 @@ set.univ_inter set.preimage_univ set.prod_mk_mem_set_prod_eq and_true set.mem_un
 set.mem_image_of_mem true_and set.mem_inter_eq set.mem_preimage function.comp_app
 set.inter_subset_left set.mem_prod set.range_id and_self set.mem_range_self
 eq_self_iff_true forall_const forall_true_iff set.inter_univ set.preimage_id function.comp.right_id
-not_false_iff and_imp set.prod_inter_prod set.univ_prod_univ true_or or_true
+not_false_iff and_imp set.prod_inter_prod set.univ_prod_univ true_or or_true prod.map_mk
 
 namespace tactic.interactive
 

src/geometry/Lie_group/lie_group.lean

@@ -0,0 +1,224 @@
+/-
+Copyright © 2020 Nicolò Cavalleri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Nicolò Cavalleri.
+-/
+
+import geometry.manifold.constructions
+
+noncomputable theory
+
+/-!
+# Lie groups
+
+We define Lie groups.
+
+## Main definitions and statements
+
+* `Lie_add_group I G` : a Lie additive group where `G` is a manifold on the model with corners `I`.
+* `Lie_group I G`     : a Lie multiplicative group where `G` is a manifold on the model with
+                        corners `I`.
+
+## Implementation notes
+A priori, a Lie group here is a manifold with corner.
+-/
+
+section Lie_group
+
+universes u v
+
+/-- A Lie (additive) group is a group and a smooth manifold at the same time in which
+the addition and negation operations are smooth. -/
+class Lie_add_group {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+  {E : Type*} [normed_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E E)
+  (G : Type*) [add_group G] [topological_space G] [topological_add_group G]
+  [charted_space E G] [smooth_manifold_with_corners I G] : Prop :=
+  (smooth_add : smooth (I.prod I) I (λ p : G×G, p.1 + p.2))
+  (smooth_neg : smooth I I (λ a:G, -a))
+
+/-- A Lie group is a group and a smooth manifold at the same time in which
+the multiplication and inverse operations are smooth. -/
+@[to_additive Lie_add_group]
+class Lie_group {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+  {E : Type*} [normed_group E]
+  [normed_space 𝕜 E] (I : model_with_corners 𝕜 E E)
+  (G : Type*) [group G] [topological_space G] [topological_group G]
+  [charted_space E G] [smooth_manifold_with_corners I G] : Prop :=
+  (smooth_mul : smooth (I.prod I) I (λ p : G×G, p.1 * p.2))
+  (smooth_inv : smooth I I (λ a:G, a⁻¹))
+
+section
+
+variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+{E : Type*} [normed_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E E}
+{F : Type*} [normed_group F] [normed_space 𝕜 F] {J : model_with_corners 𝕜 F F}
+{G : Type*} [topological_space G] [charted_space E G] [smooth_manifold_with_corners I G] [group G]
+[topological_group G] [Lie_group I G]
+{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]
+{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']
+
+@[to_additive]
+lemma smooth_mul : smooth (I.prod I) I (λ p : G×G, p.1 * p.2) :=
+Lie_group.smooth_mul
+
+@[to_additive]
+lemma smooth.mul {f : M → G} {g : M → G} (hf : smooth I' I f) (hg : smooth I' I g) :
+  smooth I' I (f * g) :=
+smooth_mul.comp (hf.prod_mk hg)
+
+@[to_additive]
+lemma smooth_mul_left (a : G) : smooth I I (λ b : G, a * b) :=
+smooth_mul.comp (smooth_const.prod_mk smooth_id)
+
+/-- `L g` denotes left multiplication by `g` -/
+def L : G → G → G := λ g : G, λ x : G, g * x
+
+@[to_additive]
+lemma smooth_mul_right (a : G) : smooth I I (λ b : G, b * a) :=
+smooth_mul.comp (smooth_id.prod_mk smooth_const)
+
+/-- `R g` denotes right multiplication by `g` -/
+def R : G → G → G := λ g : G, λ x : G, x * g
+
+@[to_additive]
+lemma smooth_on.mul {f : M → G} {g : M → G} {s : set M}
+  (hf : smooth_on I' I f s) (hg : smooth_on I' I g s) :
+  smooth_on I' I (f * g) s :=
+(smooth_mul.comp_smooth_on (hf.prod_mk hg) : _)
+
+lemma smooth_pow : ∀ n : ℕ, smooth I I (λ a : G, a ^ n)
+| 0 := by { simp only [pow_zero], exact smooth_const }
+| (k+1) := show smooth I I (λ (a : G), a * a ^ k), from smooth_id.mul (smooth_pow _)
+
+@[to_additive]
+lemma smooth_inv : smooth I I (λ x : G, x⁻¹) :=
+Lie_group.smooth_inv
+
+@[to_additive]
+lemma smooth.inv {f : M → G}
+  (hf : smooth I' I f) : smooth I' I (λx, (f x)⁻¹) :=
+smooth_inv.comp hf
+
+@[to_additive]
+lemma smooth_on.inv {f : M → G} {s : set M}
+  (hf : smooth_on I' I f s) : smooth_on I' I (λx, (f x)⁻¹) s :=
+smooth_inv.comp_smooth_on hf
+
+end
+
+section
+
+/- Instance of product group -/
+/-
+PRODUCT GOT BROKEN AFTER `model_prod` WAS INTRODUCED.
+instance prod_Lie_group {𝕜 : Type*} [nondiscrete_normed_field 𝕜] -/
+/-@[to_additive] how does it work here? The purpose is not replacing prod with sum-/
+/-
+{E : Type*} [normed_group E] [normed_space 𝕜 E]  {I : model_with_corners 𝕜 E E}
+{G : Type*} [topological_space G] [charted_space E G] [smooth_manifold_with_corners I G] [group G]
+[h : Lie_group I G]
+{E' : Type*} [normed_group E'] [normed_space 𝕜 E'] [finite_dimensional 𝕜 E']
+{I' : model_with_corners 𝕜 E' E'}
+{G' : Type*} [topological_space G'] [charted_space E' G'] [smooth_manifold_with_corners I' G']
+[group G'] [h' : Lie_group I' G'] : Lie_group (I.prod I') (G×G') :=
+{ smooth_mul := ((smooth_fst.comp smooth_fst).mul (smooth_fst.comp smooth_snd)).prod_mk
+    ((smooth_snd.comp smooth_fst).mul (smooth_snd.comp smooth_snd)),
+  smooth_inv := smooth_fst.inv.prod_mk smooth_snd.inv, } -/
+
+end
+
+section
+
+variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+{E : Type*} [normed_group E] [normed_space 𝕜 E]
+{E' : Type*} [normed_group E'] [normed_space 𝕜 E']
+
+/-- Morphism of additive Lie groups. -/
+structure Lie_add_group_morphism (I : model_with_corners 𝕜 E E) (I' : model_with_corners 𝕜 E' E')
+(G : Type*) [topological_space G] [charted_space E G] [smooth_manifold_with_corners I G]
+[add_group G] [topological_add_group G] [Lie_add_group I G]
+(G' : Type*) [topological_space G'] [charted_space E' G'] [smooth_manifold_with_corners I' G']
+[add_group G'] [topological_add_group G'] [Lie_add_group I' G'] extends add_monoid_hom G G' :=
+  (smooth_to_fun : smooth I I' to_fun)
+
+/-- Morphism of Lie groups. -/
+@[to_additive Lie_add_group_morphism]
+structure Lie_group_morphism (I : model_with_corners 𝕜 E E) (I' : model_with_corners 𝕜 E' E')
+(G : Type*) [topological_space G] [charted_space E G] [smooth_manifold_with_corners I G] [group G]
+[topological_group G] [Lie_group I G]
+(G' : Type*) [topological_space G'] [charted_space E' G'] [smooth_manifold_with_corners I' G']
+[group G'] [topological_group G'] [Lie_group I' G'] extends monoid_hom G G' :=
+  (smooth_to_fun : smooth I I' to_fun)
+
+variables {I : model_with_corners 𝕜 E E} {I' : model_with_corners 𝕜 E' E'}
+{G : Type*} [topological_space G] [charted_space E G] [smooth_manifold_with_corners I G]
+[group G] [topological_group G] [Lie_group I G]
+{G' : Type*} [topological_space G'] [charted_space E' G'] [smooth_manifold_with_corners I' G']
+[group G'] [topological_group G'] [Lie_group I' G']
+
+@[to_additive]
+instance : has_one (Lie_group_morphism I I' G G') := ⟨⟨1, smooth_const⟩⟩
+
+@[to_additive]
+instance : inhabited (Lie_group_morphism I I' G G') := ⟨1⟩
+
+@[to_additive]
+instance : has_coe_to_fun (Lie_group_morphism I I' G G') := ⟨_, λ a, a.to_fun⟩
+
+end
+
+end Lie_group
+
+section Lie_group_core
+
+/-- Sometimes one might want to define a Lie additive group `G` without having proved previously
+that `G` is a topological additive group. In such case it is possible to use `Lie_add_group_core`
+that does not require such instance, and then get a Lie group by invoking `to_Lie_ad_group`. -/
+@[nolint has_inhabited_instance]
+structure Lie_add_group_core {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+  {E : Type*} [normed_group E]
+  [normed_space 𝕜 E] (I : model_with_corners 𝕜 E E)
+  (G : Type*) [add_group G] [topological_space G]
+  [charted_space E G] [smooth_manifold_with_corners I G] : Prop :=
+  (smooth_add : smooth (I.prod I) I (λ p : G×G, p.1 + p.2))
+  (smooth_neg : smooth I I (λ a:G, -a))
+
+/-- Sometimes one might want to define a Lie group `G` without having proved previously that `G` is
+a topological group. In such case it is possible to use `Lie_group_core` that does not require such
+instance, and then get a Lie group by invoking `to_Lie_group` defined below. -/
+@[nolint has_inhabited_instance, to_additive Lie_add_group_core]
+structure Lie_group_core {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+  {E : Type*} [normed_group E]
+  [normed_space 𝕜 E] (I : model_with_corners 𝕜 E E)
+  (G : Type*) [group G] [topological_space G]
+  [charted_space E G] [smooth_manifold_with_corners I G] : Prop :=
+  (smooth_mul : smooth (I.prod I) I (λ p : G×G, p.1 * p.2))
+  (smooth_inv : smooth I I (λ a:G, a⁻¹))
+
+variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+{E : Type*} [normed_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E E}
+{F : Type*} [normed_group F] [normed_space 𝕜 F] {J : model_with_corners 𝕜 F F}
+{G : Type*} [topological_space G] [charted_space E G] [smooth_manifold_with_corners I G] [group G]
+[topological_group G] [Lie_group I G]
+
+namespace Lie_group_core
+
+variables (c : Lie_group_core I G)
+
+@[to_additive]
+protected lemma to_topological_group : topological_group G :=
+{ continuous_mul := c.smooth_mul.continuous,
+  continuous_inv := c.smooth_inv.continuous, }
+
+@[to_additive]
+protected lemma to_Lie_group : @Lie_group 𝕜 _ E _ _ I G _ _ c.to_topological_group _ _ :=
+{ smooth_mul := c.smooth_mul,
+  smooth_inv := c.smooth_inv, }
+
+end Lie_group_core
+
+end Lie_group_core