The maximal atlas of compatible trivializations of a C^n vector bundle

Mathlib makes the total space of a vector bundle E with fibre F over B a charted space modelled on B × F, whose charts are the trivializations of the bundle's atlas, and shows that for a C^n vector bundle these charts are compatible for the groupoid contMDiffFiberwiseLinear B F IB n of bi-C^n fiberwise linear maps. The maximal atlas of that groupoid is the set of all trivializations compatible with the bundle's C^n structure. Over 𝓘(ℂ, EB) and for positive regularity n ≠ 0 it is the maximal atlas of holomorphic trivializations of a holomorphic vector bundle; for n = 0 it only records continuity.

This file characterizes that maximal atlas by gauges. For two linear trivializations e and e', the coordinate change e.symm ≫ₕ e' lies in the groupoid exactly when the fibrewise coordinate changes e.coordChangeL 𝕜 e' and e'.coordChangeL 𝕜 e are C^n on the overlap of the base sets. Hence a linear trivialization lies in the maximal atlas exactly when its coordinate changes with every trivialization of the bundle's atlas are C^n gauges, and the coordinate changes between any two members of the maximal atlas are C^n.

Changes of frame are gauge transforms. Bundle.Trivialization.transFiberwiseLinear modifies a trivialization e by a family φ : B → F ≃L[𝕜] F, and a gauge transform of a member of the maximal atlas is again a member exactly when φ and its fibrewise inverse are C^n on the base set. Finally, the smoothness criteria for maps into the total space and for sections, which Mathlib states for trivializations of the bundle's atlas, hold verbatim for every member of the maximal atlas.

Main results

• Bundle.Trivialization.symm_trans_mem_contMDiffFiberwiseLinear_iff: the coordinate change between two linear trivializations is bi-C^n fiberwise linear exactly when both fibrewise coordinate changes are C^n on the overlap.
• Bundle.Trivialization.mem_maximalAtlas_contMDiffFiberwiseLinear_iff: a linear trivialization lies in the maximal atlas exactly when its coordinate changes with the atlas are C^n.
• Bundle.Trivialization.contMDiffOn_coordChangeL_of_mem_maximalAtlas: coordinate changes between members of the maximal atlas are C^n.
• Bundle.Trivialization.transFiberwiseLinear: the gauge transform of a trivialization, with coordinate changes Bundle.Trivialization.coordChangeL_transFiberwiseLinear_left and Bundle.Trivialization.coordChangeL_transFiberwiseLinear_right.
• Bundle.Trivialization.transFiberwiseLinear_mem_maximalAtlas_iff: a gauge transform of a member of the maximal atlas is a member exactly when the gauge is bi-C^n.
• Bundle.Trivialization.contMDiffWithinAt_iff_of_mem_maximalAtlas, Bundle.Trivialization.contMDiffAt_section_iff_of_mem_maximalAtlas: smoothness of maps into the total space and of sections can be read off in any member of the maximal atlas.

Provenance

No formal source is vendored. The proofs follow Mathlib's Mathlib/Geometry/Manifold/VectorBundle/Basic.lean and Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean, by Floris van Doorn and Heather Macbeth: the proof of ContMDiffFiberwiseLinear.hasGroupoid and the characterization mem_contMDiffFiberwiseLinear_iff drive the groupoid criterion, the gauge transform is built from FiberwiseLinear.openPartialHomeomorph, and the section criteria extend Bundle.Trivialization.contMDiffWithinAt_iff and Bundle.Trivialization.contMDiffAt_section_iff from trivializations of the bundle's atlas to the maximal atlas.

References

• Norman Steenrod, The Topology of Fibre Bundles, Princeton University Press, 1951, Part I, §§2–3 (coordinate bundles, coordinate transformations and equivalent atlases).
• Daniel Huybrechts, Complex Geometry: An Introduction, Springer, 2005, Section 2.2 (holomorphic vector bundles and their holomorphic trivializations).

Gauge transforms of trivializations

