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 _→ Type _
.
We provide a type synonym of Σ x, E x
as Bundle.TotalSpace E
, to be able to endow it with
a topology which is not the disjoint union topology Sigma.TopologicalSpace
. 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.totalSpaceMk
the constructor for the total space.
References #
- https://en.wikipedia.org/wiki/Bundle_(mathematics)
Bundle.TotalSpace 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.TotalSpace E = ((x : B) × E x)
Equations
- Bundle.instInhabitedTotalSpace E = { default := { fst := default, snd := default } }
The canonical projection defining a bundle.
Equations
- Bundle.termπ_ = Lean.ParserDescr.node `Bundle.termπ_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "π") (Lean.ParserDescr.cat `term 0))
Constructor for the total space of a bundle.
Equations
- Bundle.totalSpaceMk b a = { fst := b, snd := a }
Equations
- Bundle.instCoeTCTotalSpace = { coe := Bundle.totalSpaceMk x }
The direct sum of two bundles.
Equations
- Bundle.«term_×ᵇ_» = Lean.ParserDescr.trailingNode `Bundle.term_×ᵇ_ 100 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ᵇ ") (Lean.ParserDescr.cat `term 0))
Bundle.Trivial B F
is the trivial bundle over B
of fiber F
.
Equations
- Bundle.Trivial B F = Function.const B F
Equations
- Bundle.instInhabitedTrivial = { default := default }
The trivial bundle, unlike other bundles, has a canonical projection on the fiber.
Equations
- Bundle.Trivial.projSnd B F = Sigma.snd
The pullback of a bundle E
over a base B
under a map f : B' → B→ B
, denoted by Pullback f E
or f *ᵖ E
, is the bundle over B'
whose fiber over b'
is E (f b')
.
Equations
- Bundle.«term_*ᵖ_» = Lean.ParserDescr.trailingNode `Bundle.term_*ᵖ_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *ᵖ ") (Lean.ParserDescr.cat `term 0))
Natural embedding of the total space of f *ᵖ E
into B' × TotalSpace E× TotalSpace E
.
Equations
- Bundle.pullbackTotalSpaceEmbedding f z = (Bundle.TotalSpace.proj z, Bundle.totalSpaceMk (f (Bundle.TotalSpace.proj z)) z.snd)
The base map f : B' → B→ B
lifts to a canonical map on the total spaces.
Equations
- Bundle.Pullback.lift f z = Bundle.totalSpaceMk (f (Bundle.TotalSpace.proj z)) z.snd
Equations
- Bundle.instAddCommMonoidTrivial b = inst
Equations
- Bundle.instAddCommGroupTrivial b = inst