feat(topology/vector_bundle): define some useful linear maps globally (…

…#14484)

* Define `pretrivialization.symmₗ`, `pretrivialization.linear_map_at`, `trivialization.symmL`, `trivialization.continuous_linear_map_at`
* These are globally-defined (continuous) linear maps. They are linear equivalences on `e.base_set`, but it is useful to define these globally. They are defined as `0` outside `e.base_set`
* These are convenient to define the vector bundle of continuous linear maps.



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

src/topology/continuous_on.lean

@@ -1026,10 +1026,15 @@ lemma continuous.if {p : α → Prop} {f g : α → β} [∀ a, decidable (p a)]
   continuous (λ a, if p a then f a else g a) :=
 continuous_if hp hf.continuous_on hg.continuous_on
 
+lemma continuous_if_const (p : Prop) {f g : α → β} [decidable p]
+  (hf : p → continuous f) (hg : ¬ p → continuous g) :
+  continuous (λ a, if p then f a else g a) :=
+by { split_ifs, exact hf h, exact hg h }
+
 lemma continuous.if_const (p : Prop) {f g : α → β} [decidable p]
   (hf : continuous f) (hg : continuous g) :
   continuous (λ a, if p then f a else g a) :=
-continuous_if (if h : p then by simp [h] else by simp [h]) hf.continuous_on hg.continuous_on
+continuous_if_const p (λ _, hf) (λ _, hg)
 
 lemma continuous_piecewise {s : set α} {f g : α → β} [∀ a, decidable (a ∈ s)]
   (hs : ∀ a ∈ frontier s, f a = g a) (hf : continuous_on f (closure s))

src/topology/vector_bundle.lean

@@ -157,6 +157,10 @@ lemma symm_apply_of_not_mem (e : pretrivialization R F E) {b : B} (hb : b ∉ e.
   e.symm b y = 0 :=
 dif_neg hb
 
+lemma coe_symm_of_not_mem (e : pretrivialization R F E) {b : B} (hb : b ∉ e.base_set) :
+  (e.symm b : F → E b) = 0 :=
+funext $ λ y, dif_neg hb
+
 lemma mk_symm (e : pretrivialization R F E) {b : B} (hb : b ∈ e.base_set) (y : F) :
   total_space_mk b (e.symm b y) = e.to_local_equiv.symm (b, y) :=
 by rw [e.symm_apply hb, total_space.mk_cast, total_space.eta]
@@ -174,6 +178,16 @@ lemma apply_mk_symm (e : pretrivialization R F E) {b : B} (hb : b ∈ e.base_set
   e (total_space_mk b (e.symm b y)) = (b, y) :=
 by rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)]
 
+/-- A fiberwise linear inverse to `e`. -/
+@[simps] protected def symmₗ (e : pretrivialization R F E) (b : B) : F →ₗ[R] E b :=
+begin
+  refine is_linear_map.mk' (e.symm b) _,
+  by_cases hb : b ∈ e.base_set,
+  { exact (((e.linear hb).mk' _).inverse (e.symm b) (e.symm_apply_apply_mk hb)
+      (λ v, congr_arg prod.snd $ e.apply_mk_symm hb v)).is_linear },
+  { rw [e.coe_symm_of_not_mem hb], exact (0 : F →ₗ[R] E b).is_linear }
+end
+
 /-- A pretrivialization for a topological vector bundle defines linear equivalences between the
 fibers and the model space. -/
 @[simps {fully_applied := ff}] def linear_equiv_at (e : pretrivialization R F E) (b : B)
@@ -186,6 +200,43 @@ fibers and the model space. -/
   map_add' := λ v w, (e.linear hb).map_add v w,
   map_smul' := λ c v, (e.linear hb).map_smul c v }
 
+/-- A fiberwise linear map equal to `e` on `e.base_set`. -/
+protected def linear_map_at (e : pretrivialization R F E) (b : B) : E b →ₗ[R] F :=
+if hb : b ∈ e.base_set then e.linear_equiv_at b hb else 0
+
+lemma coe_linear_map_at (e : pretrivialization R F E) (b : B) :
+  ⇑(e.linear_map_at b) = λ y, if b ∈ e.base_set then (e (total_space_mk b y)).2 else 0 :=
+by { rw [pretrivialization.linear_map_at], split_ifs; refl }
+
+lemma coe_linear_map_at_of_mem (e : pretrivialization R F E) {b : B} (hb : b ∈ e.base_set) :
+  ⇑(e.linear_map_at b) = λ y, (e (total_space_mk b y)).2 :=
+by simp_rw [coe_linear_map_at, if_pos hb]
+
+lemma linear_map_at_apply (e : pretrivialization R F E) {b : B} (y : E b) :
+  e.linear_map_at b y = if b ∈ e.base_set then (e (total_space_mk b y)).2 else 0 :=
+by rw [coe_linear_map_at]
+
+lemma linear_map_at_def_of_mem (e : pretrivialization R F E) {b : B} (hb : b ∈ e.base_set) :
+  e.linear_map_at b = e.linear_equiv_at b hb :=
+dif_pos hb
+
+lemma linear_map_at_def_of_not_mem (e : pretrivialization R F E) {b : B} (hb : b ∉ e.base_set) :
+  e.linear_map_at b = 0 :=
+dif_neg hb
+
+lemma linear_map_at_eq_zero (e : pretrivialization R F E) {b : B} (hb : b ∉ e.base_set) :
+  e.linear_map_at b = 0 :=
+dif_neg hb
+
+lemma symmₗ_linear_map_at (e : pretrivialization R F E) {b : B} (hb : b ∈ e.base_set) (y : E b) :
+  e.symmₗ b (e.linear_map_at b y) = y :=
+by { rw [e.linear_map_at_def_of_mem hb], exact (e.linear_equiv_at b hb).left_inv y }
+
+lemma linear_map_at_symmₗ (e : pretrivialization R F E) {b : B} (hb : b ∈ e.base_set) (y : F) :
+  e.linear_map_at b (e.symmₗ b y) = y :=
+by { rw [e.linear_map_at_def_of_mem hb], exact (e.linear_equiv_at b hb).right_inv y }
+
+
 end topological_vector_bundle.pretrivialization
 
 variable [topological_space (total_space E)]
@@ -325,6 +376,53 @@ def linear_equiv_at (e : trivialization R F E) (b : B) (hb : b ∈ e.base_set) :
   E b ≃ₗ[R] F :=
 e.to_pretrivialization.linear_equiv_at b hb
 
+@[simp]
+lemma linear_equiv_at_apply (e : trivialization R F E) (b : B) (hb : b ∈ e.base_set) (v : E b) :
+  e.linear_equiv_at b hb v = (e (total_space_mk b v)).2 := rfl
+
+@[simp]
+lemma linear_equiv_at_symm_apply (e : trivialization R F E) (b : B) (hb : b ∈ e.base_set) (v : F) :
+  (e.linear_equiv_at b hb).symm v = e.symm b v := rfl
+
+/-- A fiberwise linear inverse to `e`. -/
+protected def symmₗ (e : trivialization R F E) (b : B) : F →ₗ[R] E b :=
+e.to_pretrivialization.symmₗ b
+
+lemma coe_symmₗ (e : trivialization R F E) (b : B) : ⇑(e.symmₗ b) = e.symm b :=
+rfl
+
+/-- A fiberwise linear map equal to `e` on `e.base_set`. -/
+protected def linear_map_at (e : trivialization R F E) (b : B) : E b →ₗ[R] F :=
+e.to_pretrivialization.linear_map_at b
+
+lemma coe_linear_map_at (e : trivialization R F E) (b : B) :
+  ⇑(e.linear_map_at b) = λ y, if b ∈ e.base_set then (e (total_space_mk b y)).2 else 0 :=
+e.to_pretrivialization.coe_linear_map_at b
+
+lemma coe_linear_map_at_of_mem (e : trivialization R F E) {b : B} (hb : b ∈ e.base_set) :
+  ⇑(e.linear_map_at b) = λ y, (e (total_space_mk b y)).2 :=
+by simp_rw [coe_linear_map_at, if_pos hb]
+
+lemma linear_map_at_apply (e : trivialization R F E) {b : B} (y : E b) :
+  e.linear_map_at b y = if b ∈ e.base_set then (e (total_space_mk b y)).2 else 0 :=
+by rw [coe_linear_map_at]
+
+lemma linear_map_at_def_of_mem (e : trivialization R F E) {b : B} (hb : b ∈ e.base_set) :
+  e.linear_map_at b = e.linear_equiv_at b hb :=
+dif_pos hb
+
+lemma linear_map_at_def_of_not_mem (e : trivialization R F E) {b : B} (hb : b ∉ e.base_set) :
+  e.linear_map_at b = 0 :=
+dif_neg hb
+
+lemma symmₗ_linear_map_at (e : trivialization R F E) {b : B} (hb : b ∈ e.base_set) (y : E b) :
+  e.symmₗ b (e.linear_map_at b y) = y :=
+e.to_pretrivialization.symmₗ_linear_map_at hb y
+
+lemma linear_map_at_symmₗ (e : trivialization R F E) {b : B} (hb : b ∈ e.base_set) (y : F) :
+  e.linear_map_at b (e.symmₗ b y) = y :=
+e.to_pretrivialization.linear_map_at_symmₗ hb y
+
 /-- A coordinate change function between two trivializations, as a continuous linear equivalence.
   Defined to be the identity when `b` does not lie in the base set of both trivializations. -/
 def coord_change (e e' : trivialization R F E) (b : B) : F ≃L[R] F :=
@@ -428,20 +526,61 @@ namespace topological_vector_bundle
 
 namespace trivialization
 
+/-- Forward map of `continuous_linear_equiv_at` (only propositionally equal),
+  defined everywhere (`0` outside domain). -/
+@[simps apply {fully_applied := ff}]
+def continuous_linear_map_at (e : trivialization R F E) (b : B) :
+  E b →L[R] F :=
+{ cont := begin
+    dsimp,
+    rw [e.coe_linear_map_at b],
+    refine continuous_if_const _ (λ hb, _) (λ _, continuous_zero),
+    exact 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))
+  end,
+  .. e.linear_map_at 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
+    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)
+        (λ x, mk_mem_prod hb (mem_univ x)) },
+    { refine continuous_zero.congr (λ x, (e.symm_apply_of_not_mem hb x).symm) },
+  end,
+  .. e.symmₗ b }
+
+lemma symmL_continuous_linear_map_at (e : trivialization R F E) {b : B} (hb : b ∈ e.base_set)
+  (y : E b) :
+  e.symmL b (e.continuous_linear_map_at b y) = y :=
+e.symmₗ_linear_map_at hb y
+
+lemma continuous_linear_map_at_symmL (e : trivialization R F E) {b : B} (hb : b ∈ e.base_set)
+  (y : F) :
+  e.continuous_linear_map_at b (e.symmL b y) = y :=
+e.linear_map_at_symmₗ hb y
+
 /-- In a topological vector bundle, a trivialization in the fiber (which is a priori only linear)
 is in fact a continuous linear equiv between the fibers and the model fiber. -/
