chore: move Pretrivialization, Trivialization to the Bundle namespace (#31338)

As suggested in #30083.

Author: grunweg

Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean

@@ -197,7 +197,7 @@ theorem UniqueMDiffOn.bundle_preimage (hs : UniqueMDiffOn I s) :
 -- TODO: move me to `Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean`
 variable [∀ b, AddCommMonoid (Z b)] [∀ b, Module 𝕜 (Z b)] [VectorBundle 𝕜 F Z]
 
-theorem Trivialization.mdifferentiable [ContMDiffVectorBundle 1 F Z I]
+theorem Bundle.Trivialization.mdifferentiable [ContMDiffVectorBundle 1 F Z I]
     (e : Trivialization F (π F Z)) [MemTrivializationAtlas e] :
     e.MDifferentiable (I.prod 𝓘(𝕜, F)) (I.prod 𝓘(𝕜, F)) :=
   ⟨e.contMDiffOn.mdifferentiableOn one_ne_zero, e.contMDiffOn_symm.mdifferentiableOn one_ne_zero⟩

Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

@@ -383,7 +383,7 @@ protected theorem ContMDiff.coordChange (hf : ContMDiff IM IB n f)
 variable (e e')
 
 variable (IB) in
-theorem Trivialization.contMDiffOn_symm_trans :
+theorem Bundle.Trivialization.contMDiffOn_symm_trans :
     ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n
       (e.toOpenPartialHomeomorph.symm ≫ₕ e'.toOpenPartialHomeomorph) (e.target ∩ e'.target) := by
   have Hmaps : MapsTo Prod.fst (e.target ∩ e'.target) (e.baseSet ∩ e'.baseSet) := fun x hx ↦
@@ -411,7 +411,7 @@ theorem ContMDiffWithinAt.change_section_trivialization {f : M → TotalSpace F
     rw [Function.comp_apply, e.coordChange_apply_snd _ hy]
   · rw [Function.comp_apply, e.coordChange_apply_snd _ he]
 
-theorem Trivialization.contMDiffWithinAt_snd_comp_iff₂ {f : M → TotalSpace F E}
+theorem Bundle.Trivialization.contMDiffWithinAt_snd_comp_iff₂ {f : M → TotalSpace F E}
     (hp : ContMDiffWithinAt IM IB n (π F E ∘ f) s x)
     (he : f x ∈ e.source) (he' : f x ∈ e'.source) :
     ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y ↦ (e (f y)).2) s x ↔
@@ -462,41 +462,43 @@ section
 variable {F E}
 variable {e e' : Trivialization F (π F E)} [MemTrivializationAtlas e] [MemTrivializationAtlas e']
 
-theorem Trivialization.contMDiffWithinAt_iff {f : M → TotalSpace F E} {s : Set M} {x₀ : M}
+namespace Bundle.Trivialization
+
+theorem contMDiffWithinAt_iff {f : M → TotalSpace F E} {s : Set M} {x₀ : M}
     (he : f x₀ ∈ e.source) :
     ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x₀ ↔
       ContMDiffWithinAt IM IB n (fun x => (f x).proj) s x₀ ∧
       ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) s x₀ :=
   contMDiffWithinAt_totalSpace.trans <| and_congr_right fun h ↦
     Trivialization.contMDiffWithinAt_snd_comp_iff₂ h FiberBundle.mem_trivializationAt_proj_source he
 
-theorem Trivialization.contMDiffAt_iff {f : M → TotalSpace F E} {x₀ : M} (he : f x₀ ∈ e.source) :
+theorem contMDiffAt_iff {f : M → TotalSpace F E} {x₀ : M} (he : f x₀ ∈ e.source) :
     ContMDiffAt IM (IB.prod 𝓘(𝕜, F)) n f x₀ ↔
       ContMDiffAt IM IB n (fun x => (f x).proj) x₀ ∧
       ContMDiffAt IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) x₀ :=
   e.contMDiffWithinAt_iff he
 
