Continuity of inversion in the weak Whitney topology

For compact manifolds with a locally compact source model space, the inverse of a diffeomorphism depends continuously on the diffeomorphism in the weak Whitney topology. Together with continuity of composition, this makes the self-diffeomorphisms a topological group. The result includes manifolds with boundary and corners and arbitrary differentiability order, including smooth maps.

Higher inverse derivatives are recovered recursively from the Faà di Bruno formula for f.symm ∘ f = id. The singleton-partition term is invertible; every remaining term uses a strictly lower derivative of the inverse. Compactness then turns joint continuity of inverse jets into openness of the defining chart tests.

The topology convention follows M. Hirsch, Differential Topology, GTM 33, Chapter 2, §1.

theorem Diffeomorph.taylorComp_symm_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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] (f : Diffeomorph I J M N n) {x : M} {y : N} {w : F} (hw : w ∈ (extChartAt J y).target) (hf : f.symm (↑(extChartAt J y).symm w) ∈ (extChartAt I x).source) {m : ℕ} (hm : ↑m ≤ n) : (ftaylorSeriesWithin 𝕜 (↑(extChartAt I x) ∘ ⇑f.symm ∘ ↑(extChartAt J y).symm) (extChartAt J y).target w).taylorComp (ftaylorSeriesWithin 𝕜 (↑(extChartAt J y) ∘ ⇑f ∘ ↑(extChartAt I x).symm) (extChartAt I x).target (↑(extChartAt I x) (f.symm (↑(extChartAt J y).symm w)))) m = iteratedFDerivWithin 𝕜 m id (extChartAt I x).target (↑(extChartAt I x) (f.symm (↑(extChartAt J y).symm w)))

Composing the inverse and forward coordinate Taylor series gives the Taylor series of the identity at the source point.

theorem TauCeti.tendsto_iteratedFDerivWithin_diffeomorph_symm_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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [T2Space N] [LocallyCompactSpace E] [IsManifold I n M] [IsManifold J n N] {f₀ : Diffeomorph I J M N n} {x : M} {y : N} {w₀ : F} (hw₀ : w₀ ∈ (extChartAt J y).target) (hf₀ : f₀.symm (↑(extChartAt J y).symm w₀) ∈ (extChartAt I x).source) {m : ℕ} (hm : ↑m ≤ n) : Filter.Tendsto (fun (p : Diffeomorph I J M N n × F) => iteratedFDerivWithin 𝕜 m (↑(extChartAt I x) ∘ ⇑p.1.symm ∘ ↑(extChartAt J y).symm) (extChartAt J y).target p.2) (nhds f₀ ×ˢ nhdsWithin w₀ (extChartAt J y).target) (nhds (iteratedFDerivWithin 𝕜 m (↑(extChartAt I x) ∘ ⇑f₀.symm ∘ ↑(extChartAt J y).symm) (extChartAt J y).target w₀))

Every inverse coordinate derivative varies continuously with the diffeomorphism and the point of the target chart, including boundary and corner points.

theorem Diffeomorph.continuous_symm {𝕜 : 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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [CompactSpace N] [T2Space N] [LocallyCompactSpace E] [IsManifold I n M] [IsManifold J n N] : Continuous Diffeomorph.symm

Inversion of diffeomorphisms is continuous for the weak Whitney topology on compact manifolds whose source model space is locally compact, at every differentiability order.

theorem Diffeomorph.isTopologicalGroup {𝕜 : 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] {n : WithTop ℕ∞} [CompactSpace M] [LocallyCompactSpace E] [IsManifold I n M] [T2Space M] : IsTopologicalGroup (Diffeomorph I I M M n)

Self-diffeomorphisms of a compact Hausdorff manifold with a locally compact model space form a topological group for the weak Whitney topology.