feat(data/bundle): make arguments to proj and total_space_mk implicit (…

…#14359)

I will wait for a later PR to (maybe) fix the reducibility/simp of these declarations.

src/data/bundle.lean

@@ -11,10 +11,19 @@ import algebra.module.basic
 # Bundle
 Basic data structure to implement fiber bundles, vector bundles (maybe fibrations?), etc. This file
 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.
 
+## 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.
+
 ## References
 - https://en.wikipedia.org/wiki/Bundle_(mathematics)
 -/
@@ -24,41 +33,44 @@ namespace bundle
 variables {B : Type*} (E : B → Type*)
 
 /--
-`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 `Σ x, E x`.
+This type synonym is used to avoid conflicts with general sigma types.
 -/
 def total_space := Σ x, E x
 
 instance [inhabited B] [inhabited (E default)] :
   inhabited (total_space E) := ⟨⟨default, default⟩⟩
 
-/-- `bundle.proj E` is the canonical projection `total_space E → B` on the base space. -/
-@[simp, reducible] def proj : total_space E → B := sigma.fst
+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
 
-/-- Constructor for the total space of a `topological_fiber_bundle_core`. -/
-@[simp, reducible] def total_space_mk (E : B → Type*) (b : B) (a : E b) :
+/-- 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} : proj E (total_space_mk E x y) = x :=
+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 E x y :=
+lemma sigma_mk_eq_total_space_mk {x : B} {y : E x} : sigma.mk x y = total_space_mk x y :=
 rfl
 
 lemma total_space.mk_cast {x x' : B} (h : x = x') (b : E x) :
-  total_space_mk E x' (cast (congr_arg E h) b) = total_space_mk E x b :=
+  total_space_mk x' (cast (congr_arg E h) b) = total_space_mk x b :=
 by { subst h, refl }
 
-lemma total_space.eta {B} {E : B → Type*} (z : total_space E) :
-  total_space_mk E (proj E z) z.2 = z :=
+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 E) := ⟨total_space_mk E x⟩
+instance {x : B} : has_coe_t (E x) (total_space E) := ⟨total_space_mk x⟩
 
 @[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 to_total_space_coe {x : B} (v : E x) : (v : total_space E) = total_space_mk E x v := rfl
+lemma to_total_space_coe {x : B} (v : E x) : (v : total_space E) = total_space_mk x v := rfl
 
 -- notation for the direct sum of two bundles over the same base
 notation E₁ `×ᵇ`:100 E₂ := λ x, E₁ x × E₂ x
@@ -84,22 +96,22 @@ notation f ` *ᵖ ` E := pullback f E
 /-- 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, (proj (f *ᵖ E) z, total_space_mk E (f (proj (f *ᵖ E) z)) z.2)
+λ 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 E (f (proj (f *ᵖ E) z)) z.2
+λ z, total_space_mk (f z.proj) z.2
 
 @[simp] lemma pullback.proj_lift (f : B' → B) (x : total_space (f *ᵖ E)) :
-  proj E (pullback.lift E f x) = f x.1 :=
+  (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 E f (total_space_mk (f *ᵖ E) x y) = total_space_mk E (f x) y :=
+  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 E f x).2 = pullback.lift E f x :=
+  (pullback_total_space_embedding f x).2 = pullback.lift f x :=
 rfl
 
 end pullback
@@ -119,7 +131,6 @@ variables (R : Type*) [semiring R] [∀ x, module R (E x)]
 end fiber_structures
 
 section trivial_instances
-local attribute [reducible] bundle.trivial
 
 variables {F : Type*} {R : Type*} [semiring R] (b : B)
 

src/geometry/manifold/cont_mdiff.lean

@@ -1548,7 +1548,7 @@ begin
   { 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 : M), total_space_mk (tangent_space I) x 0) x :=
+  have A : mdifferentiable_at I I.tangent (λ x, @total_space_mk M (tangent_space I) x 0) x :=
     tangent_bundle.smooth_zero_section.mdifferentiable_at,
   have B : fderiv_within 𝕜 (λ (x_1 : E), (x_1, (0 : E))) (set.range ⇑I) (I ((chart_at H x) x)) v
     = (v, 0),

src/topology/fiber_bundle.lean

@@ -150,7 +150,7 @@ Fiber bundle, topological bundle, local trivialization, structure group
 
 variables {ι : Type*} {B : Type*} {F : Type*}
 
-open topological_space filter set
+open topological_space filter set bundle
 open_locale topological_space classical
 
 /-! ### General definition of topological fiber bundles -/
@@ -769,15 +769,14 @@ namespace bundle
 
 variable (E : B → Type*)
 
-attribute [mfld_simps] proj total_space_mk coe_fst coe_snd coe_snd_map_apply coe_snd_map_smul
-  total_space.mk_cast
+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)) :=
-topological_space.induced (proj (trivial B F)) t₁ ⊓
-  topological_space.induced (trivial.proj_snd B F) t₂
+induced total_space.proj t₁ ⊓ induced (trivial.proj_snd B F) t₂
 
 end bundle
 
@@ -836,7 +835,7 @@ different name for typeclass inference. -/
 def total_space := bundle.total_space Z.fiber
 
 /-- The projection from the total space of a topological fiber bundle core, on its base. -/
-@[reducible, simp, mfld_simps] def proj : Z.total_space → B := bundle.proj Z.fiber
+@[reducible, simp, mfld_simps] def proj : Z.total_space → B := bundle.total_space.proj
 
 /-- Local homeomorphism version of the trivialization change. -/
 def triv_change (i j : ι) : local_homeomorph (B × F) (B × F) :=
@@ -929,7 +928,8 @@ begin
   { rintros ⟨x, v⟩ hx,
     simp only [triv_change, local_triv_as_local_equiv, local_equiv.symm, true_and, prod.mk.inj_iff,
       prod_mk_mem_set_prod_eq, local_equiv.trans_source, mem_inter_eq, and_true, mem_preimage, proj,
-      mem_univ, local_equiv.coe_mk, eq_self_iff_true, local_equiv.coe_trans, bundle.proj] at hx ⊢,
+      mem_univ, local_equiv.coe_mk, eq_self_iff_true, local_equiv.coe_trans,
+      total_space.proj] at hx ⊢,
     simp only [Z.coord_change_comp, hx, mem_inter_eq, and_self, mem_base_set_at], }
 end
 
@@ -1071,11 +1071,10 @@ by { rw [local_triv_at, local_triv_apply, coord_change_self], exact Z.mem_base_s
   b ∈ (Z.local_triv_at b).base_set :=
 by { rw [local_triv_at, ←base_set_at], exact Z.mem_base_set_at b, }
 
-open bundle
-
 /-- The inclusion of a fiber into the total space is a continuous map. -/
 @[continuity]
-lemma continuous_total_space_mk (b : B) : continuous (λ a, total_space_mk Z.fiber b a) :=
+lemma continuous_total_space_mk (b : B) :
+  continuous (total_space_mk b : Z.fiber b → bundle.total_space Z.fiber) :=
 begin
   rw [continuous_iff_le_induced, topological_fiber_bundle_core.to_topological_space],
   apply le_induced_generate_from,
@@ -1085,7 +1084,7 @@ begin
   rw [←((Z.local_triv i).source_inter_preimage_target_inter t), preimage_inter, ←preimage_comp,
     trivialization.source_eq],
   apply is_open.inter,
-  { simp only [bundle.proj, proj, ←preimage_comp],
+  { simp only [total_space.proj, proj, ←preimage_comp],
     by_cases (b ∈ (Z.local_triv i).base_set),
     { rw preimage_const_of_mem h, exact is_open_univ, },
     { rw preimage_const_of_not_mem h, exact is_open_empty, }},