Documentation

Mathlib.Topology.FiberBundle.Constructions

Standard constructions on fiber bundles #

This file contains several standard constructions on fiber bundles:

Tags #

fiber bundle, fibre bundle, fiberwise product, pullback

The trivial bundle #

@[deprecated Bundle.Trivial.isInducing_toProd]

Alias of Bundle.Trivial.isInducing_toProd.

Homeomorphism between the total space of the trivial bundle and the Cartesian product.

Equations
Instances For
    def Bundle.Trivial.trivialization (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :
    Trivialization F Bundle.TotalSpace.proj

    Local trivialization for trivial bundle.

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

      Fiber bundle instance on the trivial bundle.

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

      Fibrewise product of two bundles #

      instance FiberBundle.Prod.topologicalSpace {B : Type u_1} (F₁ : Type u_2) (E₁ : B β†’ Type u_3) (Fβ‚‚ : Type u_4) (Eβ‚‚ : B β†’ Type u_5) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] :
      TopologicalSpace (Bundle.TotalSpace (F₁ Γ— Fβ‚‚) fun (x : B) => E₁ x Γ— Eβ‚‚ x)

      Equip the total space of the fiberwise product of two fiber bundles E₁, Eβ‚‚ with the induced topology from the diagonal embedding into TotalSpace F₁ E₁ Γ— TotalSpace Fβ‚‚ Eβ‚‚.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem FiberBundle.Prod.isInducing_diag {B : Type u_1} (F₁ : Type u_2) (E₁ : B β†’ Type u_3) (Fβ‚‚ : Type u_4) (Eβ‚‚ : B β†’ Type u_5) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] :
      Topology.IsInducing fun (p : Bundle.TotalSpace (F₁ Γ— Fβ‚‚) fun (x : B) => E₁ x Γ— Eβ‚‚ x) => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })

      The diagonal map from the total space of the fiberwise product of two fiber bundles E₁, Eβ‚‚ into TotalSpace F₁ E₁ Γ— TotalSpace Fβ‚‚ Eβ‚‚ is an inducing map.

      @[deprecated FiberBundle.Prod.isInducing_diag]
      theorem FiberBundle.Prod.inducing_diag {B : Type u_1} (F₁ : Type u_2) (E₁ : B β†’ Type u_3) (Fβ‚‚ : Type u_4) (Eβ‚‚ : B β†’ Type u_5) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] :
      Topology.IsInducing fun (p : Bundle.TotalSpace (F₁ Γ— Fβ‚‚) fun (x : B) => E₁ x Γ— Eβ‚‚ x) => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })

      Alias of FiberBundle.Prod.isInducing_diag.


      The diagonal map from the total space of the fiberwise product of two fiber bundles E₁, Eβ‚‚ into TotalSpace F₁ E₁ Γ— TotalSpace Fβ‚‚ Eβ‚‚ is an inducing map.

      def Trivialization.Prod.toFun' {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B β†’ Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {Fβ‚‚ : Type u_4} [TopologicalSpace Fβ‚‚] {Eβ‚‚ : B β†’ Type u_5} [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (eβ‚‚ : Trivialization Fβ‚‚ Bundle.TotalSpace.proj) :
      (Bundle.TotalSpace (F₁ Γ— Fβ‚‚) fun (x : B) => E₁ x Γ— Eβ‚‚ x) β†’ B Γ— F₁ Γ— Fβ‚‚

      Given trivializations e₁, eβ‚‚ for fiber bundles E₁, Eβ‚‚ over a base B, the forward function for the construction Trivialization.prod, the induced trivialization for the fiberwise product of E₁ and Eβ‚‚.

      Equations
      • Trivialization.Prod.toFun' e₁ eβ‚‚ p = (p.proj, (↑e₁ { proj := p.proj, snd := p.snd.1 }).2, (↑eβ‚‚ { proj := p.proj, snd := p.snd.2 }).2)
      Instances For
        theorem Trivialization.Prod.continuous_to_fun {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B β†’ Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {Fβ‚‚ : Type u_4} [TopologicalSpace Fβ‚‚] {Eβ‚‚ : B β†’ Type u_5} [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {eβ‚‚ : Trivialization Fβ‚‚ Bundle.TotalSpace.proj} :
        ContinuousOn (Trivialization.Prod.toFun' e₁ eβ‚‚) (Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ eβ‚‚.baseSet))
        noncomputable def Trivialization.Prod.invFun' {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B β†’ Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {Fβ‚‚ : Type u_4} [TopologicalSpace Fβ‚‚] {Eβ‚‚ : B β†’ Type u_5} [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (eβ‚‚ : Trivialization Fβ‚‚ Bundle.TotalSpace.proj) [(x : B) β†’ Zero (E₁ x)] [(x : B) β†’ Zero (Eβ‚‚ x)] (p : B Γ— F₁ Γ— Fβ‚‚) :
        Bundle.TotalSpace (F₁ Γ— Fβ‚‚) fun (x : B) => E₁ x Γ— Eβ‚‚ x

        Given trivializations e₁, eβ‚‚ for fiber bundles E₁, Eβ‚‚ over a base B, the inverse function for the construction Trivialization.prod, the induced trivialization for the fiberwise product of E₁ and Eβ‚‚.

        Equations
        Instances For
          theorem Trivialization.Prod.left_inv {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B β†’ Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {Fβ‚‚ : Type u_4} [TopologicalSpace Fβ‚‚] {Eβ‚‚ : B β†’ Type u_5} [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {eβ‚‚ : Trivialization Fβ‚‚ Bundle.TotalSpace.proj} [(x : B) β†’ Zero (E₁ x)] [(x : B) β†’ Zero (Eβ‚‚ x)] {x : Bundle.TotalSpace (F₁ Γ— Fβ‚‚) fun (x : B) => E₁ x Γ— Eβ‚‚ x} (h : x ∈ Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ eβ‚‚.baseSet)) :
          Trivialization.Prod.invFun' e₁ eβ‚‚ (Trivialization.Prod.toFun' e₁ eβ‚‚ x) = x
          theorem Trivialization.Prod.right_inv {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B β†’ Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {Fβ‚‚ : Type u_4} [TopologicalSpace Fβ‚‚] {Eβ‚‚ : B β†’ Type u_5} [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {eβ‚‚ : Trivialization Fβ‚‚ Bundle.TotalSpace.proj} [(x : B) β†’ Zero (E₁ x)] [(x : B) β†’ Zero (Eβ‚‚ x)] {x : B Γ— F₁ Γ— Fβ‚‚} (h : x ∈ (e₁.baseSet ∩ eβ‚‚.baseSet) Γ—Λ’ Set.univ) :
          Trivialization.Prod.toFun' e₁ eβ‚‚ (Trivialization.Prod.invFun' e₁ eβ‚‚ x) = x
          theorem Trivialization.Prod.continuous_inv_fun {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B β†’ Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {Fβ‚‚ : Type u_4} [TopologicalSpace Fβ‚‚] {Eβ‚‚ : B β†’ Type u_5} [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {eβ‚‚ : Trivialization Fβ‚‚ Bundle.TotalSpace.proj} [(x : B) β†’ Zero (E₁ x)] [(x : B) β†’ Zero (Eβ‚‚ x)] :
          ContinuousOn (Trivialization.Prod.invFun' e₁ eβ‚‚) ((e₁.baseSet ∩ eβ‚‚.baseSet) Γ—Λ’ Set.univ)
          noncomputable def Trivialization.prod {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B β†’ Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {Fβ‚‚ : Type u_4} [TopologicalSpace Fβ‚‚] {Eβ‚‚ : B β†’ Type u_5} [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (eβ‚‚ : Trivialization Fβ‚‚ Bundle.TotalSpace.proj) [(x : B) β†’ Zero (E₁ x)] [(x : B) β†’ Zero (Eβ‚‚ x)] :
          Trivialization (F₁ Γ— Fβ‚‚) Bundle.TotalSpace.proj

          Given trivializations e₁, eβ‚‚ for bundle types E₁, Eβ‚‚ over a base B, the induced trivialization for the fiberwise product of E₁ and Eβ‚‚, whose base set is e₁.baseSet ∩ eβ‚‚.baseSet.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem Trivialization.baseSet_prod {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B β†’ Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {Fβ‚‚ : Type u_4} [TopologicalSpace Fβ‚‚] {Eβ‚‚ : B β†’ Type u_5} [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (eβ‚‚ : Trivialization Fβ‚‚ Bundle.TotalSpace.proj) [(x : B) β†’ Zero (E₁ x)] [(x : B) β†’ Zero (Eβ‚‚ x)] :
            (e₁.prod eβ‚‚).baseSet = e₁.baseSet ∩ eβ‚‚.baseSet
            theorem Trivialization.prod_symm_apply {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B β†’ Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {Fβ‚‚ : Type u_4} [TopologicalSpace Fβ‚‚] {Eβ‚‚ : B β†’ Type u_5} [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (eβ‚‚ : Trivialization Fβ‚‚ Bundle.TotalSpace.proj) [(x : B) β†’ Zero (E₁ x)] [(x : B) β†’ Zero (Eβ‚‚ x)] (x : B) (w₁ : F₁) (wβ‚‚ : Fβ‚‚) :
            ↑(e₁.prod eβ‚‚).symm (x, w₁, wβ‚‚) = { proj := x, snd := (e₁.symm x w₁, eβ‚‚.symm x wβ‚‚) }
            noncomputable instance FiberBundle.prod {B : Type u_1} [TopologicalSpace B] (F₁ : Type u_2) [TopologicalSpace F₁] (E₁ : B β†’ Type u_3) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (Fβ‚‚ : Type u_4) [TopologicalSpace Fβ‚‚] (Eβ‚‚ : B β†’ Type u_5) [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] [(x : B) β†’ Zero (E₁ x)] [(x : B) β†’ Zero (Eβ‚‚ x)] [(x : B) β†’ TopologicalSpace (E₁ x)] [(x : B) β†’ TopologicalSpace (Eβ‚‚ x)] [FiberBundle F₁ E₁] [FiberBundle Fβ‚‚ Eβ‚‚] :
            FiberBundle (F₁ Γ— Fβ‚‚) fun (x : B) => E₁ x Γ— Eβ‚‚ x

            The product of two fiber bundles is a fiber bundle.

            Equations
            • One or more equations did not get rendered due to their size.
            theorem instMemTrivializationAtlasProdProd {B : Type u_1} [TopologicalSpace B] (F₁ : Type u_2) [TopologicalSpace F₁] (E₁ : B β†’ Type u_3) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (Fβ‚‚ : Type u_4) [TopologicalSpace Fβ‚‚] (Eβ‚‚ : B β†’ Type u_5) [TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] [(x : B) β†’ Zero (E₁ x)] [(x : B) β†’ Zero (Eβ‚‚ x)] [(x : B) β†’ TopologicalSpace (E₁ x)] [(x : B) β†’ TopologicalSpace (Eβ‚‚ x)] [FiberBundle F₁ E₁] [FiberBundle Fβ‚‚ Eβ‚‚] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {eβ‚‚ : Trivialization Fβ‚‚ Bundle.TotalSpace.proj} [MemTrivializationAtlas e₁] [MemTrivializationAtlas eβ‚‚] :
            MemTrivializationAtlas (e₁.prod eβ‚‚)

            Pullbacks of fiber bundles #

            instance instTopologicalSpacePullback {B : Type u} (E : B β†’ Type w₁) {B' : Type wβ‚‚} (f : B' β†’ B) [(x : B) β†’ TopologicalSpace (E x)] (x : B') :
            Equations
            theorem pullbackTopology_def {B : Type u_1} (F : Type u_2) (E : B β†’ Type u_3) {B' : Type u_4} (f : B' β†’ B) [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] :
            pullbackTopology F E f = TopologicalSpace.induced Bundle.TotalSpace.proj inst✝ βŠ“ TopologicalSpace.induced (Bundle.Pullback.lift f) inst✝¹
            @[irreducible]
            def pullbackTopology {B : Type u_1} (F : Type u_2) (E : B β†’ Type u_3) {B' : Type u_4} (f : B' β†’ B) [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] :

            Definition of Pullback.TotalSpace.topologicalSpace, which we make irreducible.

            Equations
            Instances For
              instance Pullback.TotalSpace.topologicalSpace {B : Type u} (F : Type v) (E : B β†’ Type w₁) {B' : Type wβ‚‚} (f : B' β†’ B) [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] :

              The topology on the total space of a pullback bundle is the coarsest topology for which both the projections to the base and the map to the original bundle are continuous.

              Equations
              theorem Pullback.continuous_proj {B : Type u} (F : Type v) (E : B β†’ Type w₁) {B' : Type wβ‚‚} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] (f : B' β†’ B) :
              Continuous Bundle.TotalSpace.proj
              theorem Pullback.continuous_lift {B : Type u} (F : Type v) (E : B β†’ Type w₁) {B' : Type wβ‚‚} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] (f : B' β†’ B) :
              theorem inducing_pullbackTotalSpaceEmbedding {B : Type u} (F : Type v) (E : B β†’ Type w₁) {B' : Type wβ‚‚} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] (f : B' β†’ B) :
              theorem Pullback.continuous_totalSpaceMk {B : Type u} (F : Type v) (E : B β†’ Type w₁) {B' : Type wβ‚‚} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(x : B) β†’ TopologicalSpace (E x)] [FiberBundle F E] {f : B' β†’ B} {x : B'} :
              noncomputable def Trivialization.pullback {B : Type u} {F : Type v} {E : B β†’ Type w₁} {B' : Type wβ‚‚} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) β†’ Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F Bundle.TotalSpace.proj) (f : K) :
              Trivialization F Bundle.TotalSpace.proj

              A fiber bundle trivialization can be pulled back to a trivialization on the pullback bundle.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable instance FiberBundle.pullback {B : Type u} {F : Type v} {E : B β†’ Type w₁} {B' : Type wβ‚‚} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) β†’ Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] [(x : B) β†’ TopologicalSpace (E x)] [FiberBundle F E] (f : K) :
                FiberBundle F (⇑f *α΅– E)
                Equations
                • One or more equations did not get rendered due to their size.