feat(geometry/manifold/vector_bundle/smooth_section): define smooth s…

…ections (#19064)

* Define the module of smooth sections of a smooth vector bundle over a smooth manifold.
* Co-authored-by: Heather Macbeth [25316162+hrmacbeth@users.noreply.github.com](mailto:25316162+hrmacbeth@users.noreply.github.com)



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

src/geometry/manifold/algebra/lie_group.lean

@@ -74,7 +74,7 @@ variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
 {M : Type*} [topological_space M] [charted_space H' M]
 {E'' : Type*} [normed_add_comm_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']
+{M' : Type*} [topological_space M'] [charted_space H'' M'] {n : ℕ∞}
 
 section
 
@@ -96,24 +96,90 @@ lemma topological_group_of_lie_group : topological_group G :=
 end
 
 @[to_additive]
-lemma smooth.inv {f : M → G}
-  (hf : smooth I' I f) : smooth I' I (λx, (f x)⁻¹) :=
-(smooth_inv I).comp hf
+lemma cont_mdiff_within_at.inv {f : M → G} {s : set M} {x₀ : M}
+  (hf : cont_mdiff_within_at I' I n f s x₀) : cont_mdiff_within_at I' I n (λx, (f x)⁻¹) s x₀ :=
+((smooth_inv I).of_le le_top).cont_mdiff_at.cont_mdiff_within_at.comp x₀ hf $ set.maps_to_univ _ _
+
+@[to_additive]
+lemma cont_mdiff_at.inv {f : M → G} {x₀ : M}
+  (hf : cont_mdiff_at I' I n f x₀) : cont_mdiff_at I' I n (λx, (f x)⁻¹) x₀ :=
+((smooth_inv I).of_le le_top).cont_mdiff_at.comp x₀ hf
+
+@[to_additive]
+lemma cont_mdiff_on.inv {f : M → G} {s : set M}
+  (hf : cont_mdiff_on I' I n f s) : cont_mdiff_on I' I n (λx, (f x)⁻¹) s :=
+λ x hx, (hf x hx).inv
+
+@[to_additive]
+lemma cont_mdiff.inv {f : M → G}
+  (hf : cont_mdiff I' I n f) : cont_mdiff I' I n (λx, (f x)⁻¹) :=
+λ x, (hf x).inv
+
+@[to_additive]
+lemma smooth_within_at.inv {f : M → G} {s : set M} {x₀ : M}
+  (hf : smooth_within_at I' I f s x₀) : smooth_within_at I' I (λx, (f x)⁻¹) s x₀ :=
+hf.inv
+
+@[to_additive]
+lemma smooth_at.inv {f : M → G} {x₀ : M}
+  (hf : smooth_at I' I f x₀) : smooth_at I' I (λx, (f x)⁻¹) x₀ :=
+hf.inv
 
 @[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 I).comp_smooth_on hf
+hf.inv
 
 @[to_additive]
-lemma smooth.div {f g : M → G}
-  (hf : smooth I' I f) (hg : smooth I' I g) : smooth I' I (f / g) :=
-by { rw div_eq_mul_inv, exact ((smooth_mul I).comp (hf.prod_mk hg.inv) : _), }
+lemma smooth.inv {f : M → G}
+  (hf : smooth I' I f) : smooth I' I (λx, (f x)⁻¹) :=
+hf.inv
+
+@[to_additive]
+lemma cont_mdiff_within_at.div {f g : M → G} {s : set M} {x₀ : M}
+  (hf : cont_mdiff_within_at I' I n f s x₀) (hg : cont_mdiff_within_at I' I n g s x₀) :
+  cont_mdiff_within_at I' I n (λ x, f x / g x) s x₀ :=
+by { simp_rw div_eq_mul_inv, exact hf.mul hg.inv }
+
+@[to_additive]
+lemma cont_mdiff_at.div {f g : M → G} {x₀ : M}
+  (hf : cont_mdiff_at I' I n f x₀) (hg : cont_mdiff_at I' I n g x₀) :
+  cont_mdiff_at I' I n (λ x, f x / g x) x₀ :=
+by { simp_rw div_eq_mul_inv, exact hf.mul hg.inv }
+
+@[to_additive]
+lemma cont_mdiff_on.div {f g : M → G} {s : set M}
+  (hf : cont_mdiff_on I' I n f s) (hg : cont_mdiff_on I' I n g s) :
+  cont_mdiff_on I' I n (λ x, f x / g x) s :=
+by { simp_rw div_eq_mul_inv, exact hf.mul hg.inv }
+
+@[to_additive]
+lemma cont_mdiff.div {f g : M → G}
+  (hf : cont_mdiff I' I n f) (hg : cont_mdiff I' I n g) :
+  cont_mdiff I' I n (λ x, f x / g x) :=
+by { simp_rw div_eq_mul_inv, exact hf.mul hg.inv }
+
+@[to_additive]
+lemma smooth_within_at.div {f g : M → G} {s : set M} {x₀ : M}
+  (hf : smooth_within_at I' I f s x₀) (hg : smooth_within_at I' I g s x₀) :
+  smooth_within_at I' I (λ x, f x / g x) s x₀ :=
+hf.div hg
+
+@[to_additive]
+lemma smooth_at.div {f g : M → G} {x₀ : M}
+  (hf : smooth_at I' I f x₀) (hg : smooth_at I' I g x₀) :
+  smooth_at I' I (λ x, f x / g x) x₀ :=
+hf.div hg
 
 @[to_additive]
 lemma smooth_on.div {f 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 :=
-by { rw div_eq_mul_inv, exact ((smooth_mul I).comp_smooth_on (hf.prod_mk hg.inv) : _), }
+hf.div hg
+
+@[to_additive]
+lemma smooth.div {f g : M → G}
+  (hf : smooth I' I f) (hg : smooth I' I g) : smooth I' I (f / g) :=
+hf.div hg
 
 end lie_group
 

src/geometry/manifold/vector_bundle/basic.lean

@@ -174,6 +174,12 @@ lemma cont_mdiff_at_total_space (f : M → total_space E) (x₀ : M) :
   cont_mdiff_at IM 𝓘(𝕜, F) n (λ x, (trivialization_at F E (f x₀).proj (f x)).2) x₀ :=
 by { simp_rw [← cont_mdiff_within_at_univ], exact cont_mdiff_within_at_total_space f }
 
+/-- Characterization of C^n sections of a smooth vector bundle. -/
+lemma cont_mdiff_at_section (s : Π x, E x) (x₀ : B) :
+  cont_mdiff_at IB (IB.prod (𝓘(𝕜, F))) n (λ x, total_space_mk x (s x)) x₀ ↔
+  cont_mdiff_at IB 𝓘(𝕜, F) n (λ x, (trivialization_at F E x₀ (total_space_mk x (s x))).2) x₀ :=
+by { simp_rw [cont_mdiff_at_total_space, and_iff_right_iff_imp], intro x, exact cont_mdiff_at_id }
+
 variables (E)
 lemma cont_mdiff_proj : cont_mdiff (IB.prod 𝓘(𝕜, F)) IB n (π E) :=
 begin

src/geometry/manifold/vector_bundle/smooth_section.lean

@@ -0,0 +1,210 @@
+/-
+Copyright © 2023 Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Heather Macbeth, Floris van Doorn
+-/
+
+import geometry.manifold.cont_mdiff_mfderiv
+import topology.continuous_function.basic
+import geometry.manifold.algebra.lie_group
+
+/-!
+# Smooth sections
+
+In this file we define the type `cont_mdiff_section` of `n` times continuously differentiable
+sections of a smooth vector bundle over a manifold `M` and prove that it's a module.
+-/
+open bundle filter function
+open_locale manifold
+
+variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
+{E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
+{E' : Type*} [normed_add_comm_group E'] [normed_space 𝕜 E']
+{H : Type*} [topological_space H]
+{H' : Type*} [topological_space H']
+(I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H')
+{M : Type*} [topological_space M] [charted_space H M]
+{M' : Type*} [topological_space M'] [charted_space H' M']
+{E'' : Type*} [normed_add_comm_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]
+
+
+variables (F : Type*) [normed_add_comm_group F] [normed_space 𝕜 F] -- `F` model fiber
+  (n : ℕ∞)
+  (V : M → Type*) [topological_space (total_space V)] -- `V` vector bundle
+  [Π x, add_comm_group (V x)] [Π x, module 𝕜 (V x)]
+variables [Π x : M, topological_space (V x)]
+  [fiber_bundle F V]
+  [vector_bundle 𝕜 F V]
+  [smooth_vector_bundle F V I]
+
+/-- Bundled `n` times continuously differentiable sections of a vector bundle. -/
+@[protect_proj]
+structure cont_mdiff_section :=
+(to_fun            : Π x, V x)
+(cont_mdiff_to_fun : cont_mdiff I (I.prod 𝓘(𝕜, F)) n (λ x, total_space_mk x (to_fun x)))
+
+/-- Bundled smooth sections of a vector bundle. -/
+@[reducible] def smooth_section := cont_mdiff_section I F ⊤ V
+
+localized "notation (name := cont_mdiff_section) `Cₛ^` n `⟮` I `; ` F `, ` V `⟯` :=
+  cont_mdiff_section I F n V" in manifold
+
+namespace cont_mdiff_section
+
+variables {I} {I'} {n} {F} {V}
+
+instance : has_coe_to_fun Cₛ^n⟮I; F, V⟯ (λ s, Π x, V x) := ⟨cont_mdiff_section.to_fun⟩
+
+variables {s t : Cₛ^n⟮I; F, V⟯}
+
+@[simp] lemma coe_fn_mk (s : Π x, V x)
+  (hs : cont_mdiff I (I.prod 𝓘(𝕜, F)) n (λ x, total_space_mk x (s x))) :
+  (mk s hs : Π x, V x) = s :=
+rfl
+
+protected lemma cont_mdiff (s : Cₛ^n⟮I; F, V⟯) :
+  cont_mdiff I (I.prod 𝓘(𝕜, F)) n (λ x, total_space_mk x (s x : V x)) := s.cont_mdiff_to_fun
+
+protected lemma smooth (s : Cₛ^∞⟮I; F, V⟯) :
+  smooth I (I.prod 𝓘(𝕜, F)) (λ x, total_space_mk x (s x : V x)) := s.cont_mdiff_to_fun
+
+protected lemma mdifferentiable' (s : Cₛ^n⟮I; F, V⟯) (hn : 1 ≤ n) :
+  mdifferentiable I (I.prod 𝓘(𝕜, F)) (λ x, total_space_mk x (s x : V x)) :=
+s.cont_mdiff.mdifferentiable hn
+
+protected lemma mdifferentiable (s : Cₛ^∞⟮I; F, V⟯) :
+  mdifferentiable I (I.prod 𝓘(𝕜, F)) (λ x, total_space_mk x (s x : V x)) :=
+s.cont_mdiff.mdifferentiable le_top
+
+protected lemma mdifferentiable_at (s : Cₛ^∞⟮I; F, V⟯) {x} :
+  mdifferentiable_at I (I.prod 𝓘(𝕜, F)) (λ x, total_space_mk x (s x : V x)) x :=
+s.mdifferentiable x
+
+lemma coe_inj ⦃s t : Cₛ^n⟮I; F, V⟯⦄ (h : (s : Π x, V x) = t) : s = t :=
+by cases s; cases t; cases h; refl
+
+lemma coe_injective : injective (coe_fn : Cₛ^n⟮I; F, V⟯ → Π x, V x) :=
+coe_inj
+
+@[ext] theorem ext (h : ∀ x, s x = t x) : s = t :=
+by cases s; cases t; congr'; exact funext h
+
+instance has_add : has_add Cₛ^n⟮I; F, V⟯ :=
+begin
+  refine ⟨λ s t, ⟨s + t, _⟩⟩,
+  intro x₀,
+  have hs := s.cont_mdiff x₀,
+  have ht := t.cont_mdiff x₀,
+  rw [cont_mdiff_at_section] at hs ht ⊢,
+  set e := trivialization_at F V x₀,
+  refine (hs.add ht).congr_of_eventually_eq _,
+  refine eventually_of_mem (e.open_base_set.mem_nhds $ mem_base_set_trivialization_at F V x₀) _,
+  intros x hx,
+  apply (e.linear 𝕜 hx).1,
+end
+
+@[simp]
+lemma coe_add (s t : Cₛ^n⟮I; F, V⟯) : ⇑(s + t) = s + t := rfl
+
+instance has_sub : has_sub Cₛ^n⟮I; F, V⟯ :=
+begin
+  refine ⟨λ s t, ⟨s - t, _⟩⟩,
+  intro x₀,
+  have hs := s.cont_mdiff x₀,
+  have ht := t.cont_mdiff x₀,
+  rw [cont_mdiff_at_section] at hs ht ⊢,
+  set e := trivialization_at F V x₀,
+  refine (hs.sub ht).congr_of_eventually_eq _,
+  refine eventually_of_mem (e.open_base_set.mem_nhds $ mem_base_set_trivialization_at F V x₀) _,
+  intros x hx,
+  apply (e.linear 𝕜 hx).map_sub,
+end
+
+@[simp]
+lemma coe_sub (s t : Cₛ^n⟮I; F, V⟯) : ⇑(s - t) = s - t := rfl
+
+instance has_zero : has_zero Cₛ^n⟮I; F, V⟯ :=
+⟨⟨λ x, 0, (smooth_zero_section 𝕜 V).of_le le_top⟩⟩
+
+instance inhabited : inhabited Cₛ^n⟮I; F, V⟯ := ⟨0⟩
+
+@[simp]
+lemma coe_zero : ⇑(0 : Cₛ^n⟮I; F, V⟯) = 0 := rfl
+
+instance has_smul : has_smul 𝕜 Cₛ^n⟮I; F, V⟯ :=
+begin
+  refine ⟨λ c s, ⟨c • s, _⟩⟩,
+  intro x₀,
+  have hs := s.cont_mdiff x₀,
+  rw [cont_mdiff_at_section] at hs ⊢,
+  set e := trivialization_at F V x₀,
+  refine (cont_mdiff_at_const.smul hs).congr_of_eventually_eq _,
+  { exact c },
+  refine eventually_of_mem (e.open_base_set.mem_nhds $ mem_base_set_trivialization_at F V x₀) _,
+  intros x hx,
+  apply (e.linear 𝕜 hx).2,
+end
+
+@[simp]
+lemma coe_smul (r : 𝕜) (s : Cₛ^n⟮I; F, V⟯) : ⇑(r • s : Cₛ^n⟮I; F, V⟯) = r • s := rfl
+
+instance has_neg : has_neg Cₛ^n⟮I; F, V⟯ :=
+begin
+  refine ⟨λ s, ⟨- s, _⟩⟩,
+  intro x₀,
+  have hs := s.cont_mdiff x₀,
+  rw [cont_mdiff_at_section] at hs ⊢,
+  set e := trivialization_at F V x₀,
+  refine hs.neg.congr_of_eventually_eq _,
+  refine eventually_of_mem (e.open_base_set.mem_nhds $ mem_base_set_trivialization_at F V x₀) _,
+  intros x hx,
+  apply (e.linear 𝕜 hx).map_neg
+end
+
+@[simp]
+lemma coe_neg (s : Cₛ^n⟮I; F, V⟯) : ⇑(- s : Cₛ^n⟮I; F, V⟯) = - s := rfl
+
+instance has_nsmul : has_smul ℕ Cₛ^n⟮I; F, V⟯ :=
+⟨nsmul_rec⟩
+
+@[simp]
+lemma coe_nsmul (s : Cₛ^n⟮I; F, V⟯) (k : ℕ) : ⇑(k • s : Cₛ^n⟮I; F, V⟯) = k • s :=
+begin
+  induction k with k ih,
+  { simp_rw [zero_smul], refl },
+  simp_rw [succ_nsmul, ← ih], refl,
+end
+
+instance has_zsmul : has_smul ℤ Cₛ^n⟮I; F, V⟯ :=
+⟨zsmul_rec⟩
+
+@[simp]
+lemma coe_zsmul (s : Cₛ^n⟮I; F, V⟯) (z : ℤ) : ⇑(z • s : Cₛ^n⟮I; F, V⟯) = z • s :=
+begin
+  cases z with n n,
+  refine (coe_nsmul s n).trans _,
+  simp only [int.of_nat_eq_coe, coe_nat_zsmul],
+  refine (congr_arg has_neg.neg (coe_nsmul s (n+1))).trans _,
+  simp only [zsmul_neg_succ_of_nat, neg_inj]
+end
+
+instance add_comm_group : add_comm_group Cₛ^n⟮I; F, V⟯ :=
+coe_injective.add_comm_group _ coe_zero coe_add coe_neg coe_sub coe_nsmul coe_zsmul
+
+variables (I F V n)
+/-- The additive morphism from smooth sections to dependent maps. -/
+def coe_add_hom : Cₛ^n⟮I; F, V⟯ →+ Π x, V x :=
+{ to_fun := coe_fn,
+  map_zero' := coe_zero,
+  map_add' := coe_add }
+
+variables {I F V n}
+
+instance module : module 𝕜 Cₛ^n⟮I; F, V⟯ :=
+coe_injective.module 𝕜 (coe_add_hom I F n V) coe_smul
+
+end cont_mdiff_section