Global sections with a prescribed value #
Let V be a C^n real vector bundle, n ≤ ∞, over a finite-dimensional Hausdorff smooth
manifold. Every vector in V is the value of a global C^n section. This lets tensorial
operations on globally C^n sections define maps on individual fibres. The construction cuts off
Mathlib's locally C^n FiberBundle.extend with a smooth bump function. Equivalently,
evaluation of global C^n sections at a point is surjective.
theorem
FiberBundle.exists_contMDiff_section_eq
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[T2Space M]
[IsManifold I (↑⊤) M]
(F : Type u_4)
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(n : WithTop ℕ∞)
[ENat.LEInfty n]
[ContMDiffVectorBundle n F V I]
{x : M}
(v : V x)
:
In a C^n vector bundle with n ≤ ∞, every fibre vector is the value of a global C^n
section. The fibre need not be finite-dimensional, and the base need not be compact or
boundaryless.
theorem
ContMDiffSection.evalLinearMap_surjective
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[T2Space M]
[IsManifold I (↑⊤) M]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{V : M → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module ℝ (V x)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(n : WithTop ℕ∞)
[ENat.LEInfty n]
[ContMDiffVectorBundle n F V I]
(x : M)
:
Function.Surjective ⇑(evalLinearMap I F n V x)
In a C^n vector bundle with n ≤ ∞, evaluation of C^n sections at a point is surjective:
every fibre vector is the value of a global C^n section.