Bundle #
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
- bundle.total_space.topological_space
- topological_fiber_bundle_core.to_topological_space
- topological_vector_bundle_core.to_topological_space
- basic_smooth_vector_bundle_core.to_charted_space
- basic_smooth_vector_bundle_core.to_smooth_manifold
- tangent_bundle.topological_space
- tangent_bundle.charted_space
- tangent_bundle.smooth_manifold_with_corners
- topological_vector_bundle.bundle.total_space.topological_space
- topological_vector_bundle.prod.topological_space
- pullback.total_space.topological_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
Instances for bundle.trivial
- bundle.trivial.inhabited
- bundle.trivial.add_comm_monoid
- bundle.trivial.add_comm_group
- bundle.trivial.module
- bundle.trivial.topological_space
- topological_vector_bundle.bundle.trivial.add_comm_monoid
- topological_vector_bundle.bundle.trivial.add_comm_group
- topological_vector_bundle.bundle.trivial.module
- topological_vector_bundle.trivial_topological_vector_bundle.topological_vector_bundle
Equations
- bundle.trivial.inhabited = {default := inhabited.default _inst_1}
The trivial bundle, unlike other bundles, has a canonical projection on the fiber.
Equations
The pullback of a bundle E
over a base B
under a map f : B' → B
, denoted by pullback f E
or f *ᵖ E
, is the bundle over B'
whose fiber over b'
is E (f b')
.
Instances for bundle.pullback
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