refactor: redefine bundle.total_space (#19221)

- Use a custom structure for `bundle.total_space`.
  - Use `bundle.total_space.mk` instead of `bundle.total_space_mk`.
  - Use `bundle.total_space.to_prod` instead of `equiv.sigma_equiv_prod`.
  - Use `bundle.total_space.mk'` (scoped notation) to specify `F`.
  - Rename `bundle.trivial.proj_snd` to
    `bundle.total_space.trivial_snd` to allow dot notation. Should we
    just use `bundle.total_space.snd` since `bundle.trivial` is now
    reducible?
- Add an unused argument to `bundle.total_space`.
- Make `bundle.trivial` and `bundle.continuous_linear_map` reducible.
- Drop instances that are no longer needed.

Author: urkud

src/data/bundle.lean

@@ -15,133 +15,129 @@ should contain all possible results that do not involve any topology.
 
 We represent a bundle `E` over a base space `B` as a dependent type `E : B → Type*`.
 
-We provide a type synonym of `Σ x, E x` as `bundle.total_space E`, to be able to endow it with
-a topology which is not the disjoint union topology `sigma.topological_space`. In general, the
-constructions of fiber bundles we will make will be of this form.
+We define `bundle.total_space F E` to be the type of pairs `⟨b, x⟩`, where `b : B` and `x : E x`.
+This type is isomorphic to `Σ x, E x` and uses an extra argument `F` for reasons explained below. In
+general, the constructions of fiber bundles we will make will be of this form.
 
 ## Main Definitions
 
 * `bundle.total_space` the total space of a bundle.
 * `bundle.total_space.proj` the projection from the total space to the base space.
-* `bundle.total_space_mk` the constructor for the total space.
+* `bundle.total_space.mk` the constructor for the total space.
+
+## Implementation Notes
+
+- We use a custom structure for the total space of a bundle instead of using a type synonym for the
+  canonical disjoint union `Σ x, E x` because the total space usually has a different topology and
+  Lean 4 `simp` fails to apply lemmas about `Σ x, E x` to elements of the total space.
+
+- The definition of `bundle.total_space` has an unused argument `F`. The reason is that in some
+  constructions (e.g., `bundle.continuous_linear_map.vector_bundle`) we need access to the atlas of
+  trivializations of original fiber bundles to construct the topology on the total space of the new
+  fiber bundle.
 
 ## References
 - https://en.wikipedia.org/wiki/Bundle_(mathematics)
 -/
 
 namespace bundle
 
-variables {B : Type*} (E : B → Type*)
+variables {B F : Type*} (E : B → Type*)
 
 /--
-`bundle.total_space E` is the total space of the bundle `Σ x, E x`.
-This type synonym is used to avoid conflicts with general sigma types.
+`bundle.total_space E` is the total space of the bundle. It consists of pairs
+`(proj : B, snd : E proj)`.
 -/
-def total_space := Σ x, E x
+@[ext]
+structure total_space (F : Type*) (E : B → Type*) :=
+(proj : B)
+(snd : E proj)
 
 instance [inhabited B] [inhabited (E default)] :
-  inhabited (total_space E) := ⟨⟨default, default⟩⟩
+  inhabited (total_space F E) := ⟨⟨default, default⟩⟩
 
 variables {E}
 
 /-- `bundle.total_space.proj` is the canonical projection `bundle.total_space E → B` from the
 total space to the base space. -/
-@[simp, reducible] def total_space.proj : total_space E → B := sigma.fst
+add_decl_doc total_space.proj
 
 -- this notation won't be used in the pretty-printer
 localized "notation `π` := @bundle.total_space.proj _" in bundle
 
-/-- Constructor for the total space of a bundle. -/
-@[simp, reducible] def total_space_mk (b : B) (a : E b) :
-  bundle.total_space E := ⟨b, a⟩
-
-lemma total_space.proj_mk {x : B} {y : E x} : (total_space_mk x y).proj = x :=
-rfl
-
-lemma sigma_mk_eq_total_space_mk {x : B} {y : E x} : sigma.mk x y = total_space_mk x y :=
-rfl
+-- TODO: try `abbrev` in Lean 4
+localized "notation `total_space.mk'` F:max := @bundle.total_space.mk _ F _" in bundle
 
 lemma total_space.mk_cast {x x' : B} (h : x = x') (b : E x) :
-  total_space_mk x' (cast (congr_arg E h) b) = total_space_mk x b :=
+  total_space.mk' F x' (cast (congr_arg E h) b) = total_space.mk x b :=
 by { subst h, refl }
 
-lemma total_space.eta (z : total_space E) :
-  total_space_mk z.proj z.2 = z :=
-sigma.eta z
+instance {x : B} : has_coe_t (E x) (total_space F E) := ⟨total_space.mk x⟩
 
-instance {x : B} : has_coe_t (E x) (total_space E) := ⟨total_space_mk x⟩
+@[simp] lemma total_space.coe_proj (x : B) (v : E x) : (v : total_space F E).proj = x := rfl
+@[simp] lemma total_space.coe_snd {x : B} {y : E x} : (y : total_space F E).snd = y := rfl
 
-@[simp] lemma coe_fst (x : B) (v : E x) : (v : total_space E).fst = x := rfl
-@[simp] lemma coe_snd {x : B} {y : E x} : (y : total_space E).snd = y := rfl
+lemma total_space.coe_eq_mk {x : B} (v : E x) : (v : total_space F E) = total_space.mk x v := rfl
 
-lemma to_total_space_coe {x : B} (v : E x) : (v : total_space E) = total_space_mk x v := rfl
+lemma total_space.eta (z : total_space F E) :
+  total_space.mk z.proj z.2 = z :=
+by cases z; refl
 
 -- 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
-
-instance {F : Type*} [inhabited F] {b : B} : inhabited (bundle.trivial B F b) := ⟨(default : F)⟩
+@[reducible, nolint unused_arguments]
+def trivial (B : Type*) (F : Type*) : B → Type* := λ _, F
 
 /-- The trivial bundle, unlike other bundles, has a canonical projection on the fiber. -/
-def trivial.proj_snd (B : Type*) (F : Type*) : total_space (bundle.trivial B F) → F := sigma.snd
+def total_space.trivial_snd (B : Type*) (F : Type*) : total_space F (bundle.trivial B F) → F :=
+total_space.snd
+
+/-- A trivial bundle is equivalent to the product `B × F`. -/
+@[simps { attrs := [`simp, `mfld_simps] }]
+def total_space.to_prod (B F : Type*) : total_space F (λ _ : B, F) ≃ B × F :=
+{ to_fun := λ x, (x.1, x.2),
+  inv_fun := λ x, ⟨x.1, x.2⟩,
+  left_inv := λ ⟨_, _⟩, rfl,
+  right_inv := λ ⟨_, _⟩, rfl }
 
 section pullback
 
 variable {B' : Type*}
 
 /-- The pullback of a bundle `E` over a base `B` under a map `f : B' → B`, denoted by `pullback f E`
 or `f *ᵖ E`,  is the bundle over `B'` whose fiber over `b'` is `E (f b')`. -/
-@[nolint has_nonempty_instance] def pullback (f : B' → B) (E : B → Type*) := λ x, E (f x)
+def pullback (f : B' → B) (E : B → Type*) : B' → Type* := λ x, E (f x)
+
+notation f ` *ᵖ ` E:max := pullback f E
 
-notation f ` *ᵖ ` E := pullback f E
+instance {f : B' → B} {x : B'} [nonempty (E (f x))] : nonempty (f *ᵖ E x) := ‹nonempty (E (f x))›
 
 /-- Natural embedding of the total space of `f *ᵖ E` into `B' × total_space E`. -/
 @[simp] def pullback_total_space_embedding (f : B' → B) :
-  total_space (f *ᵖ E) → B' × total_space E :=
-λ z, (z.proj, total_space_mk (f z.proj) z.2)
+  total_space F (f *ᵖ E) → B' × total_space F E :=
+λ z, (z.proj, total_space.mk (f z.proj) z.2)
 
 /-- The base map `f : B' → B` lifts to a canonical map on the total spaces. -/
-def pullback.lift (f : B' → B) : total_space (f *ᵖ E) → total_space E :=
-λ z, total_space_mk (f z.proj) z.2
+@[simps { attrs := [`simp, `mfld_simps] }]
+def pullback.lift (f : B' → B) : total_space F (f *ᵖ E) → total_space F E :=
+λ z, ⟨f z.proj, z.2⟩
 
-@[simp] lemma pullback.proj_lift (f : B' → B) (x : total_space (f *ᵖ E)) :
-  (pullback.lift f x).proj = f x.1 :=
-rfl
-
-@[simp] lemma pullback.lift_mk (f : B' → B) (x : B') (y : E (f x)) :
-  pullback.lift f (total_space_mk x y) = total_space_mk (f x) y :=
-rfl
-
-lemma pullback_total_space_embedding_snd (f : B' → B) (x : total_space (f *ᵖ E)) :
-  (pullback_total_space_embedding f x).2 = pullback.lift f x :=
+@[simp, mfld_simps] lemma pullback.lift_mk (f : B' → B) (x : B') (y : E (f x)) :
+  pullback.lift f (total_space.mk' F x y) = ⟨f x, y⟩ :=
 rfl
 
 end pullback
 
 section fiber_structures
 
-variable [∀ x, add_comm_monoid (E x)]
-
-@[simp] lemma coe_snd_map_apply (x : B) (v w : E x) :
-  (↑(v + w) : total_space E).snd = (v : total_space E).snd + (w : total_space E).snd := rfl
+@[simp] lemma coe_snd_map_apply [∀ x, has_add (E x)] (x : B) (v w : E x) :
+  (↑(v + w) : total_space F E).snd = (v : total_space F E).snd + (w : total_space F E).snd := rfl
 
-variables (R : Type*) [semiring R] [∀ x, module R (E x)]
-
-@[simp] lemma coe_snd_map_smul (x : B) (r : R) (v : E x) :
-  (↑(r • v) : total_space E).snd = r • (v : total_space E).snd := rfl
+@[simp] lemma coe_snd_map_smul {R} [∀ x, has_smul R (E x)] (x : B) (r : R) (v : E x) :
+  (↑(r • v) : total_space F E).snd = r • (v : total_space F E).snd := rfl
 
 end fiber_structures
 
-section trivial_instances
-
-variables {F : Type*} {R : Type*} [semiring R] (b : B)
-
-instance [add_comm_monoid F] : add_comm_monoid (bundle.trivial B F b) := ‹add_comm_monoid F›
-instance [add_comm_group F] : add_comm_group (bundle.trivial B F b) := ‹add_comm_group F›
-instance [add_comm_monoid F] [module R F] : module R (bundle.trivial B F b) := ‹module R F›
-
-end trivial_instances
-
 end bundle

src/geometry/manifold/cont_mdiff_mfderiv.lean

@@ -248,7 +248,7 @@ space are model spaces in models with corners. The general fact is proved in
 lemma cont_mdiff_on.continuous_on_tangent_map_within_aux
   {f : H → H'} {s : set H}
   (hf : cont_mdiff_on I I' n f s) (hn : 1 ≤ n) (hs : unique_mdiff_on I s) :
-  continuous_on (tangent_map_within I I' f s) (π (tangent_space I) ⁻¹' s) :=
+  continuous_on (tangent_map_within I I' f s) (π E (tangent_space I) ⁻¹' s) :=
 begin
   suffices h : continuous_on (λ (p : H × E), (f p.fst,
     (fderiv_within 𝕜 (written_in_ext_chart_at I I' p.fst f) (I.symm ⁻¹' s ∩ range I)
@@ -258,7 +258,7 @@ begin
     have B := ((tangent_bundle_model_space_homeomorph H' I').symm.continuous.comp_continuous_on h)
       .comp' A,
     have : (univ ∩ ⇑(tangent_bundle_model_space_homeomorph H I) ⁻¹' (prod.fst ⁻¹' s)) =
-      π (tangent_space I) ⁻¹' s,
+      π E (tangent_space I) ⁻¹' s,
       by { ext ⟨x, v⟩, simp only with mfld_simps },
     rw this at B,
     apply B.congr,
@@ -307,7 +307,8 @@ are model spaces in models with corners. The general fact is proved in
 lemma cont_mdiff_on.cont_mdiff_on_tangent_map_within_aux
   {f : H → H'} {s : set H}
   (hf : cont_mdiff_on I I' n f s) (hmn : m + 1 ≤ n) (hs : unique_mdiff_on I s) :
-  cont_mdiff_on I.tangent I'.tangent m (tangent_map_within I I' f s) (π (tangent_space I) ⁻¹' s) :=
+  cont_mdiff_on I.tangent I'.tangent m (tangent_map_within I I' f s)
+    (π E (tangent_space I) ⁻¹' s) :=
 begin
   have m_le_n : m ≤ n,
   { apply le_trans _ hmn,
@@ -324,13 +325,13 @@ begin
   rw cont_mdiff_on_iff,
   refine ⟨hf.continuous_on_tangent_map_within_aux one_le_n hs, λp q, _⟩,
   have A : range I ×ˢ univ ∩
-      ((equiv.sigma_equiv_prod H E).symm ∘ λ (p : E × E), ((I.symm) p.fst, p.snd)) ⁻¹'
-        (π (tangent_space I) ⁻¹' s)
+      ((total_space.to_prod H E).symm ∘ λ (p : E × E), ((I.symm) p.fst, p.snd)) ⁻¹'
+        (π E (tangent_space I) ⁻¹' s)
       = (range I ∩ I.symm ⁻¹' s) ×ˢ univ,
-    by { ext ⟨x, v⟩, simp only with mfld_simps },
+    by { ext ⟨x, v⟩, simp only with mfld_simps, },
   suffices h : cont_diff_on 𝕜 m (((λ (p : H' × E'), (I' p.fst, p.snd)) ∘
-      (equiv.sigma_equiv_prod H' E')) ∘ tangent_map_within I I' f s ∘
-      ((equiv.sigma_equiv_prod H E).symm) ∘ λ (p : E × E), (I.symm p.fst, p.snd))
+      (total_space.to_prod H' E')) ∘ tangent_map_within I I' f s ∘
+      ((total_space.to_prod H E).symm) ∘ λ (p : E × E), (I.symm p.fst, p.snd))
     ((range ⇑I ∩ ⇑(I.symm) ⁻¹' s) ×ˢ univ),
     by simpa [A] using h,
   change cont_diff_on 𝕜 m (λ (p : E × E),
@@ -369,7 +370,7 @@ is `C^m` when `m+1 ≤ n`. -/
 theorem cont_mdiff_on.cont_mdiff_on_tangent_map_within
   (hf : cont_mdiff_on I I' n f s) (hmn : m + 1 ≤ n) (hs : unique_mdiff_on I s) :
   cont_mdiff_on I.tangent I'.tangent m (tangent_map_within I I' f s)
-  (π (tangent_space I) ⁻¹' s) :=
+  (π E (tangent_space I) ⁻¹' s) :=
 begin
   /- The strategy of the proof is to avoid unfolding the definitions, and reduce by functoriality
   to the case of functions on the model spaces, where we have already proved the result.
@@ -407,20 +408,20 @@ begin
   let il := chart_at (model_prod H E) (tangent_map I I l p),
   let ir := chart_at (model_prod H' E') (tangent_map I I' (r ∘ f) p),
   let s' := f ⁻¹' r.source ∩ s ∩ l.source,
-  let s'_lift := π (tangent_space I) ⁻¹' s',
+  let s'_lift := π E (tangent_space I) ⁻¹' s',
   let s'l := l.target ∩ l.symm ⁻¹' s',
-  let s'l_lift := π (tangent_space I) ⁻¹' s'l,
+  let s'l_lift := π E (tangent_space I) ⁻¹' s'l,
   rcases continuous_on_iff'.1 hf'.1 r.source r.open_source with ⟨o, o_open, ho⟩,
   suffices h : cont_mdiff_on I.tangent I'.tangent m (tangent_map_within I I' f s) s'_lift,
-  { refine ⟨π (tangent_space I) ⁻¹' (o ∩ l.source), _, _, _⟩,
-    show is_open (π (tangent_space I) ⁻¹' (o ∩ l.source)), from
+  { refine ⟨π E (tangent_space I) ⁻¹' (o ∩ l.source), _, _, _⟩,
+    show is_open (π E (tangent_space I) ⁻¹' (o ∩ l.source)), from
       (is_open.inter o_open l.open_source).preimage (continuous_proj E _) ,
-    show p ∈ π (tangent_space I) ⁻¹' (o ∩ l.source),
+    show p ∈ π E (tangent_space I) ⁻¹' (o ∩ l.source),
     { simp,
       have : p.proj ∈ f ⁻¹' r.source ∩ s, by simp [hp],
       rw ho at this,
       exact this.1 },
-    { have : π (tangent_space I) ⁻¹' s ∩ π (tangent_space I) ⁻¹' (o ∩ l.source) = s'_lift,
+    { have : π E (tangent_space I) ⁻¹' s ∩ π E (tangent_space I) ⁻¹' (o ∩ l.source) = s'_lift,
       { dsimp only [s'_lift, s'], rw [ho], mfld_set_tac },
       rw this,
       exact h } },
@@ -547,10 +548,10 @@ end
 derivative is continuous there. -/
 theorem cont_mdiff_on.continuous_on_tangent_map_within
   (hf : cont_mdiff_on I I' n f s) (hmn : 1 ≤ n) (hs : unique_mdiff_on I s) :
-  continuous_on (tangent_map_within I I' f s) (π (tangent_space I) ⁻¹' s) :=
+  continuous_on (tangent_map_within I I' f s) (π E (tangent_space I) ⁻¹' s) :=
 begin
   have : cont_mdiff_on I.tangent I'.tangent 0 (tangent_map_within I I' f s)
-         (π (tangent_space I) ⁻¹' s) :=
+         (π E (tangent_space I) ⁻¹' s) :=
     hf.cont_mdiff_on_tangent_map_within hmn hs,
   exact this.continuous_on
 end
@@ -599,15 +600,15 @@ may seem.
 
 TODO define splittings of vector bundles; state this result invariantly. -/
 lemma tangent_map_tangent_bundle_pure (p : tangent_bundle I M) :
-  tangent_map I I.tangent (zero_section (tangent_space I)) p = ⟨⟨p.proj, 0⟩, ⟨p.2, 0⟩⟩ :=
+  tangent_map I I.tangent (zero_section E (tangent_space I)) p = ⟨⟨p.proj, 0⟩, ⟨p.2, 0⟩⟩ :=
 begin
   rcases p with ⟨x, v⟩,
   have N : I.symm ⁻¹' (chart_at H x).target ∈ 𝓝 (I ((chart_at H x) x)),
   { apply is_open.mem_nhds,
     apply (local_homeomorph.open_target _).preimage I.continuous_inv_fun,
     simp only with mfld_simps },
-  have A : mdifferentiable_at I I.tangent (λ x, @total_space_mk M (tangent_space I) x 0) x,
-  { have : smooth I (I.prod 𝓘(𝕜, E)) (zero_section (tangent_space I : M → Type*)) :=
+  have A : mdifferentiable_at I I.tangent (λ x, @total_space.mk M E (tangent_space I) x 0) x,
+  { have : smooth I (I.prod 𝓘(𝕜, E)) (zero_section E (tangent_space I : M → Type*)) :=
     bundle.smooth_zero_section 𝕜 (tangent_space I : M → Type*),
     exact this.mdifferentiable_at },
   have B : fderiv_within 𝕜 (λ (x' : E), (x', (0 : E))) (set.range ⇑I) (I ((chart_at H x) x)) v
@@ -618,12 +619,12 @@ begin
     { exact differentiable_at_const _ },
     { exact model_with_corners.unique_diff_at_image I },
     { exact differentiable_at_id'.prod (differentiable_at_const _) } },
-  simp only [bundle.zero_section, tangent_map, mfderiv, total_space.proj_mk, A,
-    if_pos, chart_at, fiber_bundle.charted_space_chart_at, tangent_bundle.trivialization_at_apply,
+  simp only [bundle.zero_section, tangent_map, mfderiv, A, if_pos, chart_at,
+    fiber_bundle.charted_space_chart_at, tangent_bundle.trivialization_at_apply,
     tangent_bundle_core, function.comp, continuous_linear_map.map_zero] with mfld_simps,
   rw [← fderiv_within_inter N] at B,
   rw [← fderiv_within_inter N, ← B],
-  congr' 2,
+  congr' 1,
   refine fderiv_within_congr (λ y hy, _) _,
   { simp only with mfld_simps at hy,
     simp only [hy, prod.mk.inj_iff] with mfld_simps },