Continuity of inverse evaluation and first coordinate derivatives #
For diffeomorphisms with compact source, inverse evaluation is jointly continuous for the weak
Whitney topology. In fixed source and target charts, the differential of the inverse is the
inverse of the forward differential at the inverse image point. This formula and Mathlib's
ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse give joint continuity of the inverse
differential and openness of compact coordinate-differential tests on inverse maps.
The chart differentials are taken within extended chart targets, so the statements also apply to manifolds with boundary and corners.
The topology convention follows M. Hirsch, Differential Topology, GTM 33, Chapter 2, ยง1.
theorem
TauCeti.continuous_diffeomorph_symm_eval
{๐ : 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]
:
Continuous fun (p : Diffeomorph I J M N n ร N) => p.1.symm p.2
Evaluation of inverse diffeomorphisms is jointly continuous in the diffeomorphism and the target point, for the weak Whitney topology.
theorem
TauCeti.continuous_diffeomorph_symm_toContinuousMap
{๐ : 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]
:
Continuous fun (f : Diffeomorph I J M N n) => โf.symm.toHomeomorph
The underlying continuous maps of inverse diffeomorphisms depend continuously on the diffeomorphism. The target here carries the compact-open topology.
theorem
TauCeti.fderivWithin_diffeomorph_chart_symm_comp
{๐ : 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)
(hn : n โ 0)
{x z : M}
{y : N}
(hz : z โ (extChartAt I x).source)
(hfz : f z โ (extChartAt J y).source)
:
fderivWithin ๐ (โ(extChartAt I x) โ โf.symm โ โ(extChartAt J y).symm) (extChartAt J y).target
(โ(extChartAt J y) (f z)) โSL fderivWithin ๐ (โ(extChartAt J y) โ โf โ โ(extChartAt I x).symm) (extChartAt I x).target (โ(extChartAt I x) z) = ContinuousLinearMap.id ๐ E
The inverse and forward coordinate differentials compose to the identity, in any pair of charts containing the point and its image.
theorem
TauCeti.inverse_fderivWithin_diffeomorph_chart
{๐ : 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)
(hn : n โ 0)
{x z : M}
{y : N}
(hz : z โ (extChartAt I x).source)
(hfz : f z โ (extChartAt J y).source)
:
(fderivWithin ๐ (โ(extChartAt J y) โ โf โ โ(extChartAt I x).symm) (extChartAt I x).target
(โ(extChartAt I x) z)).inverse = fderivWithin ๐ (โ(extChartAt I x) โ โf.symm โ โ(extChartAt J y).symm) (extChartAt J y).target
(โ(extChartAt J y) (f z))
In fixed charts, the coordinate differential of the inverse is the inverse of the forward coordinate differential. The derivatives within extended chart targets include boundary points.
theorem
TauCeti.isInvertible_fderivWithin_diffeomorph_chart
{๐ : 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)
(hn : n โ 0)
{x z : M}
{y : N}
(hz : z โ (extChartAt I x).source)
(hfz : f z โ (extChartAt J y).source)
:
(fderivWithin ๐ (โ(extChartAt J y) โ โf โ โ(extChartAt I x).symm) (extChartAt I x).target
(โ(extChartAt I x) z)).IsInvertible
Coordinate differentials of a diffeomorphism are invertible, including at boundary points.
theorem
TauCeti.tendsto_extChartAt_diffeomorph_symm_eval
{๐ : 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)
:
(โแถ (p : Diffeomorph I J M N n ร F) in nhds fโ รหข nhdsWithin wโ (extChartAt J y).target, p.1.symm (โ(extChartAt J y).symm p.2) โ (extChartAt I x).source) โง Filter.Tendsto (fun (p : Diffeomorph I J M N n ร F) => โ(extChartAt I x) (p.1.symm (โ(extChartAt J y).symm p.2)))
(nhds fโ รหข nhdsWithin wโ (extChartAt J y).target)
(nhdsWithin (โ(extChartAt I x) (fโ.symm (โ(extChartAt J y).symm wโ))) (extChartAt I x).target)
Along the inverse image of a moving point of the target chart, the source chart is eventually defined and sends the inverse image to a point of the source chart target, tending to the chart image of the limit inverse image.
theorem
TauCeti.diffeomorph_toContMDiffMap_symm_extChartAt_mem_source
{๐ : 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 โโ}
{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)
:
โfโ (โ(extChartAt I x).symm (โ(extChartAt I x) (fโ.symm (โ(extChartAt J y).symm wโ)))) โ (extChartAt J y).source
The forward map sends the chart-source inverse image of a point of the target chart back into the target chart's source.
theorem
TauCeti.tendsto_fderivWithin_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}
(hn : 1 โค n)
(hwโ : wโ โ (extChartAt J y).target)
(hfโ : fโ.symm (โ(extChartAt J y).symm wโ) โ (extChartAt I x).source)
:
Filter.Tendsto
(fun (p : Diffeomorph I J M N n ร F) =>
fderivWithin ๐ (โ(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 (fderivWithin ๐ (โ(extChartAt I x) โ โfโ.symm โ โ(extChartAt J y).symm) (extChartAt J y).target wโ))
The first coordinate differential of the inverse varies continuously with the diffeomorphism and the point of the target chart.
theorem
TauCeti.isOpen_diffeomorph_symm_fderivWithin_test
{๐ : 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]
(hn : 1 โค n)
(x : M)
(y : N)
{K : Set โ(extChartAt J y).target}
(hK : IsCompact K)
{V : Set (F โL[๐] E)}
(hV : IsOpen V)
:
IsOpen
{f : Diffeomorph I J M N n | โ w โ K,
f.symm (โ(extChartAt J y).symm โw) โ (extChartAt I x).source โง fderivWithin ๐ (โ(extChartAt I x) โ โf.symm โ โ(extChartAt J y).symm) (extChartAt J y).target โw โ V}
A compact coordinate-differential test on inverse maps is open in the weak Whitney topology. The test also requires all inverse images to lie in the chosen source chart.