-theorem Trivialization.contMDiffOn_iff {f : M → TotalSpace F E} {s : Set M}
+theorem contMDiffOn_iff {f : M → TotalSpace F E} {s : Set M}
     (he : MapsTo f s e.source) :
     ContMDiffOn IM (IB.prod 𝓘(𝕜, F)) n f s ↔
       ContMDiffOn IM IB n (fun x => (f x).proj) s ∧
       ContMDiffOn IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) s := by
   simp only [ContMDiffOn, ← forall_and]
   exact forall₂_congr fun x hx ↦ e.contMDiffWithinAt_iff (he hx)
 
-theorem Trivialization.contMDiff_iff {f : M → TotalSpace F E} (he : ∀ x, f x ∈ e.source) :
+theorem contMDiff_iff {f : M → TotalSpace F E} (he : ∀ x, f x ∈ e.source) :
     ContMDiff IM (IB.prod 𝓘(𝕜, F)) n f ↔
       ContMDiff IM IB n (fun x => (f x).proj) ∧
       ContMDiff IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) :=
   (forall_congr' fun x ↦ e.contMDiffAt_iff (he x)).trans forall_and
 
-theorem Trivialization.contMDiffOn (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
+theorem contMDiffOn (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
     ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n e e.source := by
   have : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id e.source := contMDiffOn_id
   rw [e.contMDiffOn_iff (mapsTo_id _)] at this
   exact (this.1.prodMk this.2).congr fun x hx ↦ (e.mk_proj_snd hx).symm
 
-theorem Trivialization.contMDiffOn_symm (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
+theorem contMDiffOn_symm (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
     ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n e.toOpenPartialHomeomorph.symm e.target := by
   rw [e.contMDiffOn_iff e.toOpenPartialHomeomorph.symm_mapsTo]
   refine ⟨contMDiffOn_fst.congr fun x hx ↦ e.proj_symm_apply hx,
@@ -505,7 +507,7 @@ theorem Trivialization.contMDiffOn_symm (e : Trivialization F (π F E)) [MemTriv
 
 /-- Smoothness of a `C^n` section at `x₀` within a set `a` can be determined
 using any trivialisation whose `baseSet` contains `x₀`. -/
-theorem Trivialization.contMDiffWithinAt_section {s : ∀ x, E x} (a : Set B) {x₀ : B}
+theorem contMDiffWithinAt_section {s : ∀ x, E x} (a : Set B) {x₀ : B}
     {e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B)}
     [MemTrivializationAtlas e] (hx₀ : x₀ ∈ e.baseSet) :
     ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a x₀ ↔
@@ -517,7 +519,7 @@ theorem Trivialization.contMDiffWithinAt_section {s : ∀ x, E x} (a : Set B) {x
 
 /-- Smoothness of a `C^n` section at `x₀` can be determined
 using any trivialisation whose `baseSet` contains `x₀`. -/
-theorem Trivialization.contMDiffAt_section_iff {s : ∀ x, E x} {x₀ : B}
+theorem contMDiffAt_section_iff {s : ∀ x, E x} {x₀ : B}
     (e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B))
     [MemTrivializationAtlas e] (hx₀ : x₀ ∈ e.baseSet) :
     ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) x₀ ↔
@@ -530,7 +532,7 @@ alias contMDiffAt_section_of_mem_baseSet := Trivialization.contMDiffAt_section_i
 
 /-- Smoothness of a `C^n` section on `s` can be determined
 using any trivialisation whose `baseSet` contains `s`. -/
-theorem Trivialization.contMDiffOn_section_iff {s : ∀ x, E x} {a : Set B}
+theorem contMDiffOn_section_iff {s : ∀ x, E x} {a : Set B}
     (e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B))
     [MemTrivializationAtlas e] (ha : IsOpen a) (ha' : a ⊆ e.baseSet) :
     ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a ↔
@@ -545,7 +547,7 @@ alias contMDiffOn_section_of_mem_baseSet := Trivialization.contMDiffOn_section_i
 
 /-- For any trivialization `e`, the smoothness of a `C^n` section on `e.baseSet`
 can be determined using `e`. -/
-theorem Trivialization.contMDiffOn_section_baseSet_iff {s : ∀ x, E x}
+theorem contMDiffOn_section_baseSet_iff {s : ∀ x, E x}
     (e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B))
     [MemTrivializationAtlas e] :
     ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) e.baseSet ↔
@@ -555,6 +557,8 @@ theorem Trivialization.contMDiffOn_section_baseSet_iff {s : ∀ x, E x}
 @[deprecated (since := "2025-09-15")]
 alias contMDiffOn_section_of_mem_baseSet₀ := Trivialization.contMDiffOn_section_baseSet_iff
 
+end Bundle.Trivialization
+
 end
 
 /-! ### Core construction for `C^n` vector bundles -/

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

@@ -64,7 +64,7 @@ Suppose `{sᵢ}` is a local frame on `U`, and `hs : IsLocalFrameOn s U`.
 
 In the following lemmas, let `e` be a compatible local trivialisation of `V`, and `b` a basis of
 the model fiber `F`.
-* `Trivialization.basisAt e b`: for each `x ∈ e.baseSet`,
+* `Bundle.Trivialization.basisAt e b`: for each `x ∈ e.baseSet`,
   return the basis of `V x` induced by `e` and `b`
 * `e.localFrame b`: the local frame on `V` induced by `e` and `b`.
   Use `e.localFrame b i` to access the i-th section in that frame.
@@ -325,7 +325,7 @@ end IsLocalFrameOn
 
 end IsLocalFrame
 
-namespace Trivialization
+namespace Bundle.Trivialization
 
 variable [VectorBundle 𝕜 F V] [ContMDiffVectorBundle n F V I] {ι : Type*} {x : M}
   (e : Trivialization F (TotalSpace.proj : TotalSpace F V → M)) [MemTrivializationAtlas e]
@@ -436,7 +436,7 @@ lemma localFrame_coeff_eq_coeff (hxe : x ∈ e.baseSet) {i : ι} :
     e.localFrame_coeff I b i x (s x) = b.repr (e ((T% s) x)).2 i := by
   simp [e.localFrame_coeff_apply_of_mem_baseSet b hxe, basisAt]
 
-end Trivialization
+end Bundle.Trivialization
 
 /-! # Determining smoothness of a section via its local frame coefficients
 We show that for finite rank bundles over a complete field, a section is smooth iff its coefficients

Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

@@ -226,7 +226,9 @@ lemma MDifferentiableWithinAt.change_section_trivialization
     rw [Function.comp_apply, e.coordChange_apply_snd e' hy]
   · rw [Function.comp_apply, e.coordChange_apply_snd _ he]
 
-theorem Trivialization.mdifferentiableWithinAt_snd_comp_iff₂
+namespace Bundle.Trivialization
+
+theorem mdifferentiableWithinAt_snd_comp_iff₂
     {e e' : Trivialization F TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e']
     {f : M → TotalSpace F E} {s : Set M} {x₀ : M}
     (hex₀ : f x₀ ∈ e.source) (he'x₀ : f x₀ ∈ e'.source)
@@ -238,7 +240,7 @@ theorem Trivialization.mdifferentiableWithinAt_snd_comp_iff₂
 
 variable (e e')
 
-theorem Trivialization.mdifferentiableAt_snd_comp_iff₂
+theorem mdifferentiableAt_snd_comp_iff₂
     {e e' : Trivialization F TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e']
     {f : M → TotalSpace F E} {x₀ : M}
     (he : f x₀ ∈ e.source) (he' : f x₀ ∈ e'.source)
@@ -250,7 +252,7 @@ theorem Trivialization.mdifferentiableAt_snd_comp_iff₂
 
 /-- Characterization of differentiable functions into a vector bundle in terms
 of any trivialization. Version at a point within a set. -/
-theorem Trivialization.mdifferentiableWithinAt_totalSpace_iff
+theorem mdifferentiableWithinAt_totalSpace_iff
     (e : Trivialization F (TotalSpace.proj : TotalSpace F E → B)) [MemTrivializationAtlas e]
     (f : M → TotalSpace F E) {s : Set M} {x₀ : M}
     (he : f x₀ ∈ e.source) :
@@ -266,7 +268,7 @@ theorem Trivialization.mdifferentiableWithinAt_totalSpace_iff
 
 /-- Characterization of differentiable functions into a vector bundle in terms
 of any trivialization. Version at a point. -/
-theorem Trivialization.mdifferentiableAt_totalSpace_iff
+theorem mdifferentiableAt_totalSpace_iff
     (e : Trivialization F (TotalSpace.proj : TotalSpace F E → B)) [MemTrivializationAtlas e]
     (f : M → TotalSpace F E) {x₀ : M}
     (he : f x₀ ∈ e.source) :
@@ -282,7 +284,7 @@ theorem Trivialization.mdifferentiableAt_totalSpace_iff
 
 /-- Characterization of differentiable functions into a vector bundle in terms
 of any trivialization. Version at a point within a set. -/
-theorem Trivialization.mdifferentiableWithinAt_section_iff
+theorem mdifferentiableWithinAt_section_iff
     (e : Trivialization F (TotalSpace.proj : TotalSpace F E → B)) [MemTrivializationAtlas e]
     (s : Π b : B, E b) {u : Set B} {b₀ : B}
     (hex₀ : b₀ ∈ e.baseSet) :
@@ -295,7 +297,7 @@ theorem Trivialization.mdifferentiableWithinAt_section_iff
 
 /-- Characterization of differentiable functions into a vector bundle in terms
 of any trivialization. Version at a point. -/
-theorem Trivialization.mdifferentiableAt_section_iff
+theorem mdifferentiableAt_section_iff
     (e : Trivialization F (TotalSpace.proj : TotalSpace F E → B)) [MemTrivializationAtlas e]
     (s : Π b : B, E b) {b₀ : B}
     (hex₀ : b₀ ∈ e.baseSet) :
@@ -306,7 +308,7 @@ theorem Trivialization.mdifferentiableAt_section_iff
 variable {IB} in
 /-- Differentiability of a section on `s` can be determined
 using any trivialisation whose `baseSet` contains `s`. -/
-theorem Trivialization.mdifferentiableOn_section_iff {s : ∀ x, E x} {a : Set B}
+theorem mdifferentiableOn_section_iff {s : ∀ x, E x} {a : Set B}
     (e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B))
     [MemTrivializationAtlas e] (ha : IsOpen a) (ha' : a ⊆ e.baseSet) :
     MDifferentiableOn IB (IB.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) a ↔
@@ -319,13 +321,15 @@ theorem Trivialization.mdifferentiableOn_section_iff {s : ∀ x, E x} {a : Set B
 variable {IB} in
 /-- For any trivialization `e`, the differentiability of a section on `e.baseSet`
 can be determined using `e`. -/
-theorem Trivialization.mdifferentiableOn_section_baseSet_iff {s : ∀ x, E x}
+theorem mdifferentiableOn_section_baseSet_iff {s : ∀ x, E x}
     (e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B))
     [MemTrivializationAtlas e] :
     MDifferentiableOn IB (IB.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) e.baseSet ↔
       MDifferentiableOn IB 𝓘(𝕜, F) (fun x ↦ (e ⟨x, s x⟩).2) e.baseSet :=
   e.mdifferentiableOn_section_iff e.open_baseSet subset_rfl
 
+end Bundle.Trivialization
+
 end
 
 section operations

Mathlib/Topology/Covering/Basic.lean

@@ -434,7 +434,7 @@ that covers `f⁻¹(V)` such that for every `i`,
  2. `V` is contained in the image `f(Uᵢ)`,
  3. the open sets in `V` are determined by their preimages in `Uᵢ`.
 
-Then `f` admits a `Trivialization` over the base set `V`. -/
+Then `f` admits a `Bundle.Trivialization` over the base set `V`. -/
 @[simps source target baseSet] noncomputable def IsOpen.trivializationDiscrete [Nonempty (X → E)]
     {ι} [Nonempty ι] [TopologicalSpace ι] [DiscreteTopology ι] (U : ι → Set E) (V : Set X)
     (open_V : IsOpen V) (open_iff : ∀ i {W}, W ⊆ V → (IsOpen W ↔ IsOpen (f ⁻¹' W ∩ U i)))

Mathlib/Topology/Covering/Quotient.lean

@@ -76,17 +76,19 @@ include hf
 
 section MulAction
 
+open Bundle
+
 variable [ContinuousConstSMul G E]
 variable (hfG : ∀ {e₁ e₂}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂)
 include hfG
 
 /-- If a group `G` acts on a space `E` and `U` is an open subset disjoint from all other
 `G`-translates of itself, and `p` is a quotient map by this action, then `p` admits a
-`Trivialization` over the base set `p(U)`. -/
+`Bundle.Trivialization` over the base set `p(U)`. -/
 @[to_additive (attr := simps! source target baseSet)
 /-- If a group `G` acts on a space `E` and `U` is an open subset disjoint from all
 other `G`-translates of itself, and `p` is a quotient map by this action, then `p` admits a
-`Trivialization` over the base set `p(U)`. -/]
+`Bundle.Trivialization` over the base set `p(U)`. -/]
 noncomputable def trivializationOfSMulDisjoint [TopologicalSpace G] [DiscreteTopology G]
     (U : Set E) (open_U : IsOpen U) (disjoint : ∀ g : G, ((g • ·) '' U ∩ U).Nonempty → g = 1) :
     Trivialization G f := by

Mathlib/Topology/FiberBundle/Constructions.lean

@@ -122,7 +122,7 @@ variable [TopologicalSpace B] (F₁ : Type*) [TopologicalSpace F₁] (E₁ : B 
   [TopologicalSpace (TotalSpace F₁ E₁)] (F₂ : Type*) [TopologicalSpace F₂] (E₂ : B → Type*)
   [TopologicalSpace (TotalSpace F₂ E₂)]
 
-namespace Trivialization
+namespace Bundle.Trivialization
 
 variable {F₁ E₁ F₂ E₂}
 variable (e₁ : Trivialization F₁ (π F₁ E₁)) (e₂ : Trivialization F₂ (π F₂ E₂))
@@ -217,9 +217,9 @@ noncomputable def prod : Trivialization (F₁ × F₂) (π (F₁ × F₂) (E₁
 theorem prod_symm_apply (x : B) (w₁ : F₁) (w₂ : F₂) :
     (prod e₁ e₂).toPartialEquiv.symm (x, w₁, w₂) = ⟨x, e₁.symm x w₁, e₂.symm x w₂⟩ := rfl
 
-end Trivialization
+end Bundle.Trivialization
 
-open Trivialization
+open Bundle Trivialization
 
 variable [∀ x, Zero (E₁ x)] [∀ x, Zero (E₂ x)] [∀ x : B, TopologicalSpace (E₁ x)]
   [∀ x : B, TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂]
@@ -248,6 +248,8 @@ end Prod
 
 /-! ### Pullbacks of fiber bundles -/
 
+open Bundle
+
 section
 
 universe u v w₁ w₂ U
@@ -299,7 +301,7 @@ variable [∀ _b, Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass
 
 /-- A fiber bundle trivialization can be pulled back to a trivialization on the pullback bundle. -/
 @[simps]
-noncomputable def Trivialization.pullback (e : Trivialization F (π F E)) (f : K) :
+noncomputable def Bundle.Trivialization.pullback (e : Trivialization F (π F E)) (f : K) :
     Trivialization F (π F ((f : B' → B) *ᵖ E)) where
   toFun z := (z.proj, (e (Pullback.lift f z)).2)
   invFun y := @TotalSpace.mk _ F (f *ᵖ E) y.1 (e.symm (f y.1) y.2)