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) :

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.

  • linear : be.baseSet, IsLinearMap R fun (x : E b) => (e { proj := b, snd := x }).2
Instances
    theorem Pretrivialization.IsLinear.linear {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} :
    ∀ {inst : Semiring R} {inst_1 : TopologicalSpace F} {inst_2 : TopologicalSpace B} {inst_3 : AddCommMonoid F} {inst_4 : Module R F} {inst_5 : (x : B) → AddCommMonoid (E x)} {inst_6 : (x : B) → Module R (E x)} {e : Pretrivialization F Bundle.TotalSpace.proj} [self : Pretrivialization.IsLinear R e], be.baseSet, IsLinearMap R fun (x : E b) => (e { proj := b, snd := x }).2
    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 b) => (e { proj := b, snd := x }).2
    @[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) :
    (Pretrivialization.symmₗ R e b) y = e.symm b y
    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.

    Equations
    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) :
      (Pretrivialization.linearEquivAt R e b hb).symm = e.symm b
      @[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 b) => (e { proj := b, snd := y }).2
      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.

      Equations
      • Pretrivialization.linearEquivAt R e b hb = { toFun := fun (y : E b) => (e { proj := b, snd := y }).2, map_add' := , map_smul' := , invFun := e.symm b, left_inv := , right_inv := }
      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.

        Equations
        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 : E b) => if b e.baseSet then (e { proj := b, snd := y }).2 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 b) => (e { proj := b, snd := y }).2
          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 }).2 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 : be.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 : be.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) :

          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.

          • linear : be.baseSet, IsLinearMap R fun (x : E b) => (e { proj := b, snd := x }).2
          Instances
            theorem Trivialization.IsLinear.linear {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} :
            ∀ {inst : Semiring R} {inst_1 : TopologicalSpace F} {inst_2 : TopologicalSpace B} {inst_3 : TopologicalSpace (Bundle.TotalSpace F E)} {inst_4 : AddCommMonoid F} {inst_5 : Module R F} {inst_6 : (x : B) → AddCommMonoid (E x)} {inst_7 : (x : B) → Module R (E x)} {e : Trivialization F Bundle.TotalSpace.proj} [self : Trivialization.IsLinear R e], be.baseSet, IsLinearMap R fun (x : E b) => (e { proj := b, snd := x }).2
            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 b) => (e { proj := b, snd := y }).2
            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] :
            Pretrivialization.IsLinear R e.toPretrivialization
            Equations
            • =
            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.

            Equations
            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 }).2
              @[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) :
              (Trivialization.linearEquivAt R e b hb).symm v = e.symm b v
              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.

              Equations
              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) :
                (Trivialization.symmₗ R e b) = e.symm 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.

                Equations
                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 : E b) => if b e.baseSet then (e { proj := b, snd := y }).2 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 b) => (e { proj := b, snd := y }).2
                  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 }).2 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 : be.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.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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) = ((Trivialization.linearEquivAt R e b ).symm ≪≫ₗ Trivialization.linearEquivAt R e' b )
                    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 = (Trivialization.linearEquivAt R e b ).symm ≪≫ₗ Trivialization.linearEquivAt R e' b
                    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 := e.symm b y }).2
                    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 := e.symm 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' (e.symm (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' (e.symm (b, y))).2

                    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) :
                    (Trivialization.coordChangeL R e e' b).symm = ((Trivialization.linearEquivAt R e' b ).symm ≪≫ₗ Trivialization.linearEquivAt R e b )
                    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

                    Equations
                    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
                        theorem VectorBundle.trivialization_linear' {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} :
                        ∀ {inst : NontriviallyNormedField R} {inst_1 : (x : B) → AddCommMonoid (E x)} {inst_2 : (x : B) → Module R (E x)} {inst_3 : NormedAddCommGroup F} {inst_4 : NormedSpace R F} {inst_5 : TopologicalSpace B} {inst_6 : TopologicalSpace (Bundle.TotalSpace F E)} {inst_7 : (x : B) → TopologicalSpace (E x)} {inst_8 : FiberBundle F E} [self : VectorBundle R F E] (e : Trivialization F Bundle.TotalSpace.proj) [inst_9 : MemTrivializationAtlas e], Trivialization.IsLinear R e
                        theorem VectorBundle.continuousOn_coordChange' {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : BType u_4} :
                        ∀ {inst : NontriviallyNormedField R} {inst_1 : (x : B) → AddCommMonoid (E x)} {inst_2 : (x : B) → Module R (E x)} {inst_3 : NormedAddCommGroup F} {inst_4 : NormedSpace R F} {inst_5 : TopologicalSpace B} {inst_6 : TopologicalSpace (Bundle.TotalSpace F E)} {inst_7 : (x : B) → TopologicalSpace (E x)} {inst_8 : FiberBundle F E} [self : VectorBundle R F E] (e e' : Trivialization F Bundle.TotalSpace.proj) [inst_9 : MemTrivializationAtlas e] [inst_10 : MemTrivializationAtlas e'], ContinuousOn (fun (b : B) => (Trivialization.coordChangeL R e e' b)) (e.baseSet e'.baseSet)
                        @[instance 100]
                        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] :
                        Equations
                        • =
                        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 : 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).

                        Equations
                        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) :
                          (Trivialization.symmL R e b) = e.symm 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.

                          Equations
                          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) :
                            (Trivialization.continuousLinearEquivAt R e b hb).symm = e.symm b
                            @[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 b) => (e { proj := b, snd := y }).2
                            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.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            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.snd = (e x).2
                              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) :
                              e.symm (b, z) = { proj := b, snd := (Trivialization.continuousLinearEquivAt R e b hb).symm 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.

                              • baseSet : ιSet B
                              • isOpen_baseSet : ∀ (i : ι), IsOpen (self.baseSet i)
                              • indexAt : Bι
                              • mem_baseSet_at : ∀ (x : B), x self.baseSet (self.indexAt x)
                              • coordChange : ιιBF →L[R] F
                              • coordChange_self : ∀ (i : ι), xself.baseSet i, ∀ (v : F), (self.coordChange i i x) v = v
                              • continuousOn_coordChange : ∀ (i j : ι), ContinuousOn (self.coordChange i j) (self.baseSet i self.baseSet j)
                              • 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 VectorBundleCore.isOpen_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} (self : VectorBundleCore R B F ι) (i : ι) :
                                IsOpen (self.baseSet i)
                                theorem VectorBundleCore.mem_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} (self : VectorBundleCore R B F ι) (x : B) :
                                x self.baseSet (self.indexAt x)
                                theorem VectorBundleCore.coordChange_self {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (self : VectorBundleCore R B F ι) (i : ι) (x : B) :
                                x self.baseSet i∀ (v : F), (self.coordChange i i x) v = v
                                theorem VectorBundleCore.continuousOn_coordChange {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (self : VectorBundleCore R B F ι) (i : ι) (j : ι) :
                                ContinuousOn (self.coordChange i j) (self.baseSet i self.baseSet j)
                                theorem VectorBundleCore.coordChange_comp {R : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField R] [NormedAddCommGroup F] [NormedSpace R F] [TopologicalSpace B] {ι : Type u_5} (self : VectorBundleCore R 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 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.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  @[simp]
                                  theorem VectorBundleCore.toFiberBundleCore_coordChange {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 ι) :
                                  Z.toFiberBundleCore.coordChange = fun (i j : ι) (b : B) => (Z.coordChange i j b)
                                  @[simp]
                                  theorem VectorBundleCore.toFiberBundleCore_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 ι) :
                                  Z.toFiberBundleCore.baseSet = Z.baseSet
                                  @[simp]
                                  theorem VectorBundleCore.toFiberBundleCore_indexAt {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 ι) :
                                  Z.toFiberBundleCore.indexAt = Z.indexAt

                                  Natural identification to a FiberBundleCore.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem VectorBundleCore.coordChange_linear_comp {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 : ι) (k : ι) (x : B) :
                                    x Z.baseSet i Z.baseSet j Z.baseSet k(Z.coordChange j k x).comp (Z.coordChange i j x) = Z.coordChange i k x
                                    def VectorBundleCore.Index {ι : Type u_5} :
                                    Type u_5

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

                                    Equations
                                    • VectorBundleCore.Index = ι
                                    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

                                      Equations
                                      • VectorBundleCore.Base = B
                                      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

                                        Equations
                                        • Z.Fiber = Z.toFiberBundleCore.Fiber
                                        Instances For
                                          instance VectorBundleCore.topologicalSpaceFiber {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) :
                                          TopologicalSpace (Z.Fiber x)
                                          Equations
                                          • Z.topologicalSpaceFiber x = Z.toFiberBundleCore.topologicalSpaceFiber x
                                          instance VectorBundleCore.addCommGroupFiber {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) :
                                          AddCommGroup (Z.Fiber x)
                                          Equations
                                          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) :
                                          Module R (Z.Fiber x)
                                          Equations
                                          @[reducible]
                                          def VectorBundleCore.proj {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 ι) :
                                          Bundle.TotalSpace F Z.FiberB

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

                                          Equations
                                          • Z.proj = Bundle.TotalSpace.proj
                                          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.

                                            Equations
                                            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 : ι) :
                                              PartialHomeomorph (B × F) (B × F)

                                              Local homeomorphism version of the trivialization change.

                                              Equations
                                              • Z.trivChange i j = Z.toFiberBundleCore.trivChange i j
                                              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) :
                                                p (Z.trivChange i j).source p.1 Z.baseSet i Z.baseSet j
                                                instance VectorBundleCore.toTopologicalSpace {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 ι) :
                                                TopologicalSpace Z.TotalSpace

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

                                                Equations
                                                • Z.toTopologicalSpace = Z.toFiberBundleCore.toTopologicalSpace
                                                @[simp]
                                                theorem VectorBundleCore.coe_coordChange {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) (i : ι) (j : ι) :
                                                Z.toFiberBundleCore.coordChange i j b = (Z.coordChange i j b)
                                                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.

                                                Equations
                                                • Z.localTriv i = Z.toFiberBundleCore.localTriv i
                                                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 : Z.TotalSpace) :
                                                  (Z.localTriv i) p = (p.proj, (Z.coordChange (Z.indexAt p.proj) i p.proj) p.snd)
                                                  instance VectorBundleCore.localTriv.isLinear {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.IsLinear R (Z.localTriv i)

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

                                                  Equations
                                                  • =
                                                  @[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 : Z.TotalSpace) :
                                                  p (Z.localTriv i).source p.proj Z.baseSet 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 : ι) :
                                                  Z.baseSet i = (Z.localTriv i).baseSet
                                                  @[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 (Z.localTriv i).target p.1 (Z.localTriv 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) :
                                                  (Z.localTriv i).symm p = { proj := p.1, snd := (Z.coordChange i (Z.indexAt p.1) p.1) p.2 }
                                                  @[simp]
                                                  theorem VectorBundleCore.localTriv_symm_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 : ι) {b : B} (hb : b Z.baseSet i) (v : F) :
                                                  (Z.localTriv i).symm b v = (Z.coordChange i (Z.indexAt b) b) v
                                                  @[simp]
                                                  theorem VectorBundleCore.localTriv_coordChange_eq {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 : ι) {b : B} (hb : b Z.baseSet i Z.baseSet j) (v : F) :
                                                  (Trivialization.coordChangeL R (Z.localTriv i) (Z.localTriv j) b) v = (Z.coordChange i j b) v
                                                  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

                                                  Equations
                                                  • Z.localTrivAt b = Z.localTriv (Z.indexAt b)
                                                  Instances For
                                                    @[simp]
                                                    theorem VectorBundleCore.localTrivAt_def {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) :
                                                    Z.localTriv (Z.indexAt b) = Z.localTrivAt b
                                                    @[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 } (Z.localTrivAt b).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 : Z.TotalSpace) :
                                                    (Z.localTrivAt 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) :
                                                    (Z.localTrivAt 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) :
                                                    b (Z.localTrivAt b).baseSet
                                                    instance VectorBundleCore.fiberBundle {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 ι) :
                                                    FiberBundle F Z.Fiber
                                                    Equations
                                                    • Z.fiberBundle = Z.toFiberBundleCore.fiberBundle
                                                    instance VectorBundleCore.vectorBundle {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 ι) :
                                                    VectorBundle R F Z.Fiber
                                                    Equations
                                                    • =
                                                    theorem VectorBundleCore.continuous_proj {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 ι) :
                                                    Continuous Z.proj

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

                                                    theorem VectorBundleCore.isOpenMap_proj {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 ι) :
                                                    IsOpenMap Z.proj

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

                                                    @[simp]
                                                    theorem VectorBundleCore.localTriv_continuousLinearMapAt {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 : ι} {b : B} (hb : b Z.baseSet i) :
                                                    Trivialization.continuousLinearMapAt R (Z.localTriv i) b = Z.coordChange (Z.indexAt b) i b
                                                    @[simp]
                                                    theorem VectorBundleCore.trivializationAt_continuousLinearMapAt {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} {b : B} (hb : b (trivializationAt F Z.Fiber b₀).baseSet) :
                                                    Trivialization.continuousLinearMapAt R (trivializationAt F Z.Fiber b₀) b = Z.coordChange (Z.indexAt b) (Z.indexAt b₀) b
                                                    @[simp]
                                                    theorem VectorBundleCore.localTriv_symmL {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 : ι} {b : B} (hb : b Z.baseSet i) :
                                                    Trivialization.symmL R (Z.localTriv i) b = Z.coordChange i (Z.indexAt b) b
                                                    @[simp]
                                                    theorem VectorBundleCore.trivializationAt_symmL {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} {b : B} (hb : b (trivializationAt F Z.Fiber b₀).baseSet) :
                                                    Trivialization.symmL R (trivializationAt F Z.Fiber b₀) b = Z.coordChange (Z.indexAt b₀) (Z.indexAt b) b
                                                    @[simp]
                                                    theorem VectorBundleCore.trivializationAt_coordChange_eq {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} {b₁ : B} {b : B} (hb : b (trivializationAt F Z.Fiber b₀).baseSet (trivializationAt F Z.Fiber b₁).baseSet) (v : F) :
                                                    (Trivialization.coordChangeL R (trivializationAt F Z.Fiber b₀) (trivializationAt F Z.Fiber b₁) b) v = (Z.coordChange (Z.indexAt b₀) (Z.indexAt b₁) b) v

                                                    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 partial equivalences are also partial 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.

                                                    • pretrivializationAtlas : Set (Pretrivialization F Bundle.TotalSpace.proj)
                                                    • pretrivialization_linear' : eself.pretrivializationAtlas, Pretrivialization.IsLinear R e
                                                    • 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
                                                    • exists_coordChange : eself.pretrivializationAtlas, e'self.pretrivializationAtlas, ∃ (f : BF →L[R] F), ContinuousOn f (e.baseSet e'.baseSet) be.baseSet e'.baseSet, ∀ (v : F), (f b) v = (e' { proj := b, snd := e.symm b v }).2
                                                    • totalSpaceMk_isInducing : ∀ (b : B), IsInducing ((self.pretrivializationAt b) Bundle.TotalSpace.mk b)
                                                    Instances For
                                                      theorem VectorPrebundle.pretrivialization_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] [(x : B) → TopologicalSpace (E x)] (self : VectorPrebundle R F E) (e : Pretrivialization F Bundle.TotalSpace.proj) :
                                                      e self.pretrivializationAtlasPretrivialization.IsLinear R e
                                                      theorem VectorPrebundle.mem_base_pretrivializationAt {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)] (self : VectorPrebundle R F E) (x : B) :
                                                      x (self.pretrivializationAt x).baseSet
                                                      theorem VectorPrebundle.pretrivialization_mem_atlas {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)] (self : VectorPrebundle R F E) (x : B) :
                                                      self.pretrivializationAt x self.pretrivializationAtlas
                                                      theorem VectorPrebundle.exists_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)] (self : VectorPrebundle R F E) (e : Pretrivialization F Bundle.TotalSpace.proj) :
                                                      e self.pretrivializationAtlase'self.pretrivializationAtlas, ∃ (f : BF →L[R] F), ContinuousOn f (e.baseSet e'.baseSet) be.baseSet e'.baseSet, ∀ (v : F), (f b) v = (e' { proj := b, snd := e.symm b v }).2
                                                      theorem VectorPrebundle.totalSpaceMk_isInducing {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)] (self : VectorPrebundle R F E) (b : B) :
                                                      IsInducing ((self.pretrivializationAt b) Bundle.TotalSpace.mk b)
                                                      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.

                                                      Equations
                                                      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 (a.coordChange 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) :
                                                        (a.coordChange he he' b) v = (e' { proj := b, snd := e.symm b v }).2
                                                        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, (a.coordChange he he' b) v) = e' { proj := b, snd := e.symm 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.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        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.

                                                          Equations
                                                          • a.totalSpaceTopology = a.toFiberPrebundle.totalSpaceTopology
                                                          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.

                                                            Equations
                                                            • a.trivializationOfMemPretrivializationAtlas he = a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he
                                                            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) :
                                                              Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he)
                                                              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 } (a.pretrivializationAt 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) :
                                                              Bundle.TotalSpace.mk b ⁻¹' (a.pretrivializationAt b).source = Set.univ
                                                              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.

                                                              Equations
                                                              • a.toFiberBundle = a.toFiberPrebundle.toFiberBundle
                                                              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.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                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) :
                                                                  ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ = (↑(Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy)).comp (ϕ.comp (Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm)

                                                                  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 Z.baseSet (Z.indexAt x₀)) (hy : y Z'.baseSet (Z'.indexAt y₀)) :
                                                                  ContinuousLinearMap.inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ = (Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y).comp (ϕ.comp (Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x))

                                                                  Rewrite ContinuousLinearMap.inCoordinates in a VectorBundleCore.