Meagreness of critical values on manifolds

The critical values of a smooth map between finite-dimensional real manifolds without boundary form a meagre set, provided the source is Lindelöf. The dimensions need not be equal. More locally, it suffices that the map be smooth at the points of a Lindelöf set of critical points. Consequently an everywhere rank-deficient real analytic map has meagre image.

We use the existing Sard--Smale theorem in finite-dimensional coordinate domains. The regular-point comparison in arbitrary extended charts identifies the critical points in those domains. Meagreness is preserved by chart inverses, and a countable neighborhood subcover in the source gives the global assertion (TauCeti.isMeagre_image_of_forall_isMeagre_image_extChartAt). No decomposition of analytic zero sets is needed.

References

• S. Łojasiewicz, Triangulation of semi-analytic sets, Annali della Scuola Normale Superiore di Pisa (3) 18 (1964), 449–474, §2, Lemma 1 (the real analytic case).
• S. Smale, An infinite dimensional version of Sard's theorem, American Journal of Mathematics 87 (1965), 861–866; the local input is TauCeti.isMeagre_image_criticalPoints_of_isFredholm.

theorem TauCeti.isMeagre_image_of_not_isRegularPoint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [J.Boundaryless] {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J (↑⊤) N] {f : M → N} {s : Set M} [LindelofSpace ↑s] (hf : ∀ x ∈ s, ContMDiffAt I J (↑⊤) f x) (hs : ∀ x ∈ s, ¬IsRegularPoint I J f x) : IsMeagre (f '' s)

Sard's theorem, in Baire category form. The image of a Lindelöf set of critical points at which a map is smooth is meagre. Both manifolds are finite-dimensional and without boundary; their dimensions may differ. Smoothness is required in the ambient manifold at points of s, not merely within s.

theorem ContMDiff.isMeagre_image_criticalPoints {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [J.Boundaryless] {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J (↑⊤) N] {f : M → N} [LindelofSpace M] {n : WithTop ℕ∞} (hf : ContMDiff I J n f) (hn : ↑⊤ ≤ n) : IsMeagre (f '' {x : M | ¬TauCeti.IsRegularPoint I J f x})

The critical values of a smooth map from a Lindelöf finite-dimensional manifold without boundary form a meagre set.

theorem ContMDiff.isMeagre_range_of_finrank_mfderiv_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [J.Boundaryless] {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J (↑⊤) N] {f : M → N} [LindelofSpace M] {n : WithTop ℕ∞} (hf : ContMDiff I J n f) (hn : ↑⊤ ≤ n) (hrank : ∀ (x : M), Module.finrank ℝ ↥(↑(mfderiv% f x)).range < Module.finrank ℝ E') : IsMeagre (Set.range f)

An everywhere rank-deficient smooth or real analytic map from a Lindelöf manifold without boundary has meagre image. The rank is the dimension of the range of its native manifold derivative. For an analytic map, the regularity hypothesis ∞ ≤ ω is automatic.