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.
bundle_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.
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.total_space : the total space of Z, defined as a Type as B × F, but with a twisted topology coming from the fiber bundle structure Z.proj : projection from Z.total_space to B. It is continuous. Z.fiber x : the fiber above x, homeomorphic to F (and defeq to F as a type). Z.local_triv i: for i : ι, a local homeomorphism from Z.total_space to B × F, that realizes a trivialization above the set Z.base_set i, which is an open set in B.
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:
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 × F, but the topology is not the product one.
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.
Fiber bundle, topological bundle, vector bundle, local trivialization, structure group
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.
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 the domain of a bundle trivialization, the projection is continuous
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 first projection in a product is a topological fiber bundle.
The second projection in a product is a topological fiber bundle.
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.
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
Total space of a topological bundle created from core. It is equal to B × F, but as it is not marked as reducible, typeclass inference will not infer the wrong topology, and will use the instance topological_fiber_bundle_core.to_topological_space with the right topology.
The projection from the total space of a topological fiber bundle core, on its base.
Local homeomorphism version of the trivialization change.
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.
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.
Local trivialization of a topological bundle created from core, as a local homeomorphism.
The composition of two local trivializations is the trivialization change Z.triv_change i j.
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.
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 local homeomorphism
Preferred local trivialization of a fiber bundle constructed from core, at a given point, as a bundle trivialization