# mathlibdocumentation

topology.fiber_bundle

# 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 space `Z` with projection `p` and fiber `F`.

• `is_topological_fiber_bundle F p` : Prop saying that the map `p` between topological spaces is a fiber bundle with fiber `F`.

• `is_trivial_topological_fiber_bundle F p` : Prop saying that the map `p : Z → B` between topological spaces is a trivial topological fiber bundle, i.e., there exists a homeomorphism `h : Z ≃ₜ B × F` such that `proj x = (h x).1`.

### Operations on bundles #

We provide the following operations on `trivialization`s.

• `trivialization.comap`: given a local trivialization `e` of a fiber bundle `p : Z → B`, a continuous map `f : B' → B` and a point `b' : B'` such that `f 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`: if `p : Z → B` is a topological fiber bundle, then its pullback along a continuous map `f : B' → B` is a topological fiber bundle as well.

• `trivialization.comp_homeomorph`: given a local trivialization `e` of a fiber bundle `p : Z → B` and a homeomorphism `h : Z' ≃ₜ Z`, returns a local trivialization of the fiber bundle `p ∘ h`.

• `is_topological_fiber_bundle.comp_homeomorph`: if `p : Z → B` is a topological fiber bundle and `h : Z' ≃ₜ Z` is a homeomorphism, then `p ∘ 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 fiber `F` above open subsets of `B`, where local trivializations are indexed by `ι`.

Let `Z : topological_fiber_bundle_core ι B F`. Then we define

• `Z.fiber x` : the fiber above `x`, homeomorphic to `F` (and defeq to `F` as a type).

• `Z.total_space` : the total space of `Z`, defined as a `Type` as `Σ (b : B), F`, but with a twisted topology coming from the fiber bundle structure. It is (reducibly) the same as `bundle.total_space Z.fiber`.

• `Z.proj` : projection from `Z.total_space` to `B`. It is continuous.

• `Z.local_triv i`: for `i : ι`, bundle trivialization above the set `Z.base_set i`, which is an open set in `B`.

• `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` to `F`) and the manifold derivative (from `tangent_space I x` to `tangent_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 #

@[nolint]
structure topological_fiber_bundle.pretrivialization {B : Type u_2} (F : Type u_3) {Z : Type u_4} (proj : Z → B) :
Type (max u_2 u_3 u_4)

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`
@[protected, instance]
def topological_fiber_bundle.pretrivialization.has_coe_to_fun {B : Type u_2} (F : Type u_3) {Z : Type u_4} {proj : Z → B} :
(λ (_x : , Z → B × F)
Equations
@[simp]
theorem topological_fiber_bundle.pretrivialization.coe_coe {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) :
@[simp]
theorem topological_fiber_bundle.pretrivialization.coe_fst {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : x e.to_local_equiv.source) :
(e x).fst = proj x
theorem topological_fiber_bundle.pretrivialization.mem_source {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} :
proj x e.base_set
theorem topological_fiber_bundle.pretrivialization.coe_fst' {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : proj x e.base_set) :
(e x).fst = proj x
@[protected]
theorem topological_fiber_bundle.pretrivialization.eq_on {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) :
theorem topological_fiber_bundle.pretrivialization.mk_proj_snd {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : x e.to_local_equiv.source) :
(proj x, (e x).snd) = e x
theorem topological_fiber_bundle.pretrivialization.mk_proj_snd' {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : proj x e.base_set) :
(proj x, (e x).snd) = e x
def topological_fiber_bundle.pretrivialization.set_symm {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) :

Composition of inverse and coercion from the subtype of the target.

Equations
theorem topological_fiber_bundle.pretrivialization.mem_target {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : B × F} :
theorem topological_fiber_bundle.pretrivialization.proj_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : B × F} (hx : x e.to_local_equiv.target) :
proj ((e.to_local_equiv.symm) x) = x.fst
theorem topological_fiber_bundle.pretrivialization.proj_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {b : B} {x : F} (hx : b e.base_set) :
proj ((e.to_local_equiv.symm) (b, x)) = b
theorem topological_fiber_bundle.pretrivialization.proj_surj_on_base_set {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) [nonempty F] :
theorem topological_fiber_bundle.pretrivialization.apply_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : B × F} (hx : x e.to_local_equiv.target) :
theorem topological_fiber_bundle.pretrivialization.apply_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {b : B} {x : F} (hx : b e.base_set) :
e ((e.to_local_equiv.symm) (b, x)) = (b, x)
theorem topological_fiber_bundle.pretrivialization.symm_apply_apply {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (hx : x e.to_local_equiv.source) :
@[simp]
theorem topological_fiber_bundle.pretrivialization.symm_apply_mk_proj {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : x e.to_local_equiv.source) :
(e.to_local_equiv.symm) (proj x, (e x).snd) = x
@[simp]
theorem topological_fiber_bundle.pretrivialization.preimage_symm_proj_base_set {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) :
@[simp]
theorem topological_fiber_bundle.pretrivialization.preimage_symm_proj_inter {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) (s : set B) :
theorem topological_fiber_bundle.pretrivialization.target_inter_preimage_symm_source_eq {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e f : proj) :
theorem topological_fiber_bundle.pretrivialization.trans_source {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e f : proj) :
theorem topological_fiber_bundle.pretrivialization.symm_trans_symm {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e e' : proj) :
theorem topological_fiber_bundle.pretrivialization.symm_trans_source_eq {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e e' : proj) :
theorem topological_fiber_bundle.pretrivialization.symm_trans_target_eq {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e e' : proj) :
@[nolint]
structure topological_fiber_bundle.trivialization {B : Type u_2} (F : Type u_3) {Z : Type u_4} (proj : Z → B) :
Type (max u_2 u_3 u_4)

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`
def topological_fiber_bundle.trivialization.to_pretrivialization {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) :

