# Smooth vector bundles #

This file defines smooth vector bundles over a smooth manifold.

Let E be a topological vector bundle, with model fiber F and base space B. We consider E as carrying a charted space structure given by its trivializations -- these are charts to B × F. Then, by "composition", if B is itself a charted space over H (e.g. a smooth manifold), then E is also a charted space over H × F.

Now, we define SmoothVectorBundle as the Prop of having smooth transition functions. Recall the structure groupoid smoothFiberwiseLinear on B × F consisting of smooth, fiberwise linear partial homeomorphisms. We show that our definition of "smooth vector bundle" implies HasGroupoid for this groupoid, and show (by a "composition" of HasGroupoid instances) that this means that a smooth vector bundle is a smooth manifold.

Since SmoothVectorBundle is a mixin, it should be easy to make variants and for many such variants to coexist -- vector bundles can be smooth vector bundles over several different base fields, they can also be C^k vector bundles, etc.

## Main definitions and constructions #

• FiberBundle.chartedSpace: A fiber bundle E over a base B with model fiber F is naturally a charted space modelled on B × F.

• FiberBundle.chartedSpace': Let B be a charted space modelled on HB. Then a fiber bundle E over a base B with model fiber F is naturally a charted space modelled on HB.prod F.

• SmoothVectorBundle: Mixin class stating that a (topological) VectorBundle is smooth, in the sense of having smooth transition functions.

• SmoothFiberwiseLinear.hasGroupoid: For a smooth vector bundle E over B with fiber modelled on F, the change-of-co-ordinates between two trivializations e, e' for E, considered as charts to B × F, is smooth and fiberwise linear, in the sense of belonging to the structure groupoid smoothFiberwiseLinear.

• Bundle.TotalSpace.smoothManifoldWithCorners: A smooth vector bundle is naturally a smooth manifold.

• VectorBundleCore.smoothVectorBundle: If a (topological) VectorBundleCore is smooth, in the sense of having smooth transition functions (cf. VectorBundleCore.IsSmooth), then the vector bundle constructed from it is a smooth vector bundle.

• VectorPrebundle.smoothVectorBundle: If a VectorPrebundle is smooth, in the sense of having smooth transition functions (cf. VectorPrebundle.IsSmooth), then the vector bundle constructed from it is a smooth vector bundle.

• Bundle.Prod.smoothVectorBundle: The direct sum of two smooth vector bundles is a smooth vector bundle.

### Charted space structure on a fiber bundle #

instance FiberBundle.chartedSpace' {B : Type u_2} {F : Type u_4} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] [] [] :
ChartedSpace (B × F) ()

A fiber bundle E over a base B with model fiber F is naturally a charted space modelled on B × F.

Equations
• One or more equations did not get rendered due to their size.
theorem FiberBundle.chartedSpace'_chartAt {B : Type u_2} {F : Type u_4} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] [] [] (x : ) :
chartAt (B × F) x = (trivializationAt F E x.proj).toPartialHomeomorph
instance FiberBundle.chartedSpace {B : Type u_2} {F : Type u_4} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [] [] [ChartedSpace HB B] [] :

Let B be a charted space modelled on HB. Then a fiber bundle E over a base B with model fiber F is naturally a charted space modelled on HB.prod F.

