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 : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [TopologicalSpace B] [FiberBundle F E] : ChartedSpace (B × F) (Bundle.TotalSpace F E)

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 : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [TopologicalSpace B] [FiberBundle F E] (x : Bundle.TotalSpace F E) : chartAt (B × F) x = (trivializationAt F E x.proj).toPartialHomeomorph

instance FiberBundle.chartedSpace {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] : ChartedSpace (ModelProd HB F) (Bundle.TotalSpace F E)

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

• FiberBundle.chartedSpace = ChartedSpace.comp (ModelProd HB F) (B × F) (Bundle.TotalSpace F E)

theorem FiberBundle.chartedSpace_chartAt {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (x : Bundle.TotalSpace F E) : chartAt (ModelProd HB F) x = PartialHomeomorph.trans (trivializationAt F E x.proj).toPartialHomeomorph (PartialHomeomorph.prod (chartAt HB x.proj) (PartialHomeomorph.refl F))

theorem FiberBundle.chartedSpace_chartAt_symm_fst {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (x : Bundle.TotalSpace F E) (y : ModelProd HB F) (hy : y ∈ (chartAt (ModelProd HB F) x).target) : (↑(PartialHomeomorph.symm (chartAt (ModelProd HB F) x)) y).proj = ↑(PartialHomeomorph.symm (chartAt HB x.proj)) y.1

theorem FiberBundle.extChartAt {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (x : Bundle.TotalSpace F E) : extChartAt (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) x = PartialEquiv.trans (trivializationAt F E x.proj).toPartialEquiv (PartialEquiv.prod (extChartAt IB x.proj) (PartialEquiv.refl F))

theorem FiberBundle.extChartAt_target {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (x : Bundle.TotalSpace F E) : (extChartAt (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) x).target = ((extChartAt IB x.proj).target ∩ ↑(PartialEquiv.symm (extChartAt IB x.proj)) ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ Set.univ

theorem FiberBundle.writtenInExtChartAt_trivializationAt {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {x : Bundle.TotalSpace F E} {y : EB × F} (hy : y ∈ (extChartAt (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) x).target) : writtenInExtChartAt (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) 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 : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {x : Bundle.TotalSpace F E} {y : EB × F} (hy : y ∈ (extChartAt (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) x).target) : writtenInExtChartAt (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) (↑(trivializationAt F E x.proj) x) (↑(PartialHomeomorph.symm (trivializationAt F E x.proj).toPartialHomeomorph)) 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 : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {EM : Type u_10} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_11} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (f : M → Bundle.TotalSpace F E) {s : Set M} {x₀ : M} : ContMDiffWithinAt IM (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) n f s x₀ ↔ ContMDiffWithinAt IM IB n (fun (x : M) => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) 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 : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {EM : Type u_10} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_11} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (f : M → Bundle.TotalSpace F E) (x₀ : M) : ContMDiffAt IM (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) n f x₀ ↔ ContMDiffAt IM IB n (fun (x : M) => (f x).proj) x₀ ∧ ContMDiffAt IM (modelWithCornersSelf 𝕜 F) 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 : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {n : ℕ∞} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (s : (x : B) → E x) (x₀ : B) : ContMDiffAt IB (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) x₀ ↔ ContMDiffAt IB (modelWithCornersSelf 𝕜 F) 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 : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {n : ℕ∞} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] : ContMDiff (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) IB n Bundle.TotalSpace.proj

theorem Bundle.smooth_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] : Smooth (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) IB Bundle.TotalSpace.proj

theorem Bundle.contMDiffOn_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {n : ℕ∞} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {s : Set (Bundle.TotalSpace F E)} : ContMDiffOn (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) IB n Bundle.TotalSpace.proj s

theorem Bundle.smoothOn_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {s : Set (Bundle.TotalSpace F E)} : SmoothOn (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) IB Bundle.TotalSpace.proj s

theorem Bundle.contMDiffAt_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {n : ℕ∞} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {p : Bundle.TotalSpace F E} : ContMDiffAt (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) IB n Bundle.TotalSpace.proj p

theorem Bundle.smoothAt_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {p : Bundle.TotalSpace F E} : SmoothAt (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) IB Bundle.TotalSpace.proj p

theorem Bundle.contMDiffWithinAt_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {n : ℕ∞} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {s : Set (Bundle.TotalSpace F E)} {p : Bundle.TotalSpace F E} : ContMDiffWithinAt (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) IB n Bundle.TotalSpace.proj s p

theorem Bundle.smoothWithinAt_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {s : Set (Bundle.TotalSpace F E)} {p : Bundle.TotalSpace F E} : SmoothWithinAt (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) IB Bundle.TotalSpace.proj s p

theorem Bundle.smooth_zeroSection (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] : Smooth IB (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) (Bundle.zeroSection F E)

Smooth vector bundles

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

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.

• smoothOn_coordChangeL : ∀ (e e' : Trivialization F Bundle.TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'], SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

theorem smoothOn_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

theorem smoothOn_symm_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 e e' b))) (e.baseSet ∩ e'.baseSet)

theorem contMDiffOn_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

theorem contMDiffOn_symm_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 e e' b))) (e.baseSet ∩ e'.baseSet)

