Fiber bundles #
A topological fiber bundle with fiber F
over a base B
is a space projecting on B
for which the
fibers are all homeomorphic to F
, such that the local situation around each point is a direct
product. We define a predicate is_topological_fiber_bundle F p
saying that p : Z → B
is a
topological fiber bundle with fiber F
.
It is in general nontrivial to construct a fiber bundle. A way is to start from the knowledge of
how changes of local trivializations act on the fiber. From this, one can construct the total space
of the bundle and its topology by a suitable gluing construction. The main content of this file is
an implementation of this construction: starting from an object of type
topological_fiber_bundle_core
registering the trivialization changes, one gets the corresponding
fiber bundle and projection.
Similarly we implement the object topological_fiber_prebundle
which allows to define a topological
fiber bundle from trivializations given as local equivalences with minimum additional properties.
Main definitions #
Basic definitions #
-
trivialization F p
: structure extending local homeomorphisms, defining a local trivialization of a topological spaceZ
with projectionp
and fiberF
. -
is_topological_fiber_bundle F p
: Prop saying that the mapp
between topological spaces is a fiber bundle with fiberF
. -
is_trivial_topological_fiber_bundle F p
: Prop saying that the mapp : Z → B
between topological spaces is a trivial topological fiber bundle, i.e., there exists a homeomorphismh : Z ≃ₜ B × F
such thatproj x = (h x).1
.
Operations on bundles #
We provide the following operations on trivialization
s.
-
trivialization.comap
: given a local trivializatione
of a fiber bundlep : Z → B
, a continuous mapf : B' → B
and a pointb' : B'
such thatf b' ∈ e.base_set
,e.comap f hf b' hb'
is a trivialization of the pullback bundle. The pullback bundle (a.k.a., the induced bundle) has total space{(x, y) : B' × Z | f x = p y}
, and is given byλ ⟨(x, y), h⟩, x
. -
is_topological_fiber_bundle.comap
: ifp : Z → B
is a topological fiber bundle, then its pullback along a continuous mapf : B' → B
is a topological fiber bundle as well. -
trivialization.comp_homeomorph
: given a local trivializatione
of a fiber bundlep : Z → B
and a homeomorphismh : Z' ≃ₜ Z
, returns a local trivialization of the fiber bundlep ∘ h
. -
is_topological_fiber_bundle.comp_homeomorph
: ifp : Z → B
is a topological fiber bundle andh : Z' ≃ₜ Z
is a homeomorphism, thenp ∘ h : Z' → B
is a topological fiber bundle with the same fiber.
Construction of a bundle from trivializations #
bundle.total_space E
is a type synonym forΣ (x : B), E x
, that we can endow with a suitable topology.topological_fiber_bundle_core ι B F
: structure registering how changes of coordinates act on the fiberF
above open subsets ofB
, where local trivializations are indexed byι
.
Let Z : topological_fiber_bundle_core ι B F
. Then we define
-
Z.fiber x
: the fiber abovex
, homeomorphic toF
(and defeq toF
as a type). -
Z.total_space
: the total space ofZ
, defined as aType
asΣ (b : B), F
, but with a twisted topology coming from the fiber bundle structure. It is (reducibly) the same asbundle.total_space Z.fiber
. -
Z.proj
: projection fromZ.total_space
toB
. It is continuous. -
Z.local_triv i
: fori : ι
, bundle trivialization above the setZ.base_set i
, which is an open set inB
. -
pretrivialization F proj
: trivialization as a local equivalence, mainly used when the topology on the total space has not yet been defined. -
topological_fiber_prebundle F proj
: structure registering a cover of prebundle trivializations and requiring that the relative transition maps are local homeomorphisms. -
topological_fiber_prebundle.total_space_topology a
: natural topology of the total space, making the prebundle into a bundle.
Implementation notes #
A topological fiber bundle with fiber F
over a base B
is a family of spaces isomorphic to F
,
indexed by B
, which is locally trivial in the following sense: there is a covering of B
by open
sets such that, on each such open set s
, the bundle is isomorphic to s × F
.
To construct a fiber bundle formally, the main data is what happens when one changes trivializations
from s × F
to s' × F
on s ∩ s'
: one should get a family of homeomorphisms of F
, depending
continuously on the base point, satisfying basic compatibility conditions (cocycle property).
Useful classes of bundles can then be specified by requiring that these homeomorphisms of F
belong to some subgroup, preserving some structure (the "structure group of the bundle"): then
these structures are inherited by the fibers of the bundle.
Given such trivialization change data (encoded below in a structure called
topological_fiber_bundle_core
), one can construct the fiber bundle. The intrinsic canonical
mathematical construction is the following.
The fiber above x
is the disjoint union of F
over all trivializations, modulo the gluing
identifications: one gets a fiber which is isomorphic to F
, but non-canonically
(each choice of one of the trivializations around x
gives such an isomorphism). Given a
trivialization over a set s
, one gets an isomorphism between s × F
and proj^{-1} s
, by using
the identification corresponding to this trivialization. One chooses the topology on the bundle that
makes all of these into homeomorphisms.
For the practical implementation, it turns out to be more convenient to avoid completely the
gluing and quotienting construction above, and to declare above each x
that the fiber is F
,
but thinking that it corresponds to the F
coming from the choice of one trivialization around x
.
This has several practical advantages:
- without any work, one gets a topological space structure on the fiber. And if
F
has more structure it is inherited for free by the fiber. - In the case of the tangent bundle of manifolds, this implies that on vector spaces the derivative
(from
F
toF
) and the manifold derivative (fromtangent_space I x
totangent_space I' (f x)
) are equal.
A drawback is that some silly constructions will typecheck: in the case of the tangent bundle, one
can add two vectors in different tangent spaces (as they both are elements of F
from the point of
view of Lean). To solve this, one could mark the tangent space as irreducible, but then one would
lose the identification of the tangent space to F
with F
. There is however a big advantage of
this situation: even if Lean can not check that two basepoints are defeq, it will accept the fact
that the tangent spaces are the same. For instance, if two maps f
and g
are locally inverse to
each other, one can express that the composition of their derivatives is the identity of
tangent_space I x
. One could fear issues as this composition goes from tangent_space I x
to
tangent_space I (g (f x))
(which should be the same, but should not be obvious to Lean
as it does not know that g (f x) = x
). As these types are the same to Lean (equal to F
), there
are in fact no dependent type difficulties here!
For this construction of a fiber bundle from a topological_fiber_bundle_core
, we should thus
choose for each x
one specific trivialization around it. We include this choice in the definition
of the topological_fiber_bundle_core
, as it makes some constructions more
functorial and it is a nice way to say that the trivializations cover the whole space B
.
With this definition, the type of the fiber bundle space constructed from the core data is just
Σ (b : B), F
, but the topology is not the product one, in general.
We also take the indexing type (indexing all the trivializations) as a parameter to the fiber bundle
core: it could always be taken as a subtype of all the maps from open subsets of B
to continuous
maps of F
, but in practice it will sometimes be something else. For instance, on a manifold, one
will use the set of charts as a good parameterization for the trivializations of the tangent bundle.
Or for the pullback of a topological_fiber_bundle_core
, the indexing type will be the same as
for the initial bundle.
Tags #
Fiber bundle, topological bundle, local trivialization, structure group
General definition of topological fiber bundles #
- to_local_equiv : local_equiv Z (B × F)
- open_target : is_open self.to_local_equiv.target
- base_set : set B
- open_base_set : is_open self.base_set
- source_eq : self.to_local_equiv.source = proj ⁻¹' self.base_set
- target_eq : self.to_local_equiv.target = self.base_set ×ˢ set.univ
- proj_to_fun : ∀ (p : Z), p ∈ self.to_local_equiv.source → (self.to_local_equiv.to_fun p).fst = proj p
This structure contains the information left for a local trivialization (which is implemented
below as trivialization F proj
) if the total space has not been given a topology, but we
have a topology on both the fiber and the base space. Through the construction
topological_fiber_prebundle F proj
it will be possible to promote a
pretrivialization F proj
to a trivialization F proj
.
Instances for topological_fiber_bundle.pretrivialization
- topological_fiber_bundle.pretrivialization.has_sizeof_inst
- topological_fiber_bundle.pretrivialization.has_coe_to_fun
- topological_fiber_bundle.trivialization.topological_fiber_bundle.pretrivialization.has_coe
- topological_fiber_bundle.pretrivialization.has_coe
Equations
Composition of inverse and coercion from the subtype of the target.
Equations
- e.set_symm = e.to_local_equiv.target.restrict ⇑(e.to_local_equiv.symm)
- to_local_homeomorph : local_homeomorph Z (B × F)
- base_set : set B
- open_base_set : is_open self.base_set
- source_eq : self.to_local_homeomorph.to_local_equiv.source = proj ⁻¹' self.base_set
- target_eq : self.to_local_homeomorph.to_local_equiv.target = self.base_set ×ˢ set.univ
- proj_to_fun : ∀ (p : Z), p ∈ self.to_local_homeomorph.to_local_equiv.source → (⇑(self.to_local_homeomorph) p).fst = proj p
A structure extending local homeomorphisms, defining a local trivialization of a projection
proj : Z → B
with fiber F
, as a local homeomorphism between Z
and B × F
defined between two
sets of the form proj ⁻¹' base_set
and base_set × F
, acting trivially on the first coordinate.
Instances for topological_fiber_bundle.trivialization
- topological_fiber_bundle.trivialization.has_sizeof_inst
- topological_fiber_bundle.trivialization.has_coe_to_fun
- topological_fiber_bundle.trivialization.topological_fiber_bundle.pretrivialization.has_coe
- topological_fiber_bundle.trivialization.has_coe
Natural identification as a pretrivialization
.
Equations
- e.to_pretrivialization = {to_local_equiv := e.to_local_homeomorph.to_local_equiv, open_target := _, base_set := e.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
Equations
In the domain of a bundle trivialization, the projection is continuous
Composition of a trivialization
and a homeomorph
.
Equations
- e.comp_homeomorph h = {to_local_homeomorph := h.to_local_homeomorph.trans e.to_local_homeomorph, base_set := e.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
Read off the continuity of a function f : Z → X
at z : Z
by transferring via a
trivialization of Z
containing z
.
Read off the continuity of a function f : X → Z
at x : X
by transferring via a
trivialization of Z
containing f x
.
A topological fiber bundle with fiber F
over a base B
is a space projecting on B
for which the fibers are all homeomorphic to F
, such that the local situation around each point
is a direct product.
Equations
- is_topological_fiber_bundle F proj = ∀ (x : B), ∃ (e : topological_fiber_bundle.trivialization F proj), x ∈ e.base_set
A trivial topological fiber bundle with fiber F
over a base B
is a space Z
projecting on B
for which there exists a homeomorphism to B × F
that sends proj
to prod.fst
.
The projection from a topological fiber bundle to its base is continuous.
The projection from a topological fiber bundle to its base is an open map.
The projection from a topological fiber bundle with a nonempty fiber to its base is a surjective map.
The projection from a topological fiber bundle with a nonempty fiber to its base is a quotient map.
The first projection in a product is a trivial topological fiber bundle.
The first projection in a product is a topological fiber bundle.
The second projection in a product is a trivial topological fiber bundle.
The second projection in a product is a topological fiber bundle.
If e
is a trivialization
of proj : Z → B
with fiber F
and h
is a homeomorphism
F ≃ₜ F'
, then e.trans_fiber_homeomorph h
is the trivialization of proj
with the fiber F'
that sends p : Z
to ((e p).1, h (e p).2)
.
Equations
- e.trans_fiber_homeomorph h = {to_local_homeomorph := e.to_local_homeomorph.trans_homeomorph ((homeomorph.refl B).prod_congr h), base_set := e.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
Coordinate transformation in the fiber induced by a pair of bundle trivializations. See also
trivialization.coord_change_homeomorph
for a version bundled as F ≃ₜ F
.
Equations
- e₁.coord_change e₂ b x = (⇑e₂ (⇑(e₁.to_local_homeomorph.symm) (b, x))).snd
Coordinate transformation in the fiber induced by a pair of bundle trivializations, as a homeomorphism.
Equations
- e₁.coord_change_homeomorph e₂ h₁ h₂ = {to_equiv := {to_fun := e₁.coord_change e₂ b, inv_fun := e₂.coord_change e₁ b, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
Given a bundle trivialization of proj : Z → B
and a continuous map f : B' → B
,
construct a bundle trivialization of φ : {p : B' × Z | f p.1 = proj p.2} → B'
given by φ x = (x : B' × Z).1
.
Equations
- e.comap f hf b' hb' = {to_local_homeomorph := {to_local_equiv := {to_fun := λ (p : ↥{p : B' × Z | f p.fst = proj p.snd}), (↑p.fst, (⇑e ↑p.snd).snd), inv_fun := λ (p : B' × F), dite (f p.fst ∈ e.base_set) (λ (h : f p.fst ∈ e.base_set), ⟨(p.fst, ⇑(e.to_local_homeomorph.symm) (f p.fst, p.snd)), _⟩) (λ (h : f p.fst ∉ e.base_set), ⟨(b', ⇑(e.to_local_homeomorph.symm) (f b', p.snd)), _⟩), source := {p : ↥{p : B' × Z | f p.fst = proj p.snd} | f ↑p.fst ∈ e.base_set}, target := {p : B' × F | f p.fst ∈ e.base_set}, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}, base_set := f ⁻¹' e.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
If proj : Z → B
is a topological fiber bundle with fiber F
and f : B' → B
is a continuous
map, then the pullback bundle (a.k.a. induced bundle) is the topological bundle with the total space
{(x, y) : B' × Z | f x = proj y}
given by λ ⟨(x, y), h⟩, x
.
Restrict a trivialization
to an open set in the base. `
Equations
- e.restr_open s hs = {to_local_homeomorph := (_.restr _).symm, base_set := e.base_set ∩ s, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
Given two bundle trivializations e
, e'
of proj : Z → B
and a set s : set B
such that
the base sets of e
and e'
intersect frontier s
on the same set and e p = e' p
whenever
proj p ∈ e.base_set ∩ frontier s
, e.piecewise e' s Hs Heq
is the bundle trivialization over
set.ite s e.base_set e'.base_set
that is equal to e
on proj ⁻¹ s
and is equal to e'
otherwise.
Equations
- e.piecewise e' s Hs Heq = {to_local_homeomorph := e.to_local_homeomorph.piecewise e'.to_local_homeomorph (proj ⁻¹' s) (s ×ˢ set.univ) _ _ _ _, base_set := s.ite e.base_set e'.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
Given two bundle trivializations e
, e'
of a topological fiber bundle proj : Z → B
over a linearly ordered base B
and a point a ∈ e.base_set ∩ e'.base_set
such that
e
equals e'
on proj ⁻¹' {a}
, e.piecewise_le_of_eq e' a He He' Heq
is the bundle
trivialization over set.ite (Iic a) e.base_set e'.base_set
that is equal to e
on points p
such that proj p ≤ a
and is equal to e'
otherwise.
Equations
- e.piecewise_le_of_eq e' a He He' Heq = e.piecewise e' (set.Iic a) _ _
Given two bundle trivializations e
, e'
of a topological fiber bundle proj : Z → B
over a
linearly ordered base B
and a point a ∈ e.base_set ∩ e'.base_set
, e.piecewise_le e' a He He'
is the bundle trivialization over set.ite (Iic a) e.base_set e'.base_set
that is equal to e
on
points p
such that proj p ≤ a
and is equal to ((e' p).1, h (e' p).2)
otherwise, where
h =
e'.coord_change_homeomorph e _ _is the homeomorphism of the fiber such that
h (e' p).2 = (e p).2whenever
e p = a`.
Equations
- e.piecewise_le e' a He He' = e.piecewise_le_of_eq (e'.trans_fiber_homeomorph (e'.coord_change_homeomorph e He' He)) a He He' _
Given two bundle trivializations e
, e'
over disjoint sets, e.disjoint_union e' H
is the
bundle trivialization over the union of the base sets that agrees with e
and e'
over their
base sets.
Equations
- e.disjoint_union e' H = {to_local_homeomorph := e.to_local_homeomorph.disjoint_union e'.to_local_homeomorph _ _, base_set := e.base_set ∪ e'.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
If h
is a topological fiber bundle over a conditionally complete linear order,
then it is trivial over any closed interval.
Constructing topological fiber bundles #
Equations
- bundle.trivial.topological_space = λ (x : B), I
- base_set : ι → set B
- is_open_base_set : ∀ (i : ι), is_open (self.base_set i)
- index_at : B → ι
- mem_base_set_at : ∀ (x : B), x ∈ self.base_set (self.index_at x)
- coord_change : ι → ι → B → F → F
- coord_change_self : ∀ (i : ι) (x : B), x ∈ self.base_set i → ∀ (v : F), self.coord_change i i x v = v
- coord_change_continuous : ∀ (i j : ι), continuous_on (λ (p : B × F), self.coord_change i j p.fst p.snd) ((self.base_set i ∩ self.base_set j) ×ˢ set.univ)
- coord_change_comp : ∀ (i j k : ι) (x : B), x ∈ self.base_set i ∩ self.base_set j ∩ self.base_set k → ∀ (v : F), self.coord_change j k x (self.coord_change i j x v) = self.coord_change i k x v
Core data defining a locally trivial topological bundle with fiber F
over a topological
space B
. Note that "bundle" is used in its mathematical sense. This is the (computer science)
bundled version, i.e., all the relevant data is contained in the following structure. A family of
local trivializations is indexed by a type ι
, on open subsets base_set i
for each i : ι
.
Trivialization changes from i
to j
are given by continuous maps coord_change i j
from
base_set i ∩ base_set j
to the set of homeomorphisms of F
, but we express them as maps
B → F → F
and require continuity on (base_set i ∩ base_set j) × F
to avoid the topology on the
space of continuous maps on F
.
Instances for topological_fiber_bundle_core
- topological_fiber_bundle_core.has_sizeof_inst
- topological_vector_bundle_core.to_topological_fiber_bundle_core_coe
The index set of a topological fiber bundle core, as a convenience function for dot notation
The base space of a topological fiber bundle core, as a convenience function for dot notation
The fiber of a topological fiber bundle core, as a convenience function for dot notation and typeclass inference
Instances for topological_fiber_bundle_core.fiber
Equations
- Z.topological_space_fiber x = _inst_2
The total space of the topological fiber bundle, as a convenience function for dot notation.
It is by definition equal to bundle.total_space Z.fiber
, a.k.a. Σ x, Z.fiber x
but with a
different name for typeclass inference.
Equations
The projection from the total space of a topological fiber bundle core, on its base.
Equations
Local homeomorphism version of the trivialization change.
Equations
- Z.triv_change i j = {to_local_equiv := {to_fun := λ (p : B × F), (p.fst, Z.coord_change i j p.fst p.snd), inv_fun := λ (p : B × F), (p.fst, Z.coord_change j i p.fst p.snd), source := (Z.base_set i ∩ Z.base_set j) ×ˢ set.univ, target := (Z.base_set i ∩ Z.base_set j) ×ˢ set.univ, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
Associate to a trivialization index i : ι
the corresponding trivialization, i.e., a bijection
between proj ⁻¹ (base_set i)
and base_set i × F
. As the fiber above x
is F
but read in the
chart with index index_at x
, the trivialization in the fiber above x is by definition the
coordinate change from i to index_at x
, so it depends on x
.
The local trivialization will ultimately be a local homeomorphism. For now, we only introduce the
local equiv version, denoted with a prime. In further developments, avoid this auxiliary version,
and use Z.local_triv
instead.
Equations
- Z.local_triv_as_local_equiv i = {to_fun := λ (p : Z.total_space), (p.fst, Z.coord_change (Z.index_at p.fst) i p.fst p.snd), inv_fun := λ (p : B × F), ⟨p.fst, Z.coord_change i (Z.index_at p.fst) p.fst p.snd⟩, source := Z.proj ⁻¹' Z.base_set i, target := Z.base_set i ×ˢ set.univ, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}
The composition of two local trivializations is the trivialization change Z.triv_change i j.
Topological structure on the total space of a topological bundle created from core, designed so that all the local trivialization are continuous.
Equations
- topological_fiber_bundle_core.to_topological_space ι Z = topological_space.generate_from (⋃ (i : ι) (s : set (B × F)) (s_open : is_open s), {(Z.local_triv_as_local_equiv i).source ∩ ⇑(Z.local_triv_as_local_equiv i) ⁻¹' s})
Extended version of the local trivialization of a fiber bundle constructed from core, registering additionally in its type that it is a local bundle trivialization.
Equations
- Z.local_triv i = {to_local_homeomorph := {to_local_equiv := Z.local_triv_as_local_equiv i, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}, base_set := Z.base_set i, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
A topological fiber bundle constructed from core is indeed a topological fiber bundle.
The projection on the base of a topological bundle created from core is continuous
The projection on the base of a topological bundle created from core is an open map
Preferred local trivialization of a fiber bundle constructed from core, at a given point, as a bundle trivialization
Equations
- Z.local_triv_at b = Z.local_triv (Z.index_at b)
If an element of F
is invariant under all coordinate changes, then one can define a
corresponding section of the fiber bundle, which is continuous. This applies in particular to the
zero section of a vector bundle. Another example (not yet defined) would be the identity
section of the endomorphism bundle of a vector bundle.
The inclusion of a fiber into the total space is a continuous map.
- pretrivialization_atlas : set (topological_fiber_bundle.pretrivialization F proj)
- pretrivialization_at : B → topological_fiber_bundle.pretrivialization F proj
- mem_base_pretrivialization_at : ∀ (x : B), x ∈ (self.pretrivialization_at x).base_set
- pretrivialization_mem_atlas : ∀ (x : B), self.pretrivialization_at x ∈ self.pretrivialization_atlas
- continuous_triv_change : ∀ (e : topological_fiber_bundle.pretrivialization F proj), e ∈ self.pretrivialization_atlas → ∀ (e' : topological_fiber_bundle.pretrivialization F proj), e' ∈ self.pretrivialization_atlas → continuous_on (⇑e ∘ ⇑(e'.to_local_equiv.symm)) (e'.to_local_equiv.target ∩ ⇑(e'.to_local_equiv.symm) ⁻¹' e.to_local_equiv.source)
This structure permits to define a fiber bundle when trivializations are given as local equivalences but there is not yet a topology on the total space. The total space is hence given a topology in such a way that there is a fiber bundle structure for which the local equivalences are also local homeomorphism and hence local trivializations.
Instances for topological_fiber_prebundle
- topological_fiber_prebundle.has_sizeof_inst
Topology on the total space that will make the prebundle into a bundle.
Equations
- a.total_space_topology = ⨆ (e : topological_fiber_bundle.pretrivialization F proj) (he : e ∈ a.pretrivialization_atlas), topological_space.coinduced e.set_symm subtype.topological_space
Promotion from a pretrivialization
to a trivialization
.
Equations
- a.trivialization_of_mem_pretrivialization_atlas he = {to_local_homeomorph := {to_local_equiv := e.to_local_equiv, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}, base_set := e.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
For a fiber bundle Z
over B
constructed using the topological_fiber_prebundle
mechanism,
continuity of a function Z → X
on an open set s
can be checked by precomposing at each point
with the pretrivialization used for the construction at that point.