chore(topology/{fiber,vector}_bundle/*): reorganize files (#17559)

The PR #17505 was a big refactor but left declarations in place.  This PR proposes a reorganization to clean up:
- new file `topology.fiber_bundle.is_homeomorphic_trivial_bundle` for the legacy `is_homeomorphic_trivial_fiber_bundle` construction (see [discussion](#17505 (comment)))
- new file `topology.fiber_bundle.constructions` covering the trivial, fibrewise-product and pullback fiber bundles.  The trivial-bundle material was previously split between `topology.{fiber,vector}_bundle.basic`, the prod material was previously in `topology.vector_bundle.prod`, the pullback material was previously in `topology.vector_bundle.pullback`
- new file `topology.vector_bundle.constructions` covering the trivial, direct-sum and pullback vector bundles.  The trivial-bundle material was previously in `topology.vector_bundle.basic`, the prod material was previously in `topology.vector_bundle.prod`, the pullback material was previously in `topology.vector_bundle.pullback`
- delete files `topology.vector_bundle.prod` and `topology.vector_bundle.pullback`, whose material has all been moved elsewhere
- delete construction `trivialization.comap`, which was morally (though not literally) a duplicate of `trivialization.pullback`
- cleaner proof of `trivialization.prod.open_source`, removing a spurious dependence on an ambient fiber bundle structure
- updated and augmented docs

src/analysis/complex/re_im_topology.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import analysis.complex.basic
-import topology.fiber_bundle.basic
+import topology.fiber_bundle.is_homeomorphic_trivial_bundle
 
 /-!
 # Closure, interior, and frontier of preimages under `re` and `im`

src/topology/fiber_bundle/basic.lean

@@ -47,10 +47,6 @@ fiber bundle from trivializations given as local equivalences with minimum addit
 
 * `fiber_bundle F E` : Structure saying that `E : B → Type*` is a fiber bundle with fiber `F`.
 
-* `is_homeomorphic_trivial_fiber_bundle F p` : Prop saying that the map `p : Z → B` between
-  topological spaces is a trivial fiber bundle, i.e., there exists a homeomorphism
-  `h : Z ≃ₜ B × F` such that `proj x = (h x).1`.
-
 ### Construction of a bundle from trivializations
 
 * `bundle.total_space E` is a type synonym for `Σ (x : B), E x`, that we can endow with a suitable
@@ -173,15 +169,15 @@ variables {ι : Type*} {B : Type*} {F : Type*}
 open topological_space filter set bundle
 open_locale topological_space classical bundle
 
+attribute [mfld_simps] total_space.proj total_space_mk coe_fst coe_snd coe_snd_map_apply
+  coe_snd_map_smul total_space.mk_cast
+
 /-! ### General definition of fiber bundles -/
 
 section fiber_bundle
 
 variables (F) [topological_space B] [topological_space F] (E : B → Type*)
-
-/-! ### Fiber bundles -/
-
-variables [topological_space (total_space E)] [∀ b, topological_space (E b)]
+  [topological_space (total_space E)] [∀ b, topological_space (E b)]
 
 /-- A (topological) fiber bundle with fiber `F` over a base `B` is a space projecting on `B`
 for which the fibers are all homeomorphic to `F`, such that the local situation around each point
@@ -209,21 +205,6 @@ class mem_trivialization_atlas [fiber_bundle F E] (e : trivialization F (π E))
 instance [fiber_bundle F E] (b : B) : mem_trivialization_atlas (trivialization_at F E b) :=
 { out := trivialization_mem_atlas F E b }
 
-variables (F E)
-
-/-- A trivial fiber bundle with fiber `F` over a base `B` is a space `Z`
-projecting on `B` for which there exists a homeomorphism to `B × F` that sends `proj`
-to `prod.fst`. -/
-def is_homeomorphic_trivial_fiber_bundle {Z : Type*} [topological_space Z] (proj : Z → B) : Prop :=
-∃ e : Z ≃ₜ (B × F), ∀ x, (e x).1 = proj x
-
-variables {F}
-
-lemma is_homeomorphic_trivial_fiber_bundle.proj_eq {Z : Type*} [topological_space Z] {proj : Z → B}
-  (h : is_homeomorphic_trivial_fiber_bundle F proj) :
-  ∃ e : Z ≃ₜ (B × F), proj = prod.fst ∘ e :=
-⟨h.some, (funext h.some_spec).symm⟩
-
 namespace fiber_bundle
 variables (F) {E} [fiber_bundle F E]
 
@@ -258,52 +239,7 @@ lemma continuous_total_space_mk (x : B) : continuous (@total_space_mk B E x) :=
 
 end fiber_bundle
 
-variables {F}
-
-/-- The projection from a trivial fiber bundle to its base is surjective. -/
-lemma is_homeomorphic_trivial_fiber_bundle.surjective_proj [nonempty F] {Z : Type*}
-  [topological_space Z] {proj : Z → B} (h : is_homeomorphic_trivial_fiber_bundle F proj) :
-  function.surjective proj :=
-begin
-  obtain ⟨e, rfl⟩ := h.proj_eq,
-  exact prod.fst_surjective.comp e.surjective,
-end
-
-/-- The projection from a trivial fiber bundle to its base is continuous. -/
-lemma is_homeomorphic_trivial_fiber_bundle.continuous_proj {Z : Type*} [topological_space Z]
-  {proj : Z → B} (h : is_homeomorphic_trivial_fiber_bundle F proj) :
-  continuous proj :=
-begin
-  obtain ⟨e, rfl⟩ := h.proj_eq,
-  exact continuous_fst.comp e.continuous,
-end
-
-/-- The projection from a trivial fiber bundle to its base is open. -/
-lemma is_homeomorphic_trivial_fiber_bundle.is_open_map_proj {Z : Type*} [topological_space Z]
-  {proj : Z → B} (h : is_homeomorphic_trivial_fiber_bundle F proj) :
-  is_open_map proj :=
-begin
-  obtain ⟨e, rfl⟩ := h.proj_eq,
-  exact is_open_map_fst.comp e.is_open_map,
-end
-
-/-- The projection from a trivial fiber bundle to its base is open. -/
-lemma is_homeomorphic_trivial_fiber_bundle.quotient_map_proj [nonempty F] {Z : Type*}
-  [topological_space Z] {proj : Z → B} (h : is_homeomorphic_trivial_fiber_bundle F proj) :
-  quotient_map proj :=
-h.is_open_map_proj.to_quotient_map h.continuous_proj h.surjective_proj
-
-variables (F)
-
-/-- The first projection in a product is a trivial fiber bundle. -/
-lemma is_homeomorphic_trivial_fiber_bundle_fst :
-  is_homeomorphic_trivial_fiber_bundle F (prod.fst : B × F → B) :=
-⟨homeomorph.refl _, λ x, rfl⟩
-
-/-- The second projection in a product is a trivial fiber bundle. -/
-lemma is_homeomorphic_trivial_fiber_bundle_snd :
-  is_homeomorphic_trivial_fiber_bundle F (prod.snd : F × B → B) :=
-⟨homeomorph.prod_comm _ _, λ x, rfl⟩
+variables (F E)
 
 /-- If `E` is a fiber bundle over a conditionally complete linear order,
 then it is trivial over any closed interval. -/
@@ -373,20 +309,7 @@ end
 
 end fiber_bundle
 
-/-! ### Constructing fiber bundles -/
-
-namespace bundle
-
-attribute [mfld_simps] total_space.proj total_space_mk coe_fst coe_snd coe_snd_map_apply
-  coe_snd_map_smul total_space.mk_cast
-
-instance [I : topological_space F] : ∀ x : B, topological_space (trivial B F x) := λ x, I
-
-instance [t₁ : topological_space B] [t₂ : topological_space F] :
-  topological_space (total_space (trivial B F)) :=
-induced total_space.proj t₁ ⊓ induced (trivial.proj_snd B F) t₂
-
-end bundle
+/-! ### Core construction for constructing fiber bundles -/
 
 /-- Core data defining a locally trivial bundle with fiber `F` over a topological
 space `B`. Note that "bundle" is used in its mathematical sense. This is the (computer science)
@@ -737,6 +660,8 @@ lemma is_open_map_proj : is_open_map Z.proj := is_open_map_proj F Z.fiber
 
 end fiber_bundle_core
 
+/-! ### Prebundle construction for constructing fiber bundles -/
+
 variables (F) (E : B → Type*) [topological_space B] [topological_space F]
 
 /-- This structure permits to define a fiber bundle when trivializations are given as local