def Bundle.Trivialization.transFiberwiseLinear {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {Z : Type u_4} [TopologicalSpace Z] {proj : Z → B} (e : Trivialization F proj) (φ : B → F ≃L[𝕜] F) (hφ : ContinuousOn (fun (x : B) => ↑(φ x)) e.baseSet) (h2φ : ContinuousOn (fun (x : B) => ↑(φ x).symm) e.baseSet) : Trivialization F proj

The gauge transform of a trivialization e by a family φ of continuous linear automorphisms of the fibre, continuous with continuous inverse on e.baseSet: it sends p to ((e p).1, φ (e p).1 (e p).2), and has the same base set as e.

@[simp]

theorem Bundle.Trivialization.transFiberwiseLinear_apply {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {Z : Type u_4} [TopologicalSpace Z] {proj : Z → B} (e : Trivialization F proj) (φ : B → F ≃L[𝕜] F) (hφ : ContinuousOn (fun (x : B) => ↑(φ x)) e.baseSet) (h2φ : ContinuousOn (fun (x : B) => ↑(φ x).symm) e.baseSet) (p : Z) : ↑(e.transFiberwiseLinear φ hφ h2φ) p = ((↑e p).1, (φ (↑e p).1) (↑e p).2)

@[simp]

theorem Bundle.Trivialization.transFiberwiseLinear_symm_apply {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {Z : Type u_4} [TopologicalSpace Z] {proj : Z → B} (e : Trivialization F proj) (φ : B → F ≃L[𝕜] F) (hφ : ContinuousOn (fun (x : B) => ↑(φ x)) e.baseSet) (h2φ : ContinuousOn (fun (x : B) => ↑(φ x).symm) e.baseSet) (x : B × F) : ↑(e.transFiberwiseLinear φ hφ h2φ).symm x = ↑e.symm (x.1, (φ x.1).symm x.2)

@[simp]

theorem Bundle.Trivialization.baseSet_transFiberwiseLinear {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {Z : Type u_4} [TopologicalSpace Z] {proj : Z → B} (e : Trivialization F proj) (φ : B → F ≃L[𝕜] F) (hφ : ContinuousOn (fun (x : B) => ↑(φ x)) e.baseSet) (h2φ : ContinuousOn (fun (x : B) => ↑(φ x).symm) e.baseSet) : (e.transFiberwiseLinear φ hφ h2φ).baseSet = e.baseSet

instance Bundle.Trivialization.isLinear_transFiberwiseLinear {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] (e : Trivialization F TotalSpace.proj) (φ : B → F ≃L[𝕜] F) (hφ : ContinuousOn (fun (x : B) => ↑(φ x)) e.baseSet) (h2φ : ContinuousOn (fun (x : B) => ↑(φ x).symm) e.baseSet) [Trivialization.IsLinear 𝕜 e] : Trivialization.IsLinear 𝕜 (e.transFiberwiseLinear φ hφ h2φ)

A gauge transform of a linear trivialization is linear.

theorem Bundle.Trivialization.coordChangeL_transFiberwiseLinear_left {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] (e : Trivialization F TotalSpace.proj) (φ : B → F ≃L[𝕜] F) (hφ : ContinuousOn (fun (x : B) => ↑(φ x)) e.baseSet) (h2φ : ContinuousOn (fun (x : B) => ↑(φ x).symm) e.baseSet) (e' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] [Trivialization.IsLinear 𝕜 e'] {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet) : coordChangeL 𝕜 (e.transFiberwiseLinear φ hφ h2φ) e' b = (φ b).symm.trans (coordChangeL 𝕜 e e' b)

The coordinate change out of a gauge transform first undoes the gauge.

theorem Bundle.Trivialization.coordChangeL_transFiberwiseLinear_right {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] (e : Trivialization F TotalSpace.proj) (φ : B → F ≃L[𝕜] F) (hφ : ContinuousOn (fun (x : B) => ↑(φ x)) e.baseSet) (h2φ : ContinuousOn (fun (x : B) => ↑(φ x).symm) e.baseSet) (e' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] [Trivialization.IsLinear 𝕜 e'] {b : B} (hb : b ∈ e'.baseSet ∩ e.baseSet) : coordChangeL 𝕜 e' (e.transFiberwiseLinear φ hφ h2φ) b = (coordChangeL 𝕜 e' e b).trans (φ b)

The coordinate change into a gauge transform applies the gauge last.

Membership in the groupoid of fiberwise linear maps

theorem Bundle.Trivialization.symm_trans_mem_contMDiffFiberwiseLinear_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞} (e e' : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] [Trivialization.IsLinear 𝕜 e'] : e.symm.trans e'.toOpenPartialHomeomorph ∈ contMDiffFiberwiseLinear B F IB n ↔ ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet) ∧ ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(coordChangeL 𝕜 e' e b)) (e.baseSet ∩ e'.baseSet)

The coordinate change e.symm ≫ₕ e' between two linear trivializations is a bi-C^n fiberwise linear map exactly when the fibrewise coordinate changes in both directions are C^n on the overlap of the base sets.

The maximal atlas

theorem Bundle.Trivialization.contMDiffOn_coordChangeL_of_mem_maximalAtlas {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞} [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {e e' : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] [Trivialization.IsLinear 𝕜 e'] (he : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) (he' : e'.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

The fibrewise coordinate change between two members of the maximal atlas of C^n trivializations is C^n on the overlap of their base sets.

theorem Bundle.Trivialization.contMDiffAt_coordChangeL_of_mem_maximalAtlas {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞} [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {e e' : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] [Trivialization.IsLinear 𝕜 e'] (he : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) (he' : e'.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) {b : B} (hb : b ∈ e.baseSet) (hb' : b ∈ e'.baseSet) : ContMDiffAt IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(coordChangeL 𝕜 e e' b)) b

The fibrewise coordinate change between two members of the maximal atlas of C^n trivializations is C^n at every point of the overlap of their base sets.

theorem ContMDiffWithinAt.change_section_trivialization_of_mem_maximalAtlas {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞} [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [Bundle.Trivialization.IsLinear 𝕜 e] [Bundle.Trivialization.IsLinear 𝕜 e'] {EM : Type u_7} {HM : Type u_8} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} {M : Type u_9} [TopologicalSpace M] [ChartedSpace HM M] {f : M → Bundle.TotalSpace F E} {s : Set M} {x₀ : M} (he : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (Bundle.TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) (he' : e'.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (Bundle.TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) (hp : ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj ∘ f) s x₀) (hf : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (↑e (f y)).2) s x₀) (hx : f x₀ ∈ e.source) (hx' : f x₀ ∈ e'.source) : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (↑e' (f y)).2) s x₀

A map into the total space whose base map is C^n and whose fibre coordinate in one member of the maximal atlas of C^n trivializations is C^n has C^n fibre coordinate in every other member whose source contains the point.

theorem Bundle.Trivialization.mem_maximalAtlas_contMDiffFiberwiseLinear_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] (IB : ModelWithCorners 𝕜 EB HB) (n : WithTop ℕ∞) [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] (e : Trivialization F TotalSpace.proj) [Trivialization.IsLinear 𝕜 e] : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n) ↔ ∀ (e' : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e'], ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet) ∧ ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(coordChangeL 𝕜 e' e b)) (e.baseSet ∩ e'.baseSet)

A linear trivialization lies in the maximal atlas of C^n trivializations exactly when its fibrewise coordinate changes with every trivialization of the bundle's atlas, in both directions, are C^n on the overlaps of the base sets.

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

Every trivialization of the atlas of a C^n vector bundle lies in the maximal atlas of C^n trivializations. Unlike StructureGroupoid.subset_maximalAtlas, this needs no manifold structure on the base.

theorem Bundle.Trivialization.transFiberwiseLinear_mem_maximalAtlas_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞} [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] [VectorBundle 𝕜 F E] (he : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) (φ : B → F ≃L[𝕜] F) (hφ : ContinuousOn (fun (x : B) => ↑(φ x)) e.baseSet) (h2φ : ContinuousOn (fun (x : B) => ↑(φ x).symm) e.baseSet) : (e.transFiberwiseLinear φ hφ h2φ).toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n) ↔ ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => ↑(φ x)) e.baseSet ∧ ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (x : B) => ↑(φ x).symm) e.baseSet