Equations
theorem FiberBundle.chartedSpace_chartAt {B : Type u_2} {F : Type u_4} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [] [] [ChartedSpace HB B] [] (x : ) :
chartAt (ModelProd HB F) x = (trivializationAt F E x.proj).trans ((chartAt HB x.proj).prod )
theorem FiberBundle.chartedSpace_chartAt_symm_fst {B : Type u_2} {F : Type u_4} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [] [] [ChartedSpace HB B] [] (x : ) (y : ModelProd HB F) (hy : y (chartAt (ModelProd HB F) x).target) :
((chartAt (ModelProd HB F) x).symm y).proj = (chartAt HB x.proj).symm y.1
theorem FiberBundle.extChartAt {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [] (x : ) :
extChartAt (IB.prod ()) x = (trivializationAt F E x.proj).trans ((extChartAt IB x.proj).prod )
theorem FiberBundle.extChartAt_target {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [] (x : ) :
(extChartAt (IB.prod ()) x).target = ((extChartAt IB x.proj).target (extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ Set.univ
theorem FiberBundle.writtenInExtChartAt_trivializationAt {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [] {x : } {y : EB × F} (hy : y (extChartAt (IB.prod ()) x).target) :
writtenInExtChartAt (IB.prod ()) (IB.prod ()) x ((trivializationAt F E x.proj)) y = y
theorem FiberBundle.writtenInExtChartAt_trivializationAt_symm {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [] {x : } {y : EB × F} (hy : y (extChartAt (IB.prod ()) x).target) :
writtenInExtChartAt (IB.prod ()) (IB.prod ()) ((trivializationAt F E x.proj) x) ((trivializationAt F E x.proj).symm) y = y

### Smoothness of maps in/out fiber bundles #

Note: For these results we don't need that the bundle is a smooth vector bundle, or even a vector bundle at all, just that it is a fiber bundle over a charted base space.

theorem Bundle.contMDiffWithinAt_totalSpace {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} {EM : Type u_10} [] [NormedSpace 𝕜 EM] {HM : Type u_11} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [] [ChartedSpace HB B] [] (f : M) {s : Set M} {x₀ : M} :
ContMDiffWithinAt IM (IB.prod ()) n f s x₀ ContMDiffWithinAt IM IB n (fun (x : M) => (f x).proj) s x₀ ContMDiffWithinAt IM () n (fun (x : M) => ((trivializationAt F E (f x₀).proj) (f x)).2) s x₀

Characterization of C^n functions into a smooth vector bundle.

theorem Bundle.contMDiffAt_totalSpace {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} {EM : Type u_10} [] [NormedSpace 𝕜 EM] {HM : Type u_11} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [] [ChartedSpace HB B] [] (f : M) (x₀ : M) :
ContMDiffAt IM (IB.prod ()) n f x₀ ContMDiffAt IM IB n (fun (x : M) => (f x).proj) x₀ ContMDiffAt IM () n (fun (x : M) => ((trivializationAt F E (f x₀).proj) (f x)).2) x₀

Characterization of C^n functions into a smooth vector bundle.

theorem Bundle.contMDiffAt_section {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} {n : ℕ∞} [] [ChartedSpace HB B] [] (s : (x : B) → E x) (x₀ : B) :
ContMDiffAt IB (IB.prod ()) n (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) x₀ ContMDiffAt IB () n (fun (x : B) => ((trivializationAt F E x₀) { proj := x, snd := s x }).2) x₀

Characterization of C^n sections of a smooth vector bundle.

theorem Bundle.contMDiff_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : BType u_6) [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} {n : ℕ∞} [] [ChartedSpace HB B] [] :
ContMDiff (IB.prod ()) IB n Bundle.TotalSpace.proj
theorem Bundle.smooth_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : BType u_6) [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] [] :
Smooth (IB.prod ()) IB Bundle.TotalSpace.proj
theorem Bundle.contMDiffOn_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : BType u_6) [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} {n : ℕ∞} [] [ChartedSpace HB B] [] {s : Set ()} :
ContMDiffOn (IB.prod ()) IB n Bundle.TotalSpace.proj s
theorem Bundle.smoothOn_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : BType u_6) [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] [] {s : Set ()} :
SmoothOn (IB.prod ()) IB Bundle.TotalSpace.proj s
theorem Bundle.contMDiffAt_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : BType u_6) [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} {n : ℕ∞} [] [ChartedSpace HB B] [] {p : } :
ContMDiffAt (IB.prod ()) IB n Bundle.TotalSpace.proj p
theorem Bundle.smoothAt_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : BType u_6) [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] [] {p : } :
SmoothAt (IB.prod ()) IB Bundle.TotalSpace.proj p
theorem Bundle.contMDiffWithinAt_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : BType u_6) [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} {n : ℕ∞} [] [ChartedSpace HB B] [] {s : Set ()} {p : } :
ContMDiffWithinAt (IB.prod ()) IB n Bundle.TotalSpace.proj s p
theorem Bundle.smoothWithinAt_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : BType u_6) [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] [] {s : Set ()} {p : } :
SmoothWithinAt (IB.prod ()) IB Bundle.TotalSpace.proj s p
theorem Bundle.smooth_zeroSection (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : BType u_6) [] [] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] [] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] :
Smooth IB (IB.prod ()) ()

