Fiber bundles #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Mathematically, 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.

In our formalism, a fiber bundle is by definition the type bundle.total_space F E where E : B → Type* is a function associating to x : B the fiber over x. This type bundle.total_space F E is a type of pairs (proj : B, snd : E proj).

To have a fiber bundle structure on bundle.total_space F E, one should additionally have the following data:

F should be a topological space;
There should be a topology on bundle.total_space F E, for which the projection to B is a fiber bundle with fiber F (in particular, each fiber E x is homeomorphic to F);
For each x, the fiber E x should be a topological space, and the injection from E x to bundle.total_space F E should be an embedding;
There should be a distinguished set of bundle trivializations, the "trivialization atlas"
There should be a choice of bundle trivialization at each point, which belongs to this atlas.

If all these conditions are satisfied, we register the typeclass fiber_bundle F E.

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 fiber_bundle_core registering the trivialization changes, one gets the corresponding fiber bundle and projection.

Similarly we implement the object fiber_prebundle which allows to define a topological fiber bundle from trivializations given as local equivalences with minimum additional properties.

Main definitions #

Basic definitions #

fiber_bundle F E : Structure saying that E : B → Type* is a fiber bundle with fiber F.

Construction of a bundle from trivializations #

bundle.total_space F E is the type of pairs (proj : B, snd : E proj). We can use the extra argument F to construct topology on the total space.
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 : 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 bundle.total_space F Z.fiber with a custom topology.
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.
fiber_prebundle F E : structure registering a cover of prebundle trivializations and requiring that the relative transition maps are local homeomorphisms.
fiber_prebundle.total_space_topology a : natural topology of the total space, making the prebundle into a bundle.

Implementation notes #

Data vs mixins #

For both fiber and vector bundles, one faces a choice: should the definition state the existence of local trivializations (a propositional typeclass), or specify a fixed atlas of trivializations (a typeclass containing data)?

In their initial mathlib implementations, both fiber and vector bundles were defined propositionally. For vector bundles, this turns out to be mathematically wrong: in infinite dimension, the transition function between two trivializations is not automatically continuous as a map from the base B to the endomorphisms F →L[R] F of the fiber (considered with the operator-norm topology), and so the definition needs to be modified by restricting consideration to a family of trivializations (constituting the data) which are all mutually-compatible in this sense. The PRs #13052 and #13175 implemented this change.

There is still the choice about whether to hold this data at the level of fiber bundles or of vector bundles. As of PR #17505, the data is all held in fiber_bundle, with vector_bundle a (propositional) mixin stating fiberwise-linearity.

This allows bundles to carry instances of typeclasses in which the scalar field, R, does not appear as a parameter. Notably, we would like a vector bundle over R with fiber F over base B to be a charted_space (B × F), with the trivializations providing the charts. This would be a dangerous instance for typeclass inference, because R does not appear as a parameter in charted_space (B × F). But if the data of the trivializations is held in fiber_bundle, then a fiber bundle with fiber F over base B can be a charted_space (B × F), and this is safe for typeclass inference.

We expect that this choice of definition will also streamline constructions of fiber bundles with similar underlying structure (e.g., the same bundle being both a real and complex vector bundle).

Core construction #

A 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 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 fiber_bundle_core, we should thus choose for each x one specific trivialization around it. We include this choice in the definition of the 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 bundle.total_space F (λ 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 fiber_bundle_core, the indexing type will be the same as for the initial bundle.

Tags #

Fiber bundle, topological bundle, structure group