The fibre coordinate and partial diffeomorphism of a bundle trivialization

Near a point v₀ of the total space of a fibre bundle, every point can be read in the preferred trivialization at the base point v₀.proj. For a C^n model of the total space, the fibre coordinate of such a point in that trivialization is C^n at v₀. That points near v₀ lie over the base set of the trivialization is the topological fact Bundle.TotalSpace.eventually_proj_mem_baseSet_trivializationAt.

For a vector bundle, the same reading applies to a C^n map from a normed space into the total space: its fibre part, read through the linear map of the trivialization at the image of the base point, is a C^n map between normed spaces there. Read in the same way, the inclusion of a fibre into the total space is a continuous linear isomorphism onto the model fibre; hence it is C^n and has injective derivative. Moreover, every atlas trivialization of a C^n vector bundle is a C^n partial diffeomorphism between its source in TotalSpace F E and its target e.baseSet ×ˢ univ in B × F, and hence a C^n local diffeomorphism in both directions. Read back through such a trivialization, a C^n family of vectors of the model fibre is a C^n section.

Main results

• Bundle.TotalSpace.contMDiffAt_trivializationAt_snd: the fibre coordinate in the trivialization at v₀.proj is C^n at v₀.
• ContMDiffAt.contDiffAt_continuousLinearMapAt_trivializationAt: a C^n map from a normed space into the total space of a vector bundle has C^n fibre coordinates in the trivialization at the base point of its value.
• TauCeti.Manifold.contMDiff_totalSpaceMk, TauCeti.Manifold.injective_mfderiv_totalSpaceMk: the inclusion of a fibre into the total space of a vector bundle is C^n and has injective derivative.
• Bundle.Trivialization.toPartialDiffeomorph, Bundle.Trivialization.isLocalDiffeomorphAt, Bundle.Trivialization.isLocalDiffeomorphAt_symm: an atlas trivialization of a C^n vector bundle as a C^n partial diffeomorphism and local diffeomorphism.
• Bundle.Trivialization.contMDiffOn_section_symm: a C^n family of vectors of the model fibre, read through an atlas trivialization, is a C^n section over its base set.

