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*.
Bundle.TotalSpace F E to be the type of pairs
⟨b, x⟩, where
b : B and
x : E b.
This type is isomorphic to
Σ x, E x and uses an extra argument
F for reasons explained below. In
general, the constructions of fiber bundles we will make will be of this form.
Main Definitions #
Bundle.TotalSpacethe total space of a bundle.
Bundle.TotalSpace.projthe projection from the total space to the base space.
Bundle.TotalSpace.mkthe constructor for the total space.
Implementation Notes #
We use a custom structure for the total space of a bundle instead of using a type synonym for the canonical disjoint union
Σ x, E xbecause the total space usually has a different topology and Lean 4
simpfails to apply lemmas about
Σ x, E xto elements of the total space.
The definition of
Bundle.TotalSpacehas an unused argument
F. The reason is that in some constructions (e.g.,
Bundle.ContinuousLinearMap.vectorBundle) we need access to the atlas of trivializations of original fiber bundles to construct the topology on the total space of the new fiber bundle.
- proj : B
- snd : E s.proj