Bundle #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. Basic data structure to implement fiber bundles, vector bundles (maybe fibrations?), etc. This file should contain all possible results that do not involve any topology.
We represent a bundle E
over a base space B
as a dependent type E : B → Type*
.
We provide a type synonym of Σ x, E x
as bundle.total_space E
, to be able to endow it with
a topology which is not the disjoint union topology sigma.topological_space
. In general, the
constructions of fiber bundles we will make will be of this form.
Main Definitions #
bundle.total_space
the total space of a bundle.bundle.total_space.proj
the projection from the total space to the base space.bundle.total_space_mk
the constructor for the total space.
References #
- https://en.wikipedia.org/wiki/Bundle_(mathematics)
bundle.total_space E
is the total space of the bundle Σ x, E x
.
This type synonym is used to avoid conflicts with general sigma types.
Equations
- bundle.total_space E = Σ (x : B), E x
Instances for bundle.total_space
- bundle.total_space.inhabited
- bundle.total_space.has_coe_t
- fiber_bundle_core.to_topological_space
- bundle.trivial.bundle.total_space.topological_space
- fiber_bundle.prod.topological_space
- pullback.total_space.topological_space
- vector_bundle_core.to_topological_space
- fiber_bundle.charted_space
- fiber_bundle.charted_space'
- smooth_fiberwise_linear.has_groupoid
- bundle.total_space.smooth_manifold_with_corners
- tangent_bundle.topological_space
- bundle.continuous_linear_map.topological_space_total_space
Equations
- bundle.total_space.inhabited E = {default := ⟨inhabited.default _inst_1, inhabited.default _inst_2⟩}
bundle.total_space.proj
is the canonical projection bundle.total_space E → B
from the
total space to the base space.
Equations
Constructor for the total space of a bundle.
Equations
- bundle.total_space_mk b a = ⟨b, a⟩
Equations
bundle.trivial B F
is the trivial bundle over B
of fiber F
.
Equations
- bundle.trivial B F = function.const B F
Equations
- bundle.trivial.inhabited = {default := inhabited.default _inst_1}
The trivial bundle, unlike other bundles, has a canonical projection on the fiber.
Equations
Natural embedding of the total space of f *ᵖ E
into B' × total_space E
.
Equations
- bundle.pullback_total_space_embedding f = λ (z : bundle.total_space (f *ᵖ E)), (z.proj, bundle.total_space_mk (f z.proj) z.snd)
The base map f : B' → B
lifts to a canonical map on the total spaces.
Equations
- bundle.pullback.lift f = λ (z : bundle.total_space (f *ᵖ E)), bundle.total_space_mk (f z.proj) z.snd
Equations
- bundle.trivial.add_comm_monoid b = _inst_2
Equations
- bundle.trivial.add_comm_group b = _inst_2
Equations
- bundle.trivial.module b = _inst_3