Local charts in affine subspaces

Around an interior source point, a smooth map whose image lies locally in a finite-dimensional affine subspace, and whose differential identifies the source tangent space with the direction subspace, gives a local chart into that direction. The chart sends the base point to zero and identifies the original map with translation of the subtype inclusion. Its source can be chosen inside the specified smoothness neighborhood. The regularity is at least one.

Main results

• ContMDiffOn.exists_plaque_chart: a partial diffeomorphism into an affine direction subspace with the prescribed ambient map.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 19, Proposition 19.16 (Local Structure of Integral Manifolds), p. 500, for the real local-slice statement.

theorem ContMDiffOn.exists_plaque_chart {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {W : Submodule 𝕜 E} {H : Type u_4} [TopologicalSpace H] {J : ModelWithCorners 𝕜 F H} {N : Type u_5} [TopologicalSpace N] [ChartedSpace H N] {n : WithTop ℕ∞} [IsManifold J n N] {f : N → E} {x : N} {s : Set N} [FiniteDimensional 𝕜 ↥W] (hf : ContMDiffOn J (modelWithCornersSelf 𝕜 E) n f s) (hs : IsOpen s) (hxs : x ∈ s) (hn : 1 ≤ n) (hx : J.IsInteriorPoint x) (hinj : Function.Injective ⇑(mfderiv% f x)) (hrange : (↑(mfderiv% f x)).range = W) (hplaque : ∀ᶠ (y : N) in nhds x, f y - f x ∈ W) : ∃ (e : PartialDiffeomorph J (modelWithCornersSelf 𝕜 ↥W) N (↥W) n), x ∈ e.source ∧ ↑e.toPartialEquiv x = 0 ∧ e.source ⊆ s ∧ ∀ y ∈ e.source, f y = f x + ↑(↑e.toPartialEquiv y)

Around an interior source point, a C^n map, for 1 ≤ n, locally contained in a finite-dimensional affine subspace has a partial diffeomorphism into the direction subspace, provided its differential at that point is injective with range equal to that direction. The chart is centered at zero, lies inside the given smoothness neighborhood, and identifies the original map with translation of the subtype inclusion.