The weak Whitney topology on diffeomorphisms

This topology is provided only when the source manifold M is compact; the noncompact case requires a separate choice between weak and strong Whitney topologies.

The diffeomorphisms M ≃ₘ^n⟮I, J⟯ N carry the subspace topology inherited from the weak Whitney topology on C^n⟮I, M; J, N⟯. This topology is generated by chart derivative tests: a map passes a test when it carries the chosen compact chart set into the target chart and its coordinate derivative there lies in the prescribed open set. Convergence is characterized by ContMDiffMap.tendsto_manifoldWeakWhitney_iff. This is the C^n topology in the usual sense, the weak and the strong Whitney topologies agreeing for the compact source. Only the forward map is topologized; no continuity is claimed for inversion, which needs an inverse-function estimate that is not developed here.

Use open scoped TauCeti.DiffeomorphWeakWhitney to select this topology, for instance when forming continuous maps into the space of diffeomorphisms.

The reason to have the topology is to turn a smooth family of diffeomorphisms, which is what a geometric construction produces, into a continuous map into the space of diffeomorphisms, which is what a homotopy-theoretic statement about that space needs. Diffeomorph.ofSmoothFamily is that map, and TauCeti.Diffeotopy.toPath in TauCeti.Geometry.Diffeomorphism.Diffeotopy.Path uses it.

Main definitions

• Diffeomorph.weakWhitneyTopology: the topology induced from the weak Whitney topology on C^n⟮I, M; J, N⟯.
• Diffeomorph.ofSmoothFamily: a jointly C^n family of diffeomorphisms, as a continuous map into the space of diffeomorphisms M ≃ₘ^n⟮I, J⟯ N.

Main results

• Diffeomorph.isEmbedding_toContMDiffMap: the forgetful map to C^n⟮I, M; J, N⟯ is an embedding.
• Diffeomorph.continuous_weakWhitney_iff: a family of diffeomorphisms is continuous exactly when the underlying family of C^n maps is.
• Diffeomorph.continuous_eval_const: evaluation at a fixed point of the source is continuous.
• Diffeomorph.t2Space_weakWhitney: a Hausdorff target gives a Hausdorff diffeomorphism space.
• ContMDiff.continuous_diffeomorphWeakWhitney: joint C^n regularity of a family of diffeomorphisms gives continuity of the family.

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

theorem Diffeomorph.toContMDiffMap_injective {𝕜 : 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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} : Function.Injective toContMDiffMap

A diffeomorphism is determined by its underlying C^n map.

@[instance_reducible]

noncomputable def Diffeomorph.weakWhitneyTopology {𝕜 : 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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [IsManifold I n M] [IsManifold J n N] : TopologicalSpace (Diffeomorph I J M N n)

The weak Whitney topology on the C^n diffeomorphisms from M to N: the topology induced along the forgetful map to C^n⟮I, M; J, N⟯.

Equations

• Diffeomorph.weakWhitneyTopology = TopologicalSpace.induced Diffeomorph.toContMDiffMap ContMDiffMap.manifoldWeakWhitneyTopology

theorem Diffeomorph.isEmbedding_toContMDiffMap {𝕜 : 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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [IsManifold I n M] [IsManifold J n N] : Topology.IsEmbedding toContMDiffMap

The forgetful map to C^n⟮I, M; J, N⟯ realizes the diffeomorphisms as a subspace of the weak Whitney map space.

theorem Diffeomorph.continuous_toContMDiffMap {𝕜 : 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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [IsManifold I n M] [IsManifold J n N] : Continuous toContMDiffMap

The forgetful map to C^n⟮I, M; J, N⟯ is continuous.

theorem Diffeomorph.continuous_weakWhitney_iff {𝕜 : 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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [IsManifold I n M] [IsManifold J n N] {Q : Type u_11} [TopologicalSpace Q] {f : Q → Diffeomorph I J M N n} : Continuous f ↔ Continuous fun (q : Q) => ↑(f q)

A family of diffeomorphisms is continuous exactly when the underlying family of C^n maps is.

theorem Diffeomorph.continuous_eval_const {𝕜 : 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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [IsManifold I n M] [IsManifold J n N] (x : M) : Continuous fun (f : Diffeomorph I J M N n) => f x

Evaluation at a fixed point of the source is continuous.

theorem Diffeomorph.t2Space_weakWhitney {𝕜 : 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_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [IsManifold I n M] [IsManifold J n N] [T2Space N] : T2Space (Diffeomorph I J M N n)

A Hausdorff target gives a Hausdorff space of diffeomorphisms.

theorem ContMDiff.continuous_diffeomorphWeakWhitney {𝕜 : 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'] {I' : ModelWithCorners 𝕜 E' H'} {P : Type u_7} [TopologicalSpace P] [ChartedSpace H' P] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [IsManifold I n M] [IsManifold J n N] [IsManifold I' n P] {f : P → Diffeomorph I J M N n} (hf : ContMDiff (I'.prod I) J n fun (z : P × M) => (f z.1) z.2) : Continuous f

The smooth-families map: a family of diffeomorphisms which is jointly C^n on the product of the parameter manifold with the source is continuous for the weak Whitney topology. The converse fails for a general parameter space, so only this direction is available.

noncomputable def Diffeomorph.ofSmoothFamily {𝕜 : 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'] {I' : ModelWithCorners 𝕜 E' H'} {P : Type u_7} [TopologicalSpace P] [ChartedSpace H' P] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [IsManifold I n M] [IsManifold J n N] [IsManifold I' n P] (f : P → Diffeomorph I J M N n) (hf : ContMDiff (I'.prod I) J n fun (z : P × M) => (f z.1) z.2) : C(P, Diffeomorph I J M N n)

A jointly C^n family of diffeomorphisms, bundled as a continuous map into the diffeomorphisms.

Equations

• Diffeomorph.ofSmoothFamily f hf = { toFun := f, continuous_toFun := ⋯ }

@[simp]

theorem Diffeomorph.ofSmoothFamily_apply {𝕜 : 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'] {I' : ModelWithCorners 𝕜 E' H'} {P : Type u_7} [TopologicalSpace P] [ChartedSpace H' P] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_9} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [CompactSpace M] [IsManifold I n M] [IsManifold J n N] [IsManifold I' n P] (f : P → Diffeomorph I J M N n) (hf : ContMDiff (I'.prod I) J n fun (z : P × M) => (f z.1) z.2) (p : P) : (ofSmoothFamily f hf) p = f p

The smooth-families map is the family it was built from.