Meagre images in charts

Whether the image of a set under a map between manifolds is meagre can be read in extended charts. This holds over any nontrivially normed field, for a target manifold without boundary, whose extended charts are then open partial homeomorphisms, so their inverses carry meagre sets to meagre sets.

Main results

• TauCeti.isMeagre_image_of_isMeagre_image_extChartAt: if the coordinate expression of f in a pair of extended charts sends the chart image of a set u in the chart sources to a meagre set, then f '' u is meagre.
• TauCeti.isMeagre_image_of_forall_isMeagre_image_extChartAt: for a map continuous at the points of a Lindelöf set s, if this holds in the charts at each x ∈ s and at f x for the points of s in a neighbourhood of x, then f '' s is meagre.

theorem TauCeti.isMeagre_image_of_isMeagre_image_extChartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [J.Boundaryless] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {x₀ : M} {y₀ : N} {u : Set M} (hu : u ⊆ (chartAt H x₀).source ∩ f ⁻¹' (chartAt H' y₀).source) (h : IsMeagre (↑(extChartAt J y₀) ∘ f ∘ ↑(extChartAt I x₀).symm '' ↑(extChartAt I x₀) '' u)) : IsMeagre (f '' u)

Let u be a set in the source of the chart at x₀ that f maps into the source of the chart at y₀. If the coordinate expression extChartAt J y₀ ∘ f ∘ (extChartAt I x₀).symm sends the chart image of u to a meagre subset of the model of N, then f '' u is meagre. The target is without boundary, so that its extended charts are open partial homeomorphisms.

theorem TauCeti.isMeagre_image_of_forall_isMeagre_image_extChartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [J.Boundaryless] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {s : Set M} [LindelofSpace ↑s] (hf : ∀ x ∈ s, ContinuousAt f x) (hchart : ∀ x ∈ s, ∃ V ∈ nhds x, IsMeagre (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm '' ↑(extChartAt I x) '' (s ∩ V ∩ (chartAt H x).source ∩ f ⁻¹' (chartAt H' (f x)).source))) : IsMeagre (f '' s)

Meagre images can be detected in charts. Let f be continuous at the points of a Lindelöf set s. Suppose that each x ∈ s has a neighbourhood V such that the coordinate expression extChartAt J (f x) ∘ f ∘ (extChartAt I x).symm sends the chart image of the points of s ∩ V lying in the two chart sources to a meagre subset of the model of N. Then f '' s is meagre. The target is without boundary, so that its extended charts are open partial homeomorphisms.