theorem contMDiffAt_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {x : B} (h : x ∈ e.baseSet) (h' : x ∈ e'.baseSet) : ContMDiffAt IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) x

theorem smoothAt_coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {x : B} (h : x ∈ e.baseSet) (h' : x ∈ e'.baseSet) : SmoothAt IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) x

theorem ContMDiffWithinAt.coordChangeL {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} {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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} (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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} (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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} {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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} (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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} (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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {g : M → F} {x : M} (hf : ContMDiffWithinAt IM IB n f s x) (hg : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n g s x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => Trivialization.coordChange e 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} {g : M → F} {x : M} (hf : ContMDiffAt IM IB n f x) (hg : ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n g x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => Trivialization.coordChange e 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {g : M → F} (hf : ContMDiffOn IM IB n f s) (hg : ContMDiffOn IM (modelWithCornersSelf 𝕜 F) n g s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) : ContMDiffOn IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => Trivialization.coordChange e 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} {g : M → F} (hf : ContMDiff IM IB n f) (hg : ContMDiff IM (modelWithCornersSelf 𝕜 F) n g) (he : ∀ (x : M), f x ∈ e.baseSet) (he' : ∀ (x : M), f x ∈ e'.baseSet) : ContMDiff IM (modelWithCornersSelf 𝕜 F) n fun (y : M) => Trivialization.coordChange e e' (f y) (g y)

theorem SmoothWithinAt.coordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {g : M → F} {x : M} (hf : SmoothWithinAt IM IB f s x) (hg : SmoothWithinAt IM (modelWithCornersSelf 𝕜 F) g s x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : SmoothWithinAt IM (modelWithCornersSelf 𝕜 F) (fun (y : M) => Trivialization.coordChange e 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} {g : M → F} {x : M} (hf : SmoothAt IM IB f x) (hg : SmoothAt IM (modelWithCornersSelf 𝕜 F) g x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : SmoothAt IM (modelWithCornersSelf 𝕜 F) (fun (y : M) => Trivialization.coordChange e 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {g : M → F} (hf : SmoothOn IM IB f s) (hg : SmoothOn IM (modelWithCornersSelf 𝕜 F) g s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) : SmoothOn IM (modelWithCornersSelf 𝕜 F) (fun (y : M) => Trivialization.coordChange e 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} {g : M → F} (hf : Smooth IM IB f) (hg : Smooth IM (modelWithCornersSelf 𝕜 F) g) (he : ∀ (x : M), f x ∈ e.baseSet) (he' : ∀ (x : M), f x ∈ e'.baseSet) : Smooth IM (modelWithCornersSelf 𝕜 F) fun (y : M) => Trivialization.coordChange e e' (f y) (g y)

theorem Trivialization.contMDiffOn_symm_trans {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : ContMDiffOn (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) n (↑(PartialHomeomorph.trans (PartialHomeomorph.symm e.toPartialHomeomorph) 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {x : M} {f : M → Bundle.TotalSpace F E} (hp : ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj ∘ f) s x) (hf : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (↑e (f y)).2) s x) (he : f x ∈ e.source) (he' : f x ∈ e'.source) : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {x : M} {f : M → Bundle.TotalSpace F E} (hp : ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj ∘ f) s x) (he : f x ∈ e.source) (he' : f x ∈ e'.source) : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (↑e (f y)).2) s x ↔ ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) 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 : B → Type u_6) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] : HasGroupoid (Bundle.TotalSpace F E) (smoothFiberwiseLinear B F IB)

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 : B → Type u_6) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [SmoothManifoldWithCorners IB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] : SmoothManifoldWithCorners (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) (Bundle.TotalSpace 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} {s : Set M} {x₀ : M} (he : f x₀ ∈ e.source) : ContMDiffWithinAt IM (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) n f s x₀ ↔ ContMDiffWithinAt IM IB n (fun (x : M) => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} {x₀ : M} (he : f x₀ ∈ e.source) : ContMDiffAt IM (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) n f x₀ ↔ ContMDiffAt IM IB n (fun (x : M) => (f x).proj) x₀ ∧ ContMDiffAt IM (modelWithCornersSelf 𝕜 F) 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} {s : Set M} (he : Set.MapsTo f s e.source) : ContMDiffOn IM (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) n f s ↔ ContMDiffOn IM IB n (fun (x : M) => (f x).proj) s ∧ ContMDiffOn IM (modelWithCornersSelf 𝕜 F) 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞} [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} (he : ∀ (x : M), f x ∈ e.source) : ContMDiff IM (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) n f ↔ (ContMDiff IM IB n fun (x : M) => (f x).proj) ∧ ContMDiff IM (modelWithCornersSelf 𝕜 F) 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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} {s : Set M} {x₀ : M} (he : f x₀ ∈ e.source) : SmoothWithinAt IM (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) f s x₀ ↔ SmoothWithinAt IM IB (fun (x : M) => (f x).proj) s x₀ ∧ SmoothWithinAt IM (modelWithCornersSelf 𝕜 F) (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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} {x₀ : M} (he : f x₀ ∈ e.source) : SmoothAt IM (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) f x₀ ↔ SmoothAt IM IB (fun (x : M) => (f x).proj) x₀ ∧ SmoothAt IM (modelWithCornersSelf 𝕜 F) (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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} {s : Set M} (he : Set.MapsTo f s e.source) : SmoothOn IM (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) f s ↔ SmoothOn IM IB (fun (x : M) => (f x).proj) s ∧ SmoothOn IM (modelWithCornersSelf 𝕜 F) (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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} (he : ∀ (x : M), f x ∈ e.source) : Smooth IM (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) f ↔ (Smooth IM IB fun (x : M) => (f x).proj) ∧ Smooth IM (modelWithCornersSelf 𝕜 F) fun (x : M) => (↑e (f x)).2

