Transporting local statements through charts

A function k on a charted space is read in the preferred chart at x as k ∘ (chartAt H x).symm, near the coordinate chartAt H x x. This file records how such representatives transform: under a change of chart, under composition with a continuous map between charted spaces, and how punctured neighbourhoods are carried by the inverse chart. These are the facts needed to read a local notion of one variable (meromorphy, orders, ...) on a charted space in its preferred charts and to check that it is well behaved.

Main results

• TauCeti.tendsto_chartAt_symm_nhdsNE: the inverse of the chart at x maps punctured neighbourhoods of chartAt H x x into punctured neighbourhoods of x.
• TauCeti.comp_symm_eventuallyEq_comp_chartAt_symm_comp: the representative of k in a chart e at x is its representative in the preferred chart composed with the transition map.
• TauCeti.comp_comp_chartAt_symm_eventuallyEq: the representative of k ∘ φ is the representative of k composed with the representative of φ.

theorem TauCeti.tendsto_chartAt_symm_nhdsNE {H : Type u_1} {X : Type u_3} [TopologicalSpace H] [TopologicalSpace X] [ChartedSpace H X] (x : X) : Filter.Tendsto (↑(chartAt H x).symm) (nhdsWithin (↑(chartAt H x) x) {↑(chartAt H x) x}ᶜ) (nhdsWithin x {x}ᶜ)

The inverse of the chart at x maps punctured neighbourhoods of chartAt H x x into punctured neighbourhoods of x.

theorem TauCeti.comp_symm_eventuallyEq_comp_chartAt_symm_comp {H : Type u_1} {X : Type u_3} [TopologicalSpace H] [TopologicalSpace X] [ChartedSpace H X] {x : X} {α : Type u_5} (k : X → α) {e : OpenPartialHomeomorph X H} (hx : x ∈ e.source) : k ∘ ↑e.symm =ᶠ[nhds (↑e x)] (k ∘ ↑(chartAt H x).symm) ∘ ↑(chartAt H x) ∘ ↑e.symm

Near e x, the representative of k in a chart e is its representative in the preferred chart at x, composed with the transition map from e to that chart.

theorem TauCeti.comp_comp_chartAt_symm_eventuallyEq {H : Type u_1} {H' : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace X] [ChartedSpace H X] [TopologicalSpace Y] [ChartedSpace H' Y] {x : X} {α : Type u_5} (k : Y → α) {φ : X → Y} (hφ : ContinuousAt φ x) : (k ∘ φ) ∘ ↑(chartAt H x).symm =ᶠ[nhds (↑(chartAt H x) x)] (k ∘ ↑(chartAt H' (φ x)).symm) ∘ fun (z : H) => ↑(chartAt H' (φ x)) (φ (↑(chartAt H x).symm z))

Near chartAt H x x, the representative of k ∘ φ is the representative of k composed with the representative of φ.