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 bundleEover a baseBwith model fiberFis naturally a charted space modelled onB × F. -
fiber_bundle.charted_space': LetBbe a charted space modelled onHB. Then a fiber bundleEover a baseBwith model fiberFis naturally a charted space modelled onHB.prod F. -
smooth_vector_bundle: Mixin class stating that a (topological)vector_bundleis smooth, in the sense of having smooth transition functions. -
smooth_fiberwise_linear.has_groupoid: 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 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_coreis 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.