Documentation

Mathlib.Topology.VectorBundle.Basic

Vector bundles #

In this file we define (topological) vector bundles.

Let B be the base space, let F be a normed space over a normed field R, and let E : B → Type* be a FiberBundle with fiber F, in which, for each x, the fiber E x is a topological vector space over R.

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

If these conditions are satisfied, we register the typeclass VectorBundle R F E.

We define constructions on vector bundles like pullbacks and direct sums in other files.

Main Definitions #

Implementation notes #

The implementation choices in the vector bundle definition are discussed in the "Implementation notes" section of Mathlib.Topology.FiberBundle.Basic.

Tags #

Vector bundle

class Pretrivialization.IsLinear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) :
  • linear : ∀ (b : B), b e.baseSetIsLinearMap R fun x => (e { proj := b, snd := x }).snd

A mixin class for Pretrivialization, stating that a pretrivialization is fiberwise linear with respect to given module structures on its fibers and the model fiber.

Instances
    theorem Pretrivialization.linear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] (e : Pretrivialization F Bundle.TotalSpace.proj) [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [Pretrivialization.IsLinear R e] {b : B} (hb : b e.baseSet) :
    IsLinearMap R fun x => (e { proj := b, snd := x }).snd
    @[simp]
    theorem Pretrivialization.symmₗ_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] (b : B) (y : F) :
    def Pretrivialization.symmₗ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] (b : B) :
    F →ₗ[R] E b

    A fiberwise linear inverse to e.

    Instances For
      @[simp]
      theorem Pretrivialization.linearEquivAt_symm_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] (b : B) (hb : b e.baseSet) :
      @[simp]
      theorem Pretrivialization.linearEquivAt_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] (b : B) (hb : b e.baseSet) :
      ↑(Pretrivialization.linearEquivAt R e b hb) = fun y => (e { proj := b, snd := y }).snd
      def Pretrivialization.linearEquivAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] (b : B) (hb : b e.baseSet) :
      E b ≃ₗ[R] F

      A pretrivialization for a vector bundle defines linear equivalences between the fibers and the model space.

      Instances For
        def Pretrivialization.linearMapAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] (b : B) :
        E b →ₗ[R] F

        A fiberwise linear map equal to e on e.baseSet.

        Instances For
          theorem Pretrivialization.coe_linearMapAt {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] (b : B) :
          ↑(Pretrivialization.linearMapAt R e b) = fun y => if b e.baseSet then (e { proj := b, snd := y }).snd else 0
          theorem Pretrivialization.coe_linearMapAt_of_mem {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] {b : B} (hb : b e.baseSet) :
          ↑(Pretrivialization.linearMapAt R e b) = fun y => (e { proj := b, snd := y }).snd
          theorem Pretrivialization.linearMapAt_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] {b : B} (y : E b) :
          ↑(Pretrivialization.linearMapAt R e b) y = if b e.baseSet then (e { proj := b, snd := y }).snd else 0
          theorem Pretrivialization.linearMapAt_def_of_mem {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] {b : B} (hb : b e.baseSet) :
          theorem Pretrivialization.linearMapAt_def_of_not_mem {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] {b : B} (hb : ¬b e.baseSet) :
          theorem Pretrivialization.linearMapAt_eq_zero {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] {b : B} (hb : ¬b e.baseSet) :
          theorem Pretrivialization.symmₗ_linearMapAt {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] {b : B} (hb : b e.baseSet) (y : E b) :
          theorem Pretrivialization.linearMapAt_symmₗ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) [Pretrivialization.IsLinear R e] {b : B} (hb : b e.baseSet) (y : F) :
          class Trivialization.IsLinear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) :
          • linear : ∀ (b : B), b e.baseSetIsLinearMap R fun x => (e { proj := b, snd := x }).snd

          A mixin class for Trivialization, stating that a trivialization is fiberwise linear with respect to given module structures on its fibers and the model fiber.

          Instances
            theorem Trivialization.linear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] (e : Trivialization F Bundle.TotalSpace.proj) [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [Trivialization.IsLinear R e] {b : B} (hb : b e.baseSet) :
            IsLinearMap R fun y => (e { proj := b, snd := y }).snd
            instance Trivialization.toPretrivialization.isLinear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] (e : Trivialization F Bundle.TotalSpace.proj) [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [Trivialization.IsLinear R e] :
            def Trivialization.linearEquivAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) (hb : b e.baseSet) :
            E b ≃ₗ[R] F

            A trivialization for a vector bundle defines linear equivalences between the fibers and the model space.

            Instances For
              @[simp]
              theorem Trivialization.linearEquivAt_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) (hb : b e.baseSet) (v : E b) :
              ↑(Trivialization.linearEquivAt R e b hb) v = (e { proj := b, snd := v }).snd
              @[simp]
              theorem Trivialization.linearEquivAt_symm_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) (hb : b e.baseSet) (v : F) :
              def Trivialization.symmₗ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) :
              F →ₗ[R] E b

              A fiberwise linear inverse to e.

              Instances For
                theorem Trivialization.coe_symmₗ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) :
                def Trivialization.linearMapAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) :
                E b →ₗ[R] F

                A fiberwise linear map equal to e on e.baseSet.

                Instances For
                  theorem Trivialization.coe_linearMapAt {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) :
                  ↑(Trivialization.linearMapAt R e b) = fun y => if b e.baseSet then (e { proj := b, snd := y }).snd else 0
                  theorem Trivialization.coe_linearMapAt_of_mem {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : b e.baseSet) :
                  ↑(Trivialization.linearMapAt R e b) = fun y => (e { proj := b, snd := y }).snd
                  theorem Trivialization.linearMapAt_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (y : E b) :
                  ↑(Trivialization.linearMapAt R e b) y = if b e.baseSet then (e { proj := b, snd := y }).snd else 0
                  theorem Trivialization.linearMapAt_def_of_mem {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : b e.baseSet) :
                  theorem Trivialization.linearMapAt_def_of_not_mem {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : ¬b e.baseSet) :
                  theorem Trivialization.symmₗ_linearMapAt {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : b e.baseSet) (y : E b) :
                  theorem Trivialization.linearMapAt_symmₗ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : b e.baseSet) (y : F) :
                  def Trivialization.coordChangeL (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] [Trivialization.IsLinear R e'] (b : B) :
                  F ≃L[R] F

                  A coordinate change function between two trivializations, as a continuous linear equivalence. Defined to be the identity when b does not lie in the base set of both trivializations.

                  Instances For
                    theorem Trivialization.coe_coordChangeL {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] [Trivialization.IsLinear R e'] {b : B} (hb : b e.baseSet e'.baseSet) :
                    ↑(Trivialization.coordChangeL R e e' b) = ↑(LinearEquiv.trans (LinearEquiv.symm (Trivialization.linearEquivAt R e b (_ : b e.baseSet))) (Trivialization.linearEquivAt R e' b (_ : b e'.baseSet)))
                    theorem Trivialization.coe_coordChangeL' {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] [Trivialization.IsLinear R e'] {b : B} (hb : b e.baseSet e'.baseSet) :
                    (Trivialization.coordChangeL R e e' b).toLinearEquiv = LinearEquiv.trans (LinearEquiv.symm (Trivialization.linearEquivAt R e b (_ : b e.baseSet))) (Trivialization.linearEquivAt R e' b (_ : b e'.baseSet))
                    theorem Trivialization.symm_coordChangeL {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] [Trivialization.IsLinear R e'] {b : B} (hb : b e'.baseSet e.baseSet) :
                    theorem Trivialization.coordChangeL_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] [Trivialization.IsLinear R e'] {b : B} (hb : b e.baseSet e'.baseSet) (y : F) :
                    ↑(Trivialization.coordChangeL R e e' b) y = (e' { proj := b, snd := Trivialization.symm e b y }).snd
                    theorem Trivialization.mk_coordChangeL {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] [Trivialization.IsLinear R e'] {b : B} (hb : b e.baseSet e'.baseSet) (y : F) :
                    (b, ↑(Trivialization.coordChangeL R e e' b) y) = e' { proj := b, snd := Trivialization.symm e b y }
                    theorem Trivialization.apply_symm_apply_eq_coordChangeL {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] [Trivialization.IsLinear R e'] {b : B} (hb : b e.baseSet e'.baseSet) (v : F) :
                    e' (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, v)) = (b, ↑(Trivialization.coordChangeL R e e' b) v)
                    theorem Trivialization.coordChangeL_apply' {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] [Trivialization.IsLinear R e'] {b : B} (hb : b e.baseSet e'.baseSet) (y : F) :
                    ↑(Trivialization.coordChangeL R e e' b) y = (e' (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, y))).snd

                    A version of Trivialization.coordChangeL_apply that fully unfolds coordChange. The right-hand side is ugly, but has good definitional properties for specifically defined trivializations.

                    theorem Trivialization.coordChangeL_symm_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [Semiring R] [TopologicalSpace F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [AddCommMonoid F] [Module R F] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] [Trivialization.IsLinear R e'] {b : B} (hb : b e.baseSet e'.baseSet) :
                    def Bundle.zeroSection {B : Type u_2} (F : Type u_3) (E : BType u_4) [(x : B) → Zero (E x)] :

                    The zero section of a vector bundle

                    Instances For
                      @[simp]
                      theorem Bundle.zeroSection_proj {B : Type u_2} (F : Type u_3) (E : BType u_4) [(x : B) → Zero (E x)] (x : B) :
                      (Bundle.zeroSection F E x).proj = x
                      @[simp]
                      theorem Bundle.zeroSection_snd {B : Type u_2} (F : Type u_3) (E : BType u_4) [(x : B) → Zero (E x)] (x : B) :
                      (Bundle.zeroSection F E x).snd = 0
                      class VectorBundle (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : BType u_4) [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] :

                      The space Bundle.TotalSpace F E (for E : B → Type* such that each E x is a topological vector space) has a topological vector space structure with fiber F (denoted with VectorBundle R F E) if around every point there is a fiber bundle trivialization which is linear in the fibers.

                      Instances
                        instance trivialization_linear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle R F E] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] :
                        theorem continuousOn_coordChange (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle R F E] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] :
                        ContinuousOn (fun b => ↑(Trivialization.coordChangeL R e e' b)) (e.baseSet e'.baseSet)
                        @[simp]
                        theorem Trivialization.continuousLinearMapAt_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) :
                        def Trivialization.continuousLinearMapAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) :
                        E b →L[R] F

                        Forward map of Trivialization.continuousLinearEquivAt (only propositionally equal), defined everywhere (0 outside domain).

                        Instances For
                          @[simp]
                          theorem Trivialization.symmL_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) :
                          def Trivialization.symmL (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) :
                          F →L[R] E b

                          Backwards map of Trivialization.continuousLinearEquivAt, defined everywhere.

                          Instances For
                            theorem Trivialization.symmL_continuousLinearMapAt {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : b e.baseSet) (y : E b) :
                            theorem Trivialization.continuousLinearMapAt_symmL {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : b e.baseSet) (y : F) :
                            @[simp]
                            theorem Trivialization.continuousLinearEquivAt_symm_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) (hb : b e.baseSet) :
                            @[simp]
                            theorem Trivialization.continuousLinearEquivAt_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) (hb : b e.baseSet) :
                            ↑(Trivialization.continuousLinearEquivAt R e b hb) = fun y => (e { proj := b, snd := y }).snd
                            def Trivialization.continuousLinearEquivAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) (hb : b e.baseSet) :
                            E b ≃L[R] F

                            In a vector bundle, a trivialization in the fiber (which is a priori only linear) is in fact a continuous linear equiv between the fibers and the model fiber.

                            Instances For
                              theorem Trivialization.coe_continuousLinearEquivAt_eq {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : b e.baseSet) :
                              theorem Trivialization.symm_continuousLinearEquivAt_eq {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {b : B} (hb : b e.baseSet) :
                              @[simp]
                              theorem Trivialization.continuousLinearEquivAt_apply' {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (x : Bundle.TotalSpace F E) (hx : x e.source) :
                              ↑(Trivialization.continuousLinearEquivAt R e x.proj (_ : x.proj e.baseSet)) x.snd = (e x).snd
                              theorem Trivialization.apply_eq_prod_continuousLinearEquivAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) (hb : b e.baseSet) (z : E b) :
                              e { proj := b, snd := z } = (b, ↑(Trivialization.continuousLinearEquivAt R e b hb) z)
                              theorem Trivialization.zeroSection (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] {x : B} (hx : x e.baseSet) :
                              e (Bundle.zeroSection F E x) = (x, 0)
                              theorem Trivialization.symm_apply_eq_mk_continuousLinearEquivAt_symm {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] (b : B) (hb : b e.baseSet) (z : F) :
                              ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, z) = { proj := b, snd := ↑(ContinuousLinearEquiv.symm (Trivialization.continuousLinearEquivAt R e b hb)) z }
                              theorem Trivialization.comp_continuousLinearEquivAt_eq_coord_change {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (e : Trivialization F Bundle.TotalSpace.proj) (e' : Trivialization F Bundle.TotalSpace.proj) [Trivialization.IsLinear R e] [Trivialization.IsLinear R e'] {b : B} (hb : b e.baseSet e'.baseSet) :

                              Constructing vector bundles #

                              structure VectorBundleCore (R : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] (ι : Type u_5) :
                              Type (max (max u_2 u_3) u_5)

                              Analogous construction of FiberBundleCore for vector bundles. This construction gives a way to construct vector bundles from a structure registering how trivialization changes act on fibers.

                              Instances For
                                def trivialVectorBundleCore (R : Type u_1) (B : Type u_2) (F : Type u_3) [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] (ι : Type u_5) [Inhabited ι] :

                                The trivial vector bundle core, in which all the changes of coordinates are the identity.

                                Instances For
                                  @[simp]
                                  @[simp]
                                  @[simp]

                                  Natural identification to a FiberBundleCore.

                                  Instances For
                                    def VectorBundleCore.Index {ι : Type u_5} :
                                    Type u_5

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

                                    Instances For
                                      @[reducible]
                                      def VectorBundleCore.Base {B : Type u_2} :
                                      Type u_2

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

                                      Instances For
                                        def VectorBundleCore.Fiber {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) :
                                        BType u_3

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

                                        Instances For
                                          instance VectorBundleCore.moduleFiber {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (x : B) :
                                          @[reducible]

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

                                          Instances For
                                            @[reducible]
                                            def VectorBundleCore.TotalSpace {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) :
                                            Type (max u_2 u_3)

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

                                            Instances For
                                              def VectorBundleCore.trivChange {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι) (j : ι) :
                                              LocalHomeomorph (B × F) (B × F)

                                              Local homeomorphism version of the trivialization change.

                                              Instances For
                                                @[simp]
                                                theorem VectorBundleCore.mem_trivChange_source {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι) (j : ι) (p : B × F) :

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

                                                @[simp]
                                                def VectorBundleCore.localTriv {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι) :
                                                Trivialization F Bundle.TotalSpace.proj

                                                One of the standard local trivializations of a vector bundle constructed from core, taken by considering this in particular as a fiber bundle constructed from core.

                                                Instances For
                                                  @[simp]
                                                  theorem VectorBundleCore.localTriv_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) {i : ι} (p : VectorBundleCore.TotalSpace Z) :
                                                  ↑(VectorBundleCore.localTriv Z i) p = (p.proj, ↑(VectorBundleCore.coordChange Z (VectorBundleCore.indexAt Z p.proj) i p.proj) p.snd)

                                                  The standard local trivializations of a vector bundle constructed from core are linear.

                                                  @[simp]
                                                  theorem VectorBundleCore.mem_localTriv_source {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι) (p : VectorBundleCore.TotalSpace Z) :
                                                  p (VectorBundleCore.localTriv Z i).toLocalHomeomorph.toLocalEquiv.source p.proj VectorBundleCore.baseSet Z i
                                                  @[simp]
                                                  theorem VectorBundleCore.baseSet_at {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι) :
                                                  @[simp]
                                                  theorem VectorBundleCore.mem_localTriv_target {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι) (p : B × F) :
                                                  p (VectorBundleCore.localTriv Z i).toLocalHomeomorph.toLocalEquiv.target p.fst (VectorBundleCore.localTriv Z i).baseSet
                                                  @[simp]
                                                  theorem VectorBundleCore.localTriv_symm_fst {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι) (p : B × F) :
                                                  ↑(LocalHomeomorph.symm (VectorBundleCore.localTriv Z i).toLocalHomeomorph) p = { proj := p.fst, snd := ↑(VectorBundleCore.coordChange Z i (VectorBundleCore.indexAt Z p.fst) p.fst) p.snd }
                                                  def VectorBundleCore.localTrivAt {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B) :
                                                  Trivialization F Bundle.TotalSpace.proj

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

                                                  Instances For
                                                    @[simp]
                                                    theorem VectorBundleCore.mem_source_at {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B) (a : F) :
                                                    { proj := b, snd := a } (VectorBundleCore.localTrivAt Z b).toLocalHomeomorph.toLocalEquiv.source
                                                    @[simp]
                                                    theorem VectorBundleCore.localTrivAt_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (p : VectorBundleCore.TotalSpace Z) :
                                                    ↑(VectorBundleCore.localTrivAt Z p.proj) p = (p.proj, p.snd)
                                                    @[simp]
                                                    theorem VectorBundleCore.localTrivAt_apply_mk {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B) (a : F) :
                                                    ↑(VectorBundleCore.localTrivAt Z b) { proj := b, snd := a } = (b, a)
                                                    @[simp]
                                                    theorem VectorBundleCore.mem_localTrivAt_baseSet {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B) :

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

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

                                                    Vector prebundle #

                                                    structure VectorPrebundle (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : BType u_4) [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] :
                                                    Type (max (max u_2 u_3) u_4)

                                                    This structure permits to define a vector bundle when trivializations are given as local equivalences but there is not yet a topology on the total space or the fibers. The total space is hence given a topology in such a way that there is a fiber bundle structure for which the local equivalences are also local homeomorphisms and hence vector bundle trivializations. The topology on the fibers is induced from the one on the total space.

                                                    The field exists_coordChange is stated as an existential statement (instead of 3 separate fields), since it depends on propositional information (namely e e' ∈ pretrivializationAtlas). This makes it inconvenient to explicitly define a coordChange function when constructing a VectorPrebundle.

                                                    Instances For
                                                      def VectorPrebundle.coordChange {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) {e : Pretrivialization F Bundle.TotalSpace.proj} {e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) (he' : e' a.pretrivializationAtlas) (b : B) :
                                                      F →L[R] F

                                                      A randomly chosen coordinate change on a VectorPrebundle, given by the field exists_coordChange.

                                                      Instances For
                                                        theorem VectorPrebundle.continuousOn_coordChange {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) {e : Pretrivialization F Bundle.TotalSpace.proj} {e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) (he' : e' a.pretrivializationAtlas) :
                                                        ContinuousOn (VectorPrebundle.coordChange a he he') (e.baseSet e'.baseSet)
                                                        theorem VectorPrebundle.coordChange_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) {e : Pretrivialization F Bundle.TotalSpace.proj} {e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) (he' : e' a.pretrivializationAtlas) {b : B} (hb : b e.baseSet e'.baseSet) (v : F) :
                                                        ↑(VectorPrebundle.coordChange a he he' b) v = (e' { proj := b, snd := Pretrivialization.symm e b v }).snd
                                                        theorem VectorPrebundle.mk_coordChange {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) {e : Pretrivialization F Bundle.TotalSpace.proj} {e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) (he' : e' a.pretrivializationAtlas) {b : B} (hb : b e.baseSet e'.baseSet) (v : F) :
                                                        (b, ↑(VectorPrebundle.coordChange a he he' b) v) = e' { proj := b, snd := Pretrivialization.symm e b v }
                                                        def VectorPrebundle.toFiberPrebundle {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) :

                                                        Natural identification of VectorPrebundle as a FiberPrebundle.

                                                        Instances For
                                                          def VectorPrebundle.totalSpaceTopology {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) :

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

                                                          Instances For
                                                            def VectorPrebundle.trivializationOfMemPretrivializationAtlas {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) {e : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) :
                                                            Trivialization F Bundle.TotalSpace.proj

                                                            Promotion from a Pretrivialization in the pretrivializationAtlas of a VectorPrebundle to a Trivialization.

                                                            Instances For
                                                              theorem VectorPrebundle.linear_trivializationOfMemPretrivializationAtlas {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) {e : Pretrivialization F Bundle.TotalSpace.proj} (he : e a.pretrivializationAtlas) :
                                                              theorem VectorPrebundle.mem_trivialization_at_source {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) (b : B) (x : E b) :
                                                              { proj := b, snd := x } (VectorPrebundle.pretrivializationAt a b).source
                                                              @[simp]
                                                              theorem VectorPrebundle.totalSpaceMk_preimage_source {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) (b : B) :
                                                              theorem VectorPrebundle.continuous_totalSpaceMk {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) (b : B) :
                                                              def VectorPrebundle.toFiberBundle {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) :

                                                              Make a FiberBundle from a VectorPrebundle; auxiliary construction for VectorPrebundle.toVectorBundle.

                                                              Instances For
                                                                theorem VectorPrebundle.toVectorBundle {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} [NontriviallyNormedField R] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module R (E x)] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle R F E) :

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

                                                                def ContinuousLinearMap.inCoordinates {B : Type u_2} (F : Type u_3) (E : BType u_4) [(x : B) → AddCommMonoid (E x)] [NormedAddCommGroup F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} [NontriviallyNormedField 𝕜₁] [NontriviallyNormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {B' : Type u_7} [TopologicalSpace B'] [NormedSpace 𝕜₁ F] [(x : B) → Module 𝕜₁ (E x)] [TopologicalSpace (Bundle.TotalSpace F E)] (F' : Type u_8) [NormedAddCommGroup F'] [NormedSpace 𝕜₂ F'] (E' : B'Type u_9) [(x : B') → AddCommMonoid (E' x)] [(x : B') → Module 𝕜₂ (E' x)] [TopologicalSpace (Bundle.TotalSpace F' E')] [FiberBundle F E] [VectorBundle 𝕜₁ F E] [(x : B') → TopologicalSpace (E' x)] [FiberBundle F' E'] [VectorBundle 𝕜₂ F' E'] (x₀ : B) (x : B) (y₀ : B') (y : B') (ϕ : E x →SL[σ] E' y) :
                                                                F →SL[σ] F'

                                                                When ϕ is a continuous (semi)linear map between the fibers E x and E' y of two vector bundles E and E', ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ is a coordinate change of this continuous linear map w.r.t. the chart around x₀ and the chart around y₀.

                                                                It is defined by composing ϕ with appropriate coordinate changes given by the vector bundles E and E'. We use the operations Trivialization.continuousLinearMapAt and Trivialization.symmL in the definition, instead of Trivialization.continuousLinearEquivAt, so that ContinuousLinearMap.inCoordinates is defined everywhere (but see ContinuousLinearMap.inCoordinates_eq).

                                                                This is the (second component of the) underlying function of a trivialization of the hom-bundle (see hom_trivializationAt_apply). However, note that ContinuousLinearMap.inCoordinates is defined even when x and y live in different base sets. Therefore, it is also convenient when working with the hom-bundle between pulled back bundles.

                                                                Instances For
                                                                  theorem ContinuousLinearMap.inCoordinates_eq {B : Type u_2} {F : Type u_3} (E : BType u_4) [(x : B) → AddCommMonoid (E x)] [NormedAddCommGroup F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} [NontriviallyNormedField 𝕜₁] [NontriviallyNormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {B' : Type u_7} [TopologicalSpace B'] [NormedSpace 𝕜₁ F] [(x : B) → Module 𝕜₁ (E x)] [TopologicalSpace (Bundle.TotalSpace F E)] {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜₂ F'] (E' : B'Type u_9) [(x : B') → AddCommMonoid (E' x)] [(x : B') → Module 𝕜₂ (E' x)] [TopologicalSpace (Bundle.TotalSpace F' E')] [FiberBundle F E] [VectorBundle 𝕜₁ F E] [(x : B') → TopologicalSpace (E' x)] [FiberBundle F' E'] [VectorBundle 𝕜₂ F' E'] (x₀ : B) (x : B) (y₀ : B') (y : B') (ϕ : E x →SL[σ] E' y) (hx : x (trivializationAt F E x₀).baseSet) (hy : y (trivializationAt F' E' y₀).baseSet) :

                                                                  Rewrite ContinuousLinearMap.inCoordinates using continuous linear equivalences.

                                                                  theorem VectorBundleCore.inCoordinates_eq {B : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [TopologicalSpace B] {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} [NontriviallyNormedField 𝕜₁] [NontriviallyNormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {B' : Type u_7} [TopologicalSpace B'] [NormedSpace 𝕜₁ F] {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜₂ F'] {ι : Type u_10} {ι' : Type u_11} (Z : VectorBundleCore 𝕜₁ B F ι) (Z' : VectorBundleCore 𝕜₂ B' F' ι') {x₀ : B} {x : B} {y₀ : B'} {y : B'} (ϕ : F →SL[σ] F') (hx : x VectorBundleCore.baseSet Z (VectorBundleCore.indexAt Z x₀)) (hy : y VectorBundleCore.baseSet Z' (VectorBundleCore.indexAt Z' y₀)) :

                                                                  Rewrite ContinuousLinearMap.inCoordinates in a VectorBundleCore.