Continuous evaluation of diffeomorphisms #
On a compact source manifold with locally compact model, the weak Whitney topology makes
evaluation of C^n diffeomorphisms continuous in both the diffeomorphism and the point.
For self-diffeomorphisms this gives continuity of the tautological action, and evaluations
at the two ends of a path in the source are homotopic (Diffeomorph.evalAtHomotopy).
theorem
Diffeomorph.continuousEval_weakWhitney
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[LocallyCompactSpace E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[CompactSpace M]
{n : WithTop ℕ∞}
[IsManifold I n 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]
[IsManifold J n N]
:
ContinuousEval (Diffeomorph I J M N n) M N
Diffeomorphism evaluation is continuous for the weak Whitney topology.
theorem
Diffeomorph.applyContinuousSMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[LocallyCompactSpace E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[CompactSpace M]
{n : WithTop ℕ∞}
[IsManifold I n M]
:
ContinuousSMul (Diffeomorph I I M M n) M
The natural action of Diff(M) on M is continuous jointly in the diffeomorphism and
the point.
noncomputable def
Diffeomorph.evalAtHomotopy
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[LocallyCompactSpace E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[CompactSpace M]
{n : WithTop ℕ∞}
[IsManifold I n 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]
[IsManifold J n N]
{x₀ x₁ : M}
(γ : Path x₀ x₁)
:
Evaluations at two points joined by a path γ are homotopic, through evaluation along γ.
Instances For
@[simp]
theorem
Diffeomorph.evalAtHomotopy_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[LocallyCompactSpace E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[CompactSpace M]
{n : WithTop ℕ∞}
[IsManifold I n 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]
[IsManifold J n N]
{x₀ x₁ : M}
(γ : Path x₀ x₁)
(p : ↑unitInterval × Diffeomorph I J M N n)
:
At time t, the homotopy evalAtHomotopy γ evaluates at γ t.