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 bundleEover a baseBwith model fiberFis naturally a charted space modelled onB × F.FiberBundle.chartedSpace': LetBbe a charted space modelled onHB. Then a fiber bundleEover a baseBwith model fiberFis naturally a charted space modelled onHB.prod F.SmoothVectorBundle: Mixin class stating that a (topological)VectorBundleis smooth, in the sense of having smooth transition functions.SmoothFiberwiseLinear.hasGroupoid: For a smooth vector bundleEoverBwith fiber modelled onF, the change-of-co-ordinates between two trivializationse,e'forE, considered as charts toB × F, is smooth and fiberwise linear, in the sense of belonging to the structure groupoidsmoothFiberwiseLinear.Bundle.TotalSpace.smoothManifoldWithCorners: A smooth vector bundle is naturally a smooth manifold.VectorBundleCore.smoothVectorBundle: If a (topological)VectorBundleCoreis 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 aVectorPrebundleis 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 = (trivializationAt F E x.proj).trans ((chartAt HB x.proj).prod (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)
:
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 (IB.prod (modelWithCornersSelf 𝕜 F)) x = (trivializationAt F E x.proj).trans ((extChartAt IB x.proj).prod (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 (IB.prod (modelWithCornersSelf 𝕜 F)) 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 : 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 (IB.prod (modelWithCornersSelf 𝕜 F)) x).target)
:
writtenInExtChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (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 (IB.prod (modelWithCornersSelf 𝕜 F)) x).target)
:
writtenInExtChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F))
(↑(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 : 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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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]
:
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)
Instances
theorem
SmoothVectorBundle.smoothOn_coordChangeL
{𝕜 : Type u_1}
{B : Type u_2}
{F : Type u_4}
{E : B → Type u_6}
:
∀ {inst : NontriviallyNormedField 𝕜} {EB : Type u_7} {inst_1 : NormedAddCommGroup EB} {inst_2 : NormedSpace 𝕜 EB}
{HB : Type u_8} {inst_3 : TopologicalSpace HB} {IB : ModelWithCorners 𝕜 EB HB} {inst_4 : TopologicalSpace B}
{inst_5 : ChartedSpace HB B} {inst_6 : (x : B) → AddCommMonoid (E x)} {inst_7 : (x : B) → Module 𝕜 (E x)}
{inst_8 : NormedAddCommGroup F} {inst_9 : NormedSpace 𝕜 F} {inst_10 : TopologicalSpace (Bundle.TotalSpace F E)}
{inst_11 : (x : B) → TopologicalSpace (E x)} {inst_12 : FiberBundle F E} {inst_13 : VectorBundle 𝕜 F E}
[self : SmoothVectorBundle F E IB] (e e' : Trivialization F Bundle.TotalSpace.proj)
[inst_14 : MemTrivializationAtlas e] [inst_15 : 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) => ↑(Trivialization.coordChangeL 𝕜 e e' b).symm)
(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) => ↑(Trivialization.coordChangeL 𝕜 e e' b).symm)
(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) => 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 : 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) => 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 : 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) => 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 : 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) => 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 : 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) => 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 : 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) => 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 : 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) => 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 : 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) => e.coordChange 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 (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) 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 : 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]
[(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 IB B]
:
SmoothManifoldWithCorners (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (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 (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (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 (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) (↑e.symm) 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)
:
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)
Instances
theorem
VectorBundleCore.IsSmooth.smoothOn_coordChange
{𝕜 : Type u_1}
{B : Type u_2}
{F : Type u_4}
:
∀ {inst : NontriviallyNormedField 𝕜} {EB : Type u_7} {inst_1 : NormedAddCommGroup EB} {inst_2 : NormedSpace 𝕜 EB}
{HB : Type u_8} {inst_3 : TopologicalSpace HB} {inst_4 : TopologicalSpace B} {inst_5 : ChartedSpace HB B}
{inst_6 : NormedAddCommGroup F} {inst_7 : NormedSpace 𝕜 F} {ι : 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}
[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 : 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}
[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 ι)
[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)
[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)
:
Mixin for a VectorPrebundle stating smoothness of coordinate changes.
Instances
theorem
VectorPrebundle.IsSmooth.exists_smoothCoordChange
{𝕜 : Type u_1}
{B : Type u_2}
{F : Type u_4}
{E : B → Type u_6}
:
∀ {inst : NontriviallyNormedField 𝕜} {EB : Type u_7} {inst_1 : NormedAddCommGroup EB} {inst_2 : NormedSpace 𝕜 EB}
{HB : Type u_8} {inst_3 : TopologicalSpace HB} {IB : ModelWithCorners 𝕜 EB HB} {inst_4 : TopologicalSpace B}
{inst_5 : ChartedSpace HB B} {inst_6 : (x : B) → AddCommMonoid (E x)} {inst_7 : (x : B) → Module 𝕜 (E x)}
{inst_8 : NormedAddCommGroup F} {inst_9 : NormedSpace 𝕜 F} {inst_10 : (x : B) → TopologicalSpace (E x)}
{a : VectorPrebundle 𝕜 F E} [self : VectorPrebundle.IsSmooth IB a],
∀ 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 := e.symm 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)
:
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
Instances For
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 := e.symm 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 := e.symm 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.