-@[simps apply symm_apply] def continuous_linear_equiv_at (e : trivialization R F E) (b : B)
+@[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,
   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 := begin
-    rw (total_space_mk_inducing R F E b).continuous_iff,
-    exact e.continuous_on_symm.comp_continuous (continuous_const.prod_mk continuous_id)
-      (λ x, mk_mem_prod hb (mem_univ x)),
-  end,
-  .. e.linear_equiv_at b hb }
+  continuous_inv_fun := (e.symmL b).continuous,
+  .. e.to_pretrivialization.linear_equiv_at b hb }
+
+lemma coe_continuous_linear_equiv_at_eq (e : trivialization R F E) {b : B} (hb : b ∈ e.base_set) :
+  (e.continuous_linear_equiv_at b hb : E b → F) = e.continuous_linear_map_at b :=
+(e.coe_linear_map_at_of_mem hb).symm
+
+lemma symm_continuous_linear_equiv_at_eq (e : trivialization R F E) {b : B} (hb : b ∈ e.base_set) :
+  ((e.continuous_linear_equiv_at b hb).symm : F → E b) = e.symmL b :=
+rfl
 
 @[simp] lemma continuous_linear_equiv_at_apply' (e : trivialization R F E)
   (x : total_space E) (hx : x ∈ e.source) :
@@ -1293,7 +1432,7 @@ begin
   funext v,
   obtain ⟨v₁, v₂⟩ := v,
   rw [(e₁.prod e₂).continuous_linear_equiv_at_apply, trivialization.prod],
-  exact congr_arg prod.snd (prod_apply hx₁ hx₂ v₁ v₂),
+  exact (congr_arg prod.snd (prod_apply hx₁ hx₂ v₁ v₂) : _)
 end
 
 end topological_vector_bundle