feat(topology/vector_bundle/hom): define the vector bundle of continu…

…ous linear maps (#14541)

* The changes in `topology/fiber_bundle` are not necessary for this PR, but perhaps nice additions
* Co-authored by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
* Co-authored by: Patrick Massot <patrick.massot@u-psud.fr>


Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/topology/fiber_bundle.lean

@@ -217,6 +217,9 @@ lemma apply_symm_apply' {b : B} {x : F} (hx : b ∈ e.base_set) :
   e (e.to_local_equiv.symm (b, x)) = (b, x) :=
 e.apply_symm_apply (e.mem_target.2 hx)
 
+lemma symm_apply_apply {x : Z} (hx : x ∈ e.source) : e.to_local_equiv.symm (e x) = x :=
+e.to_local_equiv.left_inv hx
+
 @[simp, mfld_simps] lemma symm_apply_mk_proj {x : Z} (ex : x ∈ e.source) :
   e.to_local_equiv.symm (proj x, (e x).2) = x :=
 by rw [← e.coe_fst ex, prod.mk.eta, ← e.coe_coe, e.to_local_equiv.left_inv ex]
@@ -240,6 +243,16 @@ begin
   rw [e.proj_symm_apply' h]
 end
 
+lemma target_inter_preimage_symm_source_eq (e f : pretrivialization F proj) :
+  f.target ∩ (f.to_local_equiv.symm) ⁻¹' e.source
+  = (e.base_set ∩ f.base_set) ×ˢ (univ : set F) :=
+by rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]
+
+lemma trans_source (e f : pretrivialization F proj) :
+  (f.to_local_equiv.symm.trans e.to_local_equiv).source
+  = (e.base_set ∩ f.base_set) ×ˢ (univ : set F) :=
+by rw [local_equiv.trans_source, local_equiv.symm_source, e.target_inter_preimage_symm_source_eq]
+
 lemma symm_trans_symm (e e' : pretrivialization F proj) :
   (e.to_local_equiv.symm.trans e'.to_local_equiv).symm =
   e'.to_local_equiv.symm.trans e.to_local_equiv :=
@@ -366,6 +379,33 @@ def comp_homeomorph {Z' : Type*} [topological_space Z'] (h : Z' ≃ₜ Z) :
     have hp : h p ∈ e.source, by simpa using hp,
     by simp [hp] }
 
+/-- Read off the continuity of a function `f : Z → X` at `z : Z` by transferring via a
+trivialization of `Z` containing `z`. -/
+lemma continuous_at_of_comp_right {X : Type*} [topological_space X] {f : Z → X} {z : Z}
+  (e : trivialization F proj) (he : proj z ∈ e.base_set)
+  (hf : continuous_at (f ∘ e.to_local_equiv.symm) (e z)) :
+  continuous_at f z :=
+begin
+  have hez : z ∈ e.to_local_equiv.symm.target,
+  { rw [local_equiv.symm_target, e.mem_source],
+    exact he },
+  rwa [e.to_local_homeomorph.symm.continuous_at_iff_continuous_at_comp_right hez,
+   local_homeomorph.symm_symm]
+end
+
+/-- Read off the continuity of a function `f : X → Z` at `x : X` by transferring via a
+trivialization of `Z` containing `f x`. -/
+lemma continuous_at_of_comp_left {X : Type*} [topological_space X] {f : X → Z} {x : X}
+  (e : trivialization F proj) (hf_proj : continuous_at (proj ∘ f) x) (he : proj (f x) ∈ e.base_set)
+  (hf : continuous_at (e ∘ f) x) :
+  continuous_at f x :=
+begin
+  rw e.to_local_homeomorph.continuous_at_iff_continuous_at_comp_left,
+  { exact hf },
+  rw [e.source_eq, ← preimage_comp],
+  exact hf_proj.preimage_mem_nhds (e.open_base_set.mem_nhds he),
+end
+
 end topological_fiber_bundle.trivialization
 
 /-- A topological fiber bundle with fiber `F` over a base `B` is a space projecting on `B`
@@ -1201,4 +1241,28 @@ lemma is_topological_fiber_bundle :
 lemma continuous_proj : @continuous _ _ a.total_space_topology _ proj :=
 by { letI := a.total_space_topology, exact a.is_topological_fiber_bundle.continuous_proj, }
 
+/-- For a fiber bundle `Z` over `B` constructed using the `topological_fiber_prebundle` mechanism,
+continuity of a function `Z → X` on an open set `s` can be checked by precomposing at each point
+with the pretrivialization used for the construction at that point. -/
+lemma continuous_on_of_comp_right {X : Type*} [topological_space X] {f : Z → X} {s : set B}
+  (hs : is_open s)
+  (hf : ∀ b ∈ s, continuous_on (f ∘ (a.pretrivialization_at b).to_local_equiv.symm)
+    ((s ∩ (a.pretrivialization_at b).base_set) ×ˢ (set.univ : set F))) :
+  @continuous_on _ _ a.total_space_topology _ f (proj ⁻¹' s) :=
+begin
+  letI := a.total_space_topology,
+  intros z hz,
+  let e : trivialization F proj :=
+  a.trivialization_of_mem_pretrivialization_atlas (a.pretrivialization_mem_atlas (proj z)),
+  refine (e.continuous_at_of_comp_right _
+    ((hf (proj z) hz).continuous_at (is_open.mem_nhds _ _))).continuous_within_at,
+  { exact a.mem_base_pretrivialization_at (proj z) },
+  { exact ((hs.inter (a.pretrivialization_at (proj z)).open_base_set).prod is_open_univ) },
+  refine ⟨_, mem_univ _⟩,
+  rw e.coe_fst,
+  { exact ⟨hz, a.mem_base_pretrivialization_at (proj z)⟩ },
+  { rw e.mem_source,
+    exact a.mem_base_pretrivialization_at (proj z) },
+end
+
 end topological_fiber_prebundle

src/topology/vector_bundle/basic.lean

@@ -518,7 +518,8 @@ namespace trivialization
 @[simps apply {fully_applied := ff}]
 def continuous_linear_map_at (e : trivialization R F E) (b : B) :
   E b →L[R] F :=
-{ cont := begin
+{ to_fun := e.linear_map_at b, -- given explicitly to help `simps`
+  cont := begin
     dsimp,
     rw [e.coe_linear_map_at b],
     refine continuous_if_const _ (λ hb, _) (λ _, continuous_zero),
@@ -530,7 +531,8 @@ def continuous_linear_map_at (e : trivialization R F E) (b : B) :
 /-- Backwards map of `continuous_linear_equiv_at`, defined everywhere. -/
 @[simps apply {fully_applied := ff}]
 def symmL (e : trivialization R F E) (b : B) : F →L[R] E b :=
-{ cont := begin
+{ to_fun := e.symm b, -- given explicitly to help `simps`
+  cont := begin
     by_cases hb : b ∈ e.base_set,
     { rw (topological_vector_bundle.total_space_mk_inducing R F E b).continuous_iff,
       exact e.continuous_on_symm.comp_continuous (continuous_const.prod_mk continuous_id)
@@ -554,8 +556,8 @@ is in fact a continuous linear equiv between the fibers and the model fiber. -/
 @[simps apply symm_apply {fully_applied := ff}]
 def continuous_linear_equiv_at (e : trivialization R F E) (b : B)
   (hb : b ∈ e.base_set) : E b ≃L[R] F :=
-{ to_fun := λ y, (e (total_space_mk b y)).2,
-  inv_fun := e.symm b,
+{ to_fun := λ y, (e (total_space_mk b y)).2, -- given explicitly to help `simps`
+  inv_fun := e.symm b, -- given explicitly to help `simps`
   continuous_to_fun := continuous_snd.comp (e.to_local_homeomorph.continuous_on.comp_continuous
     (total_space_mk_inducing R F E b).continuous (λ x, e.mem_source.mpr hb)),
   continuous_inv_fun := (e.symmL b).continuous,