A regular level set of a Fredholm map is a manifold

Let f : E → F be a map between Banach spaces which, at every point of the level set {x | f x = c}, is strictly differentiable and C^m, with surjective Fredholm derivative of index n. TauCeti.levelSetChartedSpace already makes that level set a charted space modelled on Fin n → 𝕜, the charts being the implicit-function charts of TauCeti.levelSetChartAt. This file proves that those charts are smoothly compatible, so the level set is a C^m manifold of dimension the index.

The transition from the chart at z to the chart at w is k ↦ Ψ (x k - w), where x k is the point of the level set with coordinate k in the chart at z, and Ψ is the continuous linear map that reads a vector of E in the model space through the projection onto ker (D w). So everything reduces to smoothness of the inverse chart as a map into E, which is TauCeti.contDiffAt_coe_levelSetChart_symm_of_mem: the inverse chart is smooth at every point of its target, because TauCeti.levelSetChartAt was cut down to the neighbourhood TauCeti.levelSetImplicitCoordSource on which the coordinate map of the implicit function theorem keeps an invertible derivative.

This is the smooth half of the statement that the zero set of a Fredholm section is, at a regular point, a manifold of dimension the index. As with the charted-space structure it refines, no global hypothesis such as second countability is assumed, so IsManifold here is the smooth-atlas statement and not the assertion that the level set is a topological manifold in the classical sense.

Main results

• TauCeti.contDiffOn_coe_levelSetChartAt_symm: the inverse of a preferred chart, included into the ambient Banach space, is C^m on the whole chart target.
• TauCeti.contDiffOn_levelSetChartAt_trans: the transition between two preferred charts is C^m.
• TauCeti.isManifold_levelSet: a regular level set of a C^m Fredholm map, of constant index n, is a C^m manifold modelled on Fin n → 𝕜.

References

• D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix A.3.

theorem TauCeti.contDiffOn_coe_levelSetChartAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {c : F} {D : E → E →L[𝕜] F} {n : ℕ} {m : WithTop ℕ∞} (hf : ∀ x ∈ {x : E | f x = c}, HasStrictFDerivAt f (D x) x) (hFred : ∀ x ∈ {x : E | f x = c}, (D x).IsFredholm) (hsurj : ∀ x ∈ {x : E | f x = c}, Function.Surjective ⇑(D x)) (hindex : ∀ x ∈ {x : E | f x = c}, (D x).index = ↑n) (hsmooth : ∀ x ∈ {x : E | f x = c}, ContDiffAt 𝕜 m f x) (z : ↑{x : E | f x = c}) : ContDiffOn 𝕜 m (fun (k : Fin n → 𝕜) => ↑(↑(levelSetChartAt hf hFred hsurj hindex z).symm k)) (levelSetChartAt hf hFred hsurj hindex z).target

The inverse of a preferred chart is smooth on the whole chart target. Read into the ambient Banach space, the inverse of TauCeti.levelSetChartAt is as smooth as the equation is along the level set.

theorem TauCeti.contDiffOn_levelSetChartAt_trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {c : F} {D : E → E →L[𝕜] F} {n : ℕ} {m : WithTop ℕ∞} (hf : ∀ x ∈ {x : E | f x = c}, HasStrictFDerivAt f (D x) x) (hFred : ∀ x ∈ {x : E | f x = c}, (D x).IsFredholm) (hsurj : ∀ x ∈ {x : E | f x = c}, Function.Surjective ⇑(D x)) (hindex : ∀ x ∈ {x : E | f x = c}, (D x).index = ↑n) (hsmooth : ∀ x ∈ {x : E | f x = c}, ContDiffAt 𝕜 m f x) (z w : ↑{x : E | f x = c}) : ContDiffOn 𝕜 m (↑((levelSetChartAt hf hFred hsurj hindex z).symm.trans (levelSetChartAt hf hFred hsurj hindex w))) ((levelSetChartAt hf hFred hsurj hindex z).symm.trans (levelSetChartAt hf hFred hsurj hindex w)).source

Two preferred charts of a regular level set are smoothly compatible. The transition map is the inverse of one chart, followed by the linear reading of a vector of E in the model space that the other chart is.

theorem TauCeti.isManifold_levelSet {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {c : F} {D : E → E →L[𝕜] F} {n : ℕ} {m : WithTop ℕ∞} (hf : ∀ x ∈ {x : E | f x = c}, HasStrictFDerivAt f (D x) x) (hFred : ∀ x ∈ {x : E | f x = c}, (D x).IsFredholm) (hsurj : ∀ x ∈ {x : E | f x = c}, Function.Surjective ⇑(D x)) (hindex : ∀ x ∈ {x : E | f x = c}, (D x).index = ↑n) (hsmooth : ∀ x ∈ {x : E | f x = c}, ContDiffAt 𝕜 m f x) : IsManifold (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) m ↑{x : E | f x = c}

A regular level set of a Fredholm map is a C^m manifold of dimension its index. If f is strictly differentiable and C^m at every point of the level set {x | f x = c}, with surjective Fredholm derivative of index n there, then the charted-space structure of TauCeti.levelSetChartedSpace is a C^m atlas.

Together with TauCeti.levelSetChartedSpace this is the "the zero set of a Fredholm section is, at a regular point, a manifold of dimension the index" statement; as there, no global hypothesis is assumed, so this is a statement about the atlas and not about second countability.