From 43ccce552af4206cc5a96916ea72643c51cba0ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicol=C3=B2=20Cavalleri?= Date: Thu, 30 Jul 2020 17:59:32 +0000 Subject: [PATCH] feat(geometry): first stab on Lie groups (#3529) --- src/algebra/group/defs.lean | 14 + src/analysis/calculus/times_cont_diff.lean | 126 ++++- src/data/equiv/local_equiv.lean | 3 +- src/geometry/algebra/lie_group.lean | 271 ++++++++++ .../smooth_manifold_with_corners.lean | 4 +- src/geometry/manifold/times_cont_mdiff.lean | 469 +++++++++++++++++- src/topology/continuous_on.lean | 20 + 7 files changed, 872 insertions(+), 35 deletions(-) create mode 100644 src/geometry/algebra/lie_group.lean diff --git a/src/algebra/group/defs.lean b/src/algebra/group/defs.lean index 12df72b51d755..c66226158afd0 100644 --- a/src/algebra/group/defs.lean +++ b/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)) diff --git a/src/analysis/calculus/times_cont_diff.lean b/src/analysis/calculus/times_cont_diff.lean index b39141d515f2f..35a3476184723 100644 --- a/src/analysis/calculus/times_cont_diff.lean +++ b/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 `ℝ` diff --git a/src/data/equiv/local_equiv.lean b/src/data/equiv/local_equiv.lean index 2b34575485843..0344346820960 100644 --- a/src/data/equiv/local_equiv.lean +++ b/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 diff --git a/src/geometry/algebra/lie_group.lean b/src/geometry/algebra/lie_group.lean new file mode 100644 index 0000000000000..08476506d460f --- /dev/null +++ b/src/geometry/algebra/lie_group.lean @@ -0,0 +1,271 @@ +/- +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.times_cont_mdiff + +/-! +# Lie groups + +A Lie group is a group that is also a smooth manifold, in which the group operations of +multiplication and inversion are smooth maps. Smoothness of the group multiplication means that +multiplication is a smooth mapping of the product manifold `G` × `G` into `G`. + +Note that, since a manifold here is not second-countable and Hausdorff a Lie group here is not +guaranteed to be second-countable (even though it can be proved it is Hausdorff). Note also that Lie +groups here are not necessarily finite dimensional. + +## 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`. +* `lie_add_group_morphism I I' G G'` : morphism of addittive Lie groups +* `lie_group_morphism I I' G G'` : morphism of Lie groups +* `lie_add_group_core I G` : allows to define a Lie additive group without first proving + it is a topological additive group. +* `lie_group_core I G` : allows to define a Lie group without first proving + it is a topological group. + +* `reals_lie_group` : real numbers are a 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 +model space and as the model vector space, as one might hope, beause in the product situation, +the model space is `model_prod E E'` and the model vector space is `E × E'`, which are not the same, +so the definition does not apply. Hence the definition should be more general, allowing +`I : model_with_corners 𝕜 E H`. +-/ + +noncomputable theory + +section lie_group + +set_option default_priority 100 + +/-- 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 𝕜] + {H : Type*} [topological_space H] + {E : Type*} [normed_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) + (G : Type*) [add_group G] [topological_space G] [topological_add_group G] [charted_space H G] + extends 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] +class lie_group {𝕜 : Type*} [nondiscrete_normed_field 𝕜] + {H : Type*} [topological_space H] + {E : Type*} [normed_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H) + (G : Type*) [group G] [topological_space G] [topological_group G] [charted_space H G] + extends 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 lie_group + +variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] +{H : Type*} [topological_space H] +{E : Type*} [normed_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} +{F : Type*} [normed_group F] [normed_space 𝕜 F] {J : model_with_corners 𝕜 F F} +{G : Type*} [topological_space G] [charted_space H 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) + +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 + +@[to_additive] +lemma smooth_left_mul {a : G} : smooth I I (left_mul a) := +smooth_mul.comp (smooth_const.prod_mk smooth_id) + +@[to_additive] +lemma smooth_right_mul {a : G} : smooth I I (right_mul a) := +smooth_mul.comp (smooth_id.prod_mk smooth_const) + +@[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 lie_group + +section prod_lie_group + +/- Instance of product group -/ +@[to_additive] +instance {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {H : Type*} [topological_space H] + {E : Type*} [normed_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H} + {G : Type*} [topological_space G] [charted_space H G] [group G] [topological_group G] + [h : lie_group I G] {E' : Type*} [normed_group E'] [normed_space 𝕜 E'] + {H' : Type*} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} + {G' : Type*} [topological_space G'] [charted_space H' G'] + [group G'] [topological_group G'] [h' : lie_group I' G'] : lie_group (I.prod I') (G×G') := +{ smooth_mul := ((smooth_fst.comp smooth_fst).smooth.mul (smooth_fst.comp smooth_snd)).prod_mk + ((smooth_snd.comp smooth_fst).smooth.mul (smooth_snd.comp smooth_snd)), + smooth_inv := smooth_fst.inv.prod_mk smooth_snd.inv, } + +end prod_lie_group + +section lie_add_group_morphism + +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] +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 lie_add_group_morphism + +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_add_group`. -/ +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. -/ +@[to_additive] +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] + +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 + +/-! ### Real numbers are a Lie group -/ + +section real_numbers_lie_group + +instance normed_group_lie_group {𝕜 : Type*} [nondiscrete_normed_field 𝕜] +{E : Type*} [normed_group E] [normed_space 𝕜 E] : +lie_add_group (model_with_corners_self 𝕜 E) E := +{ smooth_add := + begin + rw smooth_iff, + refine ⟨continuous_add, λ x y, _⟩, + simp only [prod.mk.eta] with mfld_simps, + rw times_cont_diff_on_univ, + exact times_cont_diff_add, + end, + smooth_neg := + begin + rw smooth_iff, + refine ⟨continuous_neg, λ x y, _⟩, + simp only [prod.mk.eta] with mfld_simps, + rw times_cont_diff_on_univ, + exact times_cont_diff_neg, + end } + +instance reals_lie_group : lie_add_group (model_with_corners_self ℝ ℝ) ℝ := by apply_instance + +end real_numbers_lie_group diff --git a/src/geometry/manifold/smooth_manifold_with_corners.lean b/src/geometry/manifold/smooth_manifold_with_corners.lean index a169d7e06bcb7..b13cd7e811490 100644 --- a/src/geometry/manifold/smooth_manifold_with_corners.lean +++ b/src/geometry/manifold/smooth_manifold_with_corners.lean @@ -462,12 +462,12 @@ begin simp only at he he_symm he' he'_symm, split; simp only [local_equiv.prod_source, local_homeomorph.prod_to_local_equiv], - { have h3 := times_cont_diff_on.map_prod he he', + { have h3 := times_cont_diff_on.prod_map he he', rw [← model_with_corners.image I _, ← model_with_corners.image I' _, set.prod_image_image_eq] at h3, rw ← model_with_corners.image (I.prod I') _, exact h3, }, - { have h3 := times_cont_diff_on.map_prod he_symm he'_symm, + { have h3 := times_cont_diff_on.prod_map he_symm he'_symm, rw [← model_with_corners.image I _, ← model_with_corners.image I' _, set.prod_image_image_eq] at h3, rw ← model_with_corners.image (I.prod I') _, diff --git a/src/geometry/manifold/times_cont_mdiff.lean b/src/geometry/manifold/times_cont_mdiff.lean index 08ff6102156f0..a7e632ca02d49 100644 --- a/src/geometry/manifold/times_cont_mdiff.lean +++ b/src/geometry/manifold/times_cont_mdiff.lean @@ -53,14 +53,24 @@ open_locale topological_space manifold /-! ### Definition of smooth functions between manifolds -/ variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] +-- declare a smooth manifold `M` over the pair `(E, H)`. {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] [Is : smooth_manifold_with_corners I M] +-- declare a smooth manifold `M'` over the pair `(E', H')`. {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'] [I's : smooth_manifold_with_corners I' M'] -{f f₁ : M → M'} {s s₁ t : set M} {x : M} -{m n : with_top ℕ} +-- declare a smooth manifold `N` over the pair `(F, G)`. +{F : Type*} [normed_group F] [normed_space 𝕜 F] +{G : Type*} [topological_space G] {J : model_with_corners 𝕜 F G} +{N : Type*} [topological_space N] [charted_space G N] [Js : smooth_manifold_with_corners J N] +-- declare a smooth manifold `N'` over the pair `(F', G')`. +{F' : Type*} [normed_group F'] [normed_space 𝕜 F'] +{G' : Type*} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} +{N' : Type*} [topological_space N'] [charted_space G' N'] [J's : smooth_manifold_with_corners J' N'] +-- declare functions, sets, points and smoothness indices +{f f₁ : M → M'} {s s₁ t : set M} {x : M} {m n : with_top ℕ} /-- Property in the model space of a model with corners of being `C^n` within at set at a point, when read in the model vector space. This property will be lifted to manifolds to define smooth @@ -144,41 +154,108 @@ read in the preferred chart at this point. -/ def times_cont_mdiff_within_at (n : with_top ℕ) (f : M → M') (s : set M) (x : M) := lift_prop_within_at (times_cont_diff_within_at_prop I I' n) f s x +/-- Abbreviation for `times_cont_mdiff_within_at I I' ⊤ f s x`. See also documentation for `smooth`. +-/ +@[reducible] def smooth_within_at (f : M → M') (s : set M) (x : M) := + times_cont_mdiff_within_at I I' ⊤ f s x + /-- A function is `n` times continuously differentiable at a point in a manifold if it is continuous and it is `n` times continuously differentiable around this point, when read in the preferred chart at this point. -/ def times_cont_mdiff_at (n : with_top ℕ) (f : M → M') (x : M) := times_cont_mdiff_within_at I I' n f univ x +/-- Abbreviation for `times_cont_mdiff_at I I' ⊤ f x`. See also documentation for `smooth`. -/ +@[reducible] def smooth_at (f : M → M') (x : M) := times_cont_mdiff_at I I' ⊤ f x + /-- A function is `n` times continuously differentiable in a set of a manifold if it is continuous and, for any pair of points, it is `n` times continuously differentiable on this set in the charts around these points. -/ def times_cont_mdiff_on (n : with_top ℕ) (f : M → M') (s : set M) := ∀ x ∈ s, times_cont_mdiff_within_at I I' n f s x +/-- Abbreviation for `times_cont_mdiff_on I I' ⊤ f s`. See also documentation for `smooth`. -/ +@[reducible] def smooth_on (f : M → M') (s : set M) := times_cont_mdiff_on I I' ⊤ f s + /-- A function is `n` times continuously differentiable in a manifold if it is continuous and, for any pair of points, it is `n` times continuously differentiable in the charts around these points. -/ def times_cont_mdiff (n : with_top ℕ) (f : M → M') := ∀ x, times_cont_mdiff_at I I' n f x +/-- Abbreviation for `times_cont_mdiff I I' ⊤ f`. +Short note to work with these abbreviations: a lemma of the form `times_cont_mdiff_foo.bar` will +apply fine to an assumption `smooth_foo` using dot notation or normal notation. +If the consequence `bar` of the lemma involves `times_cont_diff`, it is still better to restate +the lemma replacing `times_cont_diff` with `smooth` both in the assumption and in the conclusion, +to make it possible to use `smooth` consistently. +This also applies to `smooth_at`, `smooth_on` and `smooth_within_at`.-/ +@[reducible] def smooth (f : M → M') := times_cont_mdiff I I' ⊤ f + /-! ### Basic properties of smooth functions between manifolds -/ variables {I I'} +lemma times_cont_mdiff.smooth (h : times_cont_mdiff I I' ⊤ f) : smooth I I' f := h + +lemma smooth.times_cont_mdiff (h : smooth I I' f) : times_cont_mdiff I I' ⊤ f := h + +lemma times_cont_mdiff_on.smooth_on (h : times_cont_mdiff_on I I' ⊤ f s) : smooth_on I I' f s := h + +lemma smooth_on.times_cont_mdiff_on (h : smooth_on I I' f s) : times_cont_mdiff_on I I' ⊤ f s := h + +lemma times_cont_mdiff_at.smooth_at (h : times_cont_mdiff_at I I' ⊤ f x) : smooth_at I I' f x := h + +lemma smooth_at.times_cont_mdiff_at (h : smooth_at I I' f x) : times_cont_mdiff_at I I' ⊤ f x := h + +lemma times_cont_mdiff_within_at.smooth_within_at (h : times_cont_mdiff_within_at I I' ⊤ f s x) : + smooth_within_at I I' f s x := h + +lemma smooth_within_at.times_cont_mdiff_within_at (h : smooth_within_at I I' f s x) : +times_cont_mdiff_within_at I I' ⊤ f s x := h + lemma times_cont_mdiff.times_cont_mdiff_at (h : times_cont_mdiff I I' n f) : times_cont_mdiff_at I I' n f x := h x +lemma smooth.smooth_at (h : smooth I I' f) : + smooth_at I I' f x := times_cont_mdiff.times_cont_mdiff_at h + lemma times_cont_mdiff_within_at_univ : times_cont_mdiff_within_at I I' n f univ x ↔ times_cont_mdiff_at I I' n f x := iff.rfl +lemma smooth_at_univ : + smooth_within_at I I' f univ x ↔ smooth_at I I' f x := times_cont_mdiff_within_at_univ + lemma times_cont_mdiff_on_univ : times_cont_mdiff_on I I' n f univ ↔ times_cont_mdiff I I' n f := by simp only [times_cont_mdiff_on, times_cont_mdiff, times_cont_mdiff_within_at_univ, forall_prop_of_true, mem_univ] +lemma smooth_on_univ : + smooth_on I I' f univ ↔ smooth I I' f := times_cont_mdiff_on_univ + +/-- One can reformulate smoothness within a set at a point as continuity within this set at this +point, and smoothness in the corresponding extended chart. -/ +lemma times_cont_mdiff_within_at_iff : + times_cont_mdiff_within_at I I' n f s x ↔ continuous_within_at f s x ∧ + times_cont_diff_within_at 𝕜 n ((ext_chart_at I' (f x)) ∘ f ∘ (ext_chart_at I x).symm) + ((ext_chart_at I x).target ∩ (ext_chart_at I x).symm ⁻¹' (s ∩ f ⁻¹' (ext_chart_at I' (f x)).source)) + (ext_chart_at I x x) := +begin + rw [times_cont_mdiff_within_at, lift_prop_within_at, times_cont_diff_within_at_prop], + congr' 3, + mfld_set_tac +end + +lemma smooth_within_at_iff : + smooth_within_at I I' f s x ↔ continuous_within_at f s x ∧ + times_cont_diff_within_at 𝕜 ∞ ((ext_chart_at I' (f x)) ∘ f ∘ (ext_chart_at I x).symm) + ((ext_chart_at I x).target ∩ (ext_chart_at I x).symm ⁻¹' (s ∩ f ⁻¹' (ext_chart_at I' (f x)).source)) + (ext_chart_at I x x) := +times_cont_mdiff_within_at_iff + include Is I's /-- One can reformulate smoothness on a set as continuity on this set, and smoothness in any @@ -210,6 +287,12 @@ begin mfld_set_tac } end +lemma smooth_on_iff : + smooth_on I I' f s ↔ continuous_on f s ∧ + ∀ (x : M) (y : M'), times_cont_diff_on 𝕜 ⊤ ((ext_chart_at I' y) ∘ f ∘ (ext_chart_at I x).symm) + ((ext_chart_at I x).target ∩ (ext_chart_at I x).symm ⁻¹' (s ∩ f ⁻¹' (ext_chart_at I' y).source)) := +times_cont_mdiff_on_iff + /-- One can reformulate smoothness as continuity and smoothness in any extended chart. -/ lemma times_cont_mdiff_iff : times_cont_mdiff I I' n f ↔ continuous f ∧ @@ -217,6 +300,12 @@ lemma times_cont_mdiff_iff : ((ext_chart_at I x).target ∩ (ext_chart_at I x).symm ⁻¹' (f ⁻¹' (ext_chart_at I' y).source)) := by simp [← times_cont_mdiff_on_univ, times_cont_mdiff_on_iff, continuous_iff_continuous_on_univ] +lemma smooth_iff : + smooth I I' f ↔ continuous f ∧ + ∀ (x : M) (y : M'), times_cont_diff_on 𝕜 ⊤ ((ext_chart_at I' y) ∘ f ∘ (ext_chart_at I x).symm) + ((ext_chart_at I x).target ∩ (ext_chart_at I x).symm ⁻¹' (f ⁻¹' (ext_chart_at I' y).source)) := +times_cont_mdiff_iff + omit Is I's /-! ### Deducing smoothness from higher smoothness -/ @@ -303,20 +392,20 @@ lemma times_cont_mdiff.mdifferentiable (hf : times_cont_mdiff I I' n f) (hn : 1 /-! ### `C^∞` smoothness -/ lemma times_cont_mdiff_within_at_top : - times_cont_mdiff_within_at I I' ∞ f s x ↔ (∀n:ℕ, times_cont_mdiff_within_at I I' n f s x) := + smooth_within_at I I' f s x ↔ (∀n:ℕ, times_cont_mdiff_within_at I I' n f s x) := ⟨λ h n, ⟨h.1, times_cont_diff_within_at_top.1 h.2 n⟩, λ H, ⟨(H 0).1, times_cont_diff_within_at_top.2 (λ n, (H n).2)⟩⟩ lemma times_cont_mdiff_at_top : - times_cont_mdiff_at I I' ∞ f x ↔ (∀n:ℕ, times_cont_mdiff_at I I' n f x) := + smooth_at I I' f x ↔ (∀n:ℕ, times_cont_mdiff_at I I' n f x) := times_cont_mdiff_within_at_top lemma times_cont_mdiff_on_top : - times_cont_mdiff_on I I' ∞ f s ↔ (∀n:ℕ, times_cont_mdiff_on I I' n f s) := + smooth_on I I' f s ↔ (∀n:ℕ, times_cont_mdiff_on I I' n f s) := ⟨λ h n, h.of_le le_top, λ h x hx, times_cont_mdiff_within_at_top.2 (λ n, h n x hx)⟩ lemma times_cont_mdiff_top : - times_cont_mdiff I I' ∞ f ↔ (∀n:ℕ, times_cont_mdiff I I' n f) := + smooth I I' f ↔ (∀n:ℕ, times_cont_mdiff I I' n f) := ⟨λ h n, h.of_le le_top, λ h x, times_cont_mdiff_within_at_top.2 (λ n, h n x)⟩ lemma times_cont_mdiff_within_at_iff_nat : @@ -340,6 +429,10 @@ lemma times_cont_mdiff_at.times_cont_mdiff_within_at (hf : times_cont_mdiff_at I times_cont_mdiff_within_at I I' n f s x := times_cont_mdiff_within_at.mono hf (subset_univ _) +lemma smooth_at.smooth_within_at (hf : smooth_at I I' f x) : + smooth_within_at I I' f s x := +times_cont_mdiff_at.times_cont_mdiff_within_at hf + lemma times_cont_mdiff_on.mono (hf : times_cont_mdiff_on I I' n f s) (hts : t ⊆ s) : times_cont_mdiff_on I I' n f t := λ x hx, (hf x (hts hx)).mono hts @@ -348,6 +441,10 @@ lemma times_cont_mdiff.times_cont_mdiff_on (hf : times_cont_mdiff I I' n f) : times_cont_mdiff_on I I' n f s := λ x hx, (hf x).times_cont_mdiff_within_at +lemma smooth.smooth_on (hf : smooth I I' f) : + smooth_on I I' f s := +times_cont_mdiff.times_cont_mdiff_on hf + lemma times_cont_mdiff_within_at_inter' (ht : t ∈ nhds_within x s) : times_cont_mdiff_within_at I I' n f (s ∩ t) x ↔ times_cont_mdiff_within_at I I' n f s x := (times_cont_diff_within_at_local_invariant_prop I I' n).lift_prop_within_at_inter' ht @@ -361,6 +458,11 @@ lemma times_cont_mdiff_within_at.times_cont_mdiff_at times_cont_mdiff_at I I' n f x := (times_cont_diff_within_at_local_invariant_prop I I' n).lift_prop_at_of_lift_prop_within_at h ht +lemma smooth_within_at.smooth_at + (h : smooth_within_at I I' f s x) (ht : s ∈ 𝓝 x) : + smooth_at I I' f x := +times_cont_mdiff_within_at.times_cont_mdiff_at h ht + include Is I's /-- A function is `C^n` within a set at a point, for `n : ℕ`, if and only if it is `C^n` on @@ -572,7 +674,7 @@ begin end /-- The composition of `C^n` functions within domains at points is `C^n`. -/ -lemma times_cont_mdiff_within_at.comp {t : set M'} {g : M' → M''} +lemma times_cont_mdiff_within_at.comp {t : set M'} {g : M' → M''} (x : M) (hg : times_cont_mdiff_within_at I' I'' n g t (f x)) (hf : times_cont_mdiff_within_at I I' n f s x) (st : s ⊆ f ⁻¹' t) : times_cont_mdiff_within_at I I'' n (g ∘ f) s x := @@ -592,17 +694,27 @@ begin end /-- The composition of `C^n` functions within domains at points is `C^n`. -/ -lemma times_cont_mdiff_within_at.comp' {t : set M'} {g : M' → M''} +lemma times_cont_mdiff_within_at.comp' {t : set M'} {g : M' → M''} (x : M) (hg : times_cont_mdiff_within_at I' I'' n g t (f x)) (hf : times_cont_mdiff_within_at I I' n f s x) : times_cont_mdiff_within_at I I'' 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 composition of `C^n` functions at points is `C^n`. -/ -lemma times_cont_mdiff_at.comp {g : M' → M''} +lemma times_cont_mdiff_at.comp {g : M' → M''} (x : M) (hg : times_cont_mdiff_at I' I'' n g (f x)) (hf : times_cont_mdiff_at I I' n f x) : times_cont_mdiff_at I I'' n (g ∘ f) x := -hg.comp hf subset_preimage_univ +hg.comp x hf subset_preimage_univ + +lemma times_cont_mdiff.comp_times_cont_mdiff_on {f : M → M'} {g : M' → M''} {s : set M} + (hg : times_cont_mdiff I' I'' n g) (hf : times_cont_mdiff_on I I' n f s) : + times_cont_mdiff_on I I'' n (g ∘ f) s := +hg.times_cont_mdiff_on.comp hf set.subset_preimage_univ + +lemma smooth.comp_smooth_on {f : M → M'} {g : M' → M''} {s : set M} + (hg : smooth I' I'' g) (hf : smooth_on I I' f s) : + smooth_on I I'' (g ∘ f) s := +hg.smooth_on.comp hf set.subset_preimage_univ end composition @@ -645,15 +757,23 @@ lemma times_cont_mdiff_id : times_cont_mdiff I I n (id : M → M) := times_cont_mdiff.of_le ((times_cont_diff_within_at_local_invariant_prop I I ∞).lift_prop_id (times_cont_diff_within_at_local_invariant_prop_id I)) le_top +lemma smooth_id : smooth I I (id : M → M) := times_cont_mdiff_id + lemma times_cont_mdiff_on_id : times_cont_mdiff_on I I n (id : M → M) s := times_cont_mdiff_id.times_cont_mdiff_on +lemma smooth_on_id : smooth_on I I (id : M → M) s := times_cont_mdiff_on_id + lemma times_cont_mdiff_at_id : times_cont_mdiff_at I I n (id : M → M) x := times_cont_mdiff_id.times_cont_mdiff_at +lemma smooth_at_id : smooth_at I I (id : M → M) x := times_cont_mdiff_at_id + lemma times_cont_mdiff_within_at_id : times_cont_mdiff_within_at I I n (id : M → M) s x := times_cont_mdiff_at_id.times_cont_mdiff_within_at +lemma smooth_within_at_id : smooth_within_at I I (id : M → M) s x := times_cont_mdiff_within_at_id + end id /-! ### Constants are smooth -/ @@ -669,15 +789,26 @@ begin exact times_cont_diff_within_at_const, end +lemma smooth_const : smooth I I' (λ (x : M), c) := times_cont_mdiff_const + lemma times_cont_mdiff_on_const : times_cont_mdiff_on I I' n (λ (x : M), c) s := times_cont_mdiff_const.times_cont_mdiff_on +lemma smooth_on_const : smooth_on I I' (λ (x : M), c) s := +times_cont_mdiff_on_const + lemma times_cont_mdiff_at_const : times_cont_mdiff_at I I' n (λ (x : M), c) x := times_cont_mdiff_const.times_cont_mdiff_at +lemma smooth_at_const : smooth_at I I' (λ (x : M), c) x := +times_cont_mdiff_at_const + lemma times_cont_mdiff_within_at_const : times_cont_mdiff_within_at I I' n (λ (x : M), c) s x := times_cont_mdiff_at_const.times_cont_mdiff_within_at +lemma smooth_within_at_const : smooth_within_at I I' (λ (x : M), c) s x := +times_cont_mdiff_within_at_const + end id /-! ### Equivalence with the basic definition for functions between vector spaces -/ @@ -1043,3 +1174,319 @@ begin end end tangent_map + +/-! ### Smoothness of the projection in a basic smooth bundle -/ + +namespace basic_smooth_bundle_core + +variables (Z : basic_smooth_bundle_core I M E') + +lemma times_cont_mdiff_proj : + times_cont_mdiff ((I.prod (model_with_corners_self 𝕜 E'))) I n + Z.to_topological_fiber_bundle_core.proj := +begin + assume x, + rw [times_cont_mdiff_at, times_cont_mdiff_within_at_iff], + refine ⟨Z.to_topological_fiber_bundle_core.continuous_proj.continuous_at.continuous_within_at, _⟩, + simp only [(∘), chart_at, chart] with mfld_simps, + apply times_cont_diff_within_at_fst.congr, + { rintros ⟨a, b⟩ hab, + simp only with mfld_simps at hab, + simp only [hab] with mfld_simps }, + { simp only with mfld_simps } +end + +lemma smooth_proj : + smooth ((I.prod (model_with_corners_self 𝕜 E'))) I Z.to_topological_fiber_bundle_core.proj := +times_cont_mdiff_proj Z + +lemma times_cont_mdiff_on_proj {s : set (Z.to_topological_fiber_bundle_core.total_space)} : + times_cont_mdiff_on ((I.prod (model_with_corners_self 𝕜 E'))) I n + Z.to_topological_fiber_bundle_core.proj s := +Z.times_cont_mdiff_proj.times_cont_mdiff_on + +lemma smooth_on_proj {s : set (Z.to_topological_fiber_bundle_core.total_space)} : + smooth_on ((I.prod (model_with_corners_self 𝕜 E'))) I Z.to_topological_fiber_bundle_core.proj s := +times_cont_mdiff_on_proj Z + +lemma times_cont_mdiff_at_proj {p : Z.to_topological_fiber_bundle_core.total_space} : + times_cont_mdiff_at ((I.prod (model_with_corners_self 𝕜 E'))) I n + Z.to_topological_fiber_bundle_core.proj p := +Z.times_cont_mdiff_proj.times_cont_mdiff_at + +lemma smooth_at_proj {p : Z.to_topological_fiber_bundle_core.total_space} : + smooth_at ((I.prod (model_with_corners_self 𝕜 E'))) I Z.to_topological_fiber_bundle_core.proj p := +Z.times_cont_mdiff_at_proj + +lemma times_cont_mdiff_within_at_proj + {s : set (Z.to_topological_fiber_bundle_core.total_space)} + {p : Z.to_topological_fiber_bundle_core.total_space} : + times_cont_mdiff_within_at ((I.prod (model_with_corners_self 𝕜 E'))) I n + Z.to_topological_fiber_bundle_core.proj s p := +Z.times_cont_mdiff_at_proj.times_cont_mdiff_within_at + +lemma smooth_within_at_proj + {s : set (Z.to_topological_fiber_bundle_core.total_space)} + {p : Z.to_topological_fiber_bundle_core.total_space} : + smooth_within_at ((I.prod (model_with_corners_self 𝕜 E'))) I + Z.to_topological_fiber_bundle_core.proj s p := +Z.times_cont_mdiff_within_at_proj + +end basic_smooth_bundle_core + +/-! ### Smoothness of the tangent bundle projection -/ + +namespace tangent_bundle + +include Is + +lemma times_cont_mdiff_proj : + times_cont_mdiff I.tangent I n (proj I M) := +basic_smooth_bundle_core.times_cont_mdiff_proj _ + +lemma smooth_proj : smooth I.tangent I (proj I M) := +basic_smooth_bundle_core.smooth_proj _ + +lemma times_cont_mdiff_on_proj {s : set (tangent_bundle I M)} : + times_cont_mdiff_on I.tangent I n (proj I M) s := +basic_smooth_bundle_core.times_cont_mdiff_on_proj _ + +lemma smooth_on_proj {s : set (tangent_bundle I M)} : + smooth_on I.tangent I (proj I M) s := +basic_smooth_bundle_core.smooth_on_proj _ + +lemma times_cont_mdiff_at_proj {p : tangent_bundle I M} : + times_cont_mdiff_at I.tangent I n + (proj I M) p := +basic_smooth_bundle_core.times_cont_mdiff_at_proj _ + +lemma smooth_at_proj {p : tangent_bundle I M} : + smooth_at I.tangent I (proj I M) p := +basic_smooth_bundle_core.smooth_at_proj _ + +lemma times_cont_mdiff_within_at_proj + {s : set (tangent_bundle I M)} {p : tangent_bundle I M} : + times_cont_mdiff_within_at I.tangent I n + (proj I M) s p := +basic_smooth_bundle_core.times_cont_mdiff_within_at_proj _ + +lemma smooth_within_at_proj + {s : set (tangent_bundle I M)} {p : tangent_bundle I M} : + smooth_within_at I.tangent I + (proj I M) s p := +basic_smooth_bundle_core.smooth_within_at_proj _ + +end tangent_bundle + +/-! ### Smoothness of standard maps associated to the product of manifolds -/ + +section prod_mk + +lemma times_cont_mdiff_within_at.prod_mk {f : M → M'} {g : M → N'} + (hf : times_cont_mdiff_within_at I I' n f s x) (hg : times_cont_mdiff_within_at I J' n g s x) : + times_cont_mdiff_within_at I (I'.prod J') n (λ x, (f x, g x)) s x := +begin + rw times_cont_mdiff_within_at_iff at *, + refine ⟨hf.1.prod hg.1, (hf.2.mono _).prod (hg.2.mono _)⟩; + mfld_set_tac, +end + +lemma times_cont_mdiff_at.prod_mk {f : M → M'} {g : M → N'} + (hf : times_cont_mdiff_at I I' n f x) (hg : times_cont_mdiff_at I J' n g x) : + times_cont_mdiff_at I (I'.prod J') n (λ x, (f x, g x)) x := +hf.prod_mk hg + +lemma times_cont_mdiff_on.prod_mk {f : M → M'} {g : M → N'} + (hf : times_cont_mdiff_on I I' n f s) (hg : times_cont_mdiff_on I J' n g s) : + times_cont_mdiff_on I (I'.prod J') n (λ x, (f x, g x)) s := +λ x hx, (hf x hx).prod_mk (hg x hx) + +lemma times_cont_mdiff.prod_mk {f : M → M'} {g : M → N'} + (hf : times_cont_mdiff I I' n f) (hg : times_cont_mdiff I J' n g) : + times_cont_mdiff I (I'.prod J') n (λ x, (f x, g x)) := +λ x, (hf x).prod_mk (hg x) + +lemma smooth_within_at.prod_mk {f : M → M'} {g : M → N'} + (hf : smooth_within_at I I' f s x) (hg : smooth_within_at I J' g s x) : + smooth_within_at I (I'.prod J') (λ x, (f x, g x)) s x := +hf.prod_mk hg + +lemma smooth_at.prod_mk {f : M → M'} {g : M → N'} + (hf : smooth_at I I' f x) (hg : smooth_at I J' g x) : + smooth_at I (I'.prod J') (λ x, (f x, g x)) x := +hf.prod_mk hg + +lemma smooth_on.prod_mk {f : M → M'} {g : M → N'} + (hf : smooth_on I I' f s) (hg : smooth_on I J' g s) : + smooth_on I (I'.prod J') (λ x, (f x, g x)) s := +hf.prod_mk hg + +lemma smooth.prod_mk {f : M → M'} {g : M → N'} + (hf : smooth I I' f) (hg : smooth I J' g) : + smooth I (I'.prod J') (λ x, (f x, g x)) := +hf.prod_mk hg + +end prod_mk + +section projections + +lemma times_cont_mdiff_within_at_fst {s : set (M × N)} {p : M × N} : + times_cont_mdiff_within_at (I.prod J) I n prod.fst s p := +begin + rw times_cont_mdiff_within_at_iff, + refine ⟨continuous_within_at_fst, _⟩, + refine times_cont_diff_within_at_fst.congr (λ y hy, _) _, + { simp only with mfld_simps at hy, + simp only [hy] with mfld_simps }, + { simp only with mfld_simps } +end + +lemma times_cont_mdiff_at_fst {p : M × N} : + times_cont_mdiff_at (I.prod J) I n prod.fst p := +times_cont_mdiff_within_at_fst + +lemma times_cont_mdiff_on_fst {s : set (M × N)} : + times_cont_mdiff_on (I.prod J) I n prod.fst s := +λ x hx, times_cont_mdiff_within_at_fst + +lemma times_cont_mdiff_fst : + times_cont_mdiff (I.prod J) I n (@prod.fst M N) := +λ x, times_cont_mdiff_at_fst + +lemma smooth_within_at_fst {s : set (M × N)} {p : M × N} : + smooth_within_at (I.prod J) I prod.fst s p := +times_cont_mdiff_within_at_fst + +lemma smooth_at_fst {p : M × N} : + smooth_at (I.prod J) I prod.fst p := +times_cont_mdiff_at_fst + +lemma smooth_on_fst {s : set (M × N)} : + smooth_on (I.prod J) I prod.fst s := +times_cont_mdiff_on_fst + +lemma smooth_fst : + smooth (I.prod J) I (@prod.fst M N) := +times_cont_mdiff_fst + +lemma times_cont_mdiff_within_at_snd {s : set (M × N)} {p : M × N} : + times_cont_mdiff_within_at (I.prod J) J n prod.snd s p := +begin + rw times_cont_mdiff_within_at_iff, + refine ⟨continuous_within_at_snd, _⟩, + refine times_cont_diff_within_at_snd.congr (λ y hy, _) _, + { simp only with mfld_simps at hy, + simp only [hy] with mfld_simps }, + { simp only with mfld_simps } +end + +lemma times_cont_mdiff_at_snd {p : M × N} : + times_cont_mdiff_at (I.prod J) J n prod.snd p := +times_cont_mdiff_within_at_snd + +lemma times_cont_mdiff_on_snd {s : set (M × N)} : + times_cont_mdiff_on (I.prod J) J n prod.snd s := +λ x hx, times_cont_mdiff_within_at_snd + +lemma times_cont_mdiff_snd : + times_cont_mdiff (I.prod J) J n (@prod.snd M N) := +λ x, times_cont_mdiff_at_snd + +lemma smooth_within_at_snd {s : set (M × N)} {p : M × N} : + smooth_within_at (I.prod J) J prod.snd s p := +times_cont_mdiff_within_at_snd + +lemma smooth_at_snd {p : M × N} : + smooth_at (I.prod J) J prod.snd p := +times_cont_mdiff_at_snd + +lemma smooth_on_snd {s : set (M × N)} : + smooth_on (I.prod J) J prod.snd s := +times_cont_mdiff_on_snd + +lemma smooth_snd : + smooth (I.prod J) J (@prod.snd M N) := +times_cont_mdiff_snd + +include Is I's J's + +lemma smooth_iff_proj_smooth {f : M → M' × N'} : + (smooth I (I'.prod J') f) ↔ (smooth I I' (prod.fst ∘ f)) ∧ (smooth I J' (prod.snd ∘ f)) := +begin + split, + { intro h, exact ⟨smooth_fst.comp h, smooth_snd.comp h⟩ }, + { rintro ⟨h_fst, h_snd⟩, simpa only [prod.mk.eta] using h_fst.prod_mk h_snd, } +end + +end projections + +section prod_map + +variables {g : N → N'} {r : set N} {y : N} +include Is I's Js J's + +/-- 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_mdiff_within_at.prod_map' {p : M × N} + (hf : times_cont_mdiff_within_at I I' n f s p.1) (hg : times_cont_mdiff_within_at J J' n g r p.2) : + times_cont_mdiff_within_at (I.prod J) (I'.prod J') n (prod.map f g) (s.prod r) p := +(hf.comp p times_cont_mdiff_within_at_fst (prod_subset_preimage_fst _ _)).prod_mk $ +hg.comp p times_cont_mdiff_within_at_snd (prod_subset_preimage_snd _ _) + +lemma times_cont_mdiff_within_at.prod_map + (hf : times_cont_mdiff_within_at I I' n f s x) (hg : times_cont_mdiff_within_at J J' n g r y) : + times_cont_mdiff_within_at (I.prod J) (I'.prod J') n (prod.map f g) (s.prod r) (x, y) := +times_cont_mdiff_within_at.prod_map' hf hg + +lemma times_cont_mdiff_at.prod_map + (hf : times_cont_mdiff_at I I' n f x) (hg : times_cont_mdiff_at J J' n g y) : + times_cont_mdiff_at (I.prod J) (I'.prod J') n (prod.map f g) (x, y) := +begin + rw ← times_cont_mdiff_within_at_univ at *, + convert hf.prod_map hg, + exact univ_prod_univ.symm +end + +lemma times_cont_mdiff_at.prod_map' {p : M × N} + (hf : times_cont_mdiff_at I I' n f p.1) (hg : times_cont_mdiff_at J J' n g p.2) : + times_cont_mdiff_at (I.prod J) (I'.prod J') n (prod.map f g) p := +begin + rcases p, + exact hf.prod_map hg +end + +lemma times_cont_mdiff_on.prod_map + (hf : times_cont_mdiff_on I I' n f s) (hg : times_cont_mdiff_on J J' n g r) : + times_cont_mdiff_on (I.prod J) (I'.prod J') n (prod.map f g) (s.prod r) := +(hf.comp times_cont_mdiff_on_fst (prod_subset_preimage_fst _ _)).prod_mk $ +hg.comp (times_cont_mdiff_on_snd) (prod_subset_preimage_snd _ _) + +lemma times_cont_mdiff.prod_map + (hf : times_cont_mdiff I I' n f) (hg : times_cont_mdiff J J' n g) : + times_cont_mdiff (I.prod J) (I'.prod J') n (prod.map f g) := +begin + assume p, + exact (hf p.1).prod_map' (hg p.2) +end + +lemma smooth_within_at.prod_map + (hf : smooth_within_at I I' f s x) (hg : smooth_within_at J J' g r y) : + smooth_within_at (I.prod J) (I'.prod J') (prod.map f g) (s.prod r) (x, y) := +hf.prod_map hg + +lemma smooth_at.prod_map + (hf : smooth_at I I' f x) (hg : smooth_at J J' g y) : + smooth_at (I.prod J) (I'.prod J') (prod.map f g) (x, y) := +hf.prod_map hg + +lemma smooth_on.prod_map + (hf : smooth_on I I' f s) (hg : smooth_on J J' g r) : + smooth_on (I.prod J) (I'.prod J') (prod.map f g) (s.prod r) := +hf.prod_map hg + +lemma smooth.prod_map + (hf : smooth I I' f) (hg : smooth J J' g) : + smooth (I.prod J) (I'.prod J') (prod.map f g) := +hf.prod_map hg + +end prod_map diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean index 928edd4f7444d..01071e3f0d36f 100644 --- a/src/topology/continuous_on.lean +++ b/src/topology/continuous_on.lean @@ -173,6 +173,12 @@ lemma nhds_within_prod_eq {α : Type*} [topological_space α] {β : Type*} [topo nhds_within (a, b) (s.prod t) = (nhds_within a s).prod (nhds_within b t) := by { unfold nhds_within, rw [nhds_prod_eq, ←filter.prod_inf_prod, filter.prod_principal_principal] } +lemma nhds_within_prod {α : Type*} [topological_space α] {β : Type*} [topological_space β] + {s u : set α} {t v : set β} {a : α} {b : β} + (hu : u ∈ nhds_within a s) (hv : v ∈ nhds_within b t) : + (u.prod v) ∈ nhds_within (a, b) (s.prod t) := +by { rw nhds_within_prod_eq, exact prod_mem_prod hu hv, } + theorem tendsto_if_nhds_within {f g : α → β} {p : α → Prop} [decidable_pred p] {a : α} {s : set α} {l : filter β} (h₀ : tendsto f (nhds_within a (s ∩ p)) l) @@ -639,3 +645,17 @@ end lemma embedding.continuous_on_iff {f : α → β} {g : β → γ} (hg : embedding g) {s : set α} : continuous_on f s ↔ continuous_on (g ∘ f) s := inducing.continuous_on_iff hg.1 + +lemma continuous_on_fst {s : set (α × β)} : continuous_on prod.fst s := +continuous_fst.continuous_on + +lemma continuous_within_at_fst {s : set (α × β)} {p : α × β} : + continuous_within_at prod.fst s p := +continuous_fst.continuous_within_at + +lemma continuous_on_snd {s : set (α × β)} : continuous_on prod.snd s := +continuous_snd.continuous_on + +lemma continuous_within_at_snd {s : set (α × β)} {p : α × β} : + continuous_within_at prod.snd s p := +continuous_snd.continuous_within_at