A gauge transform of a member of the maximal atlas of C^n trivializations is again a member exactly when the gauge and its fibrewise inverse are C^n on the base set.

Smoothness read in a member of the maximal atlas

theorem Bundle.Trivialization.contMDiffWithinAt_iff_of_mem_maximalAtlas {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞} [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] {EM : Type u_7} {HM : Type u_8} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} {M : Type u_9} [TopologicalSpace M] [ChartedSpace HM M] {f : M → TotalSpace F E} {s : Set M} {x₀ : M} [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (he : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) (hx : f x₀ ∈ e.source) : ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f s x₀ ↔ ContMDiffWithinAt IM IB n (fun (x : M) => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (x : M) => (↑e (f x)).2) s x₀

A map into the total space of a C^n vector bundle is C^n within a set at a point exactly when its base map and its fibre coordinate in a member of the maximal atlas of C^n trivializations, whose source contains the point, are.

theorem Bundle.Trivialization.contMDiffAt_iff_of_mem_maximalAtlas {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞} [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] {EM : Type u_7} {HM : Type u_8} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} {M : Type u_9} [TopologicalSpace M] [ChartedSpace HM M] {f : M → TotalSpace F E} {x₀ : M} [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (he : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) (hx : f x₀ ∈ e.source) : ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f x₀ ↔ ContMDiffAt IM IB n (fun (x : M) => (f x).proj) x₀ ∧ ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n (fun (x : M) => (↑e (f x)).2) x₀

A map into the total space of a C^n vector bundle is C^n at a point exactly when its base map and its fibre coordinate in a member of the maximal atlas of C^n trivializations, whose source contains the point, are.

theorem Bundle.Trivialization.contMDiffWithinAt_section_iff_of_mem_maximalAtlas {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞} [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (he : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) {σ : (x : B) → E x} {a : Set B} {b₀ : B} (hb₀ : b₀ ∈ e.baseSet) : ContMDiffWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => ⟨x, σ x⟩) a b₀ ↔ ContMDiffWithinAt IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑e ⟨x, σ x⟩).2) a b₀