### Smooth vector bundles #

class SmoothVectorBundle {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : BType u_6) {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] :

When B is a smooth manifold with corners with respect to a model IB and E is a topological vector bundle over B with fibers isomorphic to F, then SmoothVectorBundle F E IB registers that the bundle is smooth, in the sense of having smooth transition functions. This is a mixin, not carrying any new data.

Instances
theorem SmoothVectorBundle.smoothOn_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [self : ] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) :
SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ()) (e.baseSet e'.baseSet)
theorem smoothOn_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) :
SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ()) (e.baseSet e'.baseSet)
theorem smoothOn_symm_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) :
SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ().symm) (e.baseSet e'.baseSet)
theorem contMDiffOn_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) :
ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ()) (e.baseSet e'.baseSet)
theorem contMDiffOn_symm_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) :
ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ().symm) (e.baseSet e'.baseSet)
theorem contMDiffAt_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {x : B} (h : x e.baseSet) (h' : x e'.baseSet) :
ContMDiffAt IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ()) x
theorem smoothAt_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {x : B} (h : x e.baseSet) (h' : x e'.baseSet) :
SmoothAt IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ()) x
theorem ContMDiffWithinAt.coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {s : Set M} {f : MB} {x : M} (hf : ContMDiffWithinAt IM IB n f s x) (he : f x e.baseSet) (he' : f x e'.baseSet) :
ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (y : M) => (Trivialization.coordChangeL 𝕜 e e' (f y))) s x
theorem ContMDiffAt.coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {f : MB} {x : M} (hf : ContMDiffAt IM IB n f x) (he : f x e.baseSet) (he' : f x e'.baseSet) :
ContMDiffAt IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (y : M) => (Trivialization.coordChangeL 𝕜 e e' (f y))) x
theorem ContMDiffOn.coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {s : Set M} {f : MB} (hf : ContMDiffOn IM IB n f s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) :
ContMDiffOn IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (y : M) => (Trivialization.coordChangeL 𝕜 e e' (f y))) s
theorem ContMDiff.coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {f : MB} (hf : ContMDiff IM IB n f) (he : ∀ (x : M), f x e.baseSet) (he' : ∀ (x : M), f x e'.baseSet) :
ContMDiff IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n fun (y : M) => (Trivialization.coordChangeL 𝕜 e e' (f y))
theorem SmoothWithinAt.coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {s : Set M} {f : MB} {x : M} (hf : SmoothWithinAt IM IB f s x) (he : f x e.baseSet) (he' : f x e'.baseSet) :
SmoothWithinAt IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (y : M) => (Trivialization.coordChangeL 𝕜 e e' (f y))) s x
theorem SmoothAt.coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {f : MB} {x : M} (hf : SmoothAt IM IB f x) (he : f x e.baseSet) (he' : f x e'.baseSet) :
SmoothAt IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (y : M) => (Trivialization.coordChangeL 𝕜 e e' (f y))) x
theorem SmoothOn.coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {s : Set M} {f : MB} (hf : SmoothOn IM IB f s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) :
SmoothOn IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (y : M) => (Trivialization.coordChangeL 𝕜 e e' (f y))) s
theorem Smooth.coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {f : MB} (hf : Smooth IM IB f) (he : ∀ (x : M), f x e.baseSet) (he' : ∀ (x : M), f x e'.baseSet) :
Smooth IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) fun (y : M) => (Trivialization.coordChangeL 𝕜 e e' (f y))
theorem ContMDiffWithinAt.coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {s : Set M} {f : MB} {g : MF} {x : M} (hf : ContMDiffWithinAt IM IB n f s x) (hg : ContMDiffWithinAt IM () n g s x) (he : f x e.baseSet) (he' : f x e'.baseSet) :
ContMDiffWithinAt IM () n (fun (y : M) => e.coordChange e' (f y) (g y)) s x
theorem ContMDiffAt.coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {f : MB} {g : MF} {x : M} (hf : ContMDiffAt IM IB n f x) (hg : ContMDiffAt IM () n g x) (he : f x e.baseSet) (he' : f x e'.baseSet) :
ContMDiffAt IM () n (fun (y : M) => e.coordChange e' (f y) (g y)) x
theorem ContMDiffOn.coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {s : Set M} {f : MB} {g : MF} (hf : ContMDiffOn IM IB n f s) (hg : ContMDiffOn IM () n g s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) :
ContMDiffOn IM () n (fun (y : M) => e.coordChange e' (f y) (g y)) s
theorem ContMDiff.coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {f : MB} {g : MF} (hf : ContMDiff IM IB n f) (hg : ContMDiff IM () n g) (he : ∀ (x : M), f x e.baseSet) (he' : ∀ (x : M), f x e'.baseSet) :
ContMDiff IM () n fun (y : M) => e.coordChange e' (f y) (g y)
theorem SmoothWithinAt.coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {s : Set M} {f : MB} {g : MF} {x : M} (hf : SmoothWithinAt IM IB f s x) (hg : SmoothWithinAt IM () g s x) (he : f x e.baseSet) (he' : f x e'.baseSet) :
SmoothWithinAt IM () (fun (y : M) => e.coordChange e' (f y) (g y)) s x
theorem SmoothAt.coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {f : MB} {g : MF} {x : M} (hf : SmoothAt IM IB f x) (hg : SmoothAt IM () g x) (he : f x e.baseSet) (he' : f x e'.baseSet) :
SmoothAt IM () (fun (y : M) => e.coordChange e' (f y) (g y)) x
theorem SmoothOn.coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {s : Set M} {f : MB} {g : MF} (hf : SmoothOn IM IB f s) (hg : SmoothOn IM () g s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) :
SmoothOn IM () (fun (y : M) => e.coordChange e' (f y) (g y)) s
theorem Smooth.coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {f : MB} {g : MF} (hf : Smooth IM IB f) (hg : Smooth IM () g) (he : ∀ (x : M), f x e.baseSet) (he' : ∀ (x : M), f x e'.baseSet) :
Smooth IM () fun (y : M) => e.coordChange e' (f y) (g y)
theorem Trivialization.contMDiffOn_symm_trans {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) :
ContMDiffOn (IB.prod ()) (IB.prod ()) n ((e.symm.trans e'.toPartialHomeomorph)) (e.target e'.target)
theorem ContMDiffWithinAt.change_section_trivialization {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {s : Set M} {x : M} {f : M} (hp : ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj f) s x) (hf : ContMDiffWithinAt IM () n (fun (y : M) => (e (f y)).2) s x) (he : f x e.source) (he' : f x e'.source) :
ContMDiffWithinAt IM () n (fun (y : M) => (e' (f y)).2) s x
theorem Trivialization.contMDiffWithinAt_snd_comp_iff₂ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} {s : Set M} {x : M} {f : M} (hp : ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj f) s x) (he : f x e.source) (he' : f x e'.source) :
ContMDiffWithinAt IM () n (fun (y : M) => (e (f y)).2) s x ContMDiffWithinAt IM () n (fun (y : M) => (e' (f y)).2) s x
instance SmoothFiberwiseLinear.hasGroupoid {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : BType u_6) {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] :

For a smooth vector bundle E over B with fiber modelled on F, the change-of-co-ordinates between two trivializations e, e' for E, considered as charts to B × F, is smooth and fiberwise linear.

Equations
• =
instance Bundle.TotalSpace.smoothManifoldWithCorners {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : BType u_6) {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] :

A smooth vector bundle E is naturally a smooth manifold.

Equations
• =
theorem Trivialization.contMDiffWithinAt_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {f : M} {s : Set M} {x₀ : M} (he : f x₀ e.source) :
ContMDiffWithinAt IM (IB.prod ()) n f s x₀ ContMDiffWithinAt IM IB n (fun (x : M) => (f x).proj) s x₀ ContMDiffWithinAt IM () n (fun (x : M) => (e (f x)).2) s x₀
theorem Trivialization.contMDiffAt_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {f : M} {x₀ : M} (he : f x₀ e.source) :
ContMDiffAt IM (IB.prod ()) n f x₀ ContMDiffAt IM IB n (fun (x : M) => (f x).proj) x₀ ContMDiffAt IM () n (fun (x : M) => (e (f x)).2) x₀
theorem Trivialization.contMDiffOn_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {f : M} {s : Set M} (he : Set.MapsTo f s e.source) :
ContMDiffOn IM (IB.prod ()) n f s ContMDiffOn IM IB n (fun (x : M) => (f x).proj) s ContMDiffOn IM () n (fun (x : M) => (e (f x)).2) s
theorem Trivialization.contMDiff_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {f : M} (he : ∀ (x : M), f x e.source) :
ContMDiff IM (IB.prod ()) n f (ContMDiff IM IB n fun (x : M) => (f x).proj) ContMDiff IM () n fun (x : M) => (e (f x)).2
theorem Trivialization.smoothWithinAt_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {f : M} {s : Set M} {x₀ : M} (he : f x₀ e.source) :
SmoothWithinAt IM (IB.prod ()) f s x₀ SmoothWithinAt IM IB (fun (x : M) => (f x).proj) s x₀ SmoothWithinAt IM () (fun (x : M) => (e (f x)).2) s x₀
theorem Trivialization.smoothAt_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {f : M} {x₀ : M} (he : f x₀ e.source) :
SmoothAt IM (IB.prod ()) f x₀ SmoothAt IM IB (fun (x : M) => (f x).proj) x₀ SmoothAt IM () (fun (x : M) => (e (f x)).2) x₀
theorem Trivialization.smoothOn_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {f : M} {s : Set M} (he : Set.MapsTo f s e.source) :
SmoothOn IM (IB.prod ()) f s SmoothOn IM IB (fun (x : M) => (f x).proj) s SmoothOn IM () (fun (x : M) => (e (f x)).2) s
theorem Trivialization.smooth_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] {EM : Type u_9} [] [NormedSpace 𝕜 EM] {HM : Type u_10} [] {IM : ModelWithCorners 𝕜 EM HM} [] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] {e : Trivialization F Bundle.TotalSpace.proj} {f : M} (he : ∀ (x : M), f x e.source) :
Smooth IM (IB.prod ()) f (Smooth IM IB fun (x : M) => (f x).proj) Smooth IM () fun (x : M) => (e (f x)).2
theorem Trivialization.smoothOn {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] (e : Trivialization F Bundle.TotalSpace.proj) :
SmoothOn (IB.prod ()) (IB.prod ()) (e) e.source
theorem Trivialization.smoothOn_symm {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [] [(x : B) → TopologicalSpace (E x)] [] [VectorBundle 𝕜 F E] [] (e : Trivialization F Bundle.TotalSpace.proj) :
SmoothOn (IB.prod ()) (IB.prod ()) (e.symm) e.target

### Core construction for smooth vector bundles #

class VectorBundleCore.IsSmooth {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] [] [ChartedSpace HB B] [] {ι : Type u_11} (Z : VectorBundleCore 𝕜 B F ι) (IB : ModelWithCorners 𝕜 EB HB) :

Mixin for a VectorBundleCore stating smoothness (of transition functions).

Instances
theorem VectorBundleCore.IsSmooth.smoothOn_coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] [] [ChartedSpace HB B] [] {ι : Type u_11} {Z : VectorBundleCore 𝕜 B F ι} {IB : ModelWithCorners 𝕜 EB HB} [self : Z.IsSmooth IB] (i : ι) (j : ι) :
SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (Z.coordChange i j) (Z.baseSet i Z.baseSet j)
theorem VectorBundleCore.smoothOn_coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] [] [ChartedSpace HB B] [] {ι : Type u_11} (Z : VectorBundleCore 𝕜 B F ι) (IB : ModelWithCorners 𝕜 EB HB) [h : Z.IsSmooth IB] (i : ι) (j : ι) :
SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (Z.coordChange i j) (Z.baseSet i Z.baseSet j)
instance VectorBundleCore.smoothVectorBundle {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [] {ι : Type u_11} (Z : VectorBundleCore 𝕜 B F ι) [Z.IsSmooth IB] :
SmoothVectorBundle F Z.Fiber IB

If a VectorBundleCore has the IsSmooth mixin, then the vector bundle constructed from it is a smooth vector bundle.

Equations
• =

### The trivial smooth vector bundle #

instance Bundle.Trivial.smoothVectorBundle {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [] :

A trivial vector bundle over a smooth manifold is a smooth vector bundle.

Equations
• =

### Direct sums of smooth vector bundles #

instance Bundle.Prod.smoothVectorBundle {𝕜 : Type u_1} {B : Type u_2} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] (F₁ : Type u_11) [] [NormedSpace 𝕜 F₁] (E₁ : BType u_12) [] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] (F₂ : Type u_13) [] [NormedSpace 𝕜 F₂] (E₂ : BType u_14) [] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₁ E₁] [VectorBundle 𝕜 F₂ E₂] [SmoothVectorBundle F₁ E₁ IB] [SmoothVectorBundle F₂ E₂ IB] :
SmoothVectorBundle (F₁ × F₂) (fun (x : B) => E₁ x × E₂ x) IB

The direct sum of two smooth vector bundles over the same base is a smooth vector bundle.

Equations
• =

### Prebundle construction for smooth vector bundles #

class VectorPrebundle.IsSmooth {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [(x : B) → TopologicalSpace (E x)] (a : ) :

Mixin for a VectorPrebundle stating smoothness of coordinate changes.

• exists_smoothCoordChange : ea.pretrivializationAtlas, e'a.pretrivializationAtlas, ∃ (f : BF →L[𝕜] F), SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) f (e.baseSet e'.baseSet) be.baseSet e'.baseSet, ∀ (v : F), (f b) v = (e' { proj := b, snd := e.symm b v }).2
Instances
theorem VectorPrebundle.IsSmooth.exists_smoothCoordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [(x : B) → TopologicalSpace (E x)] {a : } [self : ] (e : Pretrivialization F Bundle.TotalSpace.proj) :
e a.pretrivializationAtlase'a.pretrivializationAtlas, ∃ (f : BF →L[𝕜] F), SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) f (e.baseSet e'.baseSet) be.baseSet e'.baseSet, ∀ (v : F), (f b) v = (e' { proj := b, snd := e.symm b v }).2
noncomputable def VectorPrebundle.smoothCoordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [(x : B) → TopologicalSpace (E x)] (a : ) [ha : ] {e : Pretrivialization F Bundle.TotalSpace.proj} {e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) (he' : e' a.pretrivializationAtlas) (b : B) :
F →L[𝕜] F

A randomly chosen coordinate change on a SmoothVectorPrebundle, given by the field exists_coordChange. Note that a.smoothCoordChange need not be the same as a.coordChange.

Equations
Instances For
theorem VectorPrebundle.smoothOn_smoothCoordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [(x : B) → TopologicalSpace (E x)] (a : ) [ha : ] {e : Pretrivialization F Bundle.TotalSpace.proj} {e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) (he' : e' a.pretrivializationAtlas) :
SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) () (e.baseSet e'.baseSet)
theorem VectorPrebundle.smoothCoordChange_apply {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [(x : B) → TopologicalSpace (E x)] (a : ) [ha : ] {e : Pretrivialization F Bundle.TotalSpace.proj} {e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) (he' : e' a.pretrivializationAtlas) {b : B} (hb : b e.baseSet e'.baseSet) (v : F) :
(VectorPrebundle.smoothCoordChange IB a he he' b) v = (e' { proj := b, snd := e.symm b v }).2
theorem VectorPrebundle.mk_smoothCoordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] {IB : ModelWithCorners 𝕜 EB HB} [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [(x : B) → TopologicalSpace (E x)] (a : ) [ha : ] {e : Pretrivialization F Bundle.TotalSpace.proj} {e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) (he' : e' a.pretrivializationAtlas) {b : B} (hb : b e.baseSet e'.baseSet) (v : F) :
(b, (VectorPrebundle.smoothCoordChange IB a he he' b) v) = e' { proj := b, snd := e.symm b v }
theorem VectorPrebundle.smoothVectorBundle {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : BType u_6} {EB : Type u_7} [] [NormedSpace 𝕜 EB] {HB : Type u_8} [] (IB : ModelWithCorners 𝕜 EB HB) [] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [] [(x : B) → TopologicalSpace (E x)] (a : ) [ha : ] :

Make a SmoothVectorBundle from a SmoothVectorPrebundle.