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 smooth_vector_bundle
as the Prop
of having smooth transition functions.
Recall the structure groupoid smooth_fiberwise_linear
on B × F
consisting of smooth, fiberwise
linear local homeomorphisms. We show that our definition of "smooth vector bundle" implies
has_groupoid
for this groupoid, and show (by a "composition" of has_groupoid
instances) that
this means that a smooth vector bundle is a smooth manifold.
Since smooth_vector_bundle
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 #
-
fiber_bundle.charted_space
: A fiber bundleE
over a baseB
with model fiberF
is naturally a charted space modelled onB × F
. -
fiber_bundle.charted_space'
: 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
. -
smooth_vector_bundle
: Mixin class stating that a (topological)vector_bundle
is smooth, in the sense of having smooth transition functions. -
smooth_fiberwise_linear.has_groupoid
: 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 groupoidsmooth_fiberwise_linear
. -
bundle.total_space.smooth_manifold_with_corners
: A smooth vector bundle is naturally a smooth manifold. -
vector_bundle_core.smooth_vector_bundle
: If a (topological)vector_bundle_core
is smooth, in the sense of having smooth transition functions, then the vector bundle constructed from it is a smooth vector bundle. -
bundle.prod.smooth_vector_bundle
: 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
- fiber_bundle.charted_space = {atlas := (λ (e : trivialization F bundle.total_space.proj), e.to_local_homeomorph) '' fiber_bundle.trivialization_atlas F E, chart_at := λ (x : bundle.total_space E), (fiber_bundle.trivialization_at F E x.proj).to_local_homeomorph, mem_chart_source := _, chart_mem_atlas := _}
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
- fiber_bundle.charted_space' = charted_space.comp (model_prod HB F) (model_prod B F) (bundle.total_space E)
Smooth vector bundles #
- smooth_on_coord_change : ∀ (e e' : trivialization F bundle.total_space.proj) [_inst_16 : mem_trivialization_atlas e] [_inst_17 : mem_trivialization_atlas e'], smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (λ (b : B), ↑(trivialization.coord_changeL 𝕜 e e' b)) (e.base_set ∩ e'.base_set)
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 smooth_vector_bundle 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`.
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.
A smooth vector bundle E
is naturally a smooth manifold.
Core construction for smooth vector bundles #
- smooth_on_coord_change : ∀ (i j : ι), smooth_on IB (model_with_corners_self 𝕜 (F →L[𝕜] F)) (Z.coord_change i j) (Z.base_set i ∩ Z.base_set j)
Mixin for a vector_bundle_core
stating smoothness (of transition functions).
Instances of this typeclass
If a vector_bundle_core
has the is_smooth
mixin, then the vector bundle constructed from it
is a smooth vector bundle.
The trivial smooth vector bundle #
A trivial vector bundle over a smooth manifold is a smooth vector bundle.
Direct sums of smooth vector bundles #
The direct sum of two smooth vector bundles over the same base is a smooth vector bundle.