A section of a C^n vector bundle is C^n within a set at a point of the base set of a member of the maximal atlas of C^n trivializations exactly when its coordinate in that member is.

theorem Bundle.Trivialization.contMDiffAt_section_iff_of_mem_maximalAtlas {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞} [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (he : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) {σ : (x : B) → E x} {b₀ : B} (hb₀ : b₀ ∈ e.baseSet) : ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => ⟨x, σ x⟩) b₀ ↔ ContMDiffAt IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑e ⟨x, σ x⟩).2) b₀

A section of a C^n vector bundle is C^n at a point of the base set of a member of the maximal atlas of C^n trivializations exactly when its coordinate in that member is.

theorem Bundle.Trivialization.contMDiffOn_section_iff_of_mem_maximalAtlas {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {E : B → Type u_4} [TopologicalSpace (TotalSpace F E)] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] {EB : Type u_5} {HB : Type u_6} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] [ChartedSpace HB B] {IB : ModelWithCorners 𝕜 EB HB} {n : WithTop ℕ∞} [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {e : Trivialization F TotalSpace.proj} [Trivialization.IsLinear 𝕜 e] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (he : e.toOpenPartialHomeomorph ∈ StructureGroupoid.maximalAtlas (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)) {σ : (x : B) → E x} {a : Set B} (ha : a ⊆ e.baseSet) : ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => ⟨x, σ x⟩) a ↔ ContMDiffOn IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑e ⟨x, σ x⟩).2) a

A section of a C^n vector bundle is C^n on a subset of the base set of a member of the maximal atlas of C^n trivializations exactly when its coordinate in that member is.