Reconstructing sections in a vector-bundle frame #
A field of model vectors determines a section through the inverse of an atlas trivialization. The section has the regularity of that field on the frame domain. For Hom bundles, this is the inverse coordinate conjugation, with no algebraic condition on the field.
theorem
Bundle.Trivialization.contMDiffOn_sectionFromCoordinates
{𝕜 : Type u_1}
{M : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[TopologicalSpace M]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_4}
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[TopologicalSpace (TotalSpace F V)]
[FiberBundle F V]
(e : Trivialization F TotalSpace.proj)
[Trivialization.IsLinear 𝕜 e]
{E : Type u_5}
{H : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
[ChartedSpace H M]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
[VectorBundle 𝕜 F V]
[ContMDiffVectorBundle n F V I]
[MemTrivializationAtlas e]
(A : M → F)
(hA : ContMDiffOn I (modelWithCornersSelf 𝕜 F) n A e.baseSet)
:
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, e.sectionFromCoordinates A x⟩) e.baseSet
A reconstructed section has the regularity of its coordinates on the frame domain.
theorem
Bundle.Trivialization.contMDiff_sectionFromCoordinates
{𝕜 : Type u_1}
{M : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[TopologicalSpace M]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : M → Type u_4}
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[TopologicalSpace (TotalSpace F V)]
[FiberBundle F V]
(e : Trivialization F TotalSpace.proj)
[Trivialization.IsLinear 𝕜 e]
{E : Type u_5}
{H : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
[ChartedSpace H M]
{I : ModelWithCorners 𝕜 E H}
{n : WithTop ℕ∞}
[VectorBundle 𝕜 F V]
[ContMDiffVectorBundle n F V I]
[MemTrivializationAtlas e]
(he : e.baseSet = Set.univ)
(A : M → F)
(hA : ContMDiff I (modelWithCornersSelf 𝕜 F) n A)
:
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, e.sectionFromCoordinates A x⟩
A globally covering frame reconstructs a global section of the same regularity.