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:

• The bundle trivializations in the trivialization atlas should be continuous linear equivs in the fibers;
• For any two trivializations e, e' in the atlas the transition function considered as a map from B into F →L[R] F is continuous on e.baseSet ∩ e'.baseSet with respect to the operator norm topology on F →L[R] F.

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

• Trivialization.IsLinear: a class stating that a trivialization is fiberwise linear on its base set.
• Trivialization.linearEquivAt and Trivialization.continuousLinearMapAt are the (continuous) linear fiberwise equivalences a trivialization induces.
• They have forward maps Trivialization.linearMapAt / Trivialization.continuousLinearMapAt and inverses Trivialization.symmₗ / Trivialization.symmL. Note that these are all defined everywhere, since they are extended using the zero function.
• Trivialization.coordChangeL is the coordinate change induced by two trivializations. It only makes sense on the intersection of their base sets, but is extended outside it using the identity.
• Given a continuous (semi)linear map between E x and E' y where E and E' are bundles over possibly different base sets, ContinuousLinearMap.inCoordinates turns this into a continuous (semi)linear map between the chosen fibers of those bundles.

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 : B → Type 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) : Prop

• linear : ∀ (b : B), b ∈ e.baseSet → IsLinearMap 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.

theorem Pretrivialization.linear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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 = Pretrivialization.symm e b y

def Pretrivialization.symmₗ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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.

@[simp]

theorem Pretrivialization.linearEquivAt_symm_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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) : ↑(LinearEquiv.symm (Pretrivialization.linearEquivAt R e b hb)) = Pretrivialization.symm e b

@[simp]

theorem Pretrivialization.linearEquivAt_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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.

def Pretrivialization.linearMapAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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.

theorem Pretrivialization.coe_linearMapAt {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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 : B → Type 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 : B → Type 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 = ↑(Pretrivialization.linearEquivAt R e b hb)

theorem Pretrivialization.linearMapAt_def_of_not_mem {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 = 0

theorem Pretrivialization.linearMapAt_eq_zero {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 = 0

theorem Pretrivialization.symmₗ_linearMapAt {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : ↑(Pretrivialization.symmₗ R e b) (↑(Pretrivialization.linearMapAt R e b) y) = y

theorem Pretrivialization.linearMapAt_symmₗ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : ↑(Pretrivialization.linearMapAt R e b) (↑(Pretrivialization.symmₗ R e b) y) = y

class Trivialization.IsLinear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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) : Prop

• linear : ∀ (b : B), b ∈ e.baseSet → IsLinearMap 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.

theorem Trivialization.linear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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 (Trivialization.toPretrivialization e)

def Trivialization.linearEquivAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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.

@[simp]

theorem Trivialization.linearEquivAt_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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) : ↑(LinearEquiv.symm (Trivialization.linearEquivAt R e b hb)) v = Trivialization.symm e b v

def Trivialization.symmₗ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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.

theorem Trivialization.coe_symmₗ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) = Trivialization.symm e b

def Trivialization.linearMapAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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.

theorem Trivialization.coe_linearMapAt {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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 : B → Type 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 : B → Type 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 = ↑(Trivialization.linearEquivAt R e b hb)

theorem Trivialization.linearMapAt_def_of_not_mem {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 = 0

theorem Trivialization.symmₗ_linearMapAt {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : ↑(Trivialization.symmₗ R e b) (↑(Trivialization.linearMapAt R e b) y) = y

theorem Trivialization.linearMapAt_symmₗ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : ↑(Trivialization.linearMapAt R e b) (↑(Trivialization.symmₗ R e b) y) = y

def Trivialization.coordChangeL (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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.

theorem Trivialization.coe_coordChangeL {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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 : B → Type 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) : ContinuousLinearEquiv.symm (Trivialization.coordChangeL R e e' b) = Trivialization.coordChangeL R e' e b

theorem Trivialization.coordChangeL_apply {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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 : B → Type 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 : B → Type 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 : B → Type 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) : ↑(ContinuousLinearEquiv.symm (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)))

def Bundle.zeroSection {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [(x : B) → Zero (E x)] : B → Bundle.TotalSpace F E

The zero section of a vector bundle

@[simp]

theorem Bundle.zeroSection_proj {B : Type u_2} (F : Type u_3) (E : B → Type 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 : B → Type 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 : B → Type 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] : Prop

• trivialization_linear' : ∀ (e : Trivialization F Bundle.TotalSpace.proj) [inst : MemTrivializationAtlas e], Trivialization.IsLinear R e
• continuousOn_coordChange' : ∀ (e e' : Trivialization F Bundle.TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'], ContinuousOn (fun b => ↑(Trivialization.coordChangeL R e e' b)) (e.baseSet ∩ e'.baseSet)

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.

instance trivialization_linear (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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] : Trivialization.IsLinear R e

theorem continuousOn_coordChange (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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.continuousLinearMapAt R e b) = ↑(Trivialization.linearMapAt R e b)

def Trivialization.continuousLinearMapAt (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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).

@[simp]

theorem Trivialization.symmL_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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) = Trivialization.symm e b

def Trivialization.symmL (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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.

theorem Trivialization.symmL_continuousLinearMapAt {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : ↑(Trivialization.symmL R e b) (↑(Trivialization.continuousLinearMapAt R e b) y) = y

theorem Trivialization.continuousLinearMapAt_symmL {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : ↑(Trivialization.continuousLinearMapAt R e b) (↑(Trivialization.symmL R e b) y) = y

@[simp]

theorem Trivialization.continuousLinearEquivAt_symm_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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) : ↑(ContinuousLinearEquiv.symm (Trivialization.continuousLinearEquivAt R e b hb)) = Trivialization.symm e b

@[simp]

theorem Trivialization.continuousLinearEquivAt_apply (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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.

theorem Trivialization.coe_continuousLinearEquivAt_eq {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) = ↑(Trivialization.continuousLinearMapAt R e b)

theorem Trivialization.symm_continuousLinearEquivAt_eq {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : ↑(ContinuousLinearEquiv.symm (Trivialization.continuousLinearEquivAt R e b hb)) = ↑(Trivialization.symmL R e b)

@[simp]

theorem Trivialization.continuousLinearEquivAt_apply' {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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 : B → Type 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 : B → Type 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 : B → Type 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) : ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm (Trivialization.continuousLinearEquivAt R e b (_ : b ∈ e.baseSet))) (Trivialization.continuousLinearEquivAt R e' b (_ : b ∈ e'.baseSet)) = Trivialization.coordChangeL R e e' b

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)

• baseSet : ι → Set B
• isOpen_baseSet : ∀ (i : ι), IsOpen (VectorBundleCore.baseSet s i)
• indexAt : B → ι
• mem_baseSet_at : ∀ (x : B), x ∈ VectorBundleCore.baseSet s (VectorBundleCore.indexAt s x)
• coordChange : ι → ι → B → F →L[R] F
• coordChange_self : ∀ (i : ι) (x : B), x ∈ VectorBundleCore.baseSet s i → ∀ (v : F), ↑(VectorBundleCore.coordChange s i i x) v = v
• continuousOn_coordChange : ∀ (i j : ι), ContinuousOn (VectorBundleCore.coordChange s i j) (VectorBundleCore.baseSet s i ∩ VectorBundleCore.baseSet s j)
• coordChange_comp : ∀ (i j k : ι) (x : B), x ∈ VectorBundleCore.baseSet s i ∩ VectorBundleCore.baseSet s j ∩ VectorBundleCore.baseSet s k → ∀ (v : F), ↑(VectorBundleCore.coordChange s j k x) (↑(VectorBundleCore.coordChange s i j x) v) = ↑(VectorBundleCore.coordChange s i k x) v

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.

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 ι] : VectorBundleCore R B F ι

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

instance instInhabitedVectorBundleCore (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 ι] : Inhabited (VectorBundleCore R B F ι)

@[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 ι) : (VectorBundleCore.toFiberBundleCore Z).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 ι) : (VectorBundleCore.toFiberBundleCore Z).indexAt = Z.indexAt

@[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 ι) : (VectorBundleCore.toFiberBundleCore Z).coordChange = fun i j b => ↑(VectorBundleCore.coordChange Z i j b)

def VectorBundleCore.toFiberBundleCore {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 ι) : FiberBundleCore ι B F

Natural identification to a FiberBundleCore.

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 ∈ VectorBundleCore.baseSet Z i ∩ VectorBundleCore.baseSet Z j ∩ VectorBundleCore.baseSet Z k → ContinuousLinearMap.comp (VectorBundleCore.coordChange Z j k x) (VectorBundleCore.coordChange Z i j x) = VectorBundleCore.coordChange Z 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

@[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

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 ι) : B → Type u_3

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

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 (VectorBundleCore.Fiber Z 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 (VectorBundleCore.Fiber Z x)

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 (VectorBundleCore.Fiber Z x)

@[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 (VectorBundleCore.Fiber Z) → B

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

@[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.

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.

@[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 ∈ (VectorBundleCore.trivChange Z i j).toLocalEquiv.source ↔ p.fst ∈ VectorBundleCore.baseSet Z i ∩ VectorBundleCore.baseSet Z 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 (VectorBundleCore.TotalSpace Z)

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

@[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 : ι) : FiberBundleCore.coordChange (VectorBundleCore.toFiberBundleCore Z) i j b = ↑(VectorBundleCore.coordChange Z 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.

@[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)

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 (VectorBundleCore.localTriv Z i)

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 : ι) : VectorBundleCore.baseSet Z i = (VectorBundleCore.localTriv Z 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 ∈ (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 }

@[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 ∈ VectorBundleCore.baseSet Z i) (v : F) : Trivialization.symm (VectorBundleCore.localTriv Z i) b v = ↑(VectorBundleCore.coordChange Z i (VectorBundleCore.indexAt Z 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 ∈ VectorBundleCore.baseSet Z i ∩ VectorBundleCore.baseSet Z j) (v : F) : ↑(Trivialization.coordChangeL R (VectorBundleCore.localTriv Z i) (VectorBundleCore.localTriv Z j) b) v = ↑(VectorBundleCore.coordChange Z 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

@[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) : VectorBundleCore.localTriv Z (VectorBundleCore.indexAt Z b) = VectorBundleCore.localTrivAt Z 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 } ∈ (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) : b ∈ (VectorBundleCore.localTrivAt Z 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 (VectorBundleCore.Fiber Z)

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 (VectorBundleCore.Fiber Z)

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 (VectorBundleCore.proj Z)

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 (VectorBundleCore.proj Z)

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 ∈ VectorBundleCore.baseSet Z i) : Trivialization.continuousLinearMapAt R (VectorBundleCore.localTriv Z i) b = VectorBundleCore.coordChange Z (VectorBundleCore.indexAt Z 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 (VectorBundleCore.Fiber Z) b₀).baseSet) : Trivialization.continuousLinearMapAt R (trivializationAt F (VectorBundleCore.Fiber Z) b₀) b = VectorBundleCore.coordChange Z (VectorBundleCore.indexAt Z b) (VectorBundleCore.indexAt Z 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 ∈ VectorBundleCore.baseSet Z i) : Trivialization.symmL R (VectorBundleCore.localTriv Z i) b = VectorBundleCore.coordChange Z i (VectorBundleCore.indexAt Z 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 (VectorBundleCore.Fiber Z) b₀).baseSet) : Trivialization.symmL R (trivializationAt F (VectorBundleCore.Fiber Z) b₀) b = VectorBundleCore.coordChange Z (VectorBundleCore.indexAt Z b₀) (VectorBundleCore.indexAt Z 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 (VectorBundleCore.Fiber Z) b₀).baseSet ∩ (trivializationAt F (VectorBundleCore.Fiber Z) b₁).baseSet) (v : F) : ↑(Trivialization.coordChangeL R (trivializationAt F (VectorBundleCore.Fiber Z) b₀) (trivializationAt F (VectorBundleCore.Fiber Z) b₁) b) v = ↑(VectorBundleCore.coordChange Z (VectorBundleCore.indexAt Z b₀) (VectorBundleCore.indexAt Z b₁) b) v

Vector prebundle

structure VectorPrebundle (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type 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)

• pretrivializationAtlas : Set (Pretrivialization F Bundle.TotalSpace.proj)
• pretrivialization_linear' : ∀ (e : Pretrivialization F Bundle.TotalSpace.proj), e ∈ s.pretrivializationAtlas → Pretrivialization.IsLinear R e
• pretrivializationAt : B → Pretrivialization F Bundle.TotalSpace.proj
• mem_base_pretrivializationAt : ∀ (x : B), x ∈ (VectorPrebundle.pretrivializationAt s x).baseSet
• pretrivialization_mem_atlas : ∀ (x : B), VectorPrebundle.pretrivializationAt s x ∈ s.pretrivializationAtlas
• exists_coordChange : ∀ (e : Pretrivialization F Bundle.TotalSpace.proj), e ∈ s.pretrivializationAtlas → ∀ (e' : Pretrivialization F Bundle.TotalSpace.proj), e' ∈ s.pretrivializationAtlas → ∃ f, ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧ ∀ (b : B), b ∈ e.baseSet ∩ e'.baseSet → ∀ (v : F), ↑(f b) v = (↑e' { proj := b, snd := Pretrivialization.symm e b v }).snd
• totalSpaceMk_inducing : ∀ (b : B), Inducing (↑(VectorPrebundle.pretrivializationAt s b) ∘ Bundle.TotalSpace.mk b)

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.

def VectorPrebundle.coordChange {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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.

theorem VectorPrebundle.continuousOn_coordChange {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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 : B → Type 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 : B → Type 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) : FiberPrebundle F E

Natural identification of VectorPrebundle as a FiberPrebundle.

def VectorPrebundle.totalSpaceTopology {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : TopologicalSpace (Bundle.TotalSpace F E)

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

def VectorPrebundle.trivializationOfMemPretrivializationAtlas {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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.

theorem VectorPrebundle.linear_trivializationOfMemPretrivializationAtlas {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 (VectorPrebundle.trivializationOfMemPretrivializationAtlas a he)

theorem VectorPrebundle.mem_trivialization_at_source {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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 : B → Type 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 ⁻¹' (VectorPrebundle.pretrivializationAt a b).source = Set.univ

theorem VectorPrebundle.continuous_totalSpaceMk {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : Continuous (Bundle.TotalSpace.mk b)

def VectorPrebundle.toFiberBundle {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : FiberBundle F E

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

theorem VectorPrebundle.toVectorBundle {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type 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) : VectorBundle 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 : B → Type 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.

theorem ContinuousLinearMap.inCoordinates_eq {B : Type u_2} {F : Type u_3} (E : B → Type 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 ϕ = ContinuousLinearMap.comp (↑(Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy)) (ContinuousLinearMap.comp ϕ ↑(ContinuousLinearEquiv.symm (Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx)))

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

Rewrite ContinuousLinearMap.inCoordinates in a VectorBundleCore.