Documentation

Mathlib.Data.Bundle

Bundle #

Basic data structure to implement fiber bundles, vector bundles (maybe fibrations?), etc. This file should contain all possible results that do not involve any topology.

We represent a bundle E over a base space B as a dependent type E : B → Type*.

We define Bundle.TotalSpace F E to be the type of pairs ⟨b, x⟩, where b : B and x : E b. This type is isomorphic to Σ x, E x and uses an extra argument F for reasons explained below. In general, the constructions of fiber bundles we will make will be of this form.

Main Definitions #

Implementation Notes #

References #

theorem Bundle.TotalSpace.ext_iff {B : Type u_1} {F : Type u_4} {E : BType u_5} (x : Bundle.TotalSpace F E) (y : Bundle.TotalSpace F E) :
x = y x.proj = y.proj HEq x.snd y.snd
theorem Bundle.TotalSpace.ext {B : Type u_1} {F : Type u_4} {E : BType u_5} (x : Bundle.TotalSpace F E) (y : Bundle.TotalSpace F E) (proj : x.proj = y.proj) (snd : HEq x.snd y.snd) :
x = y
structure Bundle.TotalSpace {B : Type u_1} (F : Type u_4) (E : BType u_5) :
Type (max u_1 u_5)

Bundle.TotalSpace F E is the total space of the bundle. It consists of pairs (proj : B, snd : E proj).

Instances For
    instance Bundle.instInhabitedTotalSpaceOfDefault {B : Type u_1} {F : Type u_2} (E : BType u_3) [Inhabited B] [Inhabited (E default)] :
    Equations

    Bundle.TotalSpace.proj is the canonical projection Bundle.TotalSpace F E → B from the total space to the base space.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible, inline]
      abbrev Bundle.TotalSpace.mk' {B : Type u_1} {E : BType u_3} (F : Type u_4) (x : B) (y : E x) :
      Equations
      Instances For
        theorem Bundle.TotalSpace.mk_cast {B : Type u_1} {F : Type u_2} {E : BType u_3} {x : B} {x' : B} (h : x = x') (b : E x) :
        Bundle.TotalSpace.mk' F x' (cast b) = { proj := x, snd := b }
        @[simp]
        theorem Bundle.TotalSpace.mk_inj {B : Type u_1} {F : Type u_2} {E : BType u_3} {b : B} {y : E b} {y' : E b} :
        theorem Bundle.TotalSpace.mk_injective {B : Type u_1} {F : Type u_2} {E : BType u_3} (b : B) :
        instance Bundle.instCoeTCTotalSpace {B : Type u_1} {F : Type u_2} {E : BType u_3} {x : B} :
        Equations
        theorem Bundle.TotalSpace.eta {B : Type u_1} {F : Type u_2} {E : BType u_3} (z : Bundle.TotalSpace F E) :
        { proj := z.proj, snd := z.snd } = z
        @[simp]
        theorem Bundle.TotalSpace.exists {B : Type u_1} {F : Type u_2} {E : BType u_3} {p : Bundle.TotalSpace F EProp} :
        (∃ (x : Bundle.TotalSpace F E), p x) ∃ (b : B) (y : E b), p { proj := b, snd := y }
        @[simp]
        theorem Bundle.TotalSpace.range_mk {B : Type u_1} {F : Type u_2} {E : BType u_3} (b : B) :
        Set.range (Bundle.TotalSpace.mk b) = Bundle.TotalSpace.proj ⁻¹' {b}

        Notation for the direct sum of two bundles over the same base.

        Equations
        Instances For
          @[reducible]
          def Bundle.Trivial (B : Type u_4) (F : Type u_5) :
          BType u_5

          Bundle.Trivial B F is the trivial bundle over B of fiber F.

          Equations
          Instances For

            The trivial bundle, unlike other bundles, has a canonical projection on the fiber.

            Equations
            Instances For
              @[simp]
              theorem Bundle.TotalSpace.toProd_apply (B : Type u_4) (F : Type u_5) (x : Bundle.TotalSpace F fun (x : B) => F) :
              (Bundle.TotalSpace.toProd B F) x = (x.proj, x.snd)
              @[simp]
              theorem Bundle.TotalSpace.toProd_symm_apply_snd (B : Type u_4) (F : Type u_5) (x : B × F) :
              ((Bundle.TotalSpace.toProd B F).symm x).snd = x.2
              @[simp]
              theorem Bundle.TotalSpace.toProd_symm_apply_proj (B : Type u_4) (F : Type u_5) (x : B × F) :
              ((Bundle.TotalSpace.toProd B F).symm x).proj = x.1
              def Bundle.TotalSpace.toProd (B : Type u_4) (F : Type u_5) :
              (Bundle.TotalSpace F fun (x : B) => F) B × F

              A trivial bundle is equivalent to the product B × F.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Bundle.Pullback {B : Type u_1} {B' : Type u_4} (f : B'B) (E : BType u_5) :
                B'Type u_5

                The pullback of a bundle E over a base B under a map f : B' → B, denoted by Bundle.Pullback f E or f *ᵖ E, is the bundle over B' whose fiber over b' is E (f b').

                Equations
                Instances For

                  The pullback of a bundle E over a base B under a map f : B' → B, denoted by Bundle.Pullback f E or f *ᵖ E, is the bundle over B' whose fiber over b' is E (f b').

                  Equations
                  Instances For
                    instance Bundle.instNonemptyPullback {B : Type u_1} {E : BType u_3} {B' : Type u_4} {f : B'B} {x : B'} [Nonempty (E (f x))] :
                    Nonempty ((f *ᵖ E) x)
                    Equations
                    • = inst
                    def Bundle.pullbackTotalSpaceEmbedding {B : Type u_1} {F : Type u_2} {E : BType u_3} {B' : Type u_4} (f : B'B) :

                    Natural embedding of the total space of f *ᵖ E into B' × TotalSpace F E.

                    Equations
                    Instances For
                      @[simp]
                      theorem Bundle.Pullback.lift_proj {B : Type u_1} {F : Type u_2} {E : BType u_3} {B' : Type u_4} (f : B'B) :
                      ∀ (a : Bundle.TotalSpace F (f *ᵖ E)), (Bundle.Pullback.lift f a).proj = f a.proj
                      @[simp]
                      theorem Bundle.Pullback.lift_snd {B : Type u_1} {F : Type u_2} {E : BType u_3} {B' : Type u_4} (f : B'B) :
                      ∀ (a : Bundle.TotalSpace F (f *ᵖ E)), (Bundle.Pullback.lift f a).snd = a.snd
                      def Bundle.Pullback.lift {B : Type u_1} {F : Type u_2} {E : BType u_3} {B' : Type u_4} (f : B'B) :

                      The base map f : B' → B lifts to a canonical map on the total spaces.

                      Equations
                      Instances For
                        @[simp]
                        theorem Bundle.Pullback.lift_mk {B : Type u_1} {F : Type u_2} {E : BType u_3} {B' : Type u_4} (f : B'B) (x : B') (y : E (f x)) :
                        Bundle.Pullback.lift f (Bundle.TotalSpace.mk' F x y) = { proj := f x, snd := y }