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 define 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.TotalSpace
the total space of a bundle.Bundle.TotalSpace.proj
the projection from the total space to the base space.Bundle.TotalSpace.mk
the 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 x
because the total space usually has a different topology and Lean 4simp
fails to apply lemmas aboutΣ x, E x
to elements of the total space. -
The definition of
Bundle.TotalSpace
has an unused argumentF
. 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.
References #
- https://en.wikipedia.org/wiki/Bundle_(mathematics)
- proj : B
Bundle.TotalSpace.proj
is the canonical projectionBundle.TotalSpace F E → B
from the total space to the base space. - snd : E s.proj
Bundle.TotalSpace F E
is the total space of the bundle. It consists of pairs
(proj : B, snd : E proj)
.
Instances For
Bundle.TotalSpace.proj
is the canonical projection Bundle.TotalSpace F E → B
from the
total space to the base space.
Instances For
Instances For
Notation for the direct sum of two bundles over the same base.
Instances For
The trivial bundle, unlike other bundles, has a canonical projection on the fiber.
Instances For
A trivial bundle is equivalent to the product B × F
.
Instances For
The pullback of a bundle E
over a base B
under a map f : B' → B
, denoted by
Bundle.Pullback f E
or f *ᵖ E
, is the bundle over B'
whose fiber over b'
is E (f b')
.
Instances For
The pullback of a bundle E
over a base B
under a map f : B' → B
, denoted by
Bundle.Pullback f E
or f *ᵖ E
, is the bundle over B'
whose fiber over b'
is E (f b')
.
Instances For
Natural embedding of the total space of f *ᵖ E
into B' × TotalSpace F E
.
Instances For
The base map f : B' → B
lifts to a canonical map on the total spaces.