theorem Trivialization.smoothOn {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] : SmoothOn (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) (↑e) e.source

theorem Trivialization.smoothOn_symm {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [SmoothVectorBundle F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] : SmoothOn (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) (ModelWithCorners.prod IB (modelWithCornersSelf 𝕜 F)) (↑(PartialHomeomorph.symm e.toPartialHomeomorph)) e.target

Core construction for smooth vector bundles

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

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

• smoothOn_coordChange : ∀ (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} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_11} (Z : VectorBundleCore 𝕜 B F ι) (IB : ModelWithCorners 𝕜 EB HB) [h : VectorBundleCore.IsSmooth Z 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} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_11} (Z : VectorBundleCore 𝕜 B F ι) [VectorBundleCore.IsSmooth Z IB] : SmoothVectorBundle F (VectorBundleCore.Fiber Z) 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) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : SmoothVectorBundle F (Bundle.Trivial B F) IB

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} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] (F₁ : Type u_11) [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] (E₁ : B → Type u_12) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] (F₂ : Type u_13) [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] (E₂ : B → Type u_14) [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(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 : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) : Prop

Mixin for a VectorPrebundle stating smoothness of coordinate changes.

• exists_smoothCoordChange : ∀ e ∈ a.pretrivializationAtlas, ∀ e' ∈ a.pretrivializationAtlas, ∃ (f : B → F →L[𝕜] F), SmoothOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) f (e.baseSet ∩ e'.baseSet) ∧ ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' { proj := b, snd := Pretrivialization.symm e b v }).2

noncomputable def VectorPrebundle.smoothCoordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) [ha : VectorPrebundle.IsSmooth IB a] {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

• VectorPrebundle.smoothCoordChange IB a he he' b = Classical.choose ⋯ b

theorem VectorPrebundle.smoothOn_smoothCoordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) [ha : VectorPrebundle.IsSmooth IB a] {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)) (VectorPrebundle.smoothCoordChange IB a he he') (e.baseSet ∩ e'.baseSet)

theorem VectorPrebundle.smoothCoordChange_apply {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) [ha : VectorPrebundle.IsSmooth IB a] {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 := Pretrivialization.symm e b v }).2

theorem VectorPrebundle.mk_smoothCoordChange {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) [ha : VectorPrebundle.IsSmooth IB a] {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 := Pretrivialization.symm e b v }

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

Make a SmoothVectorBundle from a SmoothVectorPrebundle.