Documentation

Mathlib.Topology.FiberBundle.Basic

Fiber bundles #

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.TotalSpace F E where E : B → Type* is a function associating to x : B the fiber over x. This type Bundle.TotalSpace F E is a type of pairs ⟨proj : B, snd : E proj⟩.

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

If all these conditions are satisfied, we register the typeclass FiberBundle 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 FiberBundleCore registering the trivialization changes, one gets the corresponding fiber bundle and projection.

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

Main definitions #

Basic definitions #

Construction of a bundle from trivializations #

Let Z : FiberBundleCore ι B F. Then we define

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 FiberBundle, with VectorBundle 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 ChartedSpace (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 ChartedSpace (B × F). But if the data of the trivializations is held in FiberBundle, then a fiber bundle with fiber F over base B can be a ChartedSpace (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 FiberBundleCore), 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 TangentSpace I x. One could fear issues as this composition goes from TangentSpace I x to TangentSpace 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 FiberBundleCore, we should thus choose for each x one specific trivialization around it. We include this choice in the definition of the FiberBundleCore, 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.TotalSpace F (fun 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 FiberBundleCore, the indexing type will be the same as for the initial bundle.

Tags #

Fiber bundle, topological bundle, structure group

General definition of fiber bundles #

class FiberBundle {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F] (E : BType u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] :
Type (max (max u_2 u_3) u_5)

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.

Instances
    theorem FiberBundle.totalSpaceMk_inducing' {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [self : FiberBundle F E] (b : B) :
    theorem FiberBundle.mem_baseSet_trivializationAt' {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [self : FiberBundle F E] (b : B) :
    theorem FiberBundle.trivialization_mem_atlas' {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [self : FiberBundle F E] (b : B) :
    FiberBundle.trivializationAt' b FiberBundle.trivializationAtlas'
    @[reducible, inline]
    abbrev FiberBundle.trivializationAtlas {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F] (E : BType u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] :
    Set (Trivialization F Bundle.TotalSpace.proj)

    Atlas of a fiber bundle.

    Equations
    Instances For
      @[reducible, inline]
      abbrev FiberBundle.trivializationAt {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F] (E : BType u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (b : B) :
      Trivialization F Bundle.TotalSpace.proj

      Trivialization of a fiber bundle at a point.

      Equations
      Instances For
        theorem FiberBundle.mem_baseSet_trivializationAt {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F] (E : BType u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (b : B) :
        b (trivializationAt F E b).baseSet
        theorem memTrivializationAtlas_iff {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) :
        class MemTrivializationAtlas {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) :

        Given a type E equipped with a fiber bundle structure, this is a Prop typeclass for trivializations of E, expressing that a trivialization is in the designated atlas for the bundle. This is needed because lemmas about the linearity of trivializations or the continuity (as functions to F →L[R] F, where F is the model fiber) of the transition functions are only expected to hold for trivializations in the designated atlas.

        Instances
          theorem MemTrivializationAtlas.out {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] {e : Trivialization F Bundle.TotalSpace.proj} [self : MemTrivializationAtlas e] :
          Equations
          • =
          theorem FiberBundle.map_proj_nhds {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (x : Bundle.TotalSpace F E) :
          Filter.map Bundle.TotalSpace.proj (nhds x) = nhds x.proj
          theorem FiberBundle.continuous_proj {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F] (E : BType u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] :
          Continuous Bundle.TotalSpace.proj

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

          theorem FiberBundle.isOpenMap_proj {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F] (E : BType u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] :
          IsOpenMap Bundle.TotalSpace.proj

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

          theorem FiberBundle.surjective_proj {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F] (E : BType u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [Nonempty F] :
          Function.Surjective Bundle.TotalSpace.proj

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

          theorem FiberBundle.quotientMap_proj {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F] (E : BType u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [Nonempty F] :
          QuotientMap Bundle.TotalSpace.proj

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

          @[simp]
          theorem FiberBundle.mem_trivializationAt_proj_source {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] {x : Bundle.TotalSpace F E} :
          x (trivializationAt F E x.proj).source
          theorem FiberBundle.trivializationAt_proj_fst {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] {x : Bundle.TotalSpace F E} :
          ((trivializationAt F E x.proj) x).1 = x.proj
          theorem FiberBundle.continuousWithinAt_totalSpace {B : Type u_2} (F : Type u_3) {X : Type u_4} [TopologicalSpace X] [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (f : XBundle.TotalSpace F E) {s : Set X} {x₀ : X} :
          ContinuousWithinAt f s x₀ ContinuousWithinAt (fun (x : X) => (f x).proj) s x₀ ContinuousWithinAt (fun (x : X) => ((trivializationAt F E (f x₀).proj) (f x)).2) s x₀

          Characterization of continuous functions (at a point, within a set) into a fiber bundle.

          theorem FiberBundle.continuousAt_totalSpace {B : Type u_2} (F : Type u_3) {X : Type u_4} [TopologicalSpace X] [TopologicalSpace B] [TopologicalSpace F] {E : BType u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (f : XBundle.TotalSpace F E) {x₀ : X} :
          ContinuousAt f x₀ ContinuousAt (fun (x : X) => (f x).proj) x₀ ContinuousAt (fun (x : X) => ((trivializationAt F E (f x₀).proj) (f x)).2) x₀

          Characterization of continuous functions (at a point) into a fiber bundle.

          theorem FiberBundle.exists_trivialization_Icc_subset {B : Type u_2} (F : Type u_3) [TopologicalSpace B] [TopologicalSpace F] (E : BType u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [ConditionallyCompleteLinearOrder B] [OrderTopology B] [FiberBundle F E] (a : B) (b : B) :
          ∃ (e : Trivialization F Bundle.TotalSpace.proj), Set.Icc a b e.baseSet

          If E is a fiber bundle over a conditionally complete linear order, then it is trivial over any closed interval.

          Core construction for constructing fiber bundles #

          structure FiberBundleCore (ι : Type u_5) (B : Type u_6) [TopologicalSpace B] (F : Type u_7) [TopologicalSpace F] :
          Type (max (max u_5 u_6) u_7)

          Core data defining a locally trivial 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 baseSet i for each i : ι. Trivialization changes from i to j are given by continuous maps coordChange i j from baseSet i ∩ baseSet j to the set of homeomorphisms of F, but we express them as maps B → F → F and require continuity on (baseSet i ∩ baseSet j) × F to avoid the topology on the space of continuous maps on F.

          • baseSet : ιSet B
          • isOpen_baseSet : ∀ (i : ι), IsOpen (self.baseSet i)
          • indexAt : Bι
          • mem_baseSet_at : ∀ (x : B), x self.baseSet (self.indexAt x)
          • coordChange : ιιBFF
          • coordChange_self : ∀ (i : ι), xself.baseSet i, ∀ (v : F), self.coordChange i i x v = v
          • continuousOn_coordChange : ∀ (i j : ι), ContinuousOn (fun (p : B × F) => self.coordChange i j p.1 p.2) ((self.baseSet i self.baseSet j) ×ˢ Set.univ)
          • coordChange_comp : ∀ (i j k : ι), xself.baseSet i self.baseSet j self.baseSet k, ∀ (v : F), self.coordChange j k x (self.coordChange i j x v) = self.coordChange i k x v
          Instances For
            theorem FiberBundleCore.isOpen_baseSet {ι : Type u_5} {B : Type u_6} [TopologicalSpace B] {F : Type u_7} [TopologicalSpace F] (self : FiberBundleCore ι B F) (i : ι) :
            IsOpen (self.baseSet i)
            theorem FiberBundleCore.mem_baseSet_at {ι : Type u_5} {B : Type u_6} [TopologicalSpace B] {F : Type u_7} [TopologicalSpace F] (self : FiberBundleCore ι B F) (x : B) :
            x self.baseSet (self.indexAt x)
            theorem FiberBundleCore.coordChange_self {ι : Type u_5} {B : Type u_6} [TopologicalSpace B] {F : Type u_7} [TopologicalSpace F] (self : FiberBundleCore ι B F) (i : ι) (x : B) :
            x self.baseSet i∀ (v : F), self.coordChange i i x v = v
            theorem FiberBundleCore.continuousOn_coordChange {ι : Type u_5} {B : Type u_6} [TopologicalSpace B] {F : Type u_7} [TopologicalSpace F] (self : FiberBundleCore ι B F) (i : ι) (j : ι) :
            ContinuousOn (fun (p : B × F) => self.coordChange i j p.1 p.2) ((self.baseSet i self.baseSet j) ×ˢ Set.univ)
            theorem FiberBundleCore.coordChange_comp {ι : Type u_5} {B : Type u_6} [TopologicalSpace B] {F : Type u_7} [TopologicalSpace F] (self : FiberBundleCore ι B F) (i : ι) (j : ι) (k : ι) (x : B) :
            x self.baseSet i self.baseSet j self.baseSet k∀ (v : F), self.coordChange j k x (self.coordChange i j x v) = self.coordChange i k x v
            def FiberBundleCore.Index {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (_Z : FiberBundleCore ι B F) :
            Type u_1

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

            Equations
            • _Z.Index = ι
            Instances For
              @[reducible]
              def FiberBundleCore.Base {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (_Z : FiberBundleCore ι B F) :
              Type u_2

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

              Equations
              • _Z.Base = B
              Instances For
                def FiberBundleCore.Fiber {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] :
                FiberBundleCore ι B FBType u_3

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

                Equations
                • x.Fiber _x = F
                Instances For
                  instance FiberBundleCore.topologicalSpaceFiber {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (x : B) :
                  TopologicalSpace (Z.Fiber x)
                  Equations
                  • Z.topologicalSpaceFiber x = inst
                  @[reducible, inline]
                  abbrev FiberBundleCore.TotalSpace {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) :
                  Type (max u_2 u_3)

                  The total space of the fiber bundle, as a convenience function for dot notation. It is by definition equal to Bundle.TotalSpace F Z.Fiber.

                  Equations
                  Instances For
                    @[reducible]
                    def FiberBundleCore.proj {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) :
                    Z.TotalSpaceB

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

                    Equations
                    • Z.proj = Bundle.TotalSpace.proj
                    Instances For
                      def FiberBundleCore.trivChange {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (j : ι) :
                      PartialHomeomorph (B × F) (B × F)

                      Local homeomorphism version of the trivialization change.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem FiberBundleCore.mem_trivChange_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (j : ι) (p : B × F) :
                        p (Z.trivChange i j).source p.1 Z.baseSet i Z.baseSet j
                        def FiberBundleCore.localTrivAsPartialEquiv {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) :
                        PartialEquiv Z.TotalSpace (B × F)

                        Associate to a trivialization index i : ι the corresponding trivialization, i.e., a bijection between proj ⁻¹ (baseSet i) and baseSet 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 partial homeomorphism. For now, we only introduce the partial equivalence version, denoted with a prime. In further developments, avoid this auxiliary version, and use Z.local_triv instead.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem FiberBundleCore.mem_localTrivAsPartialEquiv_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (p : Z.TotalSpace) :
                          p (Z.localTrivAsPartialEquiv i).source p.proj Z.baseSet i
                          theorem FiberBundleCore.mem_localTrivAsPartialEquiv_target {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (p : B × F) :
                          p (Z.localTrivAsPartialEquiv i).target p.1 Z.baseSet i
                          theorem FiberBundleCore.localTrivAsPartialEquiv_apply {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (p : Z.TotalSpace) :
                          (Z.localTrivAsPartialEquiv i) p = (p.proj, Z.coordChange (Z.indexAt p.proj) i p.proj p.snd)
                          theorem FiberBundleCore.localTrivAsPartialEquiv_trans {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (j : ι) :
                          (Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j) (Z.trivChange i j).toPartialEquiv

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

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          theorem FiberBundleCore.open_source' {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) :
                          IsOpen (Z.localTrivAsPartialEquiv i).source
                          def FiberBundleCore.localTriv {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B 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
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def FiberBundleCore.localTrivAt {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (b : B) :
                            Trivialization F Bundle.TotalSpace.proj

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

                            Equations
                            • Z.localTrivAt b = Z.localTriv (Z.indexAt b)
                            Instances For
                              @[simp]
                              theorem FiberBundleCore.localTrivAt_def {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (b : B) :
                              Z.localTriv (Z.indexAt b) = Z.localTrivAt b
                              theorem FiberBundleCore.localTrivAt_snd {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (b : B) (p : Bundle.TotalSpace F Z.Fiber) :
                              ((Z.localTrivAt b) p).2 = Z.coordChange (Z.indexAt p.proj) (Z.indexAt b) p.proj p.snd
                              theorem FiberBundleCore.continuous_const_section {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (v : F) (h : ∀ (i j : ι), xZ.baseSet i Z.baseSet j, Z.coordChange i j x v = v) :
                              Continuous (let_fun this := fun (x : B) => { proj := x, snd := v }; this)

                              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 FiberBundleCore.localTrivAsPartialEquiv_coe {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) :
                              (Z.localTrivAsPartialEquiv i) = (Z.localTriv i)
                              @[simp]
                              theorem FiberBundleCore.localTrivAsPartialEquiv_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) :
                              (Z.localTrivAsPartialEquiv i).source = (Z.localTriv i).source
                              @[simp]
                              theorem FiberBundleCore.localTrivAsPartialEquiv_target {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) :
                              (Z.localTrivAsPartialEquiv i).target = (Z.localTriv i).target
                              @[simp]
                              theorem FiberBundleCore.localTrivAsPartialEquiv_symm {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) :
                              (Z.localTrivAsPartialEquiv i).symm = (Z.localTriv i).symm
                              @[simp]
                              theorem FiberBundleCore.baseSet_at {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) :
                              Z.baseSet i = (Z.localTriv i).baseSet
                              @[simp]
                              theorem FiberBundleCore.localTriv_apply {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (p : Z.TotalSpace) :
                              (Z.localTriv i) p = (p.proj, Z.coordChange (Z.indexAt p.proj) i p.proj p.snd)
                              @[simp]
                              theorem FiberBundleCore.localTrivAt_apply {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (p : Z.TotalSpace) :
                              (Z.localTrivAt p.proj) p = (p.proj, p.snd)
                              @[simp]
                              theorem FiberBundleCore.localTrivAt_apply_mk {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (b : B) (a : F) :
                              (Z.localTrivAt b) { proj := b, snd := a } = (b, a)
                              @[simp]
                              theorem FiberBundleCore.mem_localTriv_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (p : Z.TotalSpace) :
                              p (Z.localTriv i).source p.proj (Z.localTriv i).baseSet
                              @[simp]
                              theorem FiberBundleCore.mem_localTrivAt_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (p : Z.TotalSpace) (b : B) :
                              p (Z.localTrivAt b).source p.proj (Z.localTrivAt b).baseSet
                              @[simp]
                              theorem FiberBundleCore.mem_localTriv_target {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (p : B × F) :
                              p (Z.localTriv i).target p.1 (Z.localTriv i).baseSet
                              @[simp]
                              theorem FiberBundleCore.mem_localTrivAt_target {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (p : B × F) (b : B) :
                              p (Z.localTrivAt b).target p.1 (Z.localTrivAt b).baseSet
                              @[simp]
                              theorem FiberBundleCore.localTriv_symm_apply {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (p : B × F) :
                              (Z.localTriv i).symm p = { proj := p.1, snd := Z.coordChange i (Z.indexAt p.1) p.1 p.2 }
                              @[simp]
                              theorem FiberBundleCore.mem_localTrivAt_baseSet {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (b : B) :
                              b (Z.localTrivAt b).baseSet
                              theorem FiberBundleCore.mk_mem_localTrivAt_source {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (b : B) (a : F) :
                              { proj := b, snd := a } (Z.localTrivAt b).source
                              instance FiberBundleCore.fiberBundle {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) :
                              FiberBundle F Z.Fiber

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

                              Equations
                              • One or more equations did not get rendered due to their size.

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

                              theorem FiberBundleCore.continuous_proj {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) :
                              Continuous Z.proj

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

                              theorem FiberBundleCore.isOpenMap_proj {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) :
                              IsOpenMap Z.proj

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

                              Prebundle construction for constructing fiber bundles #

                              structure FiberPrebundle {B : Type u_2} (F : Type u_3) (E : BType u_5) [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] :
                              Type (max (max u_2 u_3) u_5)

                              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 partial equivalences are also partial homeomorphisms and hence local trivializations.

                              • pretrivializationAtlas : Set (Pretrivialization F Bundle.TotalSpace.proj)
                              • pretrivializationAt : BPretrivialization F Bundle.TotalSpace.proj
                              • mem_base_pretrivializationAt : ∀ (x : B), x (self.pretrivializationAt x).baseSet
                              • pretrivialization_mem_atlas : ∀ (x : B), self.pretrivializationAt x self.pretrivializationAtlas
                              • continuous_trivChange : eself.pretrivializationAtlas, e'self.pretrivializationAtlas, ContinuousOn (e e'.symm) (e'.target e'.symm ⁻¹' e.source)
                              • totalSpaceMk_inducing : ∀ (b : B), Inducing ((self.pretrivializationAt b) Bundle.TotalSpace.mk b)
                              Instances For
                                theorem FiberPrebundle.mem_base_pretrivializationAt {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (self : FiberPrebundle F E) (x : B) :
                                x (self.pretrivializationAt x).baseSet
                                theorem FiberPrebundle.pretrivialization_mem_atlas {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (self : FiberPrebundle F E) (x : B) :
                                self.pretrivializationAt x self.pretrivializationAtlas
                                theorem FiberPrebundle.continuous_trivChange {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (self : FiberPrebundle F E) (e : Pretrivialization F Bundle.TotalSpace.proj) :
                                e self.pretrivializationAtlase'self.pretrivializationAtlas, ContinuousOn (e e'.symm) (e'.target e'.symm ⁻¹' e.source)
                                theorem FiberPrebundle.totalSpaceMk_inducing {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (self : FiberPrebundle F E) (b : B) :
                                Inducing ((self.pretrivializationAt b) Bundle.TotalSpace.mk b)
                                def FiberPrebundle.totalSpaceTopology {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) :

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

                                Equations
                                Instances For
                                  theorem FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) {e : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) :
                                  ContinuousOn (e.symm) e.target
                                  theorem FiberPrebundle.isOpen_source {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (e : Pretrivialization F Bundle.TotalSpace.proj) :
                                  IsOpen e.source
                                  theorem FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (e : Pretrivialization F Bundle.TotalSpace.proj) (e' : Pretrivialization F Bundle.TotalSpace.proj) (he' : e' a.pretrivializationAtlas) :
                                  IsOpen (e'.target e'.symm ⁻¹' e.source)
                                  def FiberPrebundle.trivializationOfMemPretrivializationAtlas {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) {e : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) :
                                  Trivialization F Bundle.TotalSpace.proj

                                  Promotion from a Pretrivialization to a Trivialization.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem FiberPrebundle.mem_pretrivializationAt_source {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (b : B) (x : E b) :
                                    { proj := b, snd := x } (a.pretrivializationAt b).source
                                    @[simp]
                                    theorem FiberPrebundle.totalSpaceMk_preimage_source {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (b : B) :
                                    Bundle.TotalSpace.mk b ⁻¹' (a.pretrivializationAt b).source = Set.univ
                                    theorem FiberPrebundle.continuous_totalSpaceMk {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (b : B) :
                                    theorem FiberPrebundle.inducing_totalSpaceMk_of_inducing_comp {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (b : B) (h : Inducing ((a.pretrivializationAt b) Bundle.TotalSpace.mk b)) :
                                    def FiberPrebundle.toFiberBundle {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) :

                                    Make a FiberBundle from a FiberPrebundle. Concretely this means that, given a FiberPrebundle 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 FiberPrebundle.totalSpaceTopology, these "pretrivializations" are actually "trivializations" (i.e., homeomorphisms with respect to the constructed topology).

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem FiberPrebundle.continuous_proj {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) :
                                      Continuous Bundle.TotalSpace.proj
                                      instance FiberPrebundle.instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) {e₀ : Pretrivialization F Bundle.TotalSpace.proj} (he₀ : e₀ a.pretrivializationAtlas) :
                                      MemTrivializationAtlas (a.trivializationOfMemPretrivializationAtlas he₀)
                                      Equations
                                      • =
                                      theorem FiberPrebundle.continuousOn_of_comp_right {B : Type u_2} {F : Type u_3} {E : BType u_5} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) {X : Type u_6} [TopologicalSpace X] {f : Bundle.TotalSpace F EX} {s : Set B} (hs : IsOpen s) (hf : bs, ContinuousOn (f (a.pretrivializationAt b).symm) ((s (a.pretrivializationAt b).baseSet) ×ˢ Set.univ)) :
                                      ContinuousOn f (Bundle.TotalSpace.proj ⁻¹' s)

                                      For a fiber bundle E over B constructed using the FiberPrebundle mechanism, continuity of a function TotalSpace F E → X on an open set s can be checked by precomposing at each point with the pretrivialization used for the construction at that point.