Natural identification as a `pretrivialization`.

Equations
@[protected, instance]
def topological_fiber_bundle.trivialization.has_coe_to_fun {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B}  :
(λ (_x : , Z → B × F)
Equations
@[protected, instance]
def topological_fiber_bundle.trivialization.topological_fiber_bundle.pretrivialization.has_coe {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B}  :
Equations
@[simp]
theorem topological_fiber_bundle.trivialization.coe_coe {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) :
@[simp]
theorem topological_fiber_bundle.trivialization.coe_fst {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : x e.to_local_homeomorph.to_local_equiv.source) :
(e x).fst = proj x
@[protected]
theorem topological_fiber_bundle.trivialization.eq_on {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) :
theorem topological_fiber_bundle.trivialization.mem_source {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} :
proj x e.base_set
theorem topological_fiber_bundle.trivialization.coe_fst' {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : proj x e.base_set) :
(e x).fst = proj x
theorem topological_fiber_bundle.trivialization.mk_proj_snd {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : x e.to_local_homeomorph.to_local_equiv.source) :
(proj x, (e x).snd) = e x
theorem topological_fiber_bundle.trivialization.mk_proj_snd' {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : proj x e.base_set) :
(proj x, (e x).snd) = e x
theorem topological_fiber_bundle.trivialization.source_inter_preimage_target_inter {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) (s : set (B × F)) :
@[simp]
theorem topological_fiber_bundle.trivialization.coe_mk {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : (B × F)) (i : set B) (j : is_open i) (k : e.to_local_equiv.source = proj ⁻¹' i) (l : e.to_local_equiv.target = ) (m : ∀ (p : Z), (e p).fst = proj p) (x : Z) :
theorem topological_fiber_bundle.trivialization.mem_target {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : B × F} :
theorem topological_fiber_bundle.trivialization.map_target {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : B × F} (hx : x e.to_local_homeomorph.to_local_equiv.target) :
theorem topological_fiber_bundle.trivialization.proj_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : B × F} (hx : x e.to_local_homeomorph.to_local_equiv.target) :
theorem topological_fiber_bundle.trivialization.proj_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {b : B} {x : F} (hx : b e.base_set) :
proj ((e.to_local_homeomorph.symm) (b, x)) = b
theorem topological_fiber_bundle.trivialization.proj_surj_on_base_set {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) [nonempty F] :
theorem topological_fiber_bundle.trivialization.apply_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : B × F} (hx : x e.to_local_homeomorph.to_local_equiv.target) :
theorem topological_fiber_bundle.trivialization.apply_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {b : B} {x : F} (hx : b e.base_set) :
e ((e.to_local_homeomorph.symm) (b, x)) = (b, x)
@[simp]
theorem topological_fiber_bundle.trivialization.symm_apply_mk_proj {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : x e.to_local_homeomorph.to_local_equiv.source) :
(e.to_local_homeomorph.symm) (proj x, (e x).snd) = x
theorem topological_fiber_bundle.trivialization.symm_trans_source_eq {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e e' : proj) :
theorem topological_fiber_bundle.trivialization.symm_trans_target_eq {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e e' : proj) :
theorem topological_fiber_bundle.trivialization.coe_fst_eventually_eq_proj {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : x e.to_local_homeomorph.to_local_equiv.source) :
=ᶠ[nhds x] proj
theorem topological_fiber_bundle.trivialization.coe_fst_eventually_eq_proj' {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : proj x e.base_set) :
=ᶠ[nhds x] proj
theorem topological_fiber_bundle.trivialization.map_proj_nhds {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : x e.to_local_homeomorph.to_local_equiv.source) :
filter.map proj (nhds x) = nhds (proj x)
theorem topological_fiber_bundle.trivialization.continuous_at_proj {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {x : Z} (ex : x e.to_local_homeomorph.to_local_equiv.source) :

In the domain of a bundle trivialization, the projection is continuous

def topological_fiber_bundle.trivialization.comp_homeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {Z' : Type u_1} (h : Z' ≃ₜ Z) :
(proj h)

Composition of a `trivialization` and a `homeomorph`.

Equations
theorem topological_fiber_bundle.trivialization.continuous_at_of_comp_right {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} {X : Type u_1} {f : Z → X} {z : Z} (e : proj) (he : proj z e.base_set) (hf : (e z)) :

Read off the continuity of a function `f : Z → X` at `z : Z` by transferring via a trivialization of `Z` containing `z`.

theorem topological_fiber_bundle.trivialization.continuous_at_of_comp_left {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} {X : Type u_1} {f : X → Z} {x : X} (e : proj) (hf_proj : continuous_at (proj f) x) (he : proj (f x) e.base_set) (hf : continuous_at (e f) x) :

Read off the continuity of a function `f : X → Z` at `x : X` by transferring via a trivialization of `Z` containing `f x`.

def is_topological_fiber_bundle {B : Type u_2} (F : Type u_3) {Z : Type u_4} (proj : Z → B) :
Prop

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
def is_trivial_topological_fiber_bundle {B : Type u_2} (F : Type u_3) {Z : Type u_4} (proj : Z → B) :
Prop

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`.

Equations
theorem is_trivial_topological_fiber_bundle.is_topological_fiber_bundle {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (h : proj) :
theorem is_topological_fiber_bundle.map_proj_nhds {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (h : proj) (x : Z) :
filter.map proj (nhds x) = nhds (proj x)
theorem is_topological_fiber_bundle.continuous_proj {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (h : proj) :

The projection from a topological fiber bundle to its base is continuous.

theorem is_topological_fiber_bundle.is_open_map_proj {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (h : proj) :

The projection from a topological fiber bundle to its base is an open map.

theorem is_topological_fiber_bundle.surjective_proj {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} [nonempty F] (h : proj) :

The projection from a topological fiber bundle with a nonempty fiber to its base is a surjective map.

theorem is_topological_fiber_bundle.quotient_map_proj {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} [nonempty F] (h : proj) :

The projection from a topological fiber bundle with a nonempty fiber to its base is a quotient map.

theorem is_trivial_topological_fiber_bundle_fst {B : Type u_2} {F : Type u_3}  :

The first projection in a product is a trivial topological fiber bundle.

theorem is_topological_fiber_bundle_fst {B : Type u_2} {F : Type u_3}  :

The first projection in a product is a topological fiber bundle.

theorem is_trivial_topological_fiber_bundle_snd {B : Type u_2} {F : Type u_3}  :

The second projection in a product is a trivial topological fiber bundle.

theorem is_topological_fiber_bundle_snd {B : Type u_2} {F : Type u_3}  :

The second projection in a product is a topological fiber bundle.

theorem is_topological_fiber_bundle.comp_homeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} {Z' : Type u_1} (e : proj) (h : Z' ≃ₜ Z) :
(proj h)
def topological_fiber_bundle.trivialization.trans_fiber_homeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} {F' : Type u_1} (e : proj) (h : F ≃ₜ F') :

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
@[simp]
theorem topological_fiber_bundle.trivialization.trans_fiber_homeomorph_apply {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} {F' : Type u_1} (e : proj) (h : F ≃ₜ F') (x : Z) :
x = ((e x).fst, h (e x).snd)
def topological_fiber_bundle.trivialization.coord_change {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e₁ e₂ : proj) (b : B) (x : F) :
F

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
theorem topological_fiber_bundle.trivialization.mk_coord_change {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e₁ e₂ : proj) {b : B} (h₁ : b e₁.base_set) (h₂ : b e₂.base_set) (x : F) :
(b, e₁.coord_change e₂ b x) = e₂ ((e₁.to_local_homeomorph.symm) (b, x))
theorem topological_fiber_bundle.trivialization.coord_change_apply_snd {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e₁ e₂ : proj) {p : Z} (h : proj p e₁.base_set) :
e₁.coord_change e₂ (proj p) (e₁ p).snd = (e₂ p).snd
theorem topological_fiber_bundle.trivialization.coord_change_same_apply {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {b : B} (h : b e.base_set) (x : F) :
e.coord_change e b x = x
theorem topological_fiber_bundle.trivialization.coord_change_same {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) {b : B} (h : b e.base_set) :
theorem topological_fiber_bundle.trivialization.coord_change_coord_change {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e₁ e₂ e₃ : proj) {b : B} (h₁ : b e₁.base_set) (h₂ : b e₂.base_set) (x : F) :
e₂.coord_change e₃ b (e₁.coord_change e₂ b x) = e₁.coord_change e₃ b x
theorem topological_fiber_bundle.trivialization.continuous_coord_change {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e₁ e₂ : proj) {b : B} (h₁ : b e₁.base_set) (h₂ : b e₂.base_set) :
continuous (e₁.coord_change e₂ b)
def topological_fiber_bundle.trivialization.coord_change_homeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e₁ e₂ : proj) {b : B} (h₁ : b e₁.base_set) (h₂ : b e₂.base_set) :
F ≃ₜ F

Coordinate transformation in the fiber induced by a pair of bundle trivializations, as a homeomorphism.

Equations
@[simp]
theorem topological_fiber_bundle.trivialization.coord_change_homeomorph_coe {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e₁ e₂ : proj) {b : B} (h₁ : b e₁.base_set) (h₂ : b e₂.base_set) :
(e₁.coord_change_homeomorph e₂ h₁ h₂) = e₁.coord_change e₂ b
noncomputable def topological_fiber_bundle.trivialization.comap {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} {B' : Type u_5} (e : proj) (f : B' → B) (hf : continuous f) (b' : B') (hb' : f b' e.base_set) :
(λ (x : {p : B' × Z | f p.fst = proj p.snd}), x.fst)

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
theorem is_topological_fiber_bundle.comap {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} {B' : Type u_5} (h : proj) {f : B' → B} (hf : continuous f) :
(λ (x : {p : B' × Z | f p.fst = proj p.snd}), x.fst)

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`.

theorem topological_fiber_bundle.trivialization.is_image_preimage_prod {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) (s : set B) :
def topological_fiber_bundle.trivialization.restr_open {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) (s : set B) (hs : is_open s) :

Restrict a `trivialization` to an open set in the base. `

Equations
theorem topological_fiber_bundle.trivialization.frontier_preimage {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e : proj) (s : set B) :
noncomputable def topological_fiber_bundle.trivialization.piecewise {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e e' : proj) (s : set B) (Hs : = e'.base_set ) (Heq : e' (proj ⁻¹' (e.base_set frontier s))) :

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
noncomputable def topological_fiber_bundle.trivialization.piecewise_le_of_eq {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} [linear_order B] (e e' : proj) (a : B) (He : a e.base_set) (He' : a e'.base_set) (Heq : ∀ (p : Z), proj p = ae p = e' p) :

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
noncomputable def topological_fiber_bundle.trivialization.piecewise_le {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} [linear_order B] (e e' : proj) (a : B) (He : a e.base_set) (He' : a e'.base_set) :

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).2`whenever`e p = a`.

Equations
noncomputable def topological_fiber_bundle.trivialization.disjoint_union {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (e e' : proj) (H : e'.base_set) :

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
theorem is_topological_fiber_bundle.exists_trivialization_Icc_subset {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (h : proj) (a b : B) :
∃ (e : , b e.base_set

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 #

@[protected, instance]
def bundle.trivial.topological_space {B : Type u_2} {F : Type u_3} [I : topological_space F] (x : B) :
Equations
@[protected, instance]
def bundle.total_space.topological_space {B : Type u_2} {F : Type u_3} [t₁ : topological_space B] [t₂ : topological_space F] :
Equations
@[nolint]
structure topological_fiber_bundle_core (ι : Type u_4) (B : Type u_5) (F : Type u_6)  :
Type (max u_4 u_5 u_6)

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`
@[nolint]
def topological_fiber_bundle_core.index {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) :
Type u_1

The index set of a topological fiber bundle core, as a convenience function for dot notation

Equations
@[nolint]
def topological_fiber_bundle_core.base {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) :
Type u_2

The base space of a topological fiber bundle core, as a convenience function for dot notation

Equations
@[nolint]
def topological_fiber_bundle_core.fiber {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (x : B) :
Type u_3

The fiber of a topological fiber bundle core, as a convenience function for dot notation and typeclass inference

Equations
Instances for `topological_fiber_bundle_core.fiber`
@[protected, instance]
def topological_fiber_bundle_core.topological_space_fiber {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (x : B) :
Equations
• = _inst_2
@[nolint]
def topological_fiber_bundle_core.total_space {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) :
Type (max u_2 u_3)

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
@[simp]
def topological_fiber_bundle_core.proj {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) :
Z.total_space → B

The projection from the total space of a topological fiber bundle core, on its base.

Equations
def topological_fiber_bundle_core.triv_change {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i j : ι) :
local_homeomorph (B × F) (B × F)

Local homeomorphism version of the trivialization change.

Equations
@[simp]
theorem topological_fiber_bundle_core.mem_triv_change_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i j : ι) (p : B × F) :
def topological_fiber_bundle_core.local_triv_as_local_equiv {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) :
(B × F)

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
theorem topological_fiber_bundle_core.mem_local_triv_as_local_equiv_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) (p : Z.total_space) :
theorem topological_fiber_bundle_core.mem_local_triv_as_local_equiv_target {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) (p : B × F) :
theorem topological_fiber_bundle_core.local_triv_as_local_equiv_apply {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) (p : Z.total_space) :
p = (p.fst, Z.coord_change (Z.index_at p.fst) i p.fst p.snd)
theorem topological_fiber_bundle_core.local_triv_as_local_equiv_trans {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i j : ι) :

The composition of two local trivializations is the trivialization change Z.triv_change i j.

@[protected, instance]
def topological_fiber_bundle_core.to_topological_space (ι : Type u_1) {B : Type u_2} {F : Type u_3} (Z : F) :

Topological structure on the total space of a topological bundle created from core, designed so that all the local trivialization are continuous.

Equations
theorem topological_fiber_bundle_core.open_source' {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) :
def topological_fiber_bundle_core.local_triv {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) :

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
@[protected]
theorem topological_fiber_bundle_core.is_topological_fiber_bundle {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) :

A topological fiber bundle constructed from core is indeed a topological fiber bundle.

theorem topological_fiber_bundle_core.continuous_proj {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) :

The projection on the base of a topological bundle created from core is continuous

theorem topological_fiber_bundle_core.is_open_map_proj {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) :

The projection on the base of a topological bundle created from core is an open map

def topological_fiber_bundle_core.local_triv_at {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (b : B) :

Preferred local trivialization of a fiber bundle constructed from core, at a given point, as a bundle trivialization

Equations
@[simp]
theorem topological_fiber_bundle_core.local_triv_at_def {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (b : B) :
theorem topological_fiber_bundle_core.continuous_const_section {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (v : F) (h : ∀ (i j : ι) (x : B), x Z.base_set i Z.base_set jZ.coord_change i j x v = v) :
continuous (show B → Z.total_space, from λ (x : B), x, v⟩)

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.

@[simp]
theorem topological_fiber_bundle_core.local_triv_as_local_equiv_coe {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) :
@[simp]
theorem topological_fiber_bundle_core.local_triv_as_local_equiv_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) :
@[simp]
theorem topological_fiber_bundle_core.local_triv_as_local_equiv_target {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) :
@[simp]
theorem topological_fiber_bundle_core.local_triv_as_local_equiv_symm {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) :
@[simp]
theorem topological_fiber_bundle_core.base_set_at {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) :
@[simp]
theorem topological_fiber_bundle_core.local_triv_apply {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) (p : Z.total_space) :
(Z.local_triv i) p = (p.fst, Z.coord_change (Z.index_at p.fst) i p.fst p.snd)
@[simp]
theorem topological_fiber_bundle_core.local_triv_at_apply {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (p : Z.total_space) :
(Z.local_triv_at p.fst) p = (p.fst, p.snd)
@[simp]
theorem topological_fiber_bundle_core.local_triv_at_apply_mk {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (b : B) (a : F) :
(Z.local_triv_at b) b, a⟩ = (b, a)
@[simp]
theorem topological_fiber_bundle_core.mem_local_triv_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) (p : Z.total_space) :
@[simp]
theorem topological_fiber_bundle_core.mem_local_triv_at_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (p : Z.total_space) (b : B) :
@[simp]
theorem topological_fiber_bundle_core.mem_local_triv_target {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) (p : B × F) :
@[simp]
theorem topological_fiber_bundle_core.mem_local_triv_at_target {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (p : B × F) (b : B) :
@[simp]
theorem topological_fiber_bundle_core.local_triv_symm_apply {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (i : ι) (p : B × F) :
@[simp]
theorem topological_fiber_bundle_core.mem_local_triv_at_base_set {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (b : B) :
@[continuity]
theorem topological_fiber_bundle_core.continuous_total_space_mk {ι : Type u_1} {B : Type u_2} {F : Type u_3} (Z : F) (b : B) :

The inclusion of a fiber into the total space is a continuous map.

@[nolint]
structure topological_fiber_prebundle {B : Type u_2} (F : Type u_3) {Z : Type u_4} (proj : Z → B) :
Type (max u_2 u_3 u_4)

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
def topological_fiber_prebundle.total_space_topology {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (a : proj) :

Topology on the total space that will make the prebundle into a bundle.

Equations
theorem topological_fiber_prebundle.continuous_symm_of_mem_pretrivialization_atlas {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (a : proj) {e : proj} (he : e a.pretrivialization_atlas) :
theorem topological_fiber_prebundle.is_open_source {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (a : proj) (e : proj) :
theorem topological_fiber_prebundle.is_open_target_of_mem_pretrivialization_atlas_inter {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (a : proj) (e e' : proj) (he' : e' a.pretrivialization_atlas) :
def topological_fiber_prebundle.trivialization_of_mem_pretrivialization_atlas {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (a : proj) {e : proj} (he : e a.pretrivialization_atlas) :

Promotion from a `pretrivialization` to a `trivialization`.

Equations
theorem topological_fiber_prebundle.is_topological_fiber_bundle {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (a : proj) :
theorem topological_fiber_prebundle.continuous_proj {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (a : proj) :
theorem topological_fiber_prebundle.continuous_on_of_comp_right {B : Type u_2} {F : Type u_3} {Z : Type u_4} {proj : Z → B} (a : proj) {X : Type u_1} {f : Z → X} {s : set B} (hs : is_open s) (hf : ∀ (b : B), b scontinuous_on (f .symm)) ((s (a.pretrivialization_at b).base_set) ×ˢ set.univ)) :
(proj ⁻¹' s)

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.