Vector bundles #
In this file we define (topological) vector bundles.
Let B
be the base space, let F
be a normed space over a normed field R
, and let
E : B → Type*
be a FiberBundle
with fiber F
, in which, for each x
, the fiber E x
is a
topological vector space over R
.
To have a vector bundle structure on Bundle.TotalSpace F E
, one should additionally have the
following properties:
- The bundle trivializations in the trivialization atlas should be continuous linear equivs in the fibers;
- For any two trivializations
e
,e'
in the atlas the transition function considered as a map fromB
intoF →L[R] F
is continuous one.baseSet ∩ e'.baseSet
with respect to the operator norm topology onF →L[R] F
.
If these conditions are satisfied, we register the typeclass VectorBundle R F E
.
We define constructions on vector bundles like pullbacks and direct sums in other files.
Main Definitions #
Trivialization.IsLinear
: a class stating that a trivialization is fiberwise linear on its base set.Trivialization.linearEquivAt
andTrivialization.continuousLinearMapAt
are the (continuous) linear fiberwise equivalences a trivialization induces.- They have forward maps
Trivialization.linearMapAt
/Trivialization.continuousLinearMapAt
and inversesTrivialization.symmₗ
/Trivialization.symmL
. Note that these are all defined everywhere, since they are extended using the zero function. Trivialization.coordChangeL
is the coordinate change induced by two trivializations. It only makes sense on the intersection of their base sets, but is extended outside it using the identity.- Given a continuous (semi)linear map between
E x
andE' y
whereE
andE'
are bundles over possibly different base sets,ContinuousLinearMap.inCoordinates
turns this into a continuous (semi)linear map between the chosen fibers of those bundles.
Implementation notes #
The implementation choices in the vector bundle definition are discussed in the "Implementation
notes" section of Mathlib.Topology.FiberBundle.Basic
.
Tags #
Vector bundle
A mixin class for Pretrivialization
, stating that a pretrivialization is fiberwise linear with
respect to given module structures on its fibers and the model fiber.
- linear : ∀ b ∈ e.baseSet, IsLinearMap R fun (x : E b) => (↑e { proj := b, snd := x }).2
Instances
A fiberwise linear inverse to e
.
Equations
- Pretrivialization.symmₗ R e b = IsLinearMap.mk' (e.symm b) ⋯
Instances For
A pretrivialization for a vector bundle defines linear equivalences between the fibers and the model space.
Equations
- Pretrivialization.linearEquivAt R e b hb = { toFun := fun (y : E b) => (↑e { proj := b, snd := y }).2, map_add' := ⋯, map_smul' := ⋯, invFun := e.symm b, left_inv := ⋯, right_inv := ⋯ }
Instances For
A fiberwise linear map equal to e
on e.baseSet
.
Equations
- Pretrivialization.linearMapAt R e b = if hb : b ∈ e.baseSet then ↑(Pretrivialization.linearEquivAt R e b hb) else 0
Instances For
A mixin class for Trivialization
, stating that a trivialization is fiberwise linear with
respect to given module structures on its fibers and the model fiber.
- linear : ∀ b ∈ e.baseSet, IsLinearMap R fun (x : E b) => (↑e { proj := b, snd := x }).2
Instances
Equations
- ⋯ = ⋯
A trivialization for a vector bundle defines linear equivalences between the fibers and the model space.
Equations
- Trivialization.linearEquivAt R e b hb = Pretrivialization.linearEquivAt R e.toPretrivialization b hb
Instances For
A fiberwise linear inverse to e
.
Equations
- Trivialization.symmₗ R e b = Pretrivialization.symmₗ R e.toPretrivialization b
Instances For
A fiberwise linear map equal to e
on e.baseSet
.
Equations
- Trivialization.linearMapAt R e b = Pretrivialization.linearMapAt R e.toPretrivialization b
Instances For
A coordinate change function between two trivializations, as a continuous linear equivalence.
Defined to be the identity when b
does not lie in the base set of both trivializations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A version of Trivialization.coordChangeL_apply
that fully unfolds coordChange
. The
right-hand side is ugly, but has good definitional properties for specifically defined
trivializations.
The zero section of a vector bundle
Equations
- Bundle.zeroSection F E x = { proj := x, snd := 0 }
Instances For
The space Bundle.TotalSpace F E
(for E : B → Type*
such that each E x
is a topological
vector space) has a topological vector space structure with fiber F
(denoted with
VectorBundle R F E
) if around every point there is a fiber bundle trivialization which is linear
in the fibers.
- trivialization_linear' : ∀ (e : Trivialization F Bundle.TotalSpace.proj) [inst : MemTrivializationAtlas e], Trivialization.IsLinear R e
- continuousOn_coordChange' : ∀ (e e' : Trivialization F Bundle.TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'], ContinuousOn (fun (b : B) => ↑(Trivialization.coordChangeL R e e' b)) (e.baseSet ∩ e'.baseSet)
Instances
Equations
- ⋯ = ⋯
Forward map of Trivialization.continuousLinearEquivAt
(only propositionally equal),
defined everywhere (0
outside domain).
Equations
- Trivialization.continuousLinearMapAt R e b = { toFun := ⇑(Trivialization.linearMapAt R e b), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
Backwards map of Trivialization.continuousLinearEquivAt
, defined everywhere.
Equations
- Trivialization.symmL R e b = { toFun := e.symm b, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
In a vector bundle, a trivialization in the fiber (which is a priori only linear) is in fact a continuous linear equiv between the fibers and the model fiber.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructing vector bundles #
Analogous construction of FiberBundleCore
for vector bundles. This
construction gives a way to construct vector bundles from a structure registering how
trivialization changes act on fibers.
- baseSet : ι → Set B
- isOpen_baseSet : ∀ (i : ι), IsOpen (self.baseSet i)
- indexAt : B → ι
- mem_baseSet_at : ∀ (x : B), x ∈ self.baseSet (self.indexAt x)
- coordChange_self : ∀ (i : ι), ∀ x ∈ self.baseSet i, ∀ (v : F), (self.coordChange i i x) v = v
- continuousOn_coordChange : ∀ (i j : ι), ContinuousOn (self.coordChange i j) (self.baseSet i ∩ self.baseSet j)
Instances For
The trivial vector bundle core, in which all the changes of coordinates are the identity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- instInhabitedVectorBundleCore R B F ι = { default := trivialVectorBundleCore R B F ι }
Natural identification to a FiberBundleCore
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The index set of a vector bundle core, as a convenience function for dot notation
Equations
- VectorBundleCore.Index = ι
Instances For
The base space of a vector bundle core, as a convenience function for dot notation
Equations
- VectorBundleCore.Base = B
Instances For
The fiber of a vector bundle core, as a convenience function for dot notation and typeclass inference
Equations
- Z.Fiber = Z.toFiberBundleCore.Fiber
Instances For
Equations
- Z.topologicalSpaceFiber x = Z.toFiberBundleCore.topologicalSpaceFiber x
Equations
- Z.addCommGroupFiber x = inferInstanceAs (AddCommGroup F)
Equations
- Z.moduleFiber x = inferInstanceAs (Module R F)
The projection from the total space of a fiber bundle core, on its base.
Equations
- Z.proj = Bundle.TotalSpace.proj
Instances For
The total space of the vector bundle, as a convenience function for dot notation.
It is by definition equal to Bundle.TotalSpace F Z.Fiber
.
Equations
- Z.TotalSpace = Bundle.TotalSpace F Z.Fiber
Instances For
Local homeomorphism version of the trivialization change.
Equations
- Z.trivChange i j = Z.toFiberBundleCore.trivChange i j
Instances For
Topological structure on the total space of a vector bundle created from core, designed so that all the local trivialization are continuous.
Equations
- Z.toTopologicalSpace = Z.toFiberBundleCore.toTopologicalSpace
One of the standard local trivializations of a vector bundle constructed from core, taken by considering this in particular as a fiber bundle constructed from core.
Equations
- Z.localTriv i = Z.toFiberBundleCore.localTriv i
Instances For
The standard local trivializations of a vector bundle constructed from core are linear.
Equations
- ⋯ = ⋯
Preferred local trivialization of a vector bundle constructed from core, at a given point, as a bundle trivialization
Equations
- Z.localTrivAt b = Z.localTriv (Z.indexAt b)
Instances For
Equations
- Z.fiberBundle = Z.toFiberBundleCore.fiberBundle
Equations
- ⋯ = ⋯
The projection on the base of a vector bundle created from core is continuous
The projection on the base of a vector bundle created from core is an open map
Vector prebundle #
This structure permits to define a vector bundle when trivializations are given as local equivalences but there is not yet a topology on the total space or the fibers. The total space is hence given a topology in such a way that there is a fiber bundle structure for which the partial equivalences are also partial homeomorphisms and hence vector bundle trivializations. The topology on the fibers is induced from the one on the total space.
The field exists_coordChange
is stated as an existential statement (instead of 3 separate
fields), since it depends on propositional information (namely e e' ∈ pretrivializationAtlas
).
This makes it inconvenient to explicitly define a coordChange
function when constructing a
VectorPrebundle
.
- pretrivializationAtlas : Set (Pretrivialization F Bundle.TotalSpace.proj)
- pretrivialization_linear' : ∀ e ∈ self.pretrivializationAtlas, Pretrivialization.IsLinear R e
- pretrivializationAt : B → Pretrivialization F Bundle.TotalSpace.proj
- mem_base_pretrivializationAt : ∀ (x : B), x ∈ (self.pretrivializationAt x).baseSet
- pretrivialization_mem_atlas : ∀ (x : B), self.pretrivializationAt x ∈ self.pretrivializationAtlas
- totalSpaceMk_isInducing : ∀ (b : B), IsInducing (↑(self.pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)
Instances For
A randomly chosen coordinate change on a VectorPrebundle
, given by
the field exists_coordChange
.
Equations
- a.coordChange he he' b = Classical.choose ⋯ b
Instances For
Natural identification of VectorPrebundle
as a FiberPrebundle
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Topology on the total space that will make the prebundle into a bundle.
Equations
- a.totalSpaceTopology = a.toFiberPrebundle.totalSpaceTopology
Instances For
Promotion from a Pretrivialization
in the pretrivializationAtlas
of a
VectorPrebundle
to a Trivialization
.
Equations
- a.trivializationOfMemPretrivializationAtlas he = a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he
Instances For
Make a FiberBundle
from a VectorPrebundle
; auxiliary construction for
VectorPrebundle.toVectorBundle
.
Equations
- a.toFiberBundle = a.toFiberPrebundle.toFiberBundle
Instances For
Make a VectorBundle
from a VectorPrebundle
. Concretely this means
that, given a VectorPrebundle
structure for a sigma-type E
-- which consists of a
number of "pretrivializations" identifying parts of E
with product spaces U × F
-- one
establishes that for the topology constructed on the sigma-type using
VectorPrebundle.totalSpaceTopology
, these "pretrivializations" are actually
"trivializations" (i.e., homeomorphisms with respect to the constructed topology).
When ϕ
is a continuous (semi)linear map between the fibers E x
and E' y
of two vector
bundles E
and E'
, ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ
is a coordinate
change of this continuous linear map w.r.t. the chart around x₀
and the chart around y₀
.
It is defined by composing ϕ
with appropriate coordinate changes given by the vector bundles
E
and E'
.
We use the operations Trivialization.continuousLinearMapAt
and Trivialization.symmL
in the
definition, instead of Trivialization.continuousLinearEquivAt
, so that
ContinuousLinearMap.inCoordinates
is defined everywhere (but see
ContinuousLinearMap.inCoordinates_eq
).
This is the (second component of the) underlying function of a trivialization of the hom-bundle
(see hom_trivializationAt_apply
). However, note that ContinuousLinearMap.inCoordinates
is
defined even when x
and y
live in different base sets.
Therefore, it is also convenient when working with the hom-bundle between pulled back bundles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rewrite ContinuousLinearMap.inCoordinates
using continuous linear equivalences.
Rewrite ContinuousLinearMap.inCoordinates
in a VectorBundleCore
.