Smooth functions as functions of a localized chart

On a finite-dimensional Hausdorff real manifold, multiplying the extended chart at x by a bump function gives a globally smooth map with the chart's germ at x. On any finite-dimensional real manifold, near an interior point the chart expression of a smooth real function agrees with a smooth function on the model space, hence every smooth real function agrees near x with a smooth function on the model space composed with such a localized chart. These steps reduce local statements about smooth functions to the model space.

Main results

• TauCeti.exists_contMDiffMap_eventuallyEq_extChartAt: a globally smooth map with the germ of the extended chart at x.
• TauCeti.exists_contMDiffMap_comp_eventuallyEq: near an interior point, every smooth function agrees with a smooth function of that localized chart.
• TauCeti.exists_contDiff_comp_extChartAt_symm_eventuallyEq: near the image of an interior point, the chart expression of a smooth function agrees with a smooth function on the model space.

theorem TauCeti.exists_contMDiffMap_eventuallyEq_extChartAt {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] [IsManifold I (↑⊤) M] [T2Space M] (x : M) : ∃ (F : ContMDiffMap I (modelWithCornersSelf ℝ E) M E ↑⊤), ⇑F =ᶠ[nhds x] ↑(extChartAt I x)

A globally smooth map with the germ of the extended chart. There is a C^∞ map M → E that agrees with extChartAt I x on a neighbourhood of x.

theorem TauCeti.exists_contDiff_comp_extChartAt_symm_eventuallyEq {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] [IsManifold I (↑⊤) M] {x : M} (hx : I.IsInteriorPoint x) (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) : ∃ (g : E → ℝ), ContDiff ℝ (↑⊤) g ∧ ⇑f ∘ ↑(extChartAt I x).symm =ᶠ[nhds (↑(extChartAt I x) x)] g

Smooth chart expressions. Near an interior point x, the chart expression f ∘ (extChartAt I x).symm of a smooth function agrees with a smooth function on the model space. No separation assumption on M is needed.

theorem TauCeti.exists_contMDiffMap_comp_eventuallyEq {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] [IsManifold I (↑⊤) M] {x : M} (hx : I.IsInteriorPoint x) (F : ContMDiffMap I (modelWithCornersSelf ℝ E) M E ↑⊤) (hF : ⇑F =ᶠ[nhds x] ↑(extChartAt I x)) (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤) : ∃ (g' : ContMDiffMap (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) E ℝ ↑⊤), ⇑f =ᶠ[nhds x] ⇑g' ∘ ⇑F

A smooth function factors through the chart near an interior point. If F has the germ of the extended chart at an interior point x, then every f : C^∞⟮I, M; ℝ⟯ agrees near x with g' ∘ F for some C^∞ function g' on the model space.

theorem TauCeti.comp_extChartAt_symm_eventuallyEq_of_eventuallyEq_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {Y : Type u_4} {x : M} (hx : I.IsInteriorPoint x) {F : M → E} (hF : F =ᶠ[nhds x] ↑(extChartAt I x)) {f : M → Y} {g : E → Y} (hg : f =ᶠ[nhds x] g ∘ F) : f ∘ ↑(extChartAt I x).symm =ᶠ[nhds (↑(extChartAt I x) x)] g

Chart expressions of local factorizations. Near an interior point x, if f agrees with g ∘ F for a map F with the germ of the extended chart, then the chart expression f ∘ (extChartAt I x).symm agrees with g near extChartAt I x x.