feat(geometry): first stab on Lie groups (#3529)

src/algebra/group/defs.lean

@@ -48,6 +48,20 @@ universe u
    to the additive one.
 -/
 
+section has_mul
+
+variables {G : Type u} [has_mul G]
+
+/-- `left_mul g` denotes left multiplication by `g` -/
+@[to_additive "`left_add g` denotes left addition by `g`"]
+def left_mul : G → G → G := λ g : G, λ x : G, g * x
+
+/-- `right_mul g` denotes right multiplication by `g` -/
+@[to_additive "`right_add g` denotes right addition by `g`"]
+def right_mul : G → G → G := λ g : G, λ x : G, x * g
+
+end has_mul
+
 /-- A semigroup is a type with an associative `(*)`. -/
 @[protect_proj, ancestor has_mul] class semigroup (G : Type u) extends has_mul G :=
 (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))

src/analysis/calculus/times_cont_diff.lean

@@ -1488,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^∞`.
 -/
@@ -1501,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^∞`.
 -/
@@ -1980,20 +2008,23 @@ begin
   exact hf.add hg
 end
 
+lemma times_cont_diff_add {n : with_top ℕ} : times_cont_diff 𝕜 n (λp : F × F, p.1 + p.2) :=
+begin
+  apply is_bounded_linear_map.times_cont_diff,
+  exact is_bounded_linear_map.add is_bounded_linear_map.fst is_bounded_linear_map.snd,
+end
+
+/-- The sum of two `C^n`functions is `C^n`. -/
+lemma times_cont_diff.add {n : with_top ℕ} {f g : E → F}
+  (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) : times_cont_diff 𝕜 n (λx, f x + g x) :=
+times_cont_diff_add.comp (hf.prod hg)
+
 /-- The sum of two `C^n` functions on a domain is `C^n`. -/
 lemma times_cont_diff_on.add {n : with_top ℕ} {s : set E} {f g : E → F}
   (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) :
   times_cont_diff_on 𝕜 n (λx, f x + g x) s :=
 λ x hx, (hf x hx).add (hg x hx)
 
-/-- The sum of two `C^n` functions is `C^n`. -/
-lemma times_cont_diff.add {n : with_top ℕ} {f g : E → F}
-  (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) : times_cont_diff 𝕜 n (λx, f x + g x) :=
-begin
-  rw ← times_cont_diff_on_univ at *,
-  exact hf.add hg
-end
-
 /-! ### Negative -/
 
 /-- The negative of a `C^n` function within a domain at a point is `C^n` within this domain at
@@ -2015,19 +2046,22 @@ begin
   exact hf.neg
 end
 
+lemma times_cont_diff_neg {n : with_top ℕ} : times_cont_diff 𝕜 n (λp : F, -p) :=
+begin
+  apply is_bounded_linear_map.times_cont_diff,
+  exact is_bounded_linear_map.neg is_bounded_linear_map.id
+end
+
+/-- The negative of a `C^n`function is `C^n`. -/
+lemma times_cont_diff.neg {n : with_top ℕ} {f : E → F} (hf : times_cont_diff 𝕜 n f) :
+  times_cont_diff 𝕜 n (λx, -f x) :=
+times_cont_diff_neg.comp hf
+
 /-- The negative of a `C^n` function on a domain is `C^n`. -/
 lemma times_cont_diff_on.neg {n : with_top ℕ} {s : set E} {f : E → F}
   (hf : times_cont_diff_on 𝕜 n f s) : times_cont_diff_on 𝕜 n (λx, -f x) s :=
 λ x hx, (hf x hx).neg
 
-/-- The negative of a `C^n` function is `C^n`. -/
-lemma times_cont_diff.neg {n : with_top ℕ} {f : E → F} (hf : times_cont_diff 𝕜 n f) :
-  times_cont_diff 𝕜 n (λx, -f x) :=
-begin
-  rw ← times_cont_diff_on_univ at *,
-  exact hf.neg
-end
-
 /-! ### Subtraction -/
 
 /-- The difference of two `C^n` functions within a set at a point is `C^n` within this set
@@ -2094,18 +2128,68 @@ end
 
 /-! ### Cartesian product of two functions-/
 
-/-- 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']
+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) :=
+times_cont_diff_within_at.prod_map' hf hg
+
+/-- 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 {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'}
   (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
+  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
-  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),
+  rcases p,
+  exact times_cont_diff_at.prod_map hf hg
 end
 
+/-- The product map of two `C^n` functions is `C^n`. -/
+lemma times_cont_diff.prod_map
+  {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,8 @@ 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
+set.preimage_inter
 
 namespace tactic.interactive