feat(topology/vector_bundle): direct sum of topological vector bundles (

#12512)

src/data/bundle.lean

@@ -45,6 +45,9 @@ instance {x : B} : has_coe_t (E x) (total_space E) := ⟨sigma.mk x⟩
 
 lemma to_total_space_coe {x : B} (v : E x) : (v : total_space E) = ⟨x, v⟩ := rfl
 
+-- notation for the direct sum of two bundles over the same base
+notation E₁ `×ᵇ`:100 E₂ := λ x, E₁ x × E₂ x
+
 /-- `bundle.trivial B F` is the trivial bundle over `B` of fiber `F`. -/
 def trivial (B : Type*) (F : Type*) : B → Type* := function.const B F
 

src/topology/maps.lean

@@ -105,6 +105,14 @@ by { simp_rw [continuous_at, filter.tendsto, ← hf.map_nhds_of_mem _ h, filter.
 protected lemma inducing.continuous {f : α → β} (hf : inducing f) : continuous f :=
 hf.continuous_iff.mp continuous_id
 
+protected lemma inducing.inducing_iff {f : α → β} {g : β → γ} (hg : inducing g) :
+  inducing f ↔ inducing (g ∘ f) :=
+begin
+  refine ⟨λ h, hg.comp h, λ hgf, inducing_of_inducing_compose _ hg.continuous hgf⟩,
+  rw hg.continuous_iff,
+  exact hgf.continuous
+end
+
 lemma inducing.closure_eq_preimage_closure_image {f : α → β} (hf : inducing f) (s : set α) :
   closure s = f ⁻¹' closure (f '' s) :=
 by { ext x, rw [set.mem_preimage, ← closure_induced, hf.induced] }

src/topology/vector_bundle.lean

@@ -35,20 +35,19 @@ that the `topological_vector_bundle` class is `Prop`-valued.
 
 The point of this formalism is that it is unbundled in the sense that the total space of the bundle
 is a type with a topology, with which one can work or put further structure, and still one can
-perform operations on topological vector bundles (which are yet to be formalized). For instance,
-assume that `E₁ : B → Type*` and `E₂ : B → Type*` define two topological vector bundles over `R`
-with fiber models `F₁` and `F₂` which are normed spaces. Then one can construct the vector bundle of
-continuous linear maps from `E₁ x` to `E₂ x` with fiber `E x := (E₁ x →L[R] E₂ x)` (and with the
+perform operations on topological vector bundles.  For instance, assume that `E₁ : B → Type*` and
+`E₂ : B → Type*` define two topological vector bundles over `R` with fiber models `F₁` and `F₂`
+which are normed spaces. Then we construct the vector bundle `E₁ ×ᵇ E₂` of direct sums, with fiber
+`E x := (E₁ x × E₂ x)`. Then one can endow `bundle.total_space (E₁ ×ᵇ E₂)` with a topological vector
+bundle structure, `bundle.prod.topological_vector_bundle`.
+
+A similar construction (which is yet to be formalized) can be done for the vector bundle of
+continuous linear maps from `E₁ x` to `E₂ x` with fiber a type synonym
+`vector_bundle_continuous_linear_map R F₁ E₁ F₂ E₂ x := (E₁ x →L[R] E₂ x)` (and with the
 topology inherited from the norm-topology on `F₁ →L[R] F₂`, without the need to define the strong
-topology on continuous linear maps between general topological vector spaces). Let
-`vector_bundle_continuous_linear_map R F₁ E₁ F₂ E₂ (x : B)` be a type synonym for `E₁ x →L[R] E₂ x`.
-Then one can endow
-`bundle.total_space (vector_bundle_continuous_linear_map R F₁ E₁ F₂ E₂)`
-with a topology and a topological vector bundle structure.
-
-Similar constructions can be done for tensor products of topological vector bundles, exterior
-algebras, and so on, where the topology can be defined using a norm on the fiber model if this
-helps.
+topology on continuous linear maps between general topological vector spaces).  Likewise for tensor
+products of topological vector bundles, exterior algebras, and so on, where the topology can be
+defined using a norm on the fiber model if this helps.
 
 ## Tags
 Vector bundle
@@ -211,6 +210,31 @@ def continuous_linear_equiv_at (e : trivialization R F E) (b : B)
   (x : total_space E) (hx : x ∈ e.source) :
   e.continuous_linear_equiv_at (proj E x) (e.mem_source.1 hx) x.2 = (e x).2 := by { cases x, refl }
 
+lemma apply_eq_prod_continuous_linear_equiv_at (e : trivialization R F E) (b : B)
+  (hb : b ∈ e.base_set) (z : E b) :
+  e.to_local_homeomorph ⟨b, z⟩ = (b, e.continuous_linear_equiv_at b hb z) :=
+begin
+  ext,
+  { convert e.coe_fst _,
+    rw e.source_eq,
+    exact hb },
+  { simp }
+end
+
+lemma symm_apply_eq_mk_continuous_linear_equiv_at_symm (e : trivialization R F E) (b : B)
+  (hb : b ∈ e.base_set) (z : F) :
+  e.to_local_homeomorph.symm ⟨b, z⟩
+  = total_space_mk E b ((e.continuous_linear_equiv_at b hb).symm z) :=
+begin
+  have h : (b, z) ∈ e.to_local_homeomorph.target,
+  { rw e.target_eq,
+    exact ⟨hb, mem_univ _⟩ },
+  apply e.to_local_homeomorph.inj_on (e.to_local_homeomorph.map_target h),
+  { simp [e.source_eq, hb] },
+  simp [-continuous_linear_equiv_at_apply, e.apply_eq_prod_continuous_linear_equiv_at b hb,
+    e.to_local_homeomorph.right_inv h],
+end
+
 end trivialization
 
 section
@@ -270,6 +294,14 @@ lemma is_topological_vector_bundle_is_topological_fiber_bundle :
 λ x, ⟨(trivialization_at R F E x).to_fiber_bundle_trivialization,
   mem_base_set_trivialization_at R F E x⟩
 
+variables (R B F)
+include R F
+@[continuity] lemma continuous_proj : continuous (proj E) :=
+begin
+  apply @is_topological_fiber_bundle.continuous_proj B F,
+  apply @is_topological_vector_bundle_is_topological_fiber_bundle R,
+end
+
 end topological_vector_bundle
 
 /-! ### Constructing topological vector bundles -/
@@ -491,7 +523,7 @@ a.to_topological_fiber_prebundle.total_space_topology
 /-- Promotion from a `topologial_vector_prebundle.trivialization` to a
   `topological_vector_bundle.trivialization`. -/
 def trivialization_at (a : topological_vector_prebundle R F E) (x : B) :
-  @topological_vector_bundle.trivialization R _ F E _ _ _ _ _ _ _ a.total_space_topology  :=
+  @topological_vector_bundle.trivialization R _ F E _ _ _ _ _ _ _ a.total_space_topology :=
 begin
   letI := a.total_space_topology,
   exact { linear := (a.pretrivialization_at x).linear,
@@ -547,3 +579,224 @@ lemma to_topological_vector_bundle :
 end topological_vector_prebundle
 
 end
+
+/-! ### Direct sum of two vector bundles over the same base -/
+
+namespace topological_vector_bundle
+
+section defs
+variables {B₀ : Type*} (E₁ : B₀ → Type*)  (E₂ : B₀ → Type*)
+variables [topological_space (total_space E₁)] [topological_space (total_space E₂)]
+
+/-- Equip the total space of the fibrewise product of two topological vector bundles `E₁`, `E₂` with
+the induced topology from the diagonal embedding into `(total_space E₁) × (total_space E₂)`. -/
+instance prod.topological_space :
+  topological_space (total_space (E₁ ×ᵇ E₂)) :=
+topological_space.induced
+  (λ p, ((⟨p.1, p.2.1⟩ : total_space E₁), (⟨p.1, p.2.2⟩ : total_space E₂)))
+  (by apply_instance : topological_space ((total_space E₁) × (total_space E₂)))
+
+/-- The diagonal map from the total space of the fibrewise product of two topological vector bundles
+`E₁`, `E₂` into `(total_space E₁) × (total_space E₂)` is `inducing`. -/
+lemma prod.inducing_diag : inducing
+  (λ p, (⟨p.1, p.2.1⟩, ⟨p.1, p.2.2⟩) :
+    total_space (E₁ ×ᵇ E₂) → (total_space E₁) × (total_space E₂)) :=
+⟨rfl⟩
+
+end defs
+
+variables (F₁ : Type*) [topological_space F₁] [add_comm_monoid F₁] [module R F₁]
+  (E₁ : B → Type*) [topological_space (total_space E₁)]
+  [Π x, add_comm_monoid (E₁ x)] [Π x, module R (E₁ x)]
+
+variables (F₂ : Type*) [topological_space F₂] [add_comm_monoid F₂] [module R F₂]
+  (E₂ : B → Type*) [topological_space (total_space E₂)]
+  [Π x, add_comm_monoid (E₂ x)] [Π x, module R (E₂ x)]
+
+namespace trivialization
+variables (e₁ : trivialization R F₁ E₁) (e₂ : trivialization R F₂ E₂)
+include e₁ e₂
+variables {R F₁ E₁ F₂ E₂}
+
+/-- Given trivializations `e₁`, `e₂` for vector bundles `E₁`, `E₂` over a base `B`, the forward
+function for the construction `topological_vector_bundle.trivialization.prod`, the induced
+trivialization for the direct sum of `E₁` and `E₂`. -/
+def prod.to_fun' : total_space (E₁ ×ᵇ E₂) → B × (F₁ × F₂) :=
+λ ⟨x, v₁, v₂⟩, ⟨x, (e₁ ⟨x, v₁⟩).2, (e₂ ⟨x, v₂⟩).2⟩
+
+variables [Π x : B, topological_space (E₁ x)] [Π x : B, topological_space (E₂ x)]
+  [topological_vector_bundle R F₁ E₁] [topological_vector_bundle R F₂ E₂]
+
+/-- Given trivializations `e₁`, `e₂` for vector bundles `E₁`, `E₂` over a base `B`, the inverse
+function for the construction `topological_vector_bundle.trivialization.prod`, the induced
+trivialization for the direct sum of `E₁` and `E₂`. -/
+def prod.inv_fun' (p : B × (F₁ × F₂)) : total_space (E₁ ×ᵇ E₂) :=
+begin
+  obtain ⟨x, w₁, w₂⟩ := p,
+  refine ⟨x, _, _⟩,
+  { by_cases h : x ∈ e₁.base_set,
+    { exact (e₁.continuous_linear_equiv_at x h).symm w₁ },
+    { exact 0 } },
+  { by_cases h : x ∈ e₂.base_set,
+    { exact (e₂.continuous_linear_equiv_at x h).symm w₂ },
+    { exact 0 } },
+end
+
+variables {e₁ e₂}
+
+lemma prod.inv_fun'_apply {x : B} (hx₁ : x ∈ e₁.base_set) (hx₂ : x ∈ e₂.base_set)
+  (w₁ : F₁) (w₂ : F₂) :
+  prod.inv_fun' e₁ e₂ ⟨x, w₁, w₂⟩
+  = ⟨x, ((e₁.continuous_linear_equiv_at x hx₁).symm w₁,
+    (e₂.continuous_linear_equiv_at x hx₂).symm w₂)⟩ :=
+begin
+  dsimp [prod.inv_fun'],
+  rw [dif_pos, dif_pos],
+end
+
+variables (e₁ e₂)
+
+/-- Given trivializations `e₁`, `e₂` for vector bundles `E₁`, `E₂` over a base `B`, the induced
+trivialization for the direct sum of `E₁` and `E₂`, whose base set is `e₁.base_set ∩ e₂.base_set`.
+-/
+def prod : trivialization R (F₁ × F₂) (E₁ ×ᵇ E₂) :=
+{ to_fun := prod.to_fun' e₁ e₂,
+  inv_fun := prod.inv_fun' e₁ e₂,
+  source := (proj (λ x, E₁ x × E₂ x)) ⁻¹' (e₁.base_set ∩ e₂.base_set),
+  target := (e₁.base_set ∩ e₂.base_set) ×ˢ (set.univ : set (F₁ × F₂)),
+  map_source' := λ ⟨x, v₁, v₂⟩ h, ⟨h, set.mem_univ _⟩,
+  map_target' := λ ⟨x, w₁, w₂⟩ h, h.1,
+  left_inv' := λ ⟨x, v₁, v₂⟩ h,
+  begin
+    simp only [prod.to_fun', prod.inv_fun', sigma.mk.inj_iff, true_and, eq_self_iff_true,
+      prod.mk.inj_iff, heq_iff_eq],
+    split,
+    { rw [dif_pos, ← e₁.continuous_linear_equiv_at_apply x h.1,
+        continuous_linear_equiv.symm_apply_apply] },
+    { rw [dif_pos, ← e₂.continuous_linear_equiv_at_apply x h.2,
+        continuous_linear_equiv.symm_apply_apply] },
+  end,
+  right_inv' := λ ⟨x, w₁, w₂⟩ ⟨h, _⟩,
+  begin
+    dsimp [prod.to_fun', prod.inv_fun'],
+    simp only [prod.mk.inj_iff, eq_self_iff_true, true_and],
+    split,
+    { rw [dif_pos, ← e₁.continuous_linear_equiv_at_apply x h.1,
+        continuous_linear_equiv.apply_symm_apply] },
+    { rw [dif_pos, ← e₂.continuous_linear_equiv_at_apply x h.2,
+        continuous_linear_equiv.apply_symm_apply] },
+  end,
+  open_source := begin
+    refine (e₁.open_base_set.inter e₂.open_base_set).preimage _,
+    have : continuous (proj E₁) := continuous_proj R B F₁,
+    exact this.comp (continuous_fst.comp (prod.inducing_diag E₁ E₂).continuous),
+  end,
+  open_target := (e₁.open_base_set.inter e₂.open_base_set).prod is_open_univ,
+  continuous_to_fun :=
+  begin
+    let f₁ : total_space (E₁ ×ᵇ E₂) → total_space E₁ × total_space E₂ :=
+      λ p, ((⟨p.1, p.2.1⟩ : total_space E₁), (⟨p.1, p.2.2⟩ : total_space E₂)),
+    let f₂ : total_space E₁ × total_space E₂ → (B × F₁) × (B × F₂) := λ p, ⟨e₁ p.1, e₂ p.2⟩,
+    let f₃ : (B × F₁) × (B × F₂) → B × F₁ × F₂ := λ p, ⟨p.1.1, p.1.2, p.2.2⟩,
+    have hf₁ : continuous f₁ := (prod.inducing_diag E₁ E₂).continuous,
+    have hf₂ : continuous_on f₂ (e₁.source ×ˢ e₂.source) :=
+      e₁.to_local_homeomorph.continuous_on.prod_map e₂.to_local_homeomorph.continuous_on,
+    have hf₃ : continuous f₃ :=
+      (continuous_fst.comp continuous_fst).prod_mk (continuous_snd.prod_map continuous_snd),
+    refine ((hf₃.comp_continuous_on hf₂).comp hf₁.continuous_on _).congr _,
+    { rw [e₁.source_eq, e₂.source_eq],
+      exact maps_to_preimage _ _ },
+    rintros ⟨b, v₁, v₂⟩ ⟨hb₁, hb₂⟩,
+    simp only [prod.to_fun', prod.mk.inj_iff, eq_self_iff_true, and_true],
+    rw e₁.coe_fst,
+    rw [e₁.source_eq, mem_preimage],
+    exact hb₁,
+  end,
+  continuous_inv_fun :=
+  begin
+    rw (prod.inducing_diag E₁ E₂).continuous_on_iff,
+    suffices : continuous_on (λ p : B × F₁ × F₂,
+      (e₁.to_local_homeomorph.symm ⟨p.1, p.2.1⟩, e₂.to_local_homeomorph.symm ⟨p.1, p.2.2⟩))
+      ((e₁.base_set ∩ e₂.base_set) ×ˢ (univ : set (F₁ × F₂))),
+    { refine this.congr _,
+      rintros ⟨b, v₁, v₂⟩ ⟨⟨h₁, h₂⟩, _⟩,
+      dsimp at ⊢ h₁ h₂,
+      rw [prod.inv_fun'_apply h₁ h₂, e₁.symm_apply_eq_mk_continuous_linear_equiv_at_symm b h₁,
+        e₂.symm_apply_eq_mk_continuous_linear_equiv_at_symm b h₂] },
+    have H₁ : continuous (λ p : B × F₁ × F₂, ((p.1, p.2.1), (p.1, p.2.2))) :=
+      (continuous_id.prod_map continuous_fst).prod_mk (continuous_id.prod_map continuous_snd),
+    have H₂ := e₁.to_local_homeomorph.symm.continuous_on.prod_map
+      e₂.to_local_homeomorph.symm.continuous_on,
+    convert H₂.comp H₁.continuous_on (λ x h, ⟨_, _⟩),
+    { dsimp,
+      rw e₁.target_eq,
+      exact ⟨h.1.1, mem_univ _⟩ },
+    { dsimp,
+      rw e₂.target_eq,
+      exact ⟨h.1.2, mem_univ _⟩ }
+  end,
+  base_set := e₁.base_set ∩ e₂.base_set,
+  open_base_set := e₁.open_base_set.inter e₂.open_base_set,
+  source_eq := rfl,
+  target_eq := rfl,
+  proj_to_fun := λ ⟨x, v₁, v₂⟩ h, rfl,
+  linear := λ x ⟨h₁, h₂⟩,
+  { map_add := λ ⟨v₁, v₂⟩ ⟨v₁', v₂'⟩,
+      congr_arg2 prod.mk ((e₁.linear x h₁).map_add v₁ v₁') ((e₂.linear x h₂).map_add v₂ v₂'),
+    map_smul := λ c ⟨v₁, v₂⟩,
+      congr_arg2 prod.mk ((e₁.linear x h₁).map_smul c v₁) ((e₂.linear x h₂).map_smul c v₂), } }
+
+@[simp] lemma base_set_prod : (prod e₁ e₂).base_set = e₁.base_set ∩ e₂.base_set :=
+rfl
+
+variables {e₁ e₂}
+
+@[simp] lemma prod_apply {x : B} (hx₁ : x ∈ e₁.base_set) (hx₂ : x ∈ e₂.base_set) (v₁ : E₁ x)
+  (v₂ : E₂ x) :
+  prod e₁ e₂ ⟨x, (v₁, v₂)⟩
+  = ⟨x, e₁.continuous_linear_equiv_at x hx₁ v₁, e₂.continuous_linear_equiv_at x hx₂ v₂⟩ :=
+rfl
+
+lemma prod_symm_apply {x : B} (hx₁ : x ∈ e₁.base_set) (hx₂ : x ∈ e₂.base_set) (w₁ : F₁) (w₂ : F₂) :
+  (prod e₁ e₂).to_local_equiv.symm (x, (w₁, w₂))
+  = ⟨x, ((e₁.continuous_linear_equiv_at x hx₁).symm w₁,
+      (e₂.continuous_linear_equiv_at x hx₂).symm w₂)⟩ :=
+prod.inv_fun'_apply hx₁ hx₂ w₁ w₂
+
+end trivialization
+
+open trivialization
+
+variables [Π x : B, topological_space (E₁ x)] [Π x : B, topological_space (E₂ x)]
+  [topological_vector_bundle R F₁ E₁] [topological_vector_bundle R F₂ E₂]
+
+/-- The product of two vector bundles is a vector bundle. -/
+instance _root_.bundle.prod.topological_vector_bundle :
+  topological_vector_bundle R (F₁ × F₂) (E₁ ×ᵇ E₂) :=
+{ total_space_mk_inducing := λ b,
+  begin
+    rw (prod.inducing_diag E₁ E₂).inducing_iff,
+    exact (total_space_mk_inducing R F₁ E₁ b).prod_mk (total_space_mk_inducing R F₂ E₂ b),
+  end,
+  locally_trivial := λ b,
+  begin
+    obtain ⟨e₁, he₁⟩ := locally_trivial R F₁ E₁ b,
+    obtain ⟨e₂, he₂⟩ := locally_trivial R F₂ E₂ b,
+    exact ⟨e₁.prod e₂, he₁, he₂⟩
+  end }
+
+variables {R F₁ E₁ F₂ E₂}
+
+@[simp] lemma trivialization.continuous_linear_equiv_at_prod {e₁ : trivialization R F₁ E₁}
+  {e₂ : trivialization R F₂ E₂} {x : B} (hx₁ : x ∈ e₁.base_set) (hx₂ : x ∈ e₂.base_set) :
+  (e₁.prod e₂).continuous_linear_equiv_at x ⟨hx₁, hx₂⟩
+  = (e₁.continuous_linear_equiv_at x hx₁).prod (e₂.continuous_linear_equiv_at x hx₂) :=
+begin
+  ext1,
+  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₂),
+end
+
+end topological_vector_bundle