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 bundleE
over a baseB
with model fiberF
is naturally a charted space modelled onB × F
.FiberBundle.chartedSpace'
: LetB
be a charted space modelled onHB
. Then a fiber bundleE
over a baseB
with model fiberF
is naturally a charted space modelled onHB.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 bundleE
overB
with 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)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 aVectorPrebundle
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 #
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.
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)
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.
Characterization of C^n functions into a smooth vector bundle.
Characterization of C^n functions into a smooth vector bundle.
Characterization of C^n sections within a set at a point of a smooth vector bundle.
Characterization of C^n sections of a smooth vector bundle.
Alias of Bundle.contMDiff_proj
.
Alias of Bundle.contMDiffOn_proj
.
Alias of Bundle.contMDiffAt_proj
.
Alias of Bundle.contMDiffWithinAt_proj
.
Alias of Bundle.contMDiff_zeroSection
.
Smooth vector bundles #
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.
- contMDiffOn_coordChangeL : ∀ (e e' : Trivialization F Bundle.TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'], ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) ⊤ (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)
Instances
Alias of contMDiffOn_coordChangeL
.
Alias of contMDiffOn_symm_coordChangeL
.
Alias of contMDiffAt_coordChangeL
.
Alias of ContMDiffWithinAt.coordChangeL
.
Alias of ContMDiffAt.coordChangeL
.
Alias of ContMDiffOn.coordChangeL
.
Alias of ContMDiff.coordChangeL
.
Alias of ContMDiffWithinAt.coordChange
.
Alias of ContMDiffAt.coordChange
.
Alias of ContMDiffOn.coordChange
.
Alias of ContMDiff.coordChange
.
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
- ⋯ = ⋯
A smooth vector bundle E
is naturally a smooth manifold.
Equations
- ⋯ = ⋯
Alias of Trivialization.contMDiffWithinAt_iff
.
Alias of Trivialization.contMDiffAt_iff
.
Alias of Trivialization.contMDiffOn_iff
.
Alias of Trivialization.contMDiff_iff
.
Alias of Trivialization.contMDiffOn
.
Alias of Trivialization.contMDiffOn_symm
.
Core construction for smooth vector bundles #
Mixin for a VectorBundleCore
stating smoothness (of transition functions).
- contMDiffOn_coordChange : ∀ (i j : ι), ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) ⊤ (Z.coordChange i j) (Z.baseSet i ∩ Z.baseSet j)
Instances
Alias of VectorBundleCore.contMDiffOn_coordChange
.
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 #
A trivial vector bundle over a smooth manifold is a smooth vector bundle.
Equations
- ⋯ = ⋯
Direct sums of smooth vector bundles #
The direct sum of two smooth vector bundles over the same base is a smooth vector bundle.
Equations
- ⋯ = ⋯
Prebundle construction for smooth vector bundles #
Mixin for a VectorPrebundle
stating smoothness of coordinate changes.
Instances
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
Make a SmoothVectorBundle
from a SmoothVectorPrebundle
.