theorem Bundle.TotalSpace.contMDiffAt_trivializationAt_snd {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (v₀ : TotalSpace F E) : ContMDiffAt (IB.prod (modelWithCornersSelf 𝕜 F)) (modelWithCornersSelf 𝕜 F) n (fun (v : TotalSpace F E) => (↑(trivializationAt F E v₀.proj) v).2) v₀

The fibre coordinate in the trivialization at v₀.proj is C^n at v₀.

theorem ContMDiffAt.contDiffAt_continuousLinearMapAt_trivializationAt {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [VectorBundle 𝕜 F E] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {b : G → B} {s : (z : G) → E (b z)} {z₀ : G} (h : ContMDiffAt (modelWithCornersSelf 𝕜 G) (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (z : G) => ⟨b z, s z⟩) z₀) : ContDiffAt 𝕜 n (fun (z : G) => (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F E (b z₀)) (b z)) (s z)) z₀

A C^n map z ↦ (b z, s z) from a normed space into the total space of a vector bundle has C^n fibre coordinates in the trivialization at b z₀, read through its linear map.

theorem TauCeti.Manifold.contMDiff_totalSpaceMk {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → NormedSpace 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [VectorBundle 𝕜 F E] (b : B) : ContMDiff (modelWithCornersSelf 𝕜 (E b)) (IB.prod (modelWithCornersSelf 𝕜 F)) n (Bundle.TotalSpace.mk b)

The inclusion of a fibre into the total space of a vector bundle is C^n: read in the trivialization at the base point, it is a continuous linear map into the model fibre.

theorem TauCeti.Manifold.injective_mfderiv_totalSpaceMk {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → NormedSpace 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [VectorBundle 𝕜 F E] (b : B) (y : E b) : Function.Injective ⇑(mfderiv% (Bundle.TotalSpace.mk b) y)

The inclusion of a fibre into the total space of a vector bundle has injective derivative: composed with the fibre coordinate of the trivialization at the base point, it is the linear isomorphism of that fibre with the model fibre.

def Bundle.Trivialization.toPartialDiffeomorph {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] (n : WithTop ℕ∞) [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] : PartialDiffeomorph (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) (TotalSpace F E) (B × F) n

An atlas trivialization of a C^n vector bundle as a C^n partial diffeomorphism between its open source in TotalSpace F E and its open target e.baseSet ×ˢ univ in B × F.

@[simp]

theorem Bundle.Trivialization.toPartialDiffeomorph_toPartialEquiv {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] (n : WithTop ℕ∞) [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] : (toPartialDiffeomorph IB n e).toPartialEquiv = e.toPartialEquiv

The underlying PartialEquiv of e.toPartialDiffeomorph is e.toPartialEquiv.

theorem Bundle.Trivialization.toPartialDiffeomorph_source {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] (n : WithTop ℕ∞) [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] : (toPartialDiffeomorph IB n e).source = e.source

The source of e.toPartialDiffeomorph is e.source.

theorem Bundle.Trivialization.toPartialDiffeomorph_target {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] (n : WithTop ℕ∞) [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] : (toPartialDiffeomorph IB n e).target = e.target

The target of e.toPartialDiffeomorph is e.target.

theorem Bundle.Trivialization.coe_toPartialDiffeomorph {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] (n : WithTop ℕ∞) [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] : ↑(toPartialDiffeomorph IB n e).toPartialEquiv = ↑e

Coercing e.toPartialDiffeomorph to a function recovers e.

theorem Bundle.Trivialization.toPartialDiffeomorph_symm_apply {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] (n : WithTop ℕ∞) [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] (q : B × F) : ↑(toPartialDiffeomorph IB n e).symm q = ↑e.symm q

Applying the partial inverse of e.toPartialDiffeomorph agrees with e.toOpenPartialHomeomorph.symm.

theorem Bundle.Trivialization.isLocalDiffeomorphAt {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {n : WithTop ℕ∞} [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e : Trivialization F TotalSpace.proj} [MemTrivializationAtlas e] {p : TotalSpace F E} (hp : p ∈ e.source) : IsLocalDiffeomorphAt (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) n (↑e) p

An atlas trivialization of a C^n vector bundle is a C^n local diffeomorphism at every point of its source.

theorem Bundle.Trivialization.isLocalDiffeomorphAt_symm {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {n : WithTop ℕ∞} [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e : Trivialization F TotalSpace.proj} [MemTrivializationAtlas e] {q : B × F} (hq : q ∈ e.target) : IsLocalDiffeomorphAt (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) n (↑e.symm) q

The partial inverse of an atlas trivialization of a C^n vector bundle is a C^n local diffeomorphism at every point of its target.

noncomputable def Bundle.Trivialization.frameTransitionMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] {n : WithTop ℕ∞} [ContMDiffVectorBundle n F V I] (e e' : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {U : TopologicalSpace.Opens M} (hU : ↑U ⊆ e.baseSet) (hU' : ↑U ⊆ e'.baseSet) : ContMDiffMap I (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) (↥U) (F →L[𝕜] F) n

The actual frame-change operator as a smooth map on any common open frame domain.

@[simp]

theorem Bundle.Trivialization.frameTransitionMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] {n : WithTop ℕ∞} [ContMDiffVectorBundle n F V I] (e e' : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {U : TopologicalSpace.Opens M} (hU : ↑U ⊆ e.baseSet) (hU' : ↑U ⊆ e'.baseSet) (x : ↥U) : (e.frameTransitionMap e' hU hU') x = ↑(coordChangeL 𝕜 e e' ↑x)

Evaluation of the smooth frame-change operator is the native bundle coordinate change.

theorem Bundle.Trivialization.contMDiffOn_section_symm {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {n : WithTop ℕ∞} [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e : Trivialization F TotalSpace.proj) [MemTrivializationAtlas e] {U : Set B} (hU : IsOpen U) (hUe : U ⊆ e.baseSet) {u : B → F} (hu : ContMDiffOn IB (modelWithCornersSelf 𝕜 F) n u U) : ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => ⟨x, e.symm x (u x)⟩) U

A C^n family of vectors of the model fibre, read through a trivialization, is a C^n section. Over an open subset U of the base set of an atlas trivialization e, the section x ↦ e.symm x (u x) is C^n when u is.