refactor(topology/{fiber,vector}_bundle): make vector_bundle a mixin (#17505)

Previously, `is_fiber_bundle`* was a propositional typeclass on a function `p : Z → B`, stating the existence of local trivializations covering `Z`.  Then `vector_bundle`* was a class with data on a type `E : X → Type*` (with the projection from `Σ x : B, E x` to `B` playing the role of `p`), giving a fixed atlas of fibrewise-linear local trivializations.

We change this definition so that 
(i) the data is all held in `fiber_bundle`, with `vector_bundle` a mixin stating fibrewise-linearity
(ii) only sigma-types can be fiber bundles, not general topological spaces

This allows bundles to carry instances of typeclasses in which the scalar field, `R`, does not appear as a parameter.  Notably, we would like a vector bundle over `R` with fibre `F` over base `B` to be a `charted_space (B × F)`, with the trivializations providing the charts.  This would be a dangerous instance for typeclass inference, because `R` does not appear as a parameter in `charted_space (B × F)`.  But if the data of the trivializations is held in `fiber_bundle`, then a *fibre* bundle with fibre `F` over base `B` can be a `charted_space (B × F)`, and this is safe for typeclass inference.

We expect that this refector will also streamline constructions of fibre bundles with similar underlying structure (e.g., the same bundle being both a real and complex vector bundle).

[Here](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Smooth.20vector.20bundles/near/306023372) is the relevant Zulip discussion.

*We take the opportunity to rename `topological_{fiber,vector}_bundle` to `{fiber,vector}_bundle`, since in the upcoming definition of smooth bundles, smoothness will be another mixin for `fiber_bundle`.

Co-authored-by: Floris van Doorn [fpvdoorn@gmail.com](mailto:fpvdoorn@gmail.com)

Author: hrmacbeth

docs/overview.yaml

@@ -211,7 +211,8 @@ Topology:
     connectedness: 'connected_space'
     compact open topology: 'continuous_map.compact_open'
     Stone-Cech compactification: 'stone_cech'
-    topological fiber bundle: 'is_topological_fiber_bundle'
+    topological fiber bundle: 'fiber_bundle'
+    topological vector bundle: 'vector_bundle'
     Urysohn's lemma: 'exists_continuous_zero_one_of_closed'
     Stone-Weierstrass theorem: 'continuous_map.subalgebra_topological_closure_eq_top_of_separates_points'
   Uniform notions:

src/analysis/complex/re_im_topology.lean

@@ -16,7 +16,7 @@ topological properties of `complex.re` and `complex.im`.
 
 Each statement about `complex.re` listed below has a counterpart about `complex.im`.
 
-* `complex.is_trivial_topological_fiber_bundle_re`: `complex.re` turns `ℂ` into a trivial
+* `complex.is_homeomorphic_trivial_fiber_bundle_re`: `complex.re` turns `ℂ` into a trivial
   topological fiber bundle over `ℝ`;
 * `complex.is_open_map_re`, `complex.quotient_map_re`: in particular, `complex.re` is an open map
   and is a quotient map;
@@ -37,24 +37,18 @@ noncomputable theory
 namespace complex
 
 /-- `complex.re` turns `ℂ` into a trivial topological fiber bundle over `ℝ`. -/
-lemma is_trivial_topological_fiber_bundle_re : is_trivial_topological_fiber_bundle ℝ re :=
+lemma is_homeomorphic_trivial_fiber_bundle_re : is_homeomorphic_trivial_fiber_bundle ℝ re :=
 ⟨equiv_real_prodₗ.to_homeomorph, λ z, rfl⟩
 
 /-- `complex.im` turns `ℂ` into a trivial topological fiber bundle over `ℝ`. -/
-lemma is_trivial_topological_fiber_bundle_im : is_trivial_topological_fiber_bundle ℝ im :=
+lemma is_homeomorphic_trivial_fiber_bundle_im : is_homeomorphic_trivial_fiber_bundle ℝ im :=
 ⟨equiv_real_prodₗ.to_homeomorph.trans (homeomorph.prod_comm ℝ ℝ), λ z, rfl⟩
 
-lemma is_topological_fiber_bundle_re : is_topological_fiber_bundle ℝ re :=
-is_trivial_topological_fiber_bundle_re.is_topological_fiber_bundle
+lemma is_open_map_re : is_open_map re := is_homeomorphic_trivial_fiber_bundle_re.is_open_map_proj
+lemma is_open_map_im : is_open_map im := is_homeomorphic_trivial_fiber_bundle_im.is_open_map_proj
 
-lemma is_topological_fiber_bundle_im : is_topological_fiber_bundle ℝ im :=
-is_trivial_topological_fiber_bundle_im.is_topological_fiber_bundle
-
-lemma is_open_map_re : is_open_map re := is_topological_fiber_bundle_re.is_open_map_proj
-lemma is_open_map_im : is_open_map im := is_topological_fiber_bundle_im.is_open_map_proj
-
-lemma quotient_map_re : quotient_map re := is_topological_fiber_bundle_re.quotient_map_proj
-lemma quotient_map_im : quotient_map im := is_topological_fiber_bundle_im.quotient_map_proj
+lemma quotient_map_re : quotient_map re := is_homeomorphic_trivial_fiber_bundle_re.quotient_map_proj
+lemma quotient_map_im : quotient_map im := is_homeomorphic_trivial_fiber_bundle_im.quotient_map_proj
 
 lemma interior_preimage_re (s : set ℝ) : interior (re ⁻¹' s) = re ⁻¹' (interior s) :=
 (is_open_map_re.preimage_interior_eq_interior_preimage continuous_re _).symm

src/geometry/manifold/cont_mdiff_mfderiv.lean

@@ -443,30 +443,30 @@ variables (Z : basic_smooth_vector_bundle_core I M E')
 
 /-- A version of `cont_mdiff_at_iff_target` when the codomain is the total space of
   a `basic_smooth_vector_bundle_core`. The continuity condition in the RHS is weaker. -/
-lemma cont_mdiff_at_iff_target {f : N → Z.to_topological_vector_bundle_core.total_space}
+lemma cont_mdiff_at_iff_target {f : N → Z.to_vector_bundle_core.total_space}
   {x : N} {n : ℕ∞} :
   cont_mdiff_at J (I.prod 𝓘(𝕜, E')) n f x ↔ continuous_at (bundle.total_space.proj ∘ f) x ∧
     cont_mdiff_at J 𝓘(𝕜, E × E') n (ext_chart_at (I.prod 𝓘(𝕜, E')) (f x) ∘ f) x :=
 begin
-  let Z' := Z.to_topological_vector_bundle_core,
+  let Z' := Z.to_vector_bundle_core,
   rw [cont_mdiff_at_iff_target, and.congr_left_iff],
   refine λ hf, ⟨λ h, Z'.continuous_proj.continuous_at.comp h, λ h, _⟩,
   exact (Z'.local_triv ⟨chart_at _ (f x).1, chart_mem_atlas _ _⟩)
     .continuous_at_of_comp_left h (mem_chart_source _ _) (h.prod hf.continuous_at.snd)
 end
 
-lemma smooth_iff_target {f : N → Z.to_topological_vector_bundle_core.total_space} :
+lemma smooth_iff_target {f : N → Z.to_vector_bundle_core.total_space} :
   smooth J (I.prod 𝓘(𝕜, E')) f ↔ continuous (bundle.total_space.proj ∘ f) ∧
   ∀ x, smooth_at J 𝓘(𝕜, E × E') (ext_chart_at (I.prod 𝓘(𝕜, E')) (f x) ∘ f) x :=
 by simp_rw [smooth, smooth_at, cont_mdiff, Z.cont_mdiff_at_iff_target, forall_and_distrib,
   continuous_iff_continuous_at]
 
 lemma cont_mdiff_proj :
-  cont_mdiff (I.prod 𝓘(𝕜, E')) I n Z.to_topological_vector_bundle_core.proj :=
+  cont_mdiff (I.prod 𝓘(𝕜, E')) I n Z.to_vector_bundle_core.proj :=
 begin
   assume x,
   rw [cont_mdiff_at, cont_mdiff_within_at_iff'],
-  refine ⟨Z.to_topological_vector_bundle_core.continuous_proj.continuous_within_at, _⟩,
+  refine ⟨Z.to_vector_bundle_core.continuous_proj.continuous_within_at, _⟩,
   simp only [(∘), chart_at, chart] with mfld_simps,
   apply cont_diff_within_at_fst.congr,
   { rintros ⟨a, b⟩ hab,
@@ -476,39 +476,39 @@ begin
 end
 
 lemma smooth_proj :
-  smooth (I.prod 𝓘(𝕜, E')) I Z.to_topological_vector_bundle_core.proj :=
+  smooth (I.prod 𝓘(𝕜, E')) I Z.to_vector_bundle_core.proj :=
 cont_mdiff_proj Z
 
-lemma cont_mdiff_on_proj {s : set (Z.to_topological_vector_bundle_core.total_space)} :
+lemma cont_mdiff_on_proj {s : set (Z.to_vector_bundle_core.total_space)} :
   cont_mdiff_on (I.prod 𝓘(𝕜, E')) I n
-    Z.to_topological_vector_bundle_core.proj s :=
+    Z.to_vector_bundle_core.proj s :=
 Z.cont_mdiff_proj.cont_mdiff_on
 
-lemma smooth_on_proj {s : set (Z.to_topological_vector_bundle_core.total_space)} :
-  smooth_on (I.prod 𝓘(𝕜, E')) I Z.to_topological_vector_bundle_core.proj s :=
+lemma smooth_on_proj {s : set (Z.to_vector_bundle_core.total_space)} :
+  smooth_on (I.prod 𝓘(𝕜, E')) I Z.to_vector_bundle_core.proj s :=
 cont_mdiff_on_proj Z
 
-lemma cont_mdiff_at_proj {p : Z.to_topological_vector_bundle_core.total_space} :
+lemma cont_mdiff_at_proj {p : Z.to_vector_bundle_core.total_space} :
   cont_mdiff_at (I.prod 𝓘(𝕜, E')) I n
-    Z.to_topological_vector_bundle_core.proj p :=
+    Z.to_vector_bundle_core.proj p :=
 Z.cont_mdiff_proj.cont_mdiff_at
 
-lemma smooth_at_proj {p : Z.to_topological_vector_bundle_core.total_space} :
-  smooth_at (I.prod 𝓘(𝕜, E')) I Z.to_topological_vector_bundle_core.proj p :=
+lemma smooth_at_proj {p : Z.to_vector_bundle_core.total_space} :
+  smooth_at (I.prod 𝓘(𝕜, E')) I Z.to_vector_bundle_core.proj p :=
 Z.cont_mdiff_at_proj
 
 lemma cont_mdiff_within_at_proj
-  {s : set (Z.to_topological_vector_bundle_core.total_space)}
-  {p : Z.to_topological_vector_bundle_core.total_space} :
+  {s : set (Z.to_vector_bundle_core.total_space)}
+  {p : Z.to_vector_bundle_core.total_space} :
   cont_mdiff_within_at (I.prod 𝓘(𝕜, E')) I n
-    Z.to_topological_vector_bundle_core.proj s p :=
+    Z.to_vector_bundle_core.proj s p :=
 Z.cont_mdiff_at_proj.cont_mdiff_within_at
 
 lemma smooth_within_at_proj
-  {s : set (Z.to_topological_vector_bundle_core.total_space)}
-  {p : Z.to_topological_vector_bundle_core.total_space} :
+  {s : set (Z.to_vector_bundle_core.total_space)}
+  {p : Z.to_vector_bundle_core.total_space} :
   smooth_within_at (I.prod 𝓘(𝕜, E')) I
-    Z.to_topological_vector_bundle_core.proj s p :=
+    Z.to_vector_bundle_core.proj s p :=
 Z.cont_mdiff_within_at_proj
 
 /-- If an element of `E'` is invariant under all coordinate changes, then one can define a
@@ -518,24 +518,24 @@ section of the endomorphism bundle of a vector bundle. -/
 lemma smooth_const_section (v : E')
   (h : ∀ (i j : atlas H M), ∀ x ∈ i.1.source ∩ j.1.source, Z.coord_change i j (i.1 x) v = v) :
   smooth I (I.prod 𝓘(𝕜, E'))
-    (show M → Z.to_topological_vector_bundle_core.total_space, from λ x, ⟨x, v⟩) :=
+    (show M → Z.to_vector_bundle_core.total_space, from λ x, ⟨x, v⟩) :=
 begin
   assume x,
   rw [cont_mdiff_at, cont_mdiff_within_at_iff'],
   split,
   { apply continuous.continuous_within_at,
-    apply topological_fiber_bundle_core.continuous_const_section,
+    apply fiber_bundle_core.continuous_const_section,
     assume i j y hy,
     exact h _ _ _ hy },
   { have : cont_diff 𝕜 ⊤ (λ (y : E), (y, v)) := cont_diff_id.prod cont_diff_const,
     apply this.cont_diff_within_at.congr,
     { assume y hy,
       simp only with mfld_simps at hy,
-      simp only [chart, hy, chart_at, prod.mk.inj_iff, to_topological_vector_bundle_core]
+      simp only [chart, hy, chart_at, prod.mk.inj_iff, to_vector_bundle_core]
         with mfld_simps,
       apply h,
       simp only [hy, subtype.val_eq_coe] with mfld_simps },
-    { simp only [chart, chart_at, prod.mk.inj_iff, to_topological_vector_bundle_core]
+    { simp only [chart, chart_at, prod.mk.inj_iff, to_vector_bundle_core]
         with mfld_simps,
       apply h,
       simp only [subtype.val_eq_coe] with mfld_simps } }
@@ -634,7 +634,7 @@ begin
     { exact differentiable_at_id'.prod (differentiable_at_const _) } },
   simp only [tangent_bundle.zero_section, tangent_map, mfderiv,
     A, dif_pos, chart_at, basic_smooth_vector_bundle_core.chart,
-    basic_smooth_vector_bundle_core.to_topological_vector_bundle_core, tangent_bundle_core,
+    basic_smooth_vector_bundle_core.to_vector_bundle_core, tangent_bundle_core,
     function.comp, continuous_linear_map.map_zero] with mfld_simps,
   rw ← fderiv_within_inter N (I.unique_diff (I ((chart_at H x) x)) (set.mem_range_self _)) at B,
   rw [← fderiv_within_inter N (I.unique_diff (I ((chart_at H x) x)) (set.mem_range_self _)), ← B],

src/geometry/manifold/mfderiv.lean

@@ -1425,7 +1425,7 @@ begin
   -- a trivial instance is needed after the rewrite, handle it right now.
   rotate, { apply_instance },
   simp only [continuous_linear_map.coe_coe, basic_smooth_vector_bundle_core.chart, h,
-    tangent_bundle_core, basic_smooth_vector_bundle_core.to_topological_vector_bundle_core,
+    tangent_bundle_core, basic_smooth_vector_bundle_core.to_vector_bundle_core,
     chart_at, sigma.mk.inj_iff] with mfld_simps,
 end
 
@@ -1695,7 +1695,7 @@ variables {F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
 /-- In a smooth fiber bundle constructed from core, the preimage under the projection of a set with
 unique differential in the basis also has unique differential. -/
 lemma unique_mdiff_on.smooth_bundle_preimage (hs : unique_mdiff_on I s) :
-  unique_mdiff_on (I.prod (𝓘(𝕜, F))) (Z.to_topological_vector_bundle_core.proj ⁻¹' s) :=
+  unique_mdiff_on (I.prod (𝓘(𝕜, F))) (Z.to_vector_bundle_core.proj ⁻¹' s) :=
 begin
   /- Using a chart (and the fact that unique differentiability is invariant under charts), we
   reduce the situation to the model space, where we can use the fact that products respect
@@ -1706,14 +1706,14 @@ begin
   let e := chart_at (model_prod H F) p,
   -- It suffices to prove unique differentiability in a chart
   suffices h : unique_mdiff_on (I.prod (𝓘(𝕜, F)))
-    (e.target ∩ e.symm⁻¹' (Z.to_topological_vector_bundle_core.proj ⁻¹' s)),
+    (e.target ∩ e.symm⁻¹' (Z.to_vector_bundle_core.proj ⁻¹' s)),
   { have A : unique_mdiff_on (I.prod (𝓘(𝕜, F))) (e.symm.target ∩
-      e.symm.symm ⁻¹' (e.target ∩ e.symm⁻¹' (Z.to_topological_vector_bundle_core.proj ⁻¹' s))),
+      e.symm.symm ⁻¹' (e.target ∩ e.symm⁻¹' (Z.to_vector_bundle_core.proj ⁻¹' s))),
     { apply h.unique_mdiff_on_preimage,
       exact (mdifferentiable_of_mem_atlas _ (chart_mem_atlas _ _)).symm,
       apply_instance },
     have : p ∈ e.symm.target ∩
-      e.symm.symm ⁻¹' (e.target ∩ e.symm⁻¹' (Z.to_topological_vector_bundle_core.proj ⁻¹' s)),
+      e.symm.symm ⁻¹' (e.target ∩ e.symm⁻¹' (Z.to_vector_bundle_core.proj ⁻¹' s)),
         by simp only [e, hp] with mfld_simps,
     apply (A _ this).mono